Explicit bounds on complexity of System T dialogue trees below epsilon naught
An Explicit Ordinal Bound for System T Dialogue Trees
Logic in Computer Science
Summary
This paper deals with a way to represent certain mathematical computations called System T terms as trees. The authors show these trees always have a complexity—measured by a special kind of counting called ordinal height—below a known large but well-understood limit named ε₀. They provide a concrete method to calculate an upper bound on this complexity based on the structure of the original term. The proof uses a new translation technique and formal verification to ensure accuracy.
What this means in practice
- •For functional programming language designers: Estimate and guarantee termination complexity in typed higher-order recursive programs using an explicit ordinal bound.
- •For formal verification engineers: Use the ordinal bound to analyze and certify the well-foundedness of computation trees generated by recursive functionals in proof assistants.
A theory result. No direct application yet.
Authors
MingKun Xiao, YiXuan Sun
Abstract
Escardó's dialogue interpretation assigns to each closed term $t:(ι\toι)\toι$ of Gödel's System~T a well-founded, countably branching tree $D(t)$, where $ι$ is the natural-number type. We give a direct proof that its classical ordinal height is below $ε_0$. More precisely, we compute a natural number $K(t)\ge2$ from the type levels occurring in the source term and prove $h(D(t))<θ_{K(t)}$, where $θ_0=ω$ and $θ_{n+1}=ω^{θ_n}$. Our proof translates recursors into closed infinitary templates and eliminates $β$-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 $ρ$ satisfies an additive substitution bound; each pass sends rank $α$ to at most $2^α$. Combining these estimates with a computable initial bound $ω+m(t)$ and a dialogue-height bound $2^{ρ(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.