セミナー「「型の理論」と証明支援システム」紹介 [20131216]

全体概要

本セミナー「型の理論と証明支援システム――Coqの世界」は、数学的証明とコンピュータの関係という根本的な問いを起点として、型の理論の歴史的展開を俯瞰し、証明支援システムCoqの実践的な使い方までを体系的に解説したものです [p.1], [p.2]。

現在、Homotopy Type Theory（HoTT）とそれを基礎付けるUnivalent Theoryが数学・計算機科学の両分野で熱い注目を集めています。この新しい潮流は、数学者Vladimir VoevodskyがPer Martin-Löfの型の理論を「再発見」したことに端を発しており、21世紀の数学とコンピュータサイエンスに大きな影響を与えつつあります [p.3]。

本セミナーの直接の対象はHoTTそのものではなく、HoTTに至る型の理論のオーバービューを与えたうえで、Martin-Löfの型の理論に基づく証明支援システムCoqの初等的な紹介を行うことを目的としています [p.5]。Coqは2013年にACMのSIGPLANのProgramming Languages Software Awardを受賞しており、その重要性が広く認められたタイミングでの解説となっています [p.5]。

「証明支援システム」とは、人間の証明をコンピュータが支援するシステムですが、見方を変えれば、コンピュータの証明を人間が支援しているとも言えます。コンピュータの進化の先には知性を持つ機械の実現があり、証明支援システムにおける人間と機械の双対的な「共生」は、それに至る一つの段階と捉えることができます [p.4]。

セミナーは三部構成を取ります。Part Iでは型の理論の歴史を俯瞰し、Part IIではCurry-Howard対応（命題と型の対応、証明と要素の対応）を詳述し、Part IIIではCoqの実際の使い方を、関数型プログラム言語としての側面と証明支援システムとしての側面の両面から解説します [p.2]。

講義のロードマップ

■ Part I: 「型の理論」をふりかえる

• この部の核心:

型の理論の歴史は100年以上前、RussellによるFregeの集合論のパラドックスの発見に端を発します。その後、Churchのラムダ計算、Curry-Howard対応、Martin-LöfのDependent Type Theory、そしてVoevodskyのHomotopy Type Theoryへと連なる壮大な知的系譜を概観します [p.7]。型とは何か、なぜ必要とされたのかという根源的な問いに対して、歴史的文脈から答えを提示します。

• 論理展開:
• Russellのパラドックス（R = { x | ¬(x∈x) }）の発見と、非述語的定義（impredicative definition）の問題分析から、型の階層構造による解決策が導入されました [p.10], [p.11], [p.12]。
• 直観主義・構成主義の立場から「存在証明には具体的な証人の構成が必要」という思想が生まれ、型の理論の哲学的基盤となりました [p.15]。
• Churchの型のないラムダ計算（1930年代）から型を持つラムダ計算（1940年）へ。型の導入により、Ω := (λx.xx)(λx.xx)のような停止しない計算が排除され、「型を持つラムダ計算では計算は必ず停止する」という重要な特性が確立されました [p.27], [p.31], [p.32]。
• Martin-LöfはDependent Type（Π(x:A).B(x)）を導入し、型が値に依存して変化する体系を構築。これが現在のCoq、Agdaの理論的基盤となりました [p.40], [p.44], [p.45]。
• VoevodskyのHoTTでは、型を「空間」、要素を「点」として解釈し、同一性をhomotopyで捉える革新的な視点が提示されました [p.51], [p.52]。

■ Part II: Curry-Howard対応について

• この部の核心:

Curry-Howard対応（「Propositions as Types」「Proofs as Terms」）は型の理論における最も重要な発見の一つです。論理における命題は型の理論の型に対応し、証明は型の要素に対応するという双対性（p : P）を、形式的な推論規則を通じて厳密に示します [p.58], [p.59], [p.60]。

• 論理展開:
• Curryが1934年にすでに発見し、Howardが1969年に深化させた対応関係は、型付きラムダ計算の矢印（→）と論理式の含意（→）の間の対応が核心です [p.37], [p.38]。
• 命題の証明のルールは Formation / Introduction / Elimination / Computation の四種類で体系化され、∧、∨、→、⊥、∀、∃、等号（=A）のすべてについて対応する型と要素のルールが並行して展開されます [p.75], [p.76], [p.77], [p.78], [p.93], [p.94]。
• ∧の証明はペア(p,q)、→の証明はλ抽象、∨の証明はinl/inr、∀の証明はλ抽象（全ての値に対応）、∃の証明はペア(a,b)として形式化されます [p.71], [p.76], [p.85], [p.110], [p.112]。
• Coqでの証明はGoalから後ろ向きにSub Goalをさかのぼる方式を取り、各tacticがこれらの推論規則に直接対応します [p.159]。

■ Part III: Coq入門

• この部の核心:

Coqは関数型プログラム言語としての側面と証明支援システムとしての側面を兼ね備えた言語です。Martin-LöfのDependent Type Theoryに基づき、1984年にINRIAで開発が開始されました。2013年のACM SIGPLAN Software Award受賞という実績が示す通り、数学・プログラム言語研究の両コミュニティで中心的なツールとなっています [p.126], [p.127], [p.128]。

• 論理展開:
• 関数型言語としては、帰納的データ型（Inductive）によるbool、nat、list、natBinTreeの定義、パターンマッチング、Fixpointによる再帰的定義が基本です。Listについてlength、app、map、reverseなどの基本関数が実装されます [p.141], [p.142], [p.150], [p.151], [p.152], [p.153]。
• 証明支援システムとしては、tactic（assumption、intro、apply、split、destruct、left/right、induction、rewrite、reflexivity）を用いてGoalをSub Goalに分解しながら証明を進めます [p.160], [p.161], [p.163], [p.164], [p.165], [p.171], [p.172], [p.176]。
• 具体的な証明例として、命題論理の定理（A→(A→B)→B）の証明、掛け算の交換法則（n×m = m×n）の帰納法による証明、二分木に関する定理の証明が段階的に示されます [p.181], [p.191], [p.220]。
• Search / SearchAbout / SearchPatternコマンドにより、証明に必要な補題・定理をデータベースから検索できます。mult_n_SmはSearchPattern(_ + _ = _ * _)で発見できることが示されます [p.211], [p.212], [p.213]。
• Coqで証明された定理は、Extraction Language HaskellまたはOcamlまたはSchemeコマンドにより、対応する関数型プログラムとして抽出可能です（例：length、appのHaskell/OCaml/Scheme出力）。これがCurry-Howard対応「Proof as Program」の実践的な体現です [p.227], [p.228], [p.230], [p.231], [p.232]。
• 最後に、Print命令による証明の関数としての表示（S1、S3、lemma1〜4、Mult_Commute等）を通じて、p : P（証明：命題）という双対性が具体的なλ式として確認できます [p.234], [p.235], [p.236], [p.237]。