System Tの対話木の高さに明示的な順序数上界を与える
An Explicit Ordinal Bound for System T Dialogue Trees
この論文をやさしく読む
ひとことで言うと
System Tのプログラムに対応する対話木の高さへ、明示的な順序数の上限を与えます。
何に役立つ？
高階の計算が持つ整礎的な複雑さを、元の項の型から計算できる量で評価するための論理研究です。
この研究の面白いところ
各変換で対話の意味を厳密に保ったまま、型の水準に沿った有限回の処理で上限を積み上げます。Agdaでの形式化も行っています。
どこまで分かった？
指定された型の閉項が対象で、上限はε0未満です。形式化は明示した基礎論上の仮定の下で行われており、実行時間の通常の数値上限とは異なります。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
Escardóの対話解釈は、ゲーデルのSystem Tにおける各閉項t:(ι→ι)→ιに、整礎的で可算分岐する木D(t)を対応させる。ここでιは自然数型である。本研究では、その古典的な順序数としての高さがε₀未満であることを直接証明する。より正確には、元の項に現れる型のレベルから自然数K(t)≥2を計算し、h(D(t))<θ_{K(t)}を証明する。ただし、θ₀=ω、θ_{n+1}=ω^{θ_n}である。 証明では、再帰子を閉じた無限的テンプレートへ翻訳し、通常の型レベルで添字付けされた有限回の処理によってβ簡約基を除去する。翻訳と各処理は、対話の表示的意味を厳密に保存する。補助的なランクρは、代入に関する加法的上界を満たす。各処理により、ランクαは高々2^αとなる。これらの評価を、計算可能な初期上界ω+m(t)、および閉じた基底型正規形Nに対する対話の高さの上界2^{ρ(N)}と組み合わせることで、上記の指数塔による上界を得る。 意味を保存する翻訳によって、この結果をEscardóの元の組合せ子による解釈へ移す。基礎論的な仮定を明示した上で、古典的順序数を用いて証明をAgdaで形式化する。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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 $\epsilon_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))<\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.
著者のコメント
19 pages, 1 figure
arXiv ID: 2609.20369 ／ 要約の誤りについて