A Machine-checked Proof of Consistency for Impredicative Pure Type Systems

技術要約：非限定的純型システムにおける一貫性の機械検証済み証明

問題と背景
本論文は、型理論のメカニズム化、特に純型システム（PTS）のメタ理論的性質に関する課題に取り組んでいる。置換と$\beta$簡約の形式化における中心的な困難は、名前のキャプチャを防ぐための変数名の付け替えをどのように扱うかにある。従来の定義（Curry-Feysなど）は、非原始再帰的な名前の付け替えステップのために、項の長さに対する整礎的な帰納法を必要とするため、機械化が困難である。de Bruijn指数（dBI）、局所的名称付き構文（locally nameless syntax）、あるいは高階抽象構文（HOAS）といった代替手法は解決策を提供するが、それぞれ独自の欠点を持つ。dBIは人間にとっての可読性が低く、局所的名称付き構文はメタ理論的な結果を「汚染」するウェルフォームネス述語を必要とし、HOASは実行可能なコードの生成や決定可能性の問題の定式化を妨げることが多い。

著者らは、古典的な構文（名前付き変数を使用）を保持しつつ、Stoughtonの同時置換を利用するアプローチの実現可能性を評価することを目的としている。この手法は、バインドされた変数の名前の付け替えを単一の構造的再帰を通じて置換と同時に行うことで、ほとんどの証明において項の長さに対する整礎的な帰納法を必要とせずに済む。

手法
開発はAgda（v2.6.2.2）および標準ライブラリを用いて完全に機械検証されている。その手法は以下のコアコンポーネントに依存している：

1. Stoughtonの同時置換: 置換は変数から$\lambda$項への関数（$Sub = V \to \Lambda$）として定義される。演算 $M \bullet \sigma$ は構造的再帰によって定義される。$\lambda$抽象および$\Pi$型において、バインドされた変数は関数 $X$ によって選ばれた新しい名前 $y$ に書き換えられ、置換は古いバインド変数をこの新しい名前にマッピングするように更新される。これにより、抽象ごとに一度の再帰呼び出しのみが必要となり、原始再帰性が維持される。
2. $\alpha$-可換関係: 著者らは$\alpha$変換と可換な関係の理論を構築している。関係 $S$ が$\alpha$-可換であるとは、$M \sim_\alpha N$ かつ $N S P$ ならば、$M S Q$ かつ $Q \sim_\alpha P$ を満たす $Q$ が存在することを意味する。このフレームワークにより、著者らは$\alpha$変換まで含めた合流性をクリーンに扱うことができ、他の形式化で見られるような補題の重複を回避できる。
3. Takahashiによる合流証明の改訂: 元のTaitおよびMartin-Löfによる証明の代わりに、本論文では並行簡約（$\Rightarrow$）を用いたTakahashiによる改訂版を採用している。著者らは、簡約ステップの中に明示的な$\alpha$変換ルールを含まない並行簡約を定義し、代わりに五角形特性（$\alpha$変換まで含めたダイヤモンド特性の一般化）を利用して合流性を証明している。
4. 正規化の仮定: 一貫性の証明は、検討対象の特定のPTSが正規化可能である（すべての型付けられた項が弱正規化可能である）という仮定に基づいている。著者らは、Agdaのメタ言語に非限定性が欠如しているため、Agda内で非限定的なシステムの正規化を証明することは不可能であろうと指摘している。

主な貢献
本論文は、以下の3つの主要なメタ理論的性質の形式的証明を提示している：

1. $\beta$簡約の合流性: 著者らはPTSの基礎となる構文のChurch-Rosser定理を証明している。$\alpha$-可換関係の理論とTakahashiの並行簡約を利用することで、並行簡約のスター閉包が多段階$\beta$簡約と一致し、五角形特性を満たすことを確立している。
2. 型保存（Subject Reduction, SR）: 本論文は、簡約下での型の保存を形式化している。McKinnaとPollackのアイデアに従い、著者らは簡約をコンテキストへと拡張し、コンテキストの妥当性と対象の型保持に関する同時定理を証明している。これには、反転のための極めて重要な補題である**積の単射性（product injectivity）**の証明が含まれる。
3. 非限定的PTSの一貫性: 著者らは、特定の非限定的PTSのサブクラス（$(\ast, \square) \in \mathcal{A}$ および $(\square, \ast, \ast) \in \mathcal{R}$ のような特定の公理と規則を満たすもの）について、空のコンテキストにおいて型 $\Pi[x : s]x$（Curry-Howardの下での偽を表す）が空であることを証明している。この証明は、Coquandによる計算構成（CC）に対するペンと紙による証明を拡張したものである。それは、帰納的に定義された正規形式および中立形式の健全性と完全性、反転補題、および仮定された正規化の性質に依存している。

結果と評価

• 形式化の規模: 全体の開発は約**4,300行のコード（LoC）**で構成されており、そのうち3,000 LoCは先行研究によるStoughtonの置換およびPTS構文の基盤フレームワークに由来する。
• 比較: 著者らは、自らの成果をde Bruijn指数を用いた形式化（BarrasおよびWerner、約2,900 LoC）および局所的名称付き構文を用いた形式化（Aydemirら、約4,800 LoC）と比較している。彼らは、自らのアプローチが、使用される構文に関する透明性において優れていると主張している。なぜなら、古典的な表記法に極めて近い形をとるためである。
• 実現可能性: 結果は、古典的な構文と同時置換を用いるアプローチが、依存型理論に対して実現可能であることを示唆している。著者らは、わずかな補題のみが整礎的な帰納法を必要としたこと、そしてコードサイズが「爆発」しなかったことを指摘している。

意義と主張
本論文は、Stoughtonの置換を用いたアプローチが、特に$\alpha$変換の扱いに焦らず、メタ理論的な問題に対して「より明確な提示と扱い」を提供すると主張している。著者らは、自らの手法が、項を開いたり手動で新しいパラメータを管理したりする「表記上の煩雑さ」を回避しているため、局所的名称付きやde Bruijnのアプローチよりも人間にとって透明性が高いと断言している。

本研究の意義は、正規化を仮定すれば、古典的な構文を放棄することなく、非限定的システムの整合性の機械検証済み証明が可能であることを示した点にある。著者らは、不完全性定理の影響により、非限定的理論の正規化を完全に機械化することはAgdaにおいては不可能である可能性が高いことを謙虚に認めているが、一貫性の証明自体は、このようなシステムのための「正しさに基づく構築（correct-by-construction）」な型チェックアルゴリズムに向けた実質的な一歩である。本研究は、依存型理論の将来的な形式化に対する、当該フレームワークの有用性を検証するものである。