講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
「型の理論」入門と題されたこのセミナーは、現代の数理論理学・計算機科学における最も深遠な問いの一つ、すなわち「プログラムの型」と「数学的命題の証明」はなぜ同一の構造を持つのか、という問いを軸に展開されます。
出発点は1930年代にChurchが定式化した「型のないラムダ計算」です。関数の抽象化と適用という極めてシンプルな規則だけで、あらゆる計算を表現できるこの体系は、チューリングマシンと計算能力において同等であることが知られています。しかしこの体系は、Ω結合子のような自己適用によって停止しない計算を許してしまうという本質的な問題を抱えています。
この問題への応答として「型付きラムダ計算」が導入されます。型を導入することで適用に制限が加わり、計算は必ず停止することが保証されます。そしてここに、1934年のCurryの発見と1969年（公開は1980年）のHowardの洞察が重なります。型付きラムダ計算における関数型の矢印「→」と、直観主義論理における含意の矢印「→」は、形式的に完全に一致する。これが「Curry-Howard対応」であり、「命題は型であり、証明は項である（Propositions as Types, Proofs as Terms）」という深い双対性を意味します。
この対応関係はMartin-Löfの「依存型理論（Dependent Type Theory）」へと発展し、全称量化子や存在量化子までもが型として統一的に扱われる体系が完成します。さらにCoqのような証明支援システムの理論的基盤となるCIC（Calculus of Inductive Constructions）、そして最前線としてVoevodskyが構築したHomotopy Type Theory（HoTT）へと議論は昇華します。HoTTにおいては「型は空間、項は点、等号は道（path）」という幾何学的解釈が与えられ、ホモトピー論と型理論の間に驚くべき対応が見出されます。このセミナー全体は、計算・論理・数学基礎論が一つの統一的な理論へと収束していく壮大な知的旅程です。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: 型のないラムダ計算
ラムダ記法を関数の抽象化表現として導入し、変数への値の代入（β簡約）を計算の本質として定式化します。停止しないΩ結合子やY結合子（不動点結合子）を通じて、型のない体系の表現力と限界の両面を示します [p.3〜p.14]。
■ Part 2: 型付きラムダ計算
型σから型τへの関数に型σ→τを与えることで適用に制約を課します。これにより型のない体系では許容されていたΩのような無限ループが排除され、計算の停止性が保証されます [p.32〜p.53]。
■ Part 3: 判断と論理式
「命題Aは真である」という判断が「命題Aは論理式である」という判断に先行することを示します。判断は知ることであり、証明は判断を明証なものにする行為そのものです [p.54〜p.70]。
■ Part 4: Natural Deduction（自然演繹）
GentzenとPrawitzが整備した命題論理版のNatural Deductionを紹介し、各論理記号に対して導入規則（Introduction）と削除規則（Elimination）を与えます [p.71〜p.90]。
■ Part 5: Curry-Howard対応
「p:Pはpが命題Pの証明である」と「p:PはpがPの型の要素である」という二つの解釈が同一の形式的記述を持つことを示します。命題は型であり、証明は要素である、という双対性がCurry-Howard対応の核心です [p.91〜p.104]。
■ Part 6: Dependent Type Theory
Martin-Löfが1980年代に構築した依存型理論を解説します。型が別の型の要素に依存して変化するΠ型を導入し、全称量化子や多相性（Polymorphism）を型として統一的に扱う体系を示します [p.105〜p.113]。
■ Part 7: Curry-Howard対応の証明（型と証明の双対性の形式的確立）
Simon Thompsonの方針に従い、「命題の証明」と「型の要素」それぞれに対してFormation・Introduction・Elimination・Computationの四種のルールを記述し、両者の形式的記述が完全に一致することを具体的に検証します [p.114〜p.152]。
■ Part 8: Calculus of Inductive Constructions（CIC）
Coqが採用するCIC（帰納的構成の計算体系）を解説します。Inductive型natの定義から自動生成されるnat_rect・nat_ind・nat_recの三つの型が数学的帰納法そのものを表現していることを示します [p.153〜p.166]。
■ Part 9: Homotopy Type Theory（HoTT）
Voevodskyが構築したHoTTにおいて、型は空間、項は点、等号は道（path）として解釈されます。同一性がホモトピーとして幾何学的に捉えられ、数学の新しい基礎付け「Univalent Theory」への道が拓かれます [p.167〜p.181]。
ページのナビゲート