An Explicit Ordinal Bound for System T Dialogue Trees
Mingkun Xiao Affiliation: Capital Normal University E-mail Yixuan Sun Affiliation: Kean University E-mail
Abstract
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
中文速览
论文研究的是：System T 里的高阶程序生成的对话树，分支深度可能无限增长，但其序数高度究竟能有多大。作者把递归器改写成表示有限迭代的无穷项模板，再按类型层级分轮消除 β-红ex，并在整个过程中保持对话树完全不变。通过给项定义秩、控制代入和每轮转换带来的指数增长，作者证明每个程序的对话树高度都低于 ε₀，更精确地低于由源程序类型层级决定的有限层 ω 指数塔。这个结果补上了此前只被提出或略述的 ε₀ 上界证明，并且经过 Agda 形式化，说明高阶递归程序的交互复杂度可以从语法结构中得到明确、可计算的序数界。
原文 arXiv:2609.20369;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2609.20369v1