系统 T 对话树的显式序数界

中文速览

论文研究的是：System T 里的高阶程序生成的对话树，分支深度可能无限增长，但其序数高度究竟能有多大。作者把递归器改写成表示有限迭代的无穷项模板，再按类型层级分轮消除 β-红ex，并在整个过程中保持对话树完全不变。通过给项定义秩、控制代入和每轮转换带来的指数增长，作者证明每个程序的对话树高度都低于 ε₀，更精确地低于由源程序类型层级决定的有限层 ω 指数塔。这个结果补上了此前只被提出或略述的 ε₀ 上界证明，并且经过 Agda 形式化，说明高阶递归程序的交互复杂度可以从语法结构中得到明确、可计算的序数界。

摘要

Escardó 的对话解释为哥德尔系统 T 中每个闭项 $t:(\iota\to\iota)\to\iota$ 指定一棵良基、可数分支树 $D(t)$，其中 $\iota$ 是自然数类型。我们直接证明，其经典序数高度低于 $\varepsilon_{0}$。更精确地说，我们根据源项中出现的类型层级计算一个自然数 $K(t)\geq 2$，并证明 $h(D(t))<\theta_{K(t)}$，其中 $\theta_{0}=\omega$，且 $\theta_{n+1}=\omega^{\theta_{n}}$。我们的证明将递归子转换为闭无穷模板，并通过按通常类型层级索引的有限轮次消除 β-红ex。该转换以及每一轮都严格保持对话指称不变。一个辅助秩 $\rho$ 满足加性代换界；每一轮至多将秩 $\alpha$ 变为 $2^{\alpha}$。将这些估计与可计算的初始界 $\omega+m(t)$，以及针对闭的地面范式 $N$ 的对话高度界 $2^{\rho(N)}$ 相结合，即可得到所述的塔式界。一个保持语义的转换将该结果推广到 Escardó 原始的组合子解释。我们在明确的基础假设下，基于经典序数，在 Agda 中形式化了这一证明。

Escardó’s dialogue interpretation assigns to each closed term $t:(\iota\to\iota)\to\iota$ of Gödel’s System T a well-founded, countably branching tree $D(t)$ , where $\iota$ is the natural-number type. We give a direct proof that its classical ordinal height is below $\varepsilon_{0}$ . More precisely, we compute a natural number $K(t)\geq 2$ from the type levels occurring in the source term and prove $h(D(t))<\theta_{K(t)}$ , where $\theta_{0}=\omega$ and $\theta_{n+1}=\omega^{\theta_{n}}$ . Our proof translates recursors into closed infinitary templates and eliminates $\beta$ -redexes by a finite sequence of passes indexed by ordinary type level. The translation and every pass preserve the dialogue denotation exactly. An auxiliary rank $\rho$ satisfies an additive substitution bound; each pass sends rank $\alpha$ to at most $2^{\alpha}$ . Combining these estimates with a computable initial bound $\omega+m(t)$ and a dialogue-height bound $2^{\rho(N)}$ for closed ground normal forms $N$ yields the stated tower bound. A semantics-preserving translation transfers the result to Escardó’s original combinatory interpretation. We formalise the proof in Agda over classical ordinals under explicit foundational assumptions.

术语表

Gödel’s System T

哥德尔系统 T

dialogue interpretation

对话解释

dialogue tree

对话树

well-founded tree

良基树

classical ordinal height

经典序数高度

ordinal height bound

序数高度界

type level

类型层级

finite-type recursion

有限类型递归

primitive recursion

原始递归

simply typed λ-calculus

简单类型 λ 演算

infinitary term

无穷项

infinitary template

无穷模板

β-redex

β-红ex

β-reduction

β-归约

normal form

范式

ordinal rank

序数秩

additive substitution bound

加性代换界

ordinal exponentiation

序数幂

ε₀

ε₀

ω-exponential tower

ω 指数塔

countably branching tree

可数分支树

dialogue denotation

对话指称

grafting

嫁接

leaf relabelling

叶重标记

combinatory interpretation

组合子解释

System T recursor

系统 T 递归子

Agda

Agda

TypeTopology

TypeTopology