跳轉到

9.3 類型論與MARTINLOF1972#

本章導言#

1972 年，Per Martin-Löf 發表〈一個構造性數學的無限論理論〉，開創依值類型論（dependent type theory）。他的核心洞見來自 Curry–Howard 對應：命題與類型是同一物，證明與程式是同一物——「證明即程式」從詮釋（9.2 節的可實現性）升級為語法同一。Martin-Löf 類型論（MLTT）既是直覺主義邏輯的形式化、程式語言的理論、也是數學基礎的候選者——Frege 的概念文字（1.3 節）之後，第一次有人提出可以替代集合論的完整基礎。本節講 MLTT 的架構、Curry–Howard 對應、以及它如何處理羅素悖論的後裔問題（宇宙層級）。

Curry–Howard 對應：命題即類型#

Curry 1934（組合邏輯）與 Howard 1969/1980（直覺邏輯）發現：證明的結構與程式的結構完全同構：

邏輯 類型論 讀法
命題 \(A\) 類型 \(A\) 命題 = 類型
證明 \(p\) of \(A\) 項 \(p : A\) 證明 = 程式
\(\to\) 引入 \(\lambda x. b\) 函數構造
\(\to\) 消除 \(f\, a\) 函數應用
\(\wedge\) （ \(\Sigma\) 類型） \((a, b) : A \times B\) 序對
\(\vee\) （ \(+\) 類型） \(\operatorname{inl}(a), \operatorname{inr}(b)\) 帶標籤的並
\(\exists\) （ \(\Sigma\) ） \(\Sigma x:A. B(x)\) 依值對（見證在內）
\(\forall\) （ \(\Pi\) ） \(\Pi x:A. B(x)\) 依值函數（規範在內）
\(\bot\) 空類型 \(\mathbf{0}\) 假 = 無構造

「 \(p\) 是 \(A\) 的證明」=「 \(p : A\) 」——證明論與程式論合併為一門學科。羅素悖論的類型論防禦（3.1 節例題 3.1.2）在此獲得語言級的實現：型別系統從語法上排除自指。

Martin-Löf 類型論的架構#

MLTT 的四類判斷（judgement）：

\[ A \text{ 是類型}; \quad a : A; \quad a \equiv b : A; \quad A \equiv B. \]

依值類型是 MLTT 超越簡單類型論的關鍵：類型可依賴項。

  • ** \(\Pi\) （依值函數）**： \(\Pi x:A.\ B(x)\) ——「對每個 \(a : A\) 給出 \(B(a)\) 中的項」。全稱量詞 + 函數。
  • ** \(\Sigma\) （依值對）： \(\Sigma x:A.\ B(x)\) ——「 \(a : A\) 加 \(b : B(a)\) 」。存在量詞 + 序對（見證被迫攜帶**——9.2 節存在性質的語法化）。
  • 恆等類型： \(\operatorname{Id}_A(a, b)\) ——「 \(a = b\) 的證明」也是一個類型，其元素是等式的構造性證明。等式不是二值屬性而是可構造對象——這是 10.2 節同倫詮釋的門戶。
  • 歸納類型： \(\mathbb{N} = \{0, S\}\) 的生成規則 + 歸納原理（消去規則）——歸納法變成類型的規則。
  • 宇宙 \(U\) ：「小類型組成的類型」——需要分層 \(U_0 : U_1 : U_2 : \cdots\) 避免羅素悖論（4.1 節「沒有全域集合」的類型論版）。

一個具體例子#

例題 9.3.1：在 MLTT 中證明 \(\forall n:\mathbb{N}.\ \exists m:\mathbb{N}.\ m > n\) ，並寫出證明項，展示「證明即程式」。

解：命題 = 類型 \(\Pi n:\mathbb{N}.\ \Sigma m:\mathbb{N}.\ m > n\) 。證明項（即程式）：

\[ f = \lambda n.\ \langle S\,n,\ \operatorname{prf}_{>}(n)\rangle : \Pi n:\mathbb{N}.\ \Sigma m:\mathbb{N}.\ m > n, \]

其中 \(\operatorname{prf}_{>}(n) : S\,n > n\) 是「 \(S n > n\) 」的構造性證明（由 \(<\) 的歸納定義： \(S n > n\) 直接由基步構造）。

讀法： \(f\) 既是證明（每個 \(n\) 有更大的 \(m\) ），也是程式（輸入 \(n\) 輸出 \(S n\) ）。計算內容： \(f(5) = 6\) ——見證 \(m\) 由 \(\Sigma\) 類型的第一分量顯式攜帶。證明與程式在語法上不可區分：同一個項，兩種讀法。 \(\blacksquare\)

例題 9.3.2：展示宇宙分層如何排除羅素悖論：說明為什麼「所有類型的類型」 \(U : U\) 會導致 Girard 悖論，而 \(U_0 : U_1\) 不會。

解：若 \(U : U\) （類型於自身的宇宙），可定義 \(\Sigma\) 上的自指結構：Girard 1972 證明「 \(U : U\) 的多態 λ 演算（System U）不一致」——在 \(U : U\) 中可構造 \(\bot : \mathbf{0}\) （空類型的元素），即推出矛盾：構造路徑與羅素對角線同構（構造 \(R = \{X : U \mid X \notin X\}\) 的類型論版，其「屬於自身」的型別檢查通過，對角線展開得 \(\bot\) ）。

若宇宙分層： \(U_0 : U_1\) ， \(U_1 : U_2\) ，……則「 \(X : U_0\) 且 \(X \notin X\) 」型別不合法（ \(X \in X\) 要求 \(X : U_0\) 且 \(X\) 是 \(U_0\) 的「成員型別」——分層使「 \(X\) 的型別是 \(U_0\) 」與「 \(X\) 是 \(U_0\) 的元素」不同層，自指被語法排除）。宇宙層級 = 類型論的累積層級（4.1、4.3 節的思想移植）。 \(\blacksquare\)

MLTT 作為數學基礎：與 ZFC 的對照#

面向 ZFC MLTT
原始對象 集合 類型與項
存在命題 \(\exists\) （真值） \(\Sigma\) （攜帶見證）
證明 外部檢查的文本 內部的項（可計算）
等式 謂詞 \(a = b\) 類型 \(\operatorname{Id}(a,b)\)
邏輯 經典 直覺主義（構造性）
悖論防禦 限制概括 型別系統
自然的基礎函數 任意集合函數 可計算函數

MLTT 的優勢：證明可計算（Coq/Agda/Lean 的 Lean 核心是類型論）、存在攜帶算法、等式有結構。劣勢：直覺主義邏輯（經典數學家需適應）、集合的「外延性」較弱（需公理化外延等式）、與傳統數學文本的語言差異。兩種基礎在 2000 年代並存，2010 年代的 HoTT（10.2 節）試圖統一。

歷史啟示#

  • Curry–Howard 是二十世紀邏輯的第三大對應（與語法—語義對偶 5.1 節、句法—計算對應 7.3 節並列）：邏輯、程式、證明三者的結構同一——三個學科在類型論中合流。
  • Martin-Löf 的哲學堅持：他稱 MLTT 的判斷為「解釋」（explanation）而非「語義」——意義理論（meaning theory）優於模型論：構造的規則即意義。這是 Brouwer 哲學（9.1 節）最精確的形式化繼承。
  • 基礎選擇 = 語言選擇：MLTT 與 ZFC 不是真假之爭而是工作流之爭——就像程式語言的範式之爭。10.3 節將以此收束全書。

與其他章節及領域的關聯#

  • 3.1 節：羅素悖論的類型論防禦在此成為整個語言。
  • 4.1、4.3 節：宇宙分層 = 累積層級的類型論版。
  • 9.1–9.2 節：直覺主義邏輯與可實現性是 MLTT 的語義先聲。
  • 7.2 節：λ 演算是 MLTT 的計算核心。
  • 10.1 節：範疇論與類型論的語義（笛卡爾封閉範疇 = 簡單類型論的模型）。
  • 10.2 節：HoTT 把 \(\operatorname{Id}\) 類型詮釋為路徑空間。
  • 計算機科學：Haskell、Rust、TypeScript 的類型系統是 MLTT 的工程後裔；Coq、Agda、Lean、Idris 是 MLTT 的直接實現；依值類型正在進入主流軟體工程（Rust 的所有權系統、F* 的依值類型驗證）。

練習#

  1. 寫出 \(\mathbb{N}\) 的歸納類型定義（引入規則 \(0, S\) 與消去規則），並說明歸納原理如何從消去規則讀出。
  2. 在 MLTT 中構造交換律 \(\forall n, m:\mathbb{N}.\ n + m \equiv m + n\) 的證明骨架（歸納於 \(m\) ）。
  3. 證明例題 9.3.2 中 Girard 悖論的構造思想：在 \(U : U\) 假設下寫出「自否定類型」 \(R = \Sigma X:U.\ (X \to \mathbf{0})\) 型的自指展開。
  4. 比較 \(\Sigma\) 類型與集合論的「存在量詞」：寫出「每個 \(n\) 有素因子」的兩種形式化，指出證明項在何處不同。
  5. 思考題：Martin-Löf 拒絕稱他的語義為「模型論」。你認為「意義即規則」（inferentialism）與「意義即指稱」（referentialism）的分歧對教學有何實際影響？

進階研讀：三個深化場景#

場景一：從 Automath 到 Coq 的四十年。de Bruijn 的 Automath（1967–）是第一個證明檢查器（類型論式）；Coq 1989（Coquand–Huet 的歸納構造演算 CIC）加入歸納類型；Agda 2007 更純的 MLTT；Lean 2013 兼顧經典與構造。MLTT 的理論在 50 年間成為形式數學的作業系統——費馬大定理（2024 於 Lean 完整形式化）在其上運行。

場景二：類型論的哲學基礎之爭。Martin-Löf 的判斷論（judgementalist）立場 vs Dummett 的證明論意義理論 vs HoTT 的同倫結構主義——「類型的意義是什麼」仍是開放問題。有趣的是這場哲學辯論不阻礙工程進展——類型論是罕見的「哲學開放、工程穩固」的基礎。

場景三：觀察等價與外延問題。MLTT 的恆等類型是「內涵的」（兩個相等證明可以不同），這與經典數學的外延等式不同。觀察等價（observational equivalence, Altenkirch–McBride）與 setoid 模型嘗試恢復外延性——此問題的直接深化就是 10.2 節的同倫類型論：不迴避等式的內涵結構，而是把它變成數學對象。

名詞速查表#

  • Curry–Howard 對應：命題 = 類型，證明 = 程式。
  • 依值類型：類型依賴項（ \(\Pi, \Sigma\) ）。
  • **恆等類型 \(\operatorname{Id}\) **：等式的構造性證明類型。
  • 歸納類型：由生成規則定義的類型（含消去規則）。
  • **宇宙 \(U_n\) **：類型的分層系統，防 Girard 悖論。
  • CIC：歸納構造演算（Coq 的基礎）。
  • 意義理論：Martin-Löf 的構造性意義哲學。

年表速查#

  • 1934：Curry 組合邏輯的類型。
  • 1958：Curry–Feys《組合邏輯》。
  • 1967：de Bruijn Automath。
  • 1969/1980：Howard「命題即類型」論文。
  • 1971：Martin-Löf 第一版類型論（因 Girard 悖論修正）。
  • 1972：MLTT 正式論文。
  • 1972：Girard System F 與悖論。
  • 1984–86：Martin-Löf 修訂版；Coq 開發。
  • 2006：HoTT 的同倫詮釋（10.2 節）。

深化問答三則#

問：MLTT 為何用「判斷」而非「真值」？ 答：因為構造性的意義理論：命題的意義 = 其證明的構造規則，不是真值條件。判斷「 \(a : A\) 」是可執行的檢查（型別檢查），「 \(A\) 真」是派生的（存在 \(a : A\) ）。真值從屬於構造——Brouwer 的哲學在此變成語法。

問：宇宙分層「醜」嗎？ZFC 沒有這個問題。 答：ZFC 有等價的問題：它用「沒有全域集合」（4.1 節）的定理而非語法規則處理。分層是把集合論的邊界定理前移為型別規則——代價是書寫冗餘，收益是自指從語法上不可能。安全與便利的 trade-off 在兩種基礎中以相反方式支付。

問：類型論會取代集合論嗎？ 答：不是「取代」而是分工深化：集合論仍是日常數學的通用語，類型論是形式驗證與構造數學的工作語。2010 年代後兩者開始互譯（集合論模型在類型論中構造、類型論語義用範疇論）。10.3 節的結論將是：基礎的未來是多元共存 + 互操作，如同程式語言生態。

（本節完）