The Global Orientation Barrier in Step-Duplicating Recursors: Impossibility, Modular Escape, and a Certified Witness

本論文は、ステップ重複再帰関数における直接構成的測度の限界を Lean 4 で機械検証し、依存対や部分項基準に基づく射影的手法がその障壁を回避して終止性を証明できることを、TTT2 や CeTA による外部検証と組み合わせて実証しています。

要約

この論文は、**「コンピュータの計算がいつ終わるか（停止性）」を証明する際に見つかった、ある不思議な「壁」**について書かれたものです。

著者のモーゼス・ラフナマさんは、この壁を「グローバル・オリエンテーション・バリア（全体的な方向付けの壁）」と呼んでいます。

これをわかりやすく説明するために、**「巨大な積み木のお城」と「魔法の鏡」**という例えを使って解説します。

---

1. 物語の舞台：積み木のお城（KO7）

まず、この論文で扱っているのは、7 種類の積み木と 8 つのルールで動く「積み木のお城」です。
このお城には、ある**「複製ルール」**という魔法があります。

• ルール： 「ある積み木（ステップ）を、次の段の積み木に2 つコピーして乗せる」

例えば、「赤いブロック（ステップ）」を 1 つ持っている状態から、次の段を作る時に、その赤いブロックを2 つ並べて乗せるようなルールです。
この「1 つが 2 つになる」という現象が、このお城の最大の特徴（そして問題）です。

2. 壁の正体：なぜ「普通のものさし」は使えないのか？

計算がいつ終わるか（無限に続かないか）を証明するには、通常「ものさし」を使います。
「この操作を 1 回行うたびに、お城の『重さ』や『高さ』が必ず減るなら、いつか必ず地面（0）に届くはずだ」という考え方です。

しかし、この論文は**「ある特定の種類のものさし（グローバル・メジャー）」では、このお城の停止性を証明できない**と突き止めました。

🧱 例え話：「増える重さ」の罠

普通のものさしは、「積み木の重さを全部足し合わせる」という考え方をします。

• 操作前： 赤いブロックが 1 つ。重さ = 10。
• 操作後： 赤いブロックが 2 つに増え、さらに新しいブロックが乗る。
  • 普通のものさしは「2 つの赤いブロックの重さ（20）＋ 新しいブロック」を足します。
  • 結果、**操作後の重さは操作前より「増えている」**ように見えてしまいます。

「重さが増えているのに、いつか終わるなんてありえない！」と普通のものさしは判断してしまいます。
これが**「壁」です。
この壁にぶつかるのは、「複製されたブロックの重さを全部足し上げようとする、真面目で包括的なものさし」**だけなのです。

3. 壁を乗り越える方法：「魔法の鏡（DP 法）」

では、どうすればこのお城がいつか終わることを証明できるのでしょうか？
論文は、**「ある特定の部分だけを見て、他は無視する」**という方法（依存対法：Dependency Pairs）が壁を越えられると示しました。

🪞 例え話：「鏡の魔法」

この魔法の鏡は、お城の**「階段の段数（カウンター）」**にだけ焦点を当てます。

• 複製された赤いブロックは、鏡の中では**「透明」**になります。
• 鏡は「赤いブロックが 2 つになっても、段数（カウンター）は 1 つ減っているだけだ」と見ます。

「段数が減っているなら、いつか底に届くはずだ！」と、この鏡は即座に証明してしまいます。
この鏡は、「複製されたブロック（重さ）」を無視することで、壁をすり抜けたのです。

論文は、**「包括的なものさし（壁にぶつかる）」と「部分的な鏡（壁を越える）」**の境界線を、コンピュータで厳密に証明しました。

4. なぜこの発見が重要なのか？

この研究は、単に「積み木ゲーム」の話ではありません。

• 「壁」の正体： 計算の中で「同じデータを複製して使う」処理がある場合、単純な「全体の重さ」で計算の終わりを証明するのは不可能な場合がある。
• 「脱出」の正体： 複製されたデータは「計算の本質（段数）」には関係ない「邪魔な重り」に過ぎない。それを切り捨てて、本質的な部分だけを見れば、証明は簡単になる。

これは、**「複雑な問題を解くとき、全体を一度に考えようとすると行き詰まるが、重要な部分だけを取り出して考えれば解決できる」**という、プログラミングや数学の重要な教訓を示しています。

5. 論文の成果まとめ

著者は、この発見を以下の形で完成させました。

1. 不可能性の証明（壁の確認）： 「複製ルール」がある限り、特定の種類の「全体を足し上げるものさし」では絶対に証明できないことを、コンピュータ（Lean 4）に厳密に証明させました。
2. 解決策の提示（壁の脱出）： 「複製されたデータを無視する」方法（依存対法）が有効であることを示し、なぜそれが有効なのかを説明しました。
3. 安全なお城の完成： 壁にぶつからないよう、少しルールを制限した「安全なバージョン（SafeStep）」を作り、そこで「停止すること」「同じ答えにたどり着くこと（一貫性）」を証明し、実際に動く「正規化プログラム」を完成させました。
4. 外部の検証： 有名なツール（TTT2）を使って、制限のない元のルールも「停止する」ことを確認しました（ただし、その証明は「鏡」を使わないとできないことも確認）。

結論：何がすごいのか？

この論文は、**「なぜある計算手法が失敗するのか、そしてなぜ別の手法が成功するのか」**という、根本的な理由を「複製」という現象に結びつけて、数学的に厳密に解き明かしました。

まるで、**「なぜこの迷路には出口がないように見えるのか（壁）」を分析し、「実は特定の角度から見れば出口が見える（脱出）」**ことを証明したようなものです。

これにより、将来のプログラミング言語や AI の計算理論において、「どこまで単純な方法で証明できるか」という境界線が、より明確になりました。

技術概要

論文「ステップ重複再帰関数におけるグローバル・オリエント障壁：不可能性、モジュール脱出、および認証された証人」の技術的サマリー

著者: Moses Rahnama (Mina Analytics)
日付: 2026 年 2 月
形式: Lean 4 による完全機械的検証および TTT2 による外部検証を併用

1. 問題設定と背景

本論文は、第一階項書き換え系（TRS）における**「ステップ重複再帰関数（step-duplicating recursors）」の終止性（termination）証明に関する、グローバル（直接・集約的）な手法とモジュール（射影・依存対）な手法**の間に存在する明確な境界（障壁）を特定し、機械的に証明したものです。

具体的には、以下の 4 つの設計条件を満たす最小限の書き換え系 KO7 を対象としています：

1. 束縛演算子の不在: 対象言語に $\lambda$ 抽象化や自由変数がない（第一階のみ）。
2. ツリー意味論（共有なし）: 計算状態は項ツリー内にのみ保持され、外部メモリや共有ポインタは存在しない。
3. 対象レベルの公理の不在: 項構造に対する等式理論や代数法則（例：$app(t, t) \to t$）は存在しない。
4. 無制限のステップ重複再帰: 再帰規則において、ステップ引数 $s$ が右辺で重複して現れる（例：$rec(b, s, \sigma(n)) \to f(s, rec(b, s, n))$）。

この条件下では、重複した引数 $s$ が構造的には存在するが、構造的に「閉じ込め（App Trap）」られており、再帰カウンタとして機能しないという特徴があります。

2. 主要な貢献と手法

2.1. 不可能性定理の機械的証明

著者は、2 つの広範な**直接構成可能測度（Direct Compositional Measures）**のクラスを Lean 4 で形式化し、それらが KO7 の重複再帰規則を厳密に方向付け（strictly orient）できないことを証明しました。

• Tier 1（加法的測度）: 各構成子に重みを割り当て、複合項の測度を重みの和とするもの。
• Tier 2（抽象的構成測度）: 部分項測度を結合する任意の関数を持ち、$app(x, y) > x$ かつ $app(x, y) > y$ という「app 部分項公理」を満たすもの。

定理 9.1: 上記のいずれのクラスに属する測度も、すべての項インスタンスに対して重複再帰規則 $rec(b, s, \delta(n)) \to app(s, rec(b, s, n))$ を厳密に減少させることは不可能である。

• 理由: 右辺には $s$ が 2 つ現れるため、$s$ が十分に大きくなると、左辺の測度よりも右辺の測度の方が大きくなり、減少条件を満たせなくなる（「ポンピング」現象）。
• 検証: この不可能性は、最小の 4 構成子サブシグネチャ（Rec$\Delta$-core）でも成り立つことが証明されています。

2.2. モジュール脱出（DP 射影）の特定

一方、依存対（Dependency Pairs, DP）フレームワークと**部分項基準（Subterm Criterion）**を用いると、この障壁を回避できることを示しました。

• 定理 9.2: 再帰カウンタ（第 3 引数）にのみ射影する関数 $\pi$ を定義すると、重複するステップ引数 $s$ を無視（投影）できるため、規則を厳密に方向付けられます。
• メカニズム: DP フレームワークは、$app$ 構成子を「構成子」として扱い、その内部に閉じ込められた重複した $s$ をチェーン分析から除外します。これにより、重複による測度の増大を回避し、再帰カウンタの減少のみを評価することで終止性を証明します。
• 結果: この手法は、直接構成測度が要求する「app 部分項公理」を違反することで障壁を脱出します。

2.3. 認証された証人 KO7 と安全な断片（SafeStep）

KO7 系全体は終止しますが、局所的な結合性（local confluence）を持たないため、ユニークな正規形を保証できません。そこで、SafeStepと呼ばれるガード付き部分関係（安全な断片）を定義し、以下の認証チェーンを構築しました：

1. 強正規化（Strong Normalization）: 計算可能な三重辞書式測度 $\mu_3 = (\delta\text{-flag}, \kappa_M, \tau)$ を用いて証明。
   • $\delta\text{-flag}$: 再帰ステップの位相ビット。
   • $\kappa_M$: Dershowitz-Manna 多集合順序に基づくランク。
   • $\tau$: 非重複時のタイブレーク用自然数負荷。
2. 結合性（Confluence）: ニューマンの補題（SN + 局所結合性 $\Rightarrow$ 結合性）を適用。局所結合性の仮定をすべて機械的に解消（discharge）し、ユニークな正規形を証明。
3. 認証された正規化器: 上記測度に基づく全関数・健全な正規化関数を定義し、その全性と健全性を Lean で証明。
4. 順序数の較正: 証明の順序数上限を $\varepsilon_0$ 未満（具体的には $\omega^\omega \cdot 2$ 以下）に機械的に評価し、下限として $\omega^\omega$ での全射性を証明。

2.4. 外部検証（TTT2/CeTA）

KO7 の完全な書き換え系（ガードなし）の終止性を、外部ツール TTT2 で検証しました。

• 結果: 依存対＋部分項基準を用いた 3 つの戦略（FAST, COMP, LPO）が「YES（終止）」を返しました。
• 対照: 多項式解釈（POLY）や KBO などの直接/グローバルな 5 つの戦略はすべて「MAYBE（証明発見失敗）」を返し、機械的な不可能性定理と一致しました。
• 認証: CeTA による独立した証明検証も完了しています。

3. 結果と意義

3.1. 理論的意義

• 障壁の明確化: 重複再帰を持つ系において、「グローバルな集約測度」が本質的に失敗し、「モジュールな射影手法」が成功する境界を、特定の公理系に基づいて厳密に定義・証明しました。
• 証明論的コストの比較:
  • DP 部分項基準：基本的な整礎性（$\ll \varepsilon_0$）で証明可能。
  • 経路順序（LPO）：一般にはクルーザルの木定理（$\Pi^1_1\text{-CA}_0$）の強さを必要とするが、有限シグネチャでは構造的帰納法で済む。
  • 直接測度：この特定の構造では不可能。

3.2. 実用的意義

• 機械的検証の完全性: 約 7,000 行の Lean 4 形式化により、不可能性定理から安全断片の終止性・結合性、正規化器の健全性までを「sorry」なしで証明しました。
• ツールとの連携: 形式化された不可能性結果と、外部ツールの成功事例を対比させることで、終止性解析ツールの限界と可能性を定量的に示しました。
• ** ablation study（除去実験）**: 重複を除去した線形再帰版では、単純な加法的サイズ測度ですぐに終止性が証明されることを示し、障壁の根源が「重複」そのものであることを確認しました。

4. 結論

本論文は、ステップ重複再帰を持つ書き換え系において、直接構成測度が直面する構造的な不可能性を特定し、依存対フレームワークがどのようにしてこの障壁を脱出するかを機械的に証明しました。KO7 という最小限の証人系を用いて、終止性、結合性、正規化器の完全な認証チェーンを構築し、理論的な境界と実用的な検証手法の両面から、現代の書き換え理論における重要な知見を提供しています。

アーティファクト:
形式化コード（Lean 4）と TTT2/CeTA の証明証は、以下のリポジトリで公開されています。
https://github.com/MosesRahnama/OperatorKO7