論理学 III — 型の理論入門

講演資料

講義資料スライドの表紙です。スライド画像、または下の要約文中の青いページ番号リンクをクリックすると、別のタブで無駄なノイズのない、純粋な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]。

論理展開:
λx.tという記法で「tをxの関数と見る抽象化」を定義し、適用(λx.t)a = t[x:=a]というβ簡約の基本規則を確立します [p.4]〜[p.9]。
λ式の形式的定義（変数・抽象化・適用の三規則）と、α変換・β簡約・η変換の三つの計算ルールを整理します [p.11]〜[p.14]。
Ω := (λx.xx)(λx.xx)はβ簡約で自分自身に戻り、計算が停止しないことを示します [p.16]〜[p.22]。
Y結合子はY g = g(Y g)を満たし、任意の関数の不動点を与える強力な構造です [p.23]〜[p.31]。

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

この部の核心:

型σから型τへの関数に型σ→τを与えることで適用に制約を課します。これにより型のない体系では許容されていたΩのような無限ループが排除され、計算の停止性が保証されます [p.32]〜[p.53]。

論理展開:
e:τという判断の定義を変数・抽象化・適用の三規則で与えます。特に(λxσ.e):(σ→τ)と(e₁e₂):τという型付け規則が核心です [p.36]〜[p.39]。
適用はSσ→τTσ:τの形でのみ許可され、同じ型同士のSσTσは禁止されます。これによりΩは型付き体系では不正な式となります [p.44]〜[p.50]。
型付き体系では計算は必ず停止します（強正規化定理）[p.50]。
型・オブジェクト・値の三者関係を図示し、正規オブジェクト（それ以上簡約できない値）の概念を確立します [p.51]〜[p.53]。

■ Part 3: 判断と論理式

この部の核心:

「命題Aは真である」という判断が「命題Aは論理式である」という判断に先行することを示します。判断は知ることであり、証明は判断を明証なものにする行為そのものです [p.54]〜[p.70]。

論理展開:
判断は「表現」と「判断の形式」から構成され、⊢Aという形式で記述されます。明証的な判断と単なる判断の区別が重要です [p.60]〜[p.67]。
論理学者が好む横棒による推論表現を導入し、「判断2が判断1の論理的帰結である」という関係を形式化します [p.69]。
∀と∃を含む論理式の構成ルール（Formation Rule）を横棒記法で記述します [p.70]。

■ Part 4: Natural Deduction（自然演繹）

この部の核心:

GentzenとPrawitzが整備した命題論理版のNatural Deductionを紹介し、各論理記号に対して導入規則（Introduction）と削除規則（Elimination）を与えます [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]〜[p.77]。
→のルール：→E（三段論法；A→BとAからBを導出）と→I（仮定[A]からBが導けるならA→Bを導入）[p.78]〜[p.81]。
A→(B→(A∧B))の導出例で三つのルールを組み合わせた推論木を実演します [p.82]〜[p.90]。

■ Part 5: Curry-Howard対応

この部の核心:

「p:Pはpが命題Pの証明である」と「p:PはpがPの型の要素である」という二つの解釈が同一の形式的記述を持つことを示します。命題は型であり、証明は要素である、という双対性がCurry-Howard対応の核心です [p.91]〜[p.104]。

論理展開:
1934年のCurryの発見：型付きラムダ計算の→と論理的含意の→の対応 [p.93]。
1969年のHowardの発展：「論理式はラムダ計算の型と見なせる」（Propositions as Types, Proofs as Terms）[p.94]。
p:Pという記号が「証明と命題」と「要素と型」の双方を同時に表現することを図式で示します [p.97]〜[p.103]。
この対応はCoqなどの証明支援システムの理論的基盤となりました [p.104]。

■ Part 6: Dependent Type Theory

この部の核心:

Martin-Löfが1980年代に構築した依存型理論を解説します。型が別の型の要素に依存して変化するΠ型を導入し、全称量化子や多相性（Polymorphism）を型として統一的に扱う体系を示します [p.105]〜[p.113]。

論理展開:
型の理論の四つの判断形式：a:Type、a:α、a=b:α、α=β:Type [p.109]。
Π(x:A).B(x)というDependent Typeは、型Aの要素aに応じてB(a)が変化する型です [p.111]。
Vec(R,n)のようにnに依存して変化するベクトル型、さらに係数体の型に依存する多相的なベクトル型もDependent Typeとして表現されます [p.110]〜[p.112]。
Inductive Typeは定数と関数から新しい型を帰納的に定義します。Coqのnat定義が代表例です [p.113]。

■ Part 7: Curry-Howard対応の証明（型と証明の双対性の形式的確立）

この部の核心:

Simon Thompsonの方針に従い、「命題の証明」と「型の要素」それぞれに対してFormation・Introduction・Elimination・Computationの四種のルールを記述し、両者の形式的記述が完全に一致することを具体的に検証します [p.114]〜[p.152]。

論理展開:
→のルール：証明側では(λx:A).e:(A→B)という証明の構成、要素側では全く同一の記述が型の要素の構成を意味します [p.124]〜[p.135]。
∨のルール：inl q:(A∨B)とinr r:(A∨B)という導入、cases p f g:CというEliminationが証明・型の両解釈で同一です [p.137]〜[p.147]。
∀と∃のルールも同様に、(λx:A).p:(∀x:A)PとFst/Snd等を通じて両解釈が完全一致します [p.149]〜[p.152]。

■ Part 8: Calculus of Inductive Constructions（CIC）

この部の核心:

Coqが採用するCIC（帰納的構成の計算体系）を解説します。Inductive型natの定義から自動生成されるnat_rect・nat_ind・nat_recの三つの型が数学的帰納法そのものを表現していることを示します [p.153]〜[p.166]。

論理展開:
nat_rectの型をCheck命令で確認すると、∀P:nat→Type, PO→(∀n:nat, Pn→P(Sn))→∀n:nat, Pnとなり、これは数学的帰納法に他なりません [p.157]〜[p.162]。
nat_indはnat→Prop（命題の帰納法）、nat_recはnat→Set（計算の帰納法）として、Type・Prop・Setという三階層の違いを反映します [p.163]〜[p.166]。

■ Part 9: Homotopy Type Theory（HoTT）

この部の核心:

Voevodskyが構築したHoTTにおいて、型は空間、項は点、等号は道（path）として解釈されます。同一性がホモトピーとして幾何学的に捉えられ、数学の新しい基礎付け「Univalent Theory」への道が拓かれます [p.167]〜[p.181]。

論理展開:
a:Aの解釈比較：集合論（集合と要素）、構成主義（問題と解）、PAT（命題と証明）、HoTT（空間と点）[p.169]。
同一性の三性質（反射律・対称律・推移律）がPathの（定数路・逆路・路の連結）に対応し、∞-Groupoidの構造を形成します [p.172]〜[p.175]。
Dependent TypeはBという底空間上のファイバー束として解釈されます [p.176]〜[p.178]。
VoevodskyはUniMathというCoqライブラリーをGitHubで公開し、数学の証明をコンピュータ検証可能なプログラムとして表現することを実践しました [p.179]〜[p.181]。