Proof Theory and Dependent Type Theory: Distinct Foundations for Designing Proof Assistants

あなたは、究極の「証明助手（Proof Assistant）」を構築しようとしていると想像してください。それは、人間が数学や論理学の宿題を解く際に、それが100%正しいかどうかをチェックしてくれる超スマートなロボットです。何十年もの間、ほとんどのロボットは「依存型理論（Dependent Type Theory: DTT）」という特定の設計図に基づいて作られてきました。これは、非常に複雑でハイテクなレゴセットを使ってロボットを作るようなものです。そこでは、すべてのブロックに特定のラベルが付いており、パーツ同士を組み立てる前に、ラベルが完全に一致するかどうかをロボットがチェックします。

しかし、この論文の中で、著者であるデイル・ミラー（Dale Miller）は、別の、おそらくより優れたロボットの作り方を提案しています。彼は、構造的証明論（Structural Proof Theory）、具体的には**シーケント計算（Sequent Calculus）**と呼ばれるフレームワークに注目すべきだと主張しています。これは、硬直したレゴセットではなく、論理が成立している限り、パーツがスライドしたり形を変えたりできる、ダイナミックで動的なパズルとして考えることを意味します。

以下に、なぜミラーがこの「パズル」のアプローチが「レゴ」のアプローチよりも優れていると考えているのかを、6つの主要なアイデアを用いて解説します。

1. 「何（What）」と「どのように（How）」の分離

レゴの世界（DTT）では、ロボットは「どのような論理を使うか」と「どのように証明を構築するか」の2つを同時に決定します。それは、「私たちは赤いブロックだけを使ってタワーを建てることを許可され、積み上げる方法は垂直に重ねることのみである」と言うようなものです。
ミラーは、これらを分離すべきだと提案しています。まず論理（ゲームのルール）を決定し、その上で、その問題を解決するためのあらゆる証明構造を選択できるのです。これは、「サッカーをしたい」と決めた後、「ゴールを決める方法は、キックでも、ヘディングでも、あるいはルールが許すならネットキャノンを使うことでもよい」と気づくようなものです。シーケント計算を使えば、特定の硬直したスタイルを強制されることなく、多くの異なる「動き」（自然推論、タブロー、分解能など）を用いることができます。

2. 「コードとしての証明」の問題

レゴのアプローチでは、証明をコンピュータプログラム（λ項）として扱います。コンピュータはプログラムを実行することには長けていますが、非常に神経質です。時には、プログラムが答えに辿り着くまでに奇妙な経路を辿ったり、特定の型の入力を待っているために行き詰まったりすることがあります。
ミラーは、レゴのアプローチが「宇宙レベル（universe levels）」（型同士が衝突しないように整理するための複雑な仕組み）や「証明の無関連性（proof irrelevance）」（実際には重要ではない部分のチェックに時間を浪費すること）といった、厄介な問題に対処しなければならないことを指摘しています。シーケント計算のアプローチはよりシンプルです。証明を複雑なコードスクリプトとしてではなく、フローチャートのように直接的に扱うため、これらの重い型規則を心配する必要がありません。

3. 「古典論理」の扱い（「どちらか、または、どちらでもない」の問題）

ある種の論理は「直観主義的（intuitionistic）」（何かを存在させるには、それを構築して証明しなければならない）であり、別の論理は「古典的（classical）」（あることが「存在しない」ことを示すだけで、存在を証明できる）です。
レゴのアプローチは、この「古典的」なスタイルをスムーズに扱うのが苦手です。動作させるために、しばしば追加の、扱いにくいルールを加えなければなりません。ミラーは、シーケント計算が最初から両方のスタイルを等しく扱うように設計されており、かさ高いコンバーターを必要とせずに、どんなプラグにもフィットするユニバーサルアダプターのようなものであると主張しています。

4. 「たぶん（Maybe）」を受け入れる（非決定性）

これは非常に重要な点です。レゴのロボットは「決定論的（deterministic）」に作られており、証明をチェックするために単一の直線的な経路に従わなければなりません。もし行き止まりに当たると、彼らは停止します。
ミラーは、少しの「非決定性（non-determinism）」（推測とバックトラッキング）を許容することが、実はスーパーパワーになるのだと示唆しています。迷路を想像してみてください。決定論的なロボットは一つの道を歩み、壁に当たると停止します。非決定的なロボットは、一つの道を試してみて、壁に当たったら「おっと」と言って、即座に別の道を試すことができます。
ミラーは、証明チェッカーに「推測」とバックトラッキングをさせることで、提出される「証明書（証明の証拠）」をより小さくできると主張しています。ロボットが重労働（探索）を行うので、あなたはすべてのステップを書き記す必要はありません。これはトレードオフです。ロボットがより深く考える代わりに、提出する宿題の枚数を減らすことができるのです。

5. 「動くバインダ（Moving Binders）」の魔法

これがこの論文で最もエキサイティングな仕掛けです。論理では、変数（「すべての x について...」の「x」など）が「束縛（bound）」されていることがよくあります。レゴの世界では、これらの変数は固定されていることが多く、それらを扱うことは技術的な頭痛の種（有名なPOPLMarkチャレンジのような）になります。
ミラーは、これらの変数が**移動可能（mobile）**であるという視点を提案しています。彼はこれを λ-tree 構文 と呼んでいます。
変数を名札だと想像してください。レゴの世界では、もし人が動くと、名札が外れたり混乱したりするかもしれません。しかし、ミラーの世界では、名請はその人に「接着」されています。あなたが部屋の中（あるいは証明の中）でその人をどのように動かしても、名札はついて回ります。
彼は ∇-量化子（nabla quantifier） と呼ばれる特別なツールを導入しています。これは「ローカルスコープ」ボタンのようなものです。これを押すと、「この変数はこの特定の証明の部分にのみ属しており、決して外へ逃げ出すことはできない」ということを宣言します。これにより、プログラミング言語や、コンピュータ同士の通信をモデル化する方法である π-計算（パイ・カルキュラス）のような、複雑なルールを持つ言語について推論することが非常に容易になります。

6. Abella ロボット

ミラーは単にこれについて語っているだけでなく、これが機能することを証明するためのロボットを実際に構築しました。それが Abella です。
Abella は、これらのシーケント計算の原理に基づいて完全に構築された定理証明器です。Abella は、「動くバインダ」と「∇-量化子」を使用して、変数や名前付けに関する複雑な論理を容易に扱います。レゴベースのロボット（Coq や Lean など）は非常に人気があり、膨大な既成の証明ライブラリを持っていますが、Abella は、特定のトリッキーな問題（特に変数の名前付けや移動に関する問題）においては、この新しいアプローチの方がより自然でエレガントであることを示唆しています。

まとめ

ミラーは、レゴのロボット（依存型理論）が悪いとか、それらを捨て去るべきだと言っているわけではありません。それらが成熟しており、広く利用されており、多くの事柄において優れていることを認めています。
しかし、彼は、これらの証明助手の「基礎」を設計するにあたって、シーケント計算はより柔軟で、シンプルで、強力なツールキットを提供すると示唆しています。それは論理と構造を分離し、スマートな推測を取り入れ、「動く変数」という厄介な問題をエレガントに処理します。これは、論理の他の多くの分野で成功を収めてきたフレームワークを、対話型証明助手の世界でもう一度、異なる角度から見るための招待状なのです。