迂回通向零：超越原始递归的函数的另一种形式化

现有两个著名的系统将全递归形式化至超越原始递归（\textbf{PR}）的范畴，即 G"odel 的系统 \textbf{T} 以及 Girard 和 Reynolds 的系统 \textbf{F}。系统 \textbf{T} 在类型化对象上定义递归，并能构造 Heyting 算术（\textbf{HA}）的所有函数。系统 \textbf{F} 引入了类型变量，可以定义系统 \textbf{T} 的递归。其结果是一个表达力等同于二阶 Heyting 算术（\textbf{HA}$_{2}$）的系统。尽管两者都能表达增长速度难以想象的函数，但在某些应用中需要更灵活的形式化。其中一种应用是针对图式 \textbf{LK}-证明（$CERES_{s}$）的 CERES 切割消除，其中递归的形状非常重要。在本文中，我们引入了一种没有类型论基础的快速生长函数形式化。该递归以自然数的有序集为索引。我们强调了我们提出的递归与 Wainer 层级之间的关系，以便与现有系统进行比较。我们可以证明，我们的形式化能够表达使用系统 \textbf{T} 可表达的函数。我们将与系统 \textbf{F} 及更高阶系统的比较留作未来工作。