セミナー紹介

全体概要

本セミナー「型の理論入門」は、現代の計算機科学・数学基礎論・論理学を貫く一本の深い問いに答えようとする試みです。その問いとは、「計算すること」「推論すること」「証明すること」は本質的に同じことなのか、という問いです。

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]

• 論理展開:
• λ記法の導入：`λx.t`はxの関数としてのtを表し、適用`(λx.t) a = t[x:=a]`が計算の本体となります。 [p.4]〜[p.9]
• λ式の形式的定義：変数・抽象化・適用の3規則で帰納的に定義されます。 [p.11], [p.12]
• α変換・β簡約・η変換の3ルール、および自由変数と束縛変数の区別が計算の精密化を支えます。 [p.13], [p.14]
• Ω := (λx.xx)(λx.xx)は計算が停止しない例として、型なし計算の危うさを示します。 [p.16]〜[p.22]
• Yコンビネータ`Y g = g(Y g)`はgの不動点を与え、再帰の表現を可能にします。 [p.23]〜[p.31]

---

■ Part 2: 型付きラムダ計算

• この部の核心:

型の導入によりλ計算に構造的制約を与え、計算の停止性を保証します。「型σからτへの関数は型σ→τを持つ」という原則と、`e : τ`（eは型τを持つ）という判断の記法が、以後の理論全体の言語となります。 [p.32]〜[p.53]

• 論理展開:
• 型付きλ式の定義：変数・抽象化・適用それぞれに型規則が付与されます。 [p.36]
• `x:σ, e:τ ならば (λxσ.e):(σ→τ)`、`e1:(σ→τ), e2:σ ならば (e1 e2):τ`が基本型規則です。 [p.38], [p.39]
• Ω等の自己適用は同一型同士の適用であり、型付き体系では禁じられます。これにより計算が必ず停止します。 [p.44], [p.50]
• 型・オブジェクト・正規値の三角関係：計算により正規形`v:A`が得られます。 [p.52], [p.53]

---

■ Part 3: 論理的推論1 ― 判断と論理式

• この部の核心:

「命題Aは真である」という言明は単純な記号操作ではなく、「私はAが真であることを知っている」という判断（judgement）として解釈されるべきです。判断の概念は命題の概念に先立ち、証明とは判断を明証なものにする行為に他なりません。 [p.54]〜[p.70]

• 論理展開:
• 判断の構造：表現（A）と判断の形式（「…は真である」）と明証的判断の三層から成ります。 [p.61]〜[p.67]
• 証明すること＝知ること＝理解して把握すること、という認識論的立場が明示されます。 [p.68]
• 横棒表記による論理的帰結の形式化：判断1 / 判断2 の記法が導入されます。 [p.69]
• 論理式の構成規則（Formation Rule）：∀・∃・⊥の形成規則が横棒形式で示されます。 [p.70]

---

■ Part 4: 論理的推論2 ― Natural Deduction

• この部の核心:

GentzenとPrawitzによるNatural Deductionの命題論理版を提示します。各論理記号に「導入規則（I）」と「除去規則（E）」のペアを与えることで、推論の構造が透明化されます。 [p.71]〜[p.90]

• 論理展開:
• ∧I：A, B から (A∧B)を導入。∧E₁・∧E₂：(A∧B)からA, Bをそれぞれ取り出します。 [p.74], [p.75]
• ∨I₁・∨I₂：A（またはB）から(A∨B)を導入します。 [p.76]
• →E（Modus Ponens）：(A→B)とAからBへ。→I：仮定[A]のもとでBが導ければ(A→B)が成立します。 [p.78], [p.79]
• 導出例：命題`A→(B→(A∧B))`を∧I・→Iの組み合わせで形式的に導出します。 [p.82]〜[p.90]

---

■ Part 5: Curry-Howard対応

• この部の核心:

「p が命題Pの証明である」という論理的判断`p:P`と、「p が型Pの要素である」という計算論的判断`p:P`が、まったく同一の形式記述を共有するという驚くべき双対性を確立します。命題は型であり、証明は項です。 [p.91]〜[p.104]

• 論理展開:
• 1934年のCurryの発見：関数型の→と論理的含意の→の対応が最初に見出されました。 [p.93]
• Howardの精密化（1969/1980）：「Propositions as Types, Proofs as Terms（PAT）」として定式化されました。 [p.94]
• `p:P`の二重解釈：命題Pの証明p ↔ 型Pの要素pという双対性が図示されます。 [p.97]〜[p.103]
• Proof as Programの観点：Coq等の証明支援システムの理論的基礎となります。 [p.104]

---

■ Part 6: Dependent Type Theory

• この部の核心:

Martin-Löfが構築した依存型理論は、型がその要素の値に依存して変化するという概念を導入します。`Π(x:A).B(x)`という依存型により、全称量化子・存在量化子・等式命題がすべて型として統一的に扱われます。 [p.105]〜[p.113]

• 論理展開:
• 型理論の4つの判断形式：`a:Type`・`a:α`・`a=b:α`・`α=β:Type`。 [p.109]
• 依存型`Π(x:A).B(x)`：nに依存するベクトル型Vec(R,n)、多相的関数などを自然に表現します。 [p.110]〜[p.112]
• 帰納的型（Inductive Type）：自然数`nat`をO（ゼロ）とS（後者関数）で帰納的に定義する例が示されます。 [p.113]

---

■ Part 7: 「型の理論」と「証明の理論」― Curry-Howard対応の証明

• この部の核心:

Simon Thompsonの手法に従い、「命題の証明のルール」と「型の要素のルール」を、Formation・Introduction・Elimination・Computationの4規則形式で並べると、両者の形式記述がまったく同一であることを明示的に示します。 [p.114]〜[p.147]

• 論理展開:
• →の規則：証明版・型版ともに`(λx:A).e:(A→B)`（導入）、`(q a):B`（除去）、`((λx:A).e)a → e[a/x]`（計算）で一致します。 [p.128], [p.129], [p.134], [p.135]
• ∨の規則：直和型としての`A∨B`は`inl q`・`inr r`による導入と`cases p f g`による除去で記述されます。 [p.143], [p.144]
• ∀・∃の規則：依存型`Π(x:A).P`・Σ型`(∃x:A).P`として型規則が与えられます。 [p.149]〜[p.152]
• 排中律は一般には成立しません：`A∨~A`の証明はAまたは~Aのいずれかの具体的証明を要求します。 [p.139], [p.140]

---

■ 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]

• 論理展開:
• `Inductive nat : Type := | 0 : nat | S : nat -> nat.`の定義から3型が自動生成されます。 [p.155], [p.156]
• `nat_rect : ∀P:nat→Type, P 0 → (∀n:nat, Pn → P(Sn)) → ∀n:nat, Pn`は数学的帰納法そのものです。 [p.157]〜[p.162]
• Type・Prop・Setの違いにより`nat_rect`・`nat_ind`・`nat_rec`がそれぞれ対応します。 [p.166]

---

■ Part 9: Homotopy Type Theory

• この部の核心:

Voevodskyが構築したHoTTは、型を位相空間、要素を空間の点、等式の証明を点と点を結ぶパス（道）として解釈します。この幾何学的直観により、同一性の概念がhomotopy理論と深く結びつき、数学の証明をCoqで検証可能なプログラムとして記述するUnivalent Theoryへと発展します。 [p.167]〜[p.181]

• 論理展開:
• `a:A`の4つの解釈比較：集合論（要素）・構成主義（解決）・PAT（証明）・HoTT（空間上の点）。 [p.169]
• 等式の三性質：反射性→constant path、対称性→逆の道、推移性→道の結合として幾何学的に解釈されます。 [p.172]〜[p.175]
• 依存型`(Ex)x∈B`はファイブレーション（fibration over B）として解釈されます。 [p.176]〜[p.178]
• VoevodskyのUniMathライブラリ：数学の証明をCoqプログラムとしてGitHubで公開し、21世紀の数学の形式を変えようとする挑戦が提示されます。 [p.179]〜[p.181]