Cyclic Implicit Complexity

Gianluca Curzi; Anupam Das

doi:10.1145/3531130.3533340

Cyclic Implicit Complexity

Gianluca Curzi, Anupam Das

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.

Original language	English
Title of host publication	LICS '22
Subtitle of host publication	Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science
Editors	Christel Baier
Publisher	Association for Computing Machinery (ACM)
Number of pages	13
ISBN (Electronic)	9781450393515
DOIs	https://doi.org/10.1145/3531130.3533340
Publication status	Published - 4 Aug 2022
Event	37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 - Haifa, Israel Duration: 2 Aug 2022 → 5 Aug 2022

Publication series

Name	LICS: Logic in Computer Science

Conference

Conference	37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022
Country/Territory	Israel
City	Haifa
Period	2/08/22 → 5/08/22

Bibliographical note

Funding Information:
The authors would like to thank Patrick Baillot, Alexis Saurin, Denis Kuperberg, and the anonymous reviewers for useful comments and discussions. This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1.

Publisher Copyright:
© 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.

Keywords

Cyclic proofs
Function algebras
Higher-order complexity
Implicit complexity
Safe recursion

ASJC Scopus subject areas

Software
General Mathematics

Access to Document

10.1145/3531130.3533340

Structure vs. Invariants in Proofs (StrIP)
Das, A. (Principal Investigator)
Medical Research Council
1/05/20 → 31/07/24
Project: Research Councils

Cite this

@inproceedings{bb6d3fb8911c489e8ce05f4c52c2b151,

title = "Cyclic Implicit Complexity",

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 (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.",

keywords = "Cyclic proofs, Function algebras, Higher-order complexity, Implicit complexity, Safe recursion",

author = "Gianluca Curzi and Anupam Das",

note = "Funding Information: The authors would like to thank Patrick Baillot, Alexis Saurin, Denis Kuperberg, and the anonymous reviewers for useful comments and discussions. This work was supported by a UKRI Future Leaders Fellowship, {\textquoteleft}Structure vs Invariants in Proofs{\textquoteright}, project reference MR/S035540/1. Publisher Copyright: {\textcopyright} 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.; 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022 ; Conference date: 02-08-2022 Through 05-08-2022",

year = "2022",

month = aug,

day = "4",

doi = "10.1145/3531130.3533340",

language = "English",

series = "LICS: Logic in Computer Science",

publisher = "Association for Computing Machinery (ACM)",

editor = "Christel Baier",

booktitle = "LICS '22",

address = "United States",

}

Curzi, G & Das, A 2022, Cyclic Implicit Complexity. in C Baier (ed.), LICS '22: Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science., 19, LICS: Logic in Computer Science, Association for Computing Machinery (ACM), 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022, Haifa, Israel, 2/08/22. https://doi.org/10.1145/3531130.3533340

TY - GEN

T1 - Cyclic Implicit Complexity

AU - Curzi, Gianluca

AU - Das, Anupam

N1 - Funding Information: The authors would like to thank Patrick Baillot, Alexis Saurin, Denis Kuperberg, and the anonymous reviewers for useful comments and discussions. This work was supported by a UKRI Future Leaders Fellowship, ‘Structure vs Invariants in Proofs’, project reference MR/S035540/1. Publisher Copyright: © 2022 Copyright held by the owner/author(s). Publication rights licensed to ACM.

PY - 2022/8/4

Y1 - 2022/8/4

N2 - 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 (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.

AB - 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 (ICC). Namely we introduce a circular proof system based on Bellantoni and Cook's famous safe-normal function algebra, and we identify proof theoretical constraints, inspired by ICC, to characterise the polynomial-time and elementary computable functions. Along the way we introduce new recursion theoretic implicit characterisations of these classes that may be of interest in their own right.

KW - Cyclic proofs

KW - Function algebras

KW - Higher-order complexity

KW - Implicit complexity

KW - Safe recursion

UR - http://www.scopus.com/inward/record.url?scp=85137007033&partnerID=8YFLogxK

UR - https://dl.acm.org/conference/lics/proceedings

U2 - 10.1145/3531130.3533340

DO - 10.1145/3531130.3533340

M3 - Conference contribution

AN - SCOPUS:85137007033

T3 - LICS: Logic in Computer Science

BT - LICS '22

A2 - Baier, Christel

PB - Association for Computing Machinery (ACM)

T2 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2022

Y2 - 2 August 2022 through 5 August 2022

ER -

Cyclic Implicit Complexity

Abstract

Publication series

Conference

Bibliographical note

Keywords

ASJC Scopus subject areas

Access to Document

Fingerprint

Projects

Structure vs. Invariants in Proofs (StrIP)

Cite this