一句话：通过基于 safe-normal 函数代数的循环证明系统，用证明论约束刻画多项式时间与初等可计算函数，连接循环证明与隐式计算复杂度。
循环证明近年来受到关注，并被提议作为研究（共）归纳推理的替代框架，也催生了一些基于循环推理的类型系统；但其复杂性理论层面尚不清楚，其循环结构比常见递归模式更复杂。本文将循环证明与隐式计算复杂度（ICC）联系起来：在 Bellantoni 与 Cook 的 safe-normal 函数代数基础上引入一个循环证明系统，并借鉴 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.