Definitional Inversion, Without Normalisation

あなたは、あらゆる本が数学的証明であり、棚自体が論理で構成されている、巨大で魔法のような図書館を築いていると想像してください。これが、LeanやIdrisのような現代の証明助手（proof assistant）の背後にある秘密のエンジンである、**依存型システム（dependent type systems）**の世界です。この世界では、ルールは非常に厳格です。もしあなたが「数字」とラベル付けされた棚に「猫」を置こうとしたら、図書館のセキュリティシステム（型チェッカー）は即座に「エラー！」と叫んであなたを止めなければなりません。この安全性は、**定義的等価性（definitional equality）**という概念に依存しています。これは、二つのものが本質的に同じであるかどうかを判断するための、図書館のやり方です。例えば、「正方形」は「等しい辺を持つ長方形」と同じでしょうか？ もしシステムが「イエス」と言えば、それらは同一のものとして扱われます。

しかし、これらのルールをチェックするのは非常に困難です。伝統的に、図書館の安全性を証明するためには、数学者たちはすべての本を最も単純で基礎的な形へと簡略化できること（このプロセスは**正規化（normalization）**と呼ばれます）を示さなければなりませんでした。しかし、多くの現代的で強力なライブラリは、無限であったり自己参照的であったりするように設計されており、それらは「最終的な停止状態」へと簡略化することができません。それは、フラクタルの形を無理やり平坦にしようとするようなものです。ただ詳細を見つけ続けるだけになってしまいます。長い間、もしシステムを簡略化できないのであれば、その安全性を証明することはできませんでした。この論文は、フラクタルの形を先に平坦にする必要なく、図書館の安全性をチェックする新しい方法を紹介しています。

---

無限のパズルと魔法の鏡

依存型システムを、巨大な自己チェック型のパズルだと考えてみてください。ピースは型（「数字」や「関数」など）であり、目標は、二つのピースを組み合わせたときに、それらが完璧にフィットすることを確認することです。このパズルにおける最も重要なルールは、**定義的反転（definitional inversion）**です。これは、「もし二つの複雑な構造が同じに見えるなら、その構成要素もまた同じでなければならない」という論理です。例えば、二つの関数型が同一であるならば、その入力型と出力型もまた同一でなければならない、というものです。これは、コンピュータが混乱することなく、複雑なコードを小さな断片へと安全に分解することを可能にします。

数十年にわたり、これらのピースが適合することを証明する唯一の方法は、合流性（confluence）（異なる簡略化の経路が同じ結果に到達するかどうかを確認すること）や、論理的関係（logical relations）（項がどのように振る舞うかを比較する複雑な手法）を用いることでした。しかし、これらの古い道具は壁に突き当たりました。合流性は、特定の「外延的（extensional）」なルール（関数はどのように書かれているかではなく、何をするかによって定義されるという$\eta$-法則など）を追加すると崩壊します。論理的関係は通常、システムが「正規化可能（停止可能）」であることを要求しますが、これは無限ループや自己参照的な型を許容する、多くの強力で現実的なプログラミング言語を排除してしまいます。

新しいアプローチ：可能性の地図

著者たち（コンピュータサイエンティストと数学者のチーム）は、ドメイン理論（domain theory）に基づいた新しい戦略を提案しています。パズルのピースを単一の最終的な形に強制的に簡略化させるのではなく、彼らはあらゆる可能な振る舞いの地図を構築します。

あなたが暗い森の中で謎の生物を特定しようとしていると想像してください。

• 古い方法： その生物が動きを止めて、真の最終形態を現すのを待つ。もし生物が動き続けているなら（無限ループの場合）、あなたはそれを特定できず、その森は安全ではないということになります。
• 新しい方法： 生物が動き止まるのを待ちません。代わりに、その足跡を観察します。左足の跡があり、次に右足の跡があり、再び左足の跡がある、ということを記録します。たとえ生物が歩き続けることがあっても、ステップのパターンを見ることで、その形を推測することができます。

論文の言葉では、これらの「足跡」は**コンパクト要素（compact elements）または有限の観測（finite observations）と呼ばれます。著者たちは、すべての型が最終的な答えではなく、「その型について観測可能なすべての有限なもの」によって表現される数学的な「ドメイン（構造化された空間）」を構築します。彼らは有限射影（finitary projectors）**という技術を用いて、このドメインを扱いやすい塊へと切り分けていきます。

彼らが発見したこと

この「足跡」を用いた手法を用いることで、チームは以下の条件下でも定義的反転が成立することを証明することに成功しました：

1. 「型の中の型（type-in-type）」（型が自分自身を含むことができるルール）を持つような、**簡略化が停止しない（non-normalizing）**システム。
2. 関数やペアがより直感的に振る舞うようにするが、従来の証明手法を壊してしまうトリッキーなルールである$\eta$-法則を含むシステム。

彼らはこれを、MLTT$\eta$（$\eta$-法則を持つマーチン＝レーフ型理論）と呼ばれる型理論の小さなコア・バージョンで実証しました。彼らは、たとえこの混沌とした、潜在的に無限なシステムであっても、もし二つの型が等しければ、その構成要素もまた等しくなければならないことを示しました。これは、型システムの「安全網」が、システムが乱雑で無限であることを許容している場合でも機能することを証明しており、非常に大きな成果です。

なぜこれが重要なのか

著者たちは単に小さな玩具のようなシステムでパズルを解いたのではありません。彼らの手法が**堅牢（robust）**であることを示しました。彼らは証明を以下に拡張しました：

• 依存和（dependent sums）（データのペア）。
• 単一型（unit types）（値が一つしかない型）。
• 不動点結合子（fixed-point combinators）（無限再帰を可能にするツール）。
• パターンマッチングを伴う自然数。
• 同一型（identity types）（二つのものが同じであることを証明するもの）。
• 証明無関連な命題（proof-irrelevant propositions）（証明の「内容」ではなく、それが存在すること自体が重要な場合）。

彼らはさらに、「厳密な命題の宇宙」のモデルを構築し、彼らのテクニックがLean、Agda、Rocqのような実世界のツールに見られる複雑な機能を扱えることを示しました。

限界と未来

この論文は、自身が「何をしないか」についても非常に明確です。この論文は、これらのシステムが「正規化する（常に停止する）」ことを証明するものではありません。実際、これは停止しないシステムを対象としています。また、未定義の変数（まだ値が埋められていない変数、いわゆる「中立項（neutrals）」）の問題については、閉じた項（closed terms）に対して解決した方法とは異なるアプローチをとっていますが、将来どのように解決できるかについての示唆も残しています。

著者たちはすでに、彼らの数学的証明をコードへと変換し、3つの異なる証明助手（Agda、Lean、Rocq）で3回にわたって検証を行っています。これは、彼らの手法が単なる理論的なアイデアではなく、実用的なツールであることを示唆しています。

まとめ

この論文は、魔法の図書館の建設者に新しい眼鏡を手渡すようなものです。以前は、本が静止して完成していなければ、図書館の安全性をチェックすることができませんでした。しかし今では、書きかけの本や、永遠に自己参照し続ける本に対しても、その安全性をチェックできるようになりました。最終的な目的地（停止）ではなく、**観測可能な振る舞い（足跡）**に焦点を当てることで、彼らは、私たちが想像しうる最も強力で複雑、かつ潜在的に無限な型システムへの扉を開きました。これは、「Lean4Lean」や「MetaRocq」といった、証明助手が自身のコードを検証するプロジェクトへの道を開くものであり、数学やソフトウェアを構築するために私たちが使用するツールを、より信頼できるものへと進化させるものです。