一句话：研究循环证明系统 C 的表达力，证明其与 Gödel 系统 T 等价，无收缩时恰好捕获原始递归函数。
本文研究基于正则表达式类型、受线性逻辑与非良基证明论启发的循环证明系统 C。C 的证明可视为强类型 goto 程序。作者证明 C 定义可计算全函数，并比较其与 Gödel 系统 T 的表达力：一般情况下二者在自然数上刻画相同函数；在仿射情形（去掉 contraction）则精确刻画原始递归函数，从而给 Dal Lago 关于仿射系统 T 的结果提供更一般的替代证明。无 contraction 时，作者通过分析循环并将其翻译为显式递归，给出 C 到 T 的直接统一编码；有 contraction 时是否存在此类翻译仍开放。表达力上界通过在不同二阶算术子系统 ACA0 与 RCA0 中形式化小步归约语义的弱规范化获得。
We study a cyclic proof system C over regular expression types, inspired by linear logic and non-wellfounded proof theory. Proofs in C can be seen as strongly typed goto programs. We show that they denote computable total functions and we analyse the relative strength of C and Gödel’s system T. In the general case, we prove that the two systems capture the same functions on natural numbers. In the affine case, i.e., when contraction is removed, we prove that they capture precisely the primitive recursive functions—providing an alternative and more general proof of a result by Dal Lago, about an affine version of system T. Without contraction, we manage to give a direct and uniform encoding of C into T, by analysing cycles and translating them into explicit recursions. Whether such a direct and uniform translation from C to T can be given in the presence of contraction remains open. We obtain the two upper bounds on the expressivity of C using a different technique: we formalise weak normalisation of a small step reduction semantics in subsystems of second-order arithmetic: ACA 0 and RCA 0 .
@article{paperbot1155,
title = {Cyclic proofs, system t, and the power of contraction},
author = {Denis Kuperberg and Laureline Pinault and Damien Pous},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434282}
}