Lambda 演算 — 計算理論

什麼是 Lambda 演算？

Lambda 演算是阿隆佐·丘奇（Alonzo Church）在 1936 年發明的計算模型，與圖靈機等價，是函數式編程的理論基礎。與圖靈機從狀態和轉移的角度描述計算不同，Lambda 演算從函數的角度描述計算，強調函數的應用和代換。這一發現奠定了 Church-Turing 論點的基礎：任何「可有效計算」的函數都可以用 Lambda 演算或圖靈機來表示。

核心語法

Lambda 演算的語法非常精簡，只有三種表達式：

項 (Term) ::= 變數 x
            | λ 變數 . 項     (抽象/函數定義)
            | (項 項)          (應用/函數呼叫)

語法範例：

λx.x           # 恆等函數：接受 x 並返回 x
λx.λy.x        # 雙參數函數（柯里化）
(λx.x) y       # 應用：將 y 傳給恆等函數

三種轉換規則

α 轉換 (Alpha Conversion)：允許更改函數的參數名稱而不改變其語義。λx.M = λy.M[x/y]

β 歸約 (Beta Reduction)：函數應用的核心規則。(λx.M) N → M[x/N]，表示將 λx.M 應用於 N，相當於將 M 中的 x 替換為 N。

# β 歸約範例
(λx.x) y → y              # 應用恆等函數
(λx.x) (λy.y) → λy.y      # 函數作為參數
(λx.λy.x) a b → a         # 柯里化應用

η 轉換 (Eta Conversion)：反映函數的 extensionality 原則。λx.(M x) = M（前提：x 不在 M 中自由出現）。

Church 編碼

Church 編碼是一種用 Lambda 演算表示資料結構的方法：

布爾值

TRUE  = λx.λy.x    # 返回第一個參數
FALSE = λx.λy.y    # 返回第二個參數
IF    = λc.λx.λy.c x y  # 條件選擇

AND   = λp.λq.p q p
OR    = λp.λq.p p q
NOT   = λc.c FALSE TRUE

丘奇數 (Church Numerals)

ZERO  = λf.λx.x
ONE   = λf.λx.f x
TWO   = λf.λx.f (f x)

SUCC  = λn.λf.λx.f (n f x)     # 後繼：n + 1
ADD   = λm.λn.λf.λx.m f (n f x) # 加法：m + n
MULT  = λm.λn.λf.m (n f)        # 乘法：m × n

Y Combinator

Y Combinator 是實現遞迴的關鍵，允許在不具名遞迴的情況下定義遞迴函數：

Y = λf.(λx.f (x x)) (λx.f (x x))

這使得我們可以定義階層函數：fact = Y (λf n. if n==0 then 1 else n * f(n-1))

本課程範例

lambda/01-full/lambdaCalculus.py — Lambda 演算完整實現
lambda/02-short/lambdaCalculus.py — 精簡版實現
lambda/03-interpreter/lambda.py — 直譯器實作

Lambda 演算 (Lambda Calculus)