MiniLean4

# 命題上の多相的な恒等関数: すべての P について P -> P。
goal forall (P : Sort 0), P -> P
intro P
intro p
exact p
qed

本書とは

Lean、Coq、Agda といった対話的定理証明器の中核には、項が与えられた型を持つかを判定する小さなカーネル（kernel）がある。タクティクや記法、自動化などはカーネルに渡す項を作るものであり、カーネルが正しければ、ほかの部分にバグがあって定理の証明に失敗することはあっても、偽の定理を受理することはない。

MiniLean4 は、教育用の規模に縮めた証明支援系（proof assistant）のカーネルである。Lean 4、Coq、Agda が形式検証（formal verification）に使っているのと同じ種類の依存型理論を、数ファイルの Rust に収まるところまで削ぎ落としたものだ。Lean 4 が証明をどう検査するのか、Curry-Howard 対応が実際に何をもたらすのか、形式検証ツールの信頼がどこから来るのかを知りたいなら、その仕組みを何も隠さずに見せるのが本書である。

本書では、カーネルの仕組みを具体的に示す。各章で一つの概念を説明し、正確に定式化したうえで、それを実装する Rust コードを紹介する。カーネル、タクティク、パーサを合わせても実装は三千行に満たず、依存ライブラリもなく、本書はそのすべてを扱う。

本書だけで読み進められるように書いてあり、再帰関数と基本的な集合の記法が読めればよく、型理論や Lean の予備知識は必要ない。Lean を知っている読者には、見覚えのある話も多いだろう。

読み方

第 I 部では依存型理論の型検査器を作り、それがある論理の証明検査器になっていることを示す。第 II 部では帰納型（自然数、木、リスト、ベクトル、等式）と、証明項を組み立てるタクティク言語を加える。第 III 部では第 I 部と第 II 部で詳しく扱わなかった代入、α 同値、簡約の内部を調べるが、カーネルのバグが潜みやすいのはここである。第 IV 部では宇宙の階層がこの形をとる理由を説明し、メタ理論を述べる。付録には完全な証明、宇宙の設計を正当化するパラドックス、そしてスクリプト言語のリファレンスを収めた。

本書を通じて、4 種類の対話的な要素が登場する。

• プレイグラウンドはカーネルを実行する。スクリプトを編集し、実行ボタンを押して、出力を読む。
• エクスプローラはカーネル自身から見た項の姿を示す。構文木、規則ごとの型付け導出、一歩ずつの簡約、各変数がどの束縛子に属するか、そしてタクティクを適用するたびの証明状態である。エクスプローラはすべてライブで動き、項を変えればカーネルが計算し直す。
• ステッパーはアルゴリズムを一歩ずつ進め、各ステップ後の状態を示す。
• 呼び出し木は、型検査器がある項に対して行う再帰呼び出しの正確な列を、各呼び出しが対応する型付け規則とともに示す。

コードではと記したコラムは、直前に定義したものを実装している Rust の関数を指し示す。演習には解答が付いており、必要になるまで折りたたまれている。

自分でコードを動かす

リポジトリには、カーネル、コマンドラインの実行器、本書で使う例題スクリプトが含まれている。

cargo run -- examples/identity.leanmini
cargo run -- examples/nat-reflexivity.leanmini
cargo run -- examples/zero-add.leanmini
cargo run -- examples/generic-list.leanmini
cargo run -- examples/generic-vec.leanmini
cargo test

引数なしで cargo run を実行すると対話セッションが始まり、同じコマンドを一行ずつ受け付ける。言語の説明は付録 E にある。

ソースは本書の流れに沿って構成してある。