哥德尔T系统的循环版本及其抽象复杂度

循环与非良基证明已成为处理具有归纳和/或递归形式的系统的元逻辑研究中日益流行的工具。本文研究哥德尔系统T的一个变体CT的表达能力，其中程序采用循环类型而非包含显式递归组合子。我们特别考察C的抽象复杂度（即类型层级），并证明哥德尔原始递归泛函可用循环推导更简洁地类型化，所用类型恰好比T中低一层。事实上，我们给出了两种设定之间的逻辑对应，将层级n+1的T的无量词类型1理论解释到层级n的C之中，反之亦然。我们还获得了关于循环“推导”的一些进一步结果与视角，即强规范化与合流、基于遗传可计算泛函的模型、类型2处的连续性，以及到在所有类型上计算相同泛函的$\T$项的翻译。