Cyclic Implicit Complexity
Cyclic Implicit Complexity
复制标题
循环隐式复杂度
DOI：
10.1145/3531130.3533340
复制
发表时间：
2022
期刊：
影响因子：
--
通讯作者：
Curzi G
中科院分区：
文献类型：
--
作者：
Curzi G
近年来，循环（或循环）证明受到越来越多的关注，并被提议作为研究（共）归纳推理的替代设置。特别地，现在已经提出了几种基于循环推理的类型系统。然而，人们对循环证明的复杂性理论方面知之甚少，循环证明表现出复杂的循环结构，这与更常见的“递归方案”不同。本文试图弥合循环证明和隐式计算复杂性（ICC）之间的差距。也就是说，我们引入了基于 Bellantoni 和 Cook 著名的安全正规函数代数的循环证明系统，并且受 ICC 启发，我们确定了证明理论约束，以表征多项式时间和基本可计算函数。在此过程中，我们引入了这些类的新的递归理论隐式特征，这些特征本身可能令人感兴趣。
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.
登录
查看更多内容
DOI：
10.1109/lics.1991.151625
发表时间：
1991
期刊：
[1991] Proceedings Sixth Annual IEEE Symposium on Logic in Computer Science
影响因子：
--
作者：
D. Leivant
通讯作者：
D. Leivant
（克莱恩行动）的非充分证明理论（代数格）
DOI：
10.4230/lipics.csl.2018.19
发表时间：
2018
期刊：
ArXiv
影响因子：
--
作者：
Anupam Das;D. Pous
通讯作者：
D. Pous
Büchi 可判定性定理的逻辑强度
DOI：
10.23638/lmcs-15(2:16)2019
发表时间：
2016
期刊：
ArXiv
影响因子：
--
作者：
L. Kolodziejczyk;H. Michalewski;Cécilia Pradic;Michal Skrzypczak
通讯作者：
Michal Skrzypczak
更高类型的递归、分支和多项式时间
DOI：
10.1016/s0168-0072(00)00006-3
发表时间：
2000
期刊：
Ann. Pure Appl. Log.
影响因子：
--
作者：
S. Bellantoni;Karl;H. Schwichtenberg
通讯作者：
H. Schwichtenberg
循环算术相当于皮亚诺算术
DOI：
10.1007/978-3-662-54458-7_17
发表时间：
2017
期刊：
2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
--
作者：
A. Simpson
通讯作者：
A. Simpson