跳轉到

1936：Lambda 演算——邱奇奇點#

事件#

1936年，美國邏輯學家 Alonzo Church（邱奇） 在《Annals of Mathematics》發表關於 λ 演算（lambda calculus）的研究成果，提出了一個以「函數抽象與函數應用」為唯一基本運算的極簡形式系統。同一時期，Alan Turing（圖靈） 發表圖靈機模型。有趣的是，圖靈正是 Church 在普林斯頓的博士學生——兩人各自獨立提出了「可計算性」的形式化定義，並很快被證明在表達能力上完全等價。

語法/特性加入的理論與實用原因#

1. 變數綁定與 β-歸約（β-reduction）#

  • 理論原因：整個系統只靠三條規則運作——λx.M 是「抽象」（定義函數），M N 是「應用」（呼叫函數），β-歸約 (λx.M) N → M[x:=N] 則是計算的核心引擎。任何可計算的函數都能只用這三樣東西表達。
  • 實用原因：極簡性使它成為研究「計算本質」的理想工具，也成為日後設計程式語言時「函數呼叫」的數學原型。
(λx. x + 1) 5   →   5 + 1   →   6

β-歸約可以串聯多步，每一步都只是「把引數代入變數」這個機械動作：

;; 多步 β-歸約：左結合，逐層代入
(λx. (λy. x + y)) 3 2
→ (λy. 3 + y) 2      ; 代入 x := 3
→ 3 + 2              ; 代入 y := 2
→ 5

對照組：同樣的計算在組合語言裡需要先把引數放進暫存器、呼叫副程式、取出結果——「代入」這個動作完全不存在的，只有位址的搬移：

; 假想的簡化組合語言：與「代入」無關，只有暫存器搬移
LOAD  R1, 3      ; 引數 3 入暫存器
LOAD  R2, 2      ; 引數 2 入暫存器
ADD   R1, R1, R2 ; R1 := R1 + R2
STORE R3, R1     ; 結果寫回記憶體

2. α-轉換與 η-轉換#

  • 理論原因：α-轉換處理「束縛變數改名不影響語義」（λx.x 與 λy.y 相同）；η-轉換則表達「外延等價」——λx.(f x) 等同於 f。這兩條規則讓函數相等性有了嚴格定義。
  • 實用原因：現代函數式語言中的「變數遮蔽（shadowing）」與「eta 簡化（point-free 風格的理論依據）」直接源自這兩條規則。
;; α-轉換：改名不影響語義
(λx. x)  ≡α  (λy. y)          ; 兩者都是「恆等函數」

;; α-轉換用來避開捕捉衝突（capture-avoidance）
(λx. λy. x + y)  ≡α  (λx. λz. x + z)
;; 若不改名，代換時 y 會被外層的同名變數「捕捉」

;; η-轉換：消除多餘的包裝
λx. (f x)  ≡η  f
;; 這是 point-free 風格的理論依據：不必替引數命名

3. 純函數與無副作用#

  • 理論原因：λ 演算中函數是純數學物件——同樣的輸入永遠得到同樣的輸出，沒有狀態、沒有時序、沒有副作用。這使得「以函數為計算單位」在數學上完全嚴格，可進行等式推導與代換。
  • 實用原因：無副作用為日後的程式驗證、引用透明性（referential transparency）、平行計算鋪路——因為函數之間互不干擾。

引用透明性允許「等式代換」：任何表達式都可以用它的值替換，推導結果不變——這是 λ 演算能被當成代數來操作的原因：

;; 引用透明：f = λx. x * x，處處可用其定義代換
f(3 + 1)
= (3 + 1) * (3 + 1)    ; 代換 f 的定義
= 4 * 4                ; 內部先化簡
= 16

;; 反例（有副作用的世界，如命令式語言）：
;; 若 f 會印出訊息或改動全域變數，
;; 「f(4) 換成 16」就會丟失副作用，代換不再安全

4. Curry 的組合邏輯（1920s–1930）#

  • 理論原因：Haskell Curry 在 1920 年代至 1930 年間發展組合邏輯（combinatory logic），企圖消除變數綁定，只留下組合子（如 S、K）。它與 λ 演算表達能力等價。
  • 實用原因：組合子思想直接影響了 1977 年 Backus 的 FP 系統，以及後世 Haskell 語言的名字（Curry 本人的姓氏，加上邏輯學家 Haskell）。

λ 演算中最驚人的展示：只用函數就能造出數字、布林與資料結構——不需要任何內建型別。

;; Church 數：n 是「把函數 f 套用 n 次」
0 := λf. λx. x            ; f 套 0 次，直接傳回 x
1 := λf. λx. f x          ; f 套 1 次
2 := λf. λx. f (f x)      ; f 套 2 次
3 := λf. λx. f (f (f x))  ; f 套 3 次

;; 加法：把 m 的 f 迭代再交給 n 繼續迭代
add := λm. λn. λf. λx. m f (n f x)

;; 展開驗證 add 2 3
add 2 3 = λf. λx. 2 f (3 f x)
        = λf. λx. f(f( f(f(f x)) ))   ; 共套 5 次 → Church 數 5

;; Church 布林：用「二選一」定義真假
TRUE  := λa. λb. a    ; 選第一個
FALSE := λa. λb. b    ; 選第二個

;; 邏輯運算只用函數應用表達
AND := λp. λq. p q FALSE
OR  := λp. λq. p TRUE q
NOT := λp. p FALSE TRUE

;; 驗證 AND TRUE FALSE
AND TRUE FALSE = TRUE FALSE FALSE = FALSE   ; TRUE 選第二個 → FALSE

;; pair：兩個值裝進一個函數；fst/selm 用布林取件
pair := λa. λb. λf. f a b
fst  := λp. p TRUE     ; 相當於 p (λa.λb.a)，選第一個
snd  := λp. p FALSE

;; 驗證：fst (pair 1 2)
fst (pair 1 2) = (λa.λb.a) 1 2 = 1

;; Y 組合子：讓匿名函數也能遞迴——LISP 遞迴的理論前身
Y := λg. (λx. g (x x)) (λx. g (x x))

;; 對任意函數 g，Y g 是 g 的不動點：Y g = g (Y g)
;; 於是「自我呼叫」可以定義出來，例如階層：
fact := λf. λn. (ISZERO n) 1 (MULT n (f (PRED n)))
Y fact 5 → 120

彌補了什麼缺陷#

在 1936 年之前，「可計算」只是直覺概念，無法嚴格定義。Church 的 λ 演算首次把「函數即計算」形式化，與圖靈機等價性共同奠定了 Church–Turing 假說：所有直覺上可計算的函數，都可由 λ 演算（或圖靈機）計算。它彌補的最大缺陷是：數學上有了「程式的原型」，而純函數無副作用的模型成為之後所有函數式語言的理論基石——只是這塊基石要等到 22 年後的 LISP 才真正落入實用。

相關條目#