テクニカル・サマリー：グローバル・トレース条件を持つ無限型ラムダ計算

問題提起

本論文は、全域関数（total functions）と意味のある無限簡約をサポートする、堅牢な無限型ラムダ計算を定義するという課題に取り組んでいる。Kennawayらによって確立された無限型ラムダ計算（$\Lambda^\infty$）は、無限の項や簡約を許容するものの、「無意味な」項（例：$0\ 0$ や $\text{succ}(\lambda x.x)$）や、意味のある出力を生成することなく無限に赤簡約（redex）へと簡約し続ける「アクティブな」項を許容してしまう。さらに、標準的な無限型項の型システムは、型の唯一性を保証できなかったり、型 $\text{Nat}$ の閉項が必ず数（numeral）に簡約されることを保証できなかったりすることが多い。著者らは、算術定数（$0, \text{succ}, \text{cond}$）を導入した $\Lambda^\infty$ を拡張し、強収束性と全域性を保証する条件を備えた、ゲーデルのシステムTに近い型システムを構築することを目指している。

手法

1. 項集合の構成

著者らは、構文的および意味論的な健全性を確保するために、一連の連続的な制限を通じて計算系を定義している。

• 行項（Row-Terms, $\text{Row-}\Lambda^\infty_T$）: 変数、$\lambda$ 抽象、適用、および算術定数（$0, \text{succ}, \text{cond}$）によって生成される、おそらく無限の項からなる基本集合。これらの項は、有限項の距離完備化の元である。
• 有限変数項（Finite Variable Terms, $\text{FinVar-}\Lambda^\infty_T$）: 自由変数が有限個しか含まれない行項のサブセット。この制限は、曖昧さなく $\alpha$ 等価性と代入を余帰納的に定義するために極めて重要である。
• 型付けされた項（Well-Typed Terms, $\text{WTyped}$）: 特定の型システムにおける導出を許容する $\text{FinVar-}\Lambda^\infty_T$ の項。
• GTC項（GTC-Terms, $\text{GTC-}\Lambda^\infty_T$）: **グローバル・トレース条件（GTC）**を満たす型付けされた項の最終的なサブセット。

2. 型システムとトレース関係

著者らは、標準的な単純型ラムダ計算とは異なる特徴を持つ型システム（図1）を導入している。

• シーケンスとしてのコンテキスト: コンテキストは変数の型の集合ではなく有限シーケンスであり、明示的な弱化（weakening）および交換（exchange）規則（$wk$）を必要とする。
• 分割適用規則: 適用規則は、$apv$（引数が変数の場合）と$ap\neg v$（それ以外の場合）に分かれており、構造的な縮約を反映している。
• トレース関係: システムは、コンテキスト内の変数と引数の位置にある型を結びつける「トレース関係」（導出における青と赤の矢印として可視化される）を取り入れている。
  • 静止（Stationary, 青）: 非減少の参照を表す。
  • 進行（Progressing, 赤）: $\text{cond}$ 項の結論における第一引数を、前提における対応する引数へと具体的に結びつけ、値の減少を表す。

3. グローバル・トレース条件（GTC）

BrotherstonとSimpsonによる循環証明（Cyclic Proofs）、およびDasによる循環的システムT（Cyclic System T）の概念を適応させ、GTCは導出木の上の定義として導入される。

• トレース: 導出の枝に沿ったトレース関係の連鎖。
• 進行点（Progress point）: 条件分岐の簡約において発生する、赤（進行）のトレース関係。
• GTC要件: 導出がGTCを満たすとは、あらゆる無限の枝において、無限回進行するトレースが含まれることである。
• この条件は、「アクティブな」項（出力のない無限ループ）や、全域的関数体を表さない項を効果的に排除する。

4. 簡約と収束

著者らは $\beta$ 簡約と $\text{cond}$ 簡約のための簡約規則を定義している。無限の簡約を扱うために、著者らは cond-収束（cond-convergence） を導入している。

• 簡約が cond-収束 であるとは、任意の極限順序数において、縮約された赤簡約（特に $\text{cond}$ の右側の枝にあるもの）の深さが無限大に発散することである。
• これは標準的な強収束よりも強い条件であり、$\text{cond}$ による再帰呼び出しが「else」ブランチにおいて無限ループに陥らないことを保証する。

主要な貢献と結果

1. 強収束性と正規化

中心的な定理（定理 3.2）は、任意の項 $t \in \text{GTC-}\Lambda^\infty_T$ について以下を確立している。

• すべての簡約は cond-収束する（したがって強収束する）。
• 正規化: 常に最小の $\text{cond}$ 深さの赤簡約を簡約する戦略は、高々 $\omega$ ステップで正規形に停止する。
• 全域性: $t$ が型 $\text{Nat}$ の閉項である場合、これらの簡約は有限ステップで $\text{succ}^n(0)$ という形式の数に停止する。

2. 型の唯一性と型保存性（Subject Reduction）

定理 2.3 は、$\text{GTC-}\Lambda^\infty_T$ の項について以下を証明している。

• 唯一性: コンテキスト $\Gamma$ に対して、$\Gamma \vdash t : A$ が証明可能となる一意の型 $A$ が存在する。
• 型保存性（Subject Reduction）: もし $\Gamma \vdash t : A$ が証明可能であり、$t \to t'$ ならば、$\Gamma \vdash t' : A$ もまた証明可能である。
• 著者らは、証明自体は一意ではないものの、コンテキストを自由変数に制限し、冗長な弱化規則を崩壊させることで、一意の標準形へと変換できると述べている。

3. 表現力と等価性

• 本論文は、正則な項に制限した場合、この計算系が Das の循環的システム T（$\lambda$ を持たない無限型システム T のバージョン）で定義される全域関数と正確に一致することを論じている。
• したがって、本システムはゲーデルのシステム T と同じ表現力を備えている。
• 著者らは、この計算系において 極限における Church-Rosser 性 が成立すると主張しており、これにより $\text{Nat}$ の閉項に対する結果となる数の唯一性が保証される。

意義と主張

本論文は、型理論的な条件（GTC）を通じて、算術を伴う無限型ラムダ計算の全域性と強収束性を保証する健全な基礎を提供することを主張している。循環証明の技法をラムダ計算に適応させることで、著者らは、意味のない無限の項やアクティブなループを排除し、型付けされた項が全域的関数体として振る舞うことを成功させた。

その意義は、無限の項や簡約が存在する場合でも、グローバル・トレース条件が強正規化特性を強制できることを示し、無限書き換えシステムと型理論の間の溝を埋めた点にある。著者らは、自らのシステムがゲーデルのシステム T と同等の表現力を持つと控えめに推測しており、$\text{GTC-}\Lambda^\infty_T$ を Das の循環的システム T のラムダ計算による拡張として位置づけている。