Cyclic Implicit Complexity

Research output: Working paper/PreprintPreprint

3 Downloads (Pure)

Abstract

Circular (or cyclic) proofs have received increasing attention in recent years, and have been proposed as an alternative setting for studying (co)inductive reasoning. In particular, now several type systems based on circular reasoning have been proposed. However, little is known about the complexity theoretic aspects of circular proofs, which exhibit sophisticated loop structures atypical of more common 'recursion schemes'. This paper attempts to bridge the gap between circular proofs and implicit computational complexity. Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify suitable proof theoretical constraints to characterise the polynomial-time and elementary computable functions.
Original languageEnglish
PublisherarXiv
Pages1-53
Number of pages53
DOIs
Publication statusPublished - 3 Oct 2021

Bibliographical note

53 pages, 3 figures

Keywords

  • cs.LO
  • math.LO

Fingerprint

Dive into the research topics of 'Cyclic Implicit Complexity'. Together they form a unique fingerprint.

Cite this