Lambda 演算——用函数表达一切计算

λ 演算只有三种表达式——变量、函数抽象、函数应用——没有数字、没有 if、没有循环，却足以表达一切可计算的东西。

你写过函数，知道函数接收参数、返回结果。你也听过“函数式编程”，大概还背过闭包、高阶函数、递归这些词。但你有没有想过：把一门编程语言剥到最薄，最少还需要什么，它才能算东西？

1930 年代，数学家 Alonzo Church 给出了一个极端的答案：只要函数，就够了。他设计了一套叫 λ 演算（lambda calculus）的形式系统——没有数字、没有布尔、没有条件分支、没有循环，整个系统只有三种表达式。Church 证明了，这套极简的系统和图灵机一样强大，能表达一切可计算的函数。

这不是一段历史趣闻。你现在写的每一个 Racket 函数，本质都是 λ 演算里的一个项。 Racket 的 lambda、它的闭包、它“函数是一等公民”的设计，全部直接来自这套九十年前的数学。理解了 λ 演算，你就摸到了函数式编程的最底层。

这一讲先把基础打牢：λ 演算的语法、它唯一的求值规则，以及怎么用它凭空造出布尔值和自然数。

整个系统只有三种形式

λ 演算里所有合法的项（term）只有三种：

变量：x
函数抽象（abstraction）：λx. M，参数是 x，函数体是 M
函数应用（application）：M N，把函数 M 应用到参数 N

就这三种，没有第四种。把它翻译成 Racket，你立刻就眼熟：

; 变量
x

; 函数抽象：λx. M
(λ (x) M) ; λ 就是 lambda 的简写，两者完全等价
(lambda (x) M) ; 这一行和上一行没有任何区别

; 函数应用：M N
(M N) ; 函数和参数用括号包起来

Racket 允许你直接写 λ 这个字符——它在 Racket 里和 lambda 是同一个关键字。这不是巧合：Racket 的核心语法，几乎就是 λ 演算穿了件衣服。

注意 λ 演算的函数永远只吃一个参数，(λ (x) M) 对应 λx. M。那两个参数的函数怎么办？答案是再套一层——先用第一个参数返回一个新函数，再让它吃第二个：

(λ (x) (λ (y) ...)) ; 等价于一个接收 x、y 两个参数的函数

这种把多参数拆成一串单参数的技巧叫柯里化（currying），是函数式编程的看家本领，也是 λ 演算天生就支持的写法。

β 归约，唯一的求值规则

语法有了，怎么“运行”它？λ 演算只有一条求值规则，叫 β 归约（beta reduction）：

(λx. M) N → M[x := N]

把函数体 M 里所有出现的 x，替换成参数 N。一句话说就是“实参代入形参”。整个 λ 演算的计算，就是反复做这一件事。

看两个例子：

(λx. x) y → y ; 最简单的函数：恒等函数，原样返回参数

(λx. λy. x) A B → (λy. A) B ; 先归约外层，把 x 换成 A
 → A ; 再归约，丢掉 B，返回 A

第二个例子里，λx. λy. x 接收 x，返回一个接收 y 但永远吐 x 的函数——它记住了第一个参数，无视第二个。这个函数你马上还会见到，它就是“真”。

用 Racket 跑一遍，行为完全一样：

((λ (x) x) 'y)
;; 'y

(define first-of (λ (x) (λ (y) x))) ; λx.λy.x
((first-of 'A) 'B)
;; 'A 返回 A，丢掉 B

用函数造出布尔和条件判断

λ 演算里没有布尔值。Church 给出了一个惊人的编码：把“真”和“假”都写成函数。

TRUE := λt. λf. t ; 接收两个值，返回第一个
FALSE := λt. λf. f ; 接收两个值，返回第二个

TRUE 就是我们刚才那个“记住第一个、无视第二个”的函数。布尔值被编码成了“二选一”的行为。条件判断 IF 顺理成章——让布尔值自己去做选择：

IF := λp. λa. λb. p a b

IF TRUE A B → TRUE A B → A
IF FALSE A B → FALSE A B → B

这些不是比喻，是能在 Racket 里直接跑的代码：

(define TRUE (λ (t) (λ (f) t)))
(define FALSE (λ (t) (λ (f) f)))
(define IF (λ (p) (λ (a) (λ (b) ((p a) b)))))

(((IF TRUE) 'yes) 'no)
;; 'yes

(((IF FALSE) 'yes) 'no)
;; 'no

代码里没有一个 if 关键字。布尔值自己就是一个会做选择的函数。 这就是 Church 编码（Church encoding）的核心：不靠内建类型，靠函数的行为来“扮演”各种数据。

Church 数，把数字变成应用次数

数字怎么办？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 次

数字不再是“数量”，而是“应用次数”。验证一下：把 Church 数 3 作用到 add1 和 0 上，应该得到 3。

(define c0 (λ (f) (λ (x) x)))
(define c1 (λ (f) (λ (x) (f x))))
(define c2 (λ (f) (λ (x) (f (f x)))))
(define c3 (λ (f) (λ (x) (f (f (f x))))))

((c3 add1) 0)
;; 3 add1 连用 3 次：0 → 1 → 2 → 3

现在造“加一”（后继）和加法：

SUCC := λn. λf. λx. f (n f x) ; 在 n 次基础上再多用一次 f
ADD := λm. λn. λf. λx. m f (n f x) ; m 次 + n 次

SUCC 的意思：n 表示“用 f 的 n 次”，SUCC n 就再用一次 f，所以是 n+1。ADD 把 m 次和 n 次首尾相接，总共 m+n 次。用 Racket 跑：

(define succ (λ (n) (λ (f) (λ (x) (f ((n f) x))))))
(define add (λ (m) (λ (n) (λ (f) (λ (x) ((m f) ((n f) x)))))))

(((succ c2) add1) 0)
;; 3 c2 加一 = c3

((((add c2) c3) add1) 0)
;; 5 2 + 3 = 5

只用函数，我们凭空造出了布尔、条件判断和自然数加减。 这不是在“模拟”数字——Church 编码证明了一件事：函数本身，就足以表示一切可计算的东西。

α 转换，替换之前先改名

β 归约看起来直白，但藏着一个陷阱。看这个表达式：

(λx. λy. x) y

按 β 归约，要把 x 替换成 y。如果你直接替换，会得到 λy. y——但这错了。外层那个自由的 y，被内层约束的 y 意外“捕获”了，原本不该被绑定的 y 被绑死了。

正确的做法是：替换之前，先把内部那个同名的约束变量改个名，避开冲突：

(λx. λz. x) y → λz. y

把内层的 y 改成 z，再代入，结果才对。这种“改名”叫 α 转换（alpha conversion）。它背后的等价关系叫 α 等价：λx. x 和 λy. y 是同一个函数，变量叫什么名字不影响含义。

一次安全的 β 归约，要先 α 转换、再替换。 这套机制叫避免捕获的替换（capture-avoiding substitution），也是实现任何 λ 演算解释器时最容易写错的地方。

亲手写一个 λ 演算解释器

把上面的理论写成 Racket，就是一个最小的解释器。先把三种表达式表示成数据结构：

#lang racket

(struct Var (name)) ; 变量
(struct Abs (param body)) ; 函数抽象：参数 + 函数体
(struct App (func arg)) ; 函数应用：函数 + 参数

核心是替换函数——把 expr 里所有名为 x 的变量换成 v：

(define (subst expr x v)
 (match expr
 [(Var y) (if (equal? y x) v expr)] ; 是目标变量就换，否则不动
 [(Abs param body)
 (if (equal? param x)
 expr ; 参数遮蔽了 x，函数体里不用换
 (Abs param (subst body x v)))] ; 否则递归换函数体
 [(App f a) (App (subst f x v) (subst a x v))])) ; 两边都换

β 归约几乎是直译——遇到“函数遇上参数”，就执行替换：

(define (reduce expr)
 (match expr
 [(App (Abs param body) arg) (subst body param arg)] ; 函数遇参数：替换
 [(App f a) (App (reduce f) (reduce a))] ; 否则递归归约两边
 [_ expr])) ; 变量、抽象保持原样

这就是 λ 演算的“虚拟机”。注意这里的 subst 故意省略了 α 转换——它会中招于前面说的变量捕获。一个完整的实现，要在替换前自动给约束变量改名。但作为把理论变成代码的最短路径，这二十来行已经够你看清“计算”在 λ 演算里到底是怎么发生的。

在这个骨架上，你可以继续加按需求值（lazy evaluation）、加完整的 α 转换、加不同的归约策略——从数学形式一步步走到真正的语言实现。

λ 演算还有一件事没解决：它没有变量定义，没有 define，没有 let。这意味着你没法给一个函数起名字，更没法让一个函数在函数体里调用自己。没有名字，递归从哪儿来？

Church 用一个绝妙的技巧回答了这个问题——一个叫 Y 组合子（Y-combinator）的函数，它能让任何函数“找到自己”。那是 λ 演算最烧脑也最漂亮的部分。下一篇就讲它：递归，到底从哪里来。