跳轉到

1940 - 簡單型別 λ 演算#

案件摘要#

無型別 λ 演算威力強大卻暗藏殺機：它能構造自我應用 \(M\ M\) ，衍生邏輯悖論。 1940 年 Church 提出《A Formulation of the Simple Theory of Types》， 用「型別」這副手銬銬住悖論——代價是失去部分表達力，換來無懈可擊的安全性。

前因 -- 為什麼會有這個案子#

  • 無型別 λ 演算中，任一項 \(M\) 都可作用於自身： \((\lambda x. x\ x)(\lambda x. x\ x)\) 。
  • 更嚴重的是 Russell 悖論的 λ 化身：若允許「所有以自身為參數的謂詞」， 則 \(\neg (P\ P) \leftrightarrow P\ P\) 立即導致矛盾。
  • Curry 的悖論（1942 年發現）：由 \(\;Y_C = \lambda f.(\lambda x. f (x x))(\lambda x. f (x x))\;\) 加上 \((f \to g) \to f\) 可推出任意命題——無型別系統中邏輯全面崩塌。
  • Whitehead & Russell 的《Principia Mathematica》用「分層類型論」避開 悖論，但笨重不堪。Church 想要：λ 演算的優雅 + 型別的安全性。

線索與推理 -- 數學式、程式、理論#

型別文法#

簡單型別由兩條規則生成：

\[ \sigma ::= \iota \mid o \mid \sigma \to \tau \]
  • \(\iota\) ：個體（individuals）的基底型
  • \(o\) ：真值（truth values，命題）的基底型
  • \(\sigma \to \tau\) ：從 \(\sigma\) 到 \(\tau\) 的函數型

（Church 原文用 \(\alpha \beta\) 表 \(\alpha \to \beta\) ，右結合： \(\alpha \to \beta \to \gamma \equiv \alpha \to (\beta \to \gamma)\) ）

型別判斷#

項的良構性由型別環境 \(\Gamma\) （變數到型別的有限映射）判定：

\[ \Gamma \vdash M : \tau \]

推導規則：

\[ \frac{x : \tau \in \Gamma}{\Gamma \vdash x : \tau} \;(\text{Var}) \qquad \frac{\Gamma, x : \sigma \vdash M : \tau}{\Gamma \vdash \lambda x.\, M : \sigma \to \tau} \;(\to\text{-I}) \]
\[ \frac{\Gamma \vdash M : \sigma \to \tau \qquad \Gamma \vdash N : \sigma}{\Gamma \vdash M\ N : \tau} \;(\to\text{-E}) \]

例：恆等函數的型別推導

\[ \frac{\overline{x : \iota \vdash x : \iota}\;(\text{Var})}{\vdash \lambda x.\, x : \iota \to \iota}\;(\to\text{-I}) \]

對應的型別化程式（Haskell 風格）：

id :: a -> a
id x = x

apply :: (a -> b) -> a -> b
apply f x = f x

強正規化定理（Strong Normalization）#

  • 正規化（Normalization）：每個良型項都可約簡到某個正規形式。
  • 強正規化（Strong Normalization, SN）：每個良型項的所有約簡 序列都終止於正規形式。
\[ \forall M.\; \Gamma \vdash M : \tau \implies M \twoheadrightarrow_\beta N \text{（正規形式）} \]

證明採 Tait/Gödel 的「可及性邏輯解釋」（logical relations / reducibility candidates）：對型別歸納定義候選集合，證明每個良型項屬於其型別的候選集， 而候選集中的項皆強正規化。

推論：SN + Church–Rosser \(\implies\) 每個良型項有唯一正規形式， 計算必然停機——這是「型別即終止保證」的起點。

型別如何避免悖論#

關鍵：良型項中**不存在 \(M\ M\) **。若 \(M\ M\) 良型，設 \(M : \sigma\) ，則 \(M : \sigma \to \tau\) ，需要 \(\sigma = \sigma \to \tau\) ，但簡單型別 \(\sigma \to \tau\) 的「複雜度」（深度）恆大於 \(\sigma\) ，方程無解。

（形式化：定義型別深度 \(\mathrm{depth}(\iota)=0\) ， \(\mathrm{depth}(\sigma \to \tau)=1+\max(\mathrm{depth}(\sigma),\mathrm{depth}(\tau))\) ， 則 \(\sigma = \sigma \to \tau\) 要求 \(\mathrm{depth}(\sigma) = 1+\mathrm{depth}(\sigma)\) ，矛盾。）

Russell 悖論： \(\lambda x.\, \neg(x\ x)\) 的 \(x\) 必須同時是「函數型」與 「函數的參數型」，無法賦予單一簡單型別，悖論項非良構—— 手銬生效，凶手進不了案發現場。

與無型別版本的比較表#

特性 無型別 λ 演算 簡單型別 λ 演算
項的範圍 所有 λ 項 僅良型項
\(M\ M\) 允許（可產生悖論） 不可能
不動點組合子 \(Y\) 存在 不存在
強正規化 否（會發散） 是（必停機）
遞迴 用 \(Y\) 可定義 需額外加入不動點算子
可計算性 圖靈完備 僅可計算全函數
邏輯對應 無（Curry 悖論崩塌） 直覺主義命題邏輯（→ 為蘊含）
後世語言 LISP, Scheme ML, Haskell, 現代型別系統

結案 -- 後果與影響#

  • 型別論成為程式語言理論的核心：Curry–Howard 對應的直接前身。
  • 1958–60 年 Curry 系統化組合邏輯中的型別；1967 年 Milner 的 ML 把 簡單型別 + Hindley 型別推斷帶入實用語言。
  • 1970 年代 Girard 的 System F、Reynolds 的多型 λ 演算是其直接擴充。
  • 現代 Haskell、Rust、TypeScript 的型別系統，血統皆可追溯至 1940 年 這副手銬。
  • 哲學意涵：限制即力量——「不能表達一切」反而使系統獲得可證明的 安全性與停機性。

關鍵人物與文獻#

  • Alonzo Church（1903–1995）：簡單型別 λ 演算的提出者。
  • Haskell Curry：型別組合邏輯的系統化者。
  • Church, A. (1940). A Formulation of the Simple Theory of Types. J. Symbolic Logic 5(2), 56–68.
  • Howard, W. (1980). The Formulae-as-Types Notion of Construction.