全体概要

本セミナー「型の理論と証明支援システム――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]。型とは何か、なぜ必要とされたのかという根源的な問いに対して、歴史的文脈から答えを提示します。

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

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

■ Part III: Coq入門

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