講演資料
講義資料スライドの表紙です。上のスライド画像をクリックすると、同じ画面のまま全編のPDF資料を快適に閲覧・印刷することができます。
セミナーの概要
本セミナー「型の理論入門」は、現代の計算機科学・数学基礎論・論理学を貫く一本の深い問いに答えようとする試みです。その問いとは、「計算すること」「推論すること」「証明すること」は本質的に同じことなのか、という問いです。
20世紀初頭にAlonzo Churchが導入したλ計算は、関数の「名前なし」表現と計算の抽象化という革命的なアイデアをもたらしました。型のないλ計算はチューリング完全な計算モデルですが、Ω = (λx.xx)(λx.xx)のように計算が停止しない式を許容します。これに型の制約を導入した「型付きλ計算」は、計算の停止性を保証しつつ、プログラミング言語の理論的基礎を提供します。
1930年代にCurryが発見し、1960年代にHowardが精密化した「Curry-Howard対応」は、この探求における最大のブレイクスルーです。型付きλ計算の関数型「σ→τ」と、論理式「A→B」（含意）の間に深い対応関係があることを示すこの発見は、「命題は型である」「証明は項（プログラム）である」というPropositions as Types（PAT）の洞察へと結実しました。
この対応関係を基盤に、Per Martin-Löfは1980年代に「依存型理論（Dependent Type Theory）」を構築します。型が値に依存して変化するという依存型の概念は、Coq・Agdaといった証明支援システムの理論的礎となり、数学的帰納法さえも帰納的型（Inductive Type）として内部に取り込む、自己完結した論理体系を実現しました。
そしてVoevodskyによる「Homotopy Type Theory（HoTT）」は、型を位相空間として、型の要素を空間上の点として、等しさをパス（道）として解釈するという驚くべき橋架けをトポロジーと型理論の間に架けます。この視座は「数学の証明はコンピュータでチェックできるプログラムの形であるべきだ」という主張と結びつき、21世紀の数学の形式そのものを変えようとする野心的な企てへと発展しています。本セミナーはその全貌を、型なしλ計算の基礎から最先端のHoTTまで体系的に辿ります。
講義のロードマップ
ここでは、セミナーの講演資料がどのようなパートから構成されているかを示します。また、それぞれのパートのポイントを紹介します。
■ Part 1: 型のないラムダ計算
λ記法による関数の抽象化と、β簡約を中心とするλ計算の形式的ルールを確立します。名前なし関数という概念と、変数への代入による計算の本質を理解することが、後続の全議論の出発点となります。 [p.3〜p.9]
■ Part 2: 型付きラムダ計算
型の導入によりλ計算に構造的制約を与え、計算の停止性を保証します。「型σからτへの関数は型σ→τを持つ」という原則と、`e : τ`（eは型τを持つ）という判断の記法が、以後の理論全体の言語となります。 [p.32〜p.53]
■ Part 3: 論理的推論1 ― 判断と論理式
「命題Aは真である」という言明は単純な記号操作ではなく、「私はAが真であることを知っている」という**判断（judgement）**として解釈されるべきです。判断の概念は命題の概念に先立ち、証明とは判断を明証なものにする行為に他なりません。 [p.54〜p.70]
■ Part 4: 論理的推論2 ― Natural Deduction
GentzenとPrawitzによるNatural Deductionの命題論理版を提示します。各論理記号に「導入規則（I）」と「除去規則（E）」のペアを与えることで、推論の構造が透明化されます。 [p.71〜p.90]
■ Part 5: Curry-Howard対応
「p が命題Pの証明である」という論理的判断`p:P`と、「p が型Pの要素である」という計算論的判断`p:P`が、まったく同一の形式記述を共有するという驚くべき双対性を確立します。命題は型であり、証明は項です。 [p.91〜p.104]
■ Part 6: Dependent Type Theory
Martin-Löfが構築した依存型理論は、型がその要素の値に依存して変化するという概念を導入します。`Π(x:A).B(x)`という依存型により、全称量化子・存在量化子・等式命題がすべて型として統一的に扱われます。 [p.105〜p.113]
■ Part 7: 「型の理論」と「証明の理論」― Curry-Howard対応の証明
Simon Thompsonの手法に従い、「命題の証明のルール」と「型の要素のルール」を、Formation・Introduction・Elimination・Computationの4規則形式で並べると、両者の形式記述がまったく同一であることを明示的に示します。 [p.114〜p.147]
■ Part 8: Calculus of Inductive Constructions
Coqが採用するCIC（Calculus of Inductive Constructions）では、帰納的型の定義から`x_rect`・`x_ind`・`x_rec`の3つの型が自動生成されます。`nat_rect`の型を解読すると、それがまさに数学的帰納法そのものに対応していることが判明します。 [p.153〜p.166]
■ Part 9: Homotopy Type Theory
Voevodskyが構築したHoTTは、型を位相空間、要素を空間の点、等式の証明を点と点を結ぶパス（道）として解釈します。この幾何学的直観により、同一性の概念がhomotopy理論と深く結びつき、数学の証明をCoqで検証可能なプログラムとして記述するUnivalent Theoryへと発展します。 [p.167〜p.181]
ページのナビゲート