Homotopy Type Theory｜HoTT、ホモトピー型理論
Homotopy Type Theory（HoTT、ホモトピー型理論）とは、型理論（Type Theory） と ホモトピー理論（Homotopy Theory） を統合した、21世紀初頭に登場した新しい数学的基礎理論です。数学・論理・計算機科学の交差点で発展しており、特に「証明＝プログラム、型＝命題」という Curry–Howard対応 を、空間的構造と結びつけて拡張する形で構築されています。
🔧 基本構造
1. 型理論（Type Theory）
- 「命題を型として扱う」という構造を持つ
- 証明は型の要素（term）として構成される
- 元々は直観主義論理（Constructivism）に基づく
- Martin-Löf型理論が代表的
2. ホモトピー理論（Homotopy Theory）
- 空間の変形（連続的な写像）に関する理論
- 位相空間や圏の「パス」や「高次パス」（2次、3次…）を扱う
- 特に、∞-グループイド（∞-groupoid）としての空間的な振る舞いに注目
🧠 HoTTの核心的な考え方
| 概念 | HoTTにおける意味 |
|---|---|
| 型（Type） | 位相空間のような「対象」 |
| 項（Term） | 空間内の点（element） |
| 等価性（Equality） | パス（path、連続的な変形） |
| 等価の等価（Higher Equality） | パスのパス（2パス、3パス…） |
| Univalence Axiom（一価性公理） | 同型であれば同一視できるという原理（Voevodskyが提唱） |
| ∞-groupoid | 各型が高次の等価性構造をもつグループイドとみなせる |
🧩 どんな特徴があるのか？
🔹 証明の「空間的」意味づけ
- 通常の数理論理では「命題は真か偽か」だが、
- HoTTでは「命題は空間として扱える」→ 証明はその中の経路
🔹 計算機と相性がよい
- Coq、Agda などの証明支援系と親和性が高い
- 形式的証明とプログラムが一致する（「証明駆動開発」）
🔹 数学基礎論としての可能性
- 集合論（ZFC）に代わる基礎理論の候補とされる
- 構成的、計算的、空間的な直観が統合されている
🏛 歴史・背景
- 2006–2013年頃：Vladimir Voevodsky（フィールズ賞受賞者）らによって提案
- 2013年：大規模な共同プロジェクト “Univalent Foundations Program” により HoTT の基礎文書『Homotopy Type Theory: Univalent Foundations of Mathematics』が公開
- プログラマ、数学者、哲学者によって急速に関心を集めた
🪜 Groundismとの関係（補足）
HoTTは「型」と「空間」、「証明」と「経路」、「構造」と「意味」を接続する理論であるため、Groundism™（意味の構造を場的に捉える理論）と非常に親和性があります。特に：
- Groundismが定義する「意味の場（Noën）」と、
- HoTTが記述する「証明の空間的多様性」
は、共に 脱線形的な意味の重層構造 を扱おうとする点で共鳴しています。
📚 参考文献・リソース
- Homotopy Type Theory: Univalent Foundations of Mathematics
👉 https://homotopytypetheory.org/book/ - HoTT wiki: https://homotopytypetheory.org/
- AgdaやCoqのHoTTライブラリ
- HoTTに関する講義動画（YouTube、MITなど）
🧩 まとめ
| 特徴 | 内容 |
|---|---|
| 分野横断 | 数学、論理、CSをつなぐ |
| 空間的証明 | 証明をホモトピー的に再定義 |
| 計算可能性 | プログラムと証明の一致 |
| 構造の再定義 | 集合に代わる基礎体系の可能性 |
Curry–Howard対応（Curry–Howard Correspondence）
「論理の命題と型（Type）、証明とプログラム（関数） を一対一に対応させる理論的な対応関係」
です。これは 数理論理と型理論（および計算機科学） の間にある**深い構造的な同型性（isomorphism）**で、時に「命題＝型、証明＝プログラム」とも呼ばれます。
🧠 基本対応の一覧
| 論理体系（自然演繹） | 型理論（ラムダ計算） |
|---|---|
命題 P | 型 T（P型） |
証明 p : P | 項 t : T（Tの要素） |
論理積 P ∧ Q | 直積型 T × U |
論理和 P ∨ Q | 直和型 T + U |
否定 ¬P | 関数型 T → ⊥（bottom型） |
含意 P → Q | 関数型 T → U |
全称量化 ∀x.P(x) | 型族に対する依存積 Πx:T. P(x) |
存在量化 ∃x.P(x) | 型族に対する依存和 Σx:T. P(x) |
🧩 わかりやすい例
🧪 命題：
「A ならば B」：A → B
💻 型理論的解釈：
関数型 A → B、つまり「型 A の入力に対して型 B の出力を返す関数」
→ このとき、f : A → B という関数 f を書けることが、「命題 A → B の証明がある」ことと同じ。
📌 重要な特徴
1. 構成的意味論（Constructive Semantics）
- 「証明がある = その証明を“構成”できる」
- 非構成的な証明（例：「背理法による存在証明」）とは異なる
2. プログラムが証明になる
- 関数を実装することが、命題を証明することに対応
- 実際に
f : A → Bの関数を書くことは、「A → B が真である」ことの証明
3. 証明支援系と連携
- Coq、Agda などの proof assistant での形式化に使われる
- 「証明を書きながらコードを書く」ことが可能に（証明駆動開発）
🧭 歴史と命名
- Haskell Curry：論理とラムダ計算の関係を考察
- William Alvin Howard：命題と型の対応を明確化（1969年の論文で「命題と型の等価性」を指摘）
- 時に Curry–Howard–de Bruijn対応 として拡張される（de Bruijnは型付きλ計算で形式化を行った）
🧬 Homotopy Type Theoryとの接続
HoTTでは、Curry–Howard対応をさらに空間的に拡張し：
- 命題＝型（Type）
- 証明＝空間内の経路（path）
- 証明の証明＝高次ホモトピー
と再解釈され、∞-groupoid的構造として展開されます。
✅ まとめ：Curry–Howard対応とは
| 観点 | 内容 |
|---|---|
| 意味 | 命題と型、証明とプログラムの対応 |
| 応用 | プログラミング言語、証明支援系、数理論理 |
| 形式化 | λ計算と自然演繹の構造的対応 |
| 本質 | 構成的意味論・構造的一致 |
| 現代的拡張 | HoTT, ∞-groupoid, 計算可能性の空間的拡張 |