02.1 邱奇的偉大發明：只有變數與代換的宇宙#

導言：為什麼邱奇要發明 λ 演算？#

1920 年代末，Alonzo Church 在普林斯頓研究一個看似與「計算」無關的問題：邏輯與數學的基礎。他繼承弗雷格與羅素的志業，希望找出一個最精簡的符號系統，能把「函數」這個數學核心概念原生化。

當時數學中的函數是怎麼寫的？ \(f(x) = x^2 + 1\) 。這裡藏著一個語言學的尷尬： \(f\) 是函數的名字， \(x\) 是佔位符，等號右邊是表達式——「函數」本身沒有獨立的語法地位，你必須命名它才能使用它。邱奇的洞見是：函數應該像數字一樣，是可以直接寫出來的表達式。他採用 λ 這個符號（據說源自《數學原理》中表示「類」的脫字符號 \(\hat{x}\) 的排版變體）：

這就是匿名函數。今天你寫 lambda x: x**2 + 1（Python）或 \x -> x*x + 1（Haskell），用的正是邱奇 1930 年前後發明的語法。

三條文法規則，一個宇宙#

定義（λ 項）：由以下規則歸納定義， \(x\) 為變數：

就這樣。沒有數字、沒有資料結構、沒有控制流程、沒有賦值。一切都必須由函數搭建。這個刻意貧瘠的設定，正是它力量的來源——如同歐氏幾何的五條公理，公理越少，系統越純粹，能推出的結論越震撼。

慣例與括號省略#

• 應用左結合： \(M\ N\ P\) 意為 \((M\ N)\ P\) ——先呼叫 \(M\ N\) ，再把結果應用於 \(P\) ；
• λ 的身體向右延伸到底： \(\lambda x.\, M\ N\) 意為 \(\lambda x.\,(M\ N)\) ；
• 多參數透過柯里化（currying）表達： \(\lambda x.\,\lambda y.\,M\) ，即「吃 \(x\) 回傳『吃 \(y\) 的函數』」。這個技巧以 Haskell Curry 命名（雖然 Frege 與 Schönfinkel 更早使用）——歷史命名常常如此不公。

α-等價與 β-化約：這個宇宙的物理定律#

λ 演算的計算，全部濃縮成兩條規則。

α-變換（改名）： \(\lambda x.\,M\) 與 \(\lambda y.\,M[x{:=}y]\) （ \(y\) 不自由出現在 \(M\) 中）是同一個函數。就像 lambda x: x+1 與 lambda y: y+1 無異。變數的名字本身沒有意義，只有綁定關係有意義。

β-化約（代換，計算的核心）：

把「呼叫函數」定義成文字代換：將 \(M\) 中所有自由的 \(x\) 替換為 \(N\) 。就這一條規則，承擔了整個計算理論。

# β-化約的玩具實作
from dataclasses import dataclass

@dataclass
class Var:
    name: str

@dataclass
class Lam:                       # λ param . body
    param: str
    body: 'Term'

@dataclass
class App:                       # (f a)
    func: 'Term'
    arg: 'Term'

Term = Var | Lam | App

def subst(m: Term, x: str, n: Term) -> Term:
    """M[x := N] —— 最困難的一步：避免捕獲"""
    match m:
        case Var(y):
            return n if y == x else m
        case Lam(y, body):
            if y == x:
                return m                       # x 被內層綁定，代換停止
            if y in free_vars(n):
                # α-變換先改名，避免「變數捕獲」
                fresh = y + "'"
                return subst(Lam(fresh, subst(body, y, Var(fresh))), x, n)
            return Lam(y, subst(body, x, n))
        case App(f, a):
            return App(subst(f, x, n), subst(a, x, n))

def free_vars(m: Term) -> set[str]:
    match m:
        case Var(x):       return {x}
        case Lam(_, b):    return free_vars(b) - {m.param}
        case App(f, a):    return free_vars(f) | free_vars(a)

def step(m: Term) -> Term | None:
    """做一次 β-化約（由左至右找紅色子項）"""
    match m:
        case App(Lam(p, body), arg):
            return subst(body, p, arg)
        case App(f, a):
            return (App(nf, a) if (nf := step(f)) else
                    App(f, na) if (na := step(a)) else None)
        case Lam(p, body):
            return Lam(p, nb) if (nb := step(body)) else None
        case _:
            return None

# 測試：(λx. x) y → y
expr = App(Lam("x", Var("x")), Var("y"))
print(step(expr))    # Var(y)

變數捕獲：代換的暗礁#

上面的 subst 特意處理一個經典陷阱。考慮：

右邊錯了！代換後的 \(y\) 被內層 λ 捕獲，本來指外的 \(y\) 變成了指內。正確做法是先 α-改名：

這個「捕獲避免代換」的細節，看似技術小事，實則是名字與綁定理論的全部核心。程式語言的作用域規則（lexical scoping）、巨集衛生（hygienic macros）、編譯器的 renaming pass，全都是它的後裔。

歷史的第一幕：邏輯的失敗，計算的成功#

邱奇與他的學生 Kleene、Rosser 一開始的野心是邏輯的：把 λ 演算加上邏輯公理，作為數學基礎（類似羅素的類型論，但更精簡）。1932 年他發表了這套系統——然後 1935 年，他自己的學生 Kleene 與 Rosser 證明了這個系統是不一致的（能推出矛盾）。

基礎夢碎了。但在廢墟中，邱奇注意到一個碎片依然閃光：純粹的 λ 演算本身（不加邏輯公理）是一個極為精確的「可計算函數」模型。他定義：

一個自然數函數是 λ-可計算的，若它可以由某個 λ 項表示。

1936 年，邱奇用這個定義證明了判定問題無解——與圖靈同年、異途、等價。圖靈起初對這個「符號代換遊戲」與真實計算的關聯存疑，還專門寫了論文證明兩者等價（圖靈 1937）。後來的故事众所周知：Church–Turing 命題成立，兩個模型是同一個宇宙的兩種描述。

歷史教訓：λ 演算作為邏輯基礎失敗了，作為計算模型成功了。而在七十年後，經過類型化（第一章預告的 Curry–Howard 線），它又回來完成了當年失敗的使命——成為定理證明系統（Coq、Agda）的基礎。一個思想的生命週期可以長過發明者的預期。

範例：熟悉語言裡的 λ 無所不在#

# Python：邱奇語法的直系後裔
square = lambda x: x * x
compose = lambda f, g: lambda x: f(g(x))   # λf.λg.λx. f (g x) —— 柯里化版本
inc_twice = compose(square, lambda n: n + 3)
print(inc_twice(2))    # (2+3)² = 25

# functools.partial、map/filter、裝飾器……全是 λ 演算的思想結晶
from functools import reduce
print(reduce(lambda acc, n: acc + n, [1, 2, 3, 4], 0))   # 摺疊 = 反覆應用

-- Haskell：語法幾乎就是 λ 演算
-- λx. x + 1     寫作  \x -> x + 1
-- λf.λg.λx.f(gx) 寫作  \f g x -> f (g x)

compose :: (b -> c) -> (a -> b) -> a -> c
compose f g x = f (g x)          -- 注意：x 只出現在「應用」位置

-- 部分應用（currying 的實戰红利）：
add :: Int -> Int -> Int         -- 等價 λx.λy. x + y
add x y = x + y
add10 = add 10                   -- λy. 10 + y —— 函數是可分解、可組合的值

定理整理#

定義（λ 項）： \(M ::= x \mid \lambda x.\,M \mid M\ N\) 。

定義（β-化約）： \((\lambda x.\,M)\ N \to M[x{:=}N]\) ，採捕獲避免代換（必要時先 α-改名）。

定義（λ-可計算，Church 1936）：函數 \(f\) 稱為 λ-可計算，若存在 λ 項 \(F\) 使 \(F\ \bar{n} = \overline{f(n)}\) （ \(\bar{n}\) 為 \(n\) 的教會編碼，見 02.3）。

定理（Church–Rosser / 合流性，1936）：若 \(M \to^* P\) 且 \(M \to^* Q\) ，則存在 \(R\) 使 \(P \to^* R\) 且 \(Q \to^* R\) 。化約的順序不影響最終結果（就「能否到達同一個正規形式」而言）。

定理（Church–Turing）：λ-可計算＝圖靈可計算。

Church–Rosser 定理值得多看一眼：它保證了 λ 演算是決定論式的計算系統——同一個程式不會因為求值策略不同而得到不同答案（雖然可能一個停、一個不停，例如 \((\lambda x.\,y)\ \Omega\) ：先化約外層得到 \(y\) ，先化約內層則永不完結。這就是急切 vs 惰性求值的理論原型，也是 Haskell 惰性求值與 Python 立即求值在理論上的分水嶺）。

章末小結#

• 邱奇發明 λ 演算，初衷是給「函數」原生語法地位，並以此重建數學基礎。
• 只有三條文法規則（變數、抽象、應用）與兩條計算規則（α 改名、β 代換）。
• 變數捕獲與捕獲避免代換，是作用域理論的源頭。
• 邏輯版本失敗（Kleene–Rosser 不一致性），但純 λ 演算作為計算模型與圖靈機等價，成為 Church–Turing 命題的兩柱之一。
• Church–Rosser 合流性保證計算結果與求值順序無關，是函數式語言的理論基石。

下一步#

光有 \((\lambda x.\,M)\ N \to M[x{:=}N]\) 一條規則，真的能「計算」嗎？下一章（02.2）我們深入 β 化約的動力學：不動點與遞迴如何從純代換中湧現、 \(\Omega = (\lambda x.\,x\,x)(\lambda x.\,x\,x)\) 為何是無窮迴圈的原型、以及 Y 組合子如何讓「匿名函數」學會呼叫自己。你將親眼看到：遞迴不是內建功能，而是可以被從虛空中推導出來的定理。

習題#

1. 用 Python 實作 free_vars 與捕獲避免的 subst（可參考本節程式，補上完整測試）。
2. 化約 \((\lambda x.\,\lambda y.\,x\ y)\ y\) ——注意第二個 \(y\) 是自由變數，小心捕獲！
3. 證明： \((\lambda x.\,M)\ N \to M[x{:=}N]\) 中，若 \(N\) 中含有與 \(M\) 衝突的自由變數，則「直接代換」會改變語義。舉一個具體反例。
4. 思考題：邱奇系統不一致性的歷史，對「設計一個表達力強大的系統」有何警示？（提示：表達力與一致性的張力，在型別系統設計中如何重演？）