1940 年 Church 簡單型別理論：為邏輯加上身分證#
案件編號：No.1940 — 嫌疑犯：自我指涉。偵探：Alonzo Church。武器：一套型別階層。
案發現場#
1901 年的清晨，羅素寄出一封改變數學史的信。弗雷格剛在 《概念文字》 之後建成龐大的邏輯大廈，希爾伯特在 23 問題 中宣告要公理化一切，羅素與懷特海正埋頭撰寫 《數學原理》 。一切看似光明。
然而一具「屍體」出現了：羅素悖論。考慮集合 \(R\) 定義為所有不包含自己的集合之集：
那麼 \(R \in R\) 成立嗎？若成立，則依定義 \(R \notin R\) ；若不成立，則依定義 \(R \in R\) 。無論走哪條路都撞牆。
這不是文字遊戲。當時無型別的邏輯允許任何性質定義集合，允許函數吃下自己、命題談論自己。弗雷格的第五公理瞬間崩塌，希爾伯特的樂觀蒙上陰影。羅素自己提出分支型別論救火，但寫在 《數學原理》 裡的版本笨重難用，充滿特設的階數與公理。
更糟的是，1930 年代 Church 發明的無型別 \(\lambda\) 演算同樣中彈：Kleene 與 Rosser 證明其邏輯版本不一致，可以推導出矛盾。案發現場留下兩行血字：自我應用與無限制概括。
問題於是浮現：能否保留邏輯與計算的全部威力，同時讓「 \(x \in x\) 」這種句子根本說不出口？
偵查過程#
Church 在 1940 年的論文 A Formulation of the Simple Theory of Types 中亮出關鍵推理：與其禁止某些證明，不如在語法層就區分「不同階層的居民」。
線索一：型別階層#
Church 只設兩個基本型別：個體 \(o\) 為命題之型， \(i\) 為個體之型。其他型別皆由函數型別構造：若 \(a\) 與 \(b\) 為型別，則 \(a \to b\) 也是型別。例如性質「是人」不是集合，而是型別 \(i \to o\) 的函數。
偵探的規則很簡單：函數只能吃下低一層的東西。高階函數可以吃低階函數，但絕不能吃自己。用現代記號， typing 判斷形如 \(M : T\) ，讀作項 \(M\) 具有型別 \(T\) 。
核心項語言只有三種構造：
| 構造 | 寫法 | 型別規則 |
|---|---|---|
| 變元與常元 | \(x\) 、 \(c\) | 每個符號出生即帶有固定型別 |
| 函數應用 | \(M \, N\) | 若 \(M : a \to b\) 且 \(N : a\) 則 \(M \, N : b\) |
| \(\lambda\) 抽象 | \(\lambda x . M\) | 若 \(x : a\) 且 \(M : b\) 則 \(\lambda x . M : a \to b\) |
注意第二行：應用要求參數型別完全吻合。這就是身分證檢查。
線索二：悖論為何無法立案#
試圖重建羅素集合 \(R\) 。你想寫一個性質 \(R : i \to o\) ，使得 \(R \, x\) 等價於 \(\lnot (x \, x)\) 。但 \(x \, x\) 根本無法通過型別檢查：若 \(x : a\) ，則左邊的 \(x\) 必須具有 \(a \to b\) 之形，於是 \(a = a \to b\) ，在有限型別中不可能。兇手連兇器都拿不到。
Church 進一步用 \(\lambda\) 演算的化簡解釋等式： \((\lambda x . M) \, N\) 可化簡為 \(M[x := N]\) ，記作 \(\beta\) 歸約。邏輯常元 \(\lnot\) 、 \(\land\) 、 \(\forall\) 皆被編碼為高階常元，例如全稱量詞 \(\Pi_a : (a \to o) \to o\) 。於是高階邏輯的證明，就是有型別的 \(\lambda\) 項的構造。
線索三：與羅素分支型別的差異#
| 面向 | 羅素分支型別論 | Church 簡單型別理論 |
|---|---|---|
| 型別對象 | 命題按「階」分層，複雜 | 只分函數層級，簡潔 |
| 語法 | 集合論語言＋階數標記 | 純 \(\lambda\) 演算＋型別標註 |
| 可計算性 | 難以判定 | 型別檢查可判定 |
| 後續 | 幾乎被棄用 | 直接通往 HOL 與證明器 |
Church 保留了 亞里斯多德 以來對有效推理的渴望，繼承了弗雷格的高階直覺，卻砍掉了自我指涉的樓梯。哥德爾在 1931 年 證明的形式極限仍在，但至少系統內部不再自爆。
他同時證明了系統相對於 Henkin 語義的完備性，為後世留下可實作的邏輯。
結案報告#
真兇是「無限制的自我應用」。Church 的判決是：每個表達式必須有型別，型別決定它能與誰對話。羅素悖論從「推得出矛盾」降級為「寫不出來」——語法上即非法。
此案遺產極深：
- 它成為高階邏輯 HOL 的直系祖先，Gordon 在 1986 年打造的 HOL 系統前身即本案嫡傳，後續通往 Isabelle 與 Flyspeck。
- 它把 \(\lambda\) 演算從不一致的邏輯改造成有型別的計算，為後來的 Howard 對應 與 Automath 鋪路。
- 它確立「以型別拒絕壞程式、以型別拒絕壞證明」的典範，今日 Rust、Haskell、Lean 的型別系統皆是其遠親。
當然代價也存在：簡單型別理論表達力受限，無法在內部談論自身型別，也推不出 Herbrand 定理 所需的某些構造性內容。這為依賴型別與 Gentzen 結構證明論 留下續集伏筆。
但就 1940 年而言，警笛解除：數學大廈不再從地基自燃。
證據與工具#
關鍵型別公理精選：
- 基本型別： \(o\) 表命題， \(i\) 表個體。
- 函數型別：由 \(a \to b\) 封閉生成。
- 等式理論含 \(\alpha\) 、 \(\beta\) 、 \(\eta\) 轉換，例如 \(\lambda x . M \, x = M\) 當 \(x\) 不在 \(M\) 中自由出現時成立。
最小例子：恆等函數 \(\lambda x . x\) 可具型別 \(i \to i\) ，亦可具型別 \(o \to o\) ，但不能同時吃下兩種型別，除非引入多型。否定算子 \(\lnot : o \to o\) ，合取引入可視為常元 \(\land : o \to o \to o\) 。
型別檢查習題：判斷下列何者合法： \(f \, a\) 其中 \(f : i \to o\) 且 \(a : i\) 合法； \(a \, f\) 非法； \(\lambda P . P \, a\) 其中 \(P : i \to o\) 合法且具型別 \((i \to o) \to o\) 。
延伸閱讀：Church 原文 1940、Andrews《An Introduction to Mathematical Logic and Type Theory》、HOL4 官方手冊首章。下集預告：機器如何用啟發式重演 《數學原理》 ，請見 Logic Theorist 。