第四章 Lambda 演算中的计算

阅读提示

本章会频繁使用“β-归约（beta-reduction）”“可归约表达式（redex）”“范式（normal form）”“发散（divergence）”“传名调用（call-by-name）/ 传值调用（call-by-value）”“小步语义（small-step semantics）/ 大步语义（big-step semantics）”等术语。若你一时记不清这些概念或记号，可随时回查：

附录A《术语表》中的 A.2“Lambda 演算中的计算术语”；

附录B《符号速查表》中的“Lambda 演算相关记号”“容易混淆的符号对照”。

上一章我们定义了 Lambda 演算的语法、变量作用域、α-等价和替换。本章继续回答一个自然的问题：

Lambda 项到底如何计算？

如果说第三章解决的是“式子长什么样，以及变量是什么意思”，那么这一章解决的就是：

一个函数应用如何真正执行；
多个可归约位置同时出现时应先算哪一个；
怎样用规则精确定义“程序运行一步”；
为什么“不同归约顺序”不会把我们带到互相冲突的结果。

本章会在三个层次上讨论“计算”：

归约规则层：先理解 β-归约（beta-reduction）——Lambda 演算最核心的计算规则；
策略层：再理解 归约策略（reduction strategy）/ 求值策略（evaluation strategy）——当有多个地方可算时，先算哪里；
操作语义层：最后用 操作语义（operational semantics） 把“计算过程”写成标准的形式化规则。

这里先特别说明一个阅读约定：

在 4.1–4.6 节，我们会先用一些开放项例子建立“归约 / 策略”的直觉；
到 4.8–4.9 节，我们再固定到更严格的操作语义写法，并明确值与一步关系；
到 4.10 节，我们再把“值 / 范式 / 卡住”这几个概念做一次统一区分，为第 5 章的类型安全做准备。

也就是说，本章既有“帮助你先看懂主线”的直觉层，也有“把计算写成规则”的形式化层。阅读时若一时觉得例子和规则的精度不同，这是有意安排的：前半先建立工作直觉，后半再固定形式化约定。

4.1 β-归约：函数应用就是代入

Lambda 演算最核心的计算规则只有一条：

$(λ x . t) s ⟶_{β} [x \mapsto s] t$

它的直觉非常简单：

左边是一个函数 λx.t
右边给了它一个实参 s
于是就把 s 代入函数体中所有自由出现的 x

也就是说，函数应用的本质就是替换。

这里之所以要先学第三章的替换，是因为这个规则表面上看很简单，但真正严谨地执行它时，必须避免变量捕获。

4.1.1 最简单的例子

例 1：恒等函数

$(λ x . x) y ⟶_{β} y$

因为：

$[x \mapsto y] x = y$

这说明 λx.x 的行为就是“把输入原样返回”。

例 2：常函数

$(λ x . λ y . x) a b$

应用左结合，所以它等于：

$((λ x . λ y . x) a) b$

先归约最左边的应用：

$(λ x . λ y . x) a ⟶_{β} λ y . a$

于是整体变成：

$(λ y . a) b ⟶_{β} a$

这正是“忽略第二个参数，返回第一个参数”的行为。

4.1.2 为什么 β-归约依赖安全替换？

考虑下面这个项：

$(λ x . λ y . x) y$

如果你无脑把 x 换成 y，会得到：

$λ y . y$

但这是错的。因为这里代入进来的 y 原本是自由变量，如果直接写成 λy.y，它就被内层的 λy 捕获了。

正确做法是先做 α-重命名：

$λ x . λ y . x \equiv_{α} λ x . λ z . x$

然后再归约：

$(λ x . λ z . x) y ⟶_{β} λ z . y$

所以更准确地说：

β-归约不是“文本替换”，而是“避免捕获的替换”。

4.2 什么叫可归约项、范式与发散？

为了讨论“一个项还能不能继续算”，需要几个基本术语。

4.2.1 可归约表达式（redex）

形如

$(λ x . t) s$

的项叫做 β-redex，简称 redex（reducible expression）。

直观上，它就是“一个已经准备好应用的函数调用”。

例如：

(\lambda x.x) y 是 redex
(\lambda x.\lambda y.x) a 是 redex
x y 不是 redex，因为函数位置不是 Lambda 抽象

4.2.2 范式（normal form）

如果一个项中已经没有任何 redex，就说它处于 β-范式（β-normal form）。

例如：

x
λx.x
λx. x y

这些都没有形如 (\lambda x.t) s 的子项，因此是 β-范式。

要注意：

范式的定义只关心“还能不能继续按该归约规则走”；
它不等于“闭项”；
它也不等于“值（value）”的概念，后面讲求值策略时会再区分。

4.2.3 发散（divergence）：不终止的归约

并不是所有 Lambda 项都能归约到范式。

最经典的例子是：

$Ω = (λ x . x x) (λ x . x x)$

归约一步：

$(λ x . x x) (λ x . x x) ⟶_{β} (λ x . x x) (λ x . x x)$

得到的还是它自己，所以会无限循环：

$Ω ⟶_{β} Ω ⟶_{β} Ω ⟶_{β} \dots$

这种永远不会到达范式的现象，叫做发散（divergence）。

所以到这里为止，我们可以区分三种情况：

有些项已经是范式；
有些项可以归约若干步后到达范式；
有些项会无限归约下去，永远到不了范式。

这里先再提醒一次层次区别：

到目前为止，我们主要还在讨论归约关系本身；
“值”与“按某种策略前进”要到 4.6 节以后才会进入中心位置；
“卡住”则要到 4.10 节并结合第 5 章的类型安全一起看，才最自然。

4.3 一个项里可能有不止一个 redex

一旦项稍微复杂一些，就可能同时出现多个可归约位置。

例如：

$(λ x . a) ((λ y . b) c)$

这里有两个 redex：

外层的 (\lambda x.a) ((\lambda y.b) c)
内层的 (\lambda y.b) c

于是会出现一个问题：

应该先归约哪一个？

我们可以先归约外层：

$(λ x . a) ((λ y . b) c) ⟶ a$

因为函数体 a 根本不使用 x，所以参数整个被丢弃了。

也可以先归约内层：

$(λ x . a) ((λ y . b) c) ⟶ (λ x . a) b ⟶ a$

两条路径都到达了同一个结果 a。

但这只是一个例子。一般来说，我们需要一种更系统的方式来回答：

不同归约顺序会不会导致不同结果？
如果一个项能到达范式，这个范式是否唯一？

这就引出下面的合流性。

4.4 合流性（confluence）与 Church–Rosser 定理（Church–Rosser theorem）

Lambda 演算最重要的元性质之一，是 合流性（confluence）。

直观上，合流性说的是：

如果一个项可以沿不同的归约路径走下去，那么这些路径不会真正“分裂成互相冲突的结局”；它们总能重新汇合。

形式上，Church–Rosser 定理（Church–Rosser theorem）告诉我们：

如果 $t ⟶_{β}^{*} t_{1}$ 且 $t ⟶_{β}^{*} t_{2}$ ，那么存在某个项 $u$ ，使得
$t_{1} ⟶_{β}^{*} u$ 且 $t_{2} ⟶_{β}^{*} u$ 。

其中：

$⟶_{β}^{*}$ 表示“经过零步或多步 β-归约到达”

图形上可以画成：

4.4.1 这个定理意味着什么？

它最重要的推论是：

如果一个项有 β-范式，那么这个范式在 α-等价意义下是唯一的。

也就是说：

你可以用不同顺序归约；
中间过程可能不同；
但只要真的能归约到范式，最终结果不会互相矛盾。

这非常重要。否则“程序的结果”就会取决于你碰巧先算了哪一块，而不是由程序本身决定。

4.4.2 需要注意的边界

Church–Rosser 定理说的是：

不同路径可汇合
不是说所有路径都一样长
也不是说所有策略都一样高效
更不是说所有策略都一定会找到范式

例如对某些项：

一种策略可能很快到达范式；
另一种策略可能绕很久；
甚至还有一种策略可能一直在无关位置打转。

所以合流性解决的是结果一致性，而不是求值效率或一定终止。

4.5 归约策略：先归约哪个 redex？

既然一个项中可能有多个 redex，我们就需要规定“优先选哪个”。

这类规定统称为归约策略（reduction strategy）。

这里先强调：本节讨论的仍然主要是归约层面的策略，也就是“在允许的 redex 中先选哪一个”。它和后面 4.6 节开始讨论的求值策略有关，但还不是同一个层次：

归约策略更接近“在一般 β-归约图中怎么走”；
求值策略更接近“把哪类项当值、程序一步一步怎样执行”的语言语义约定。

4.5.1 正规序：最左最外优先

最经典的策略之一是 正规序（normal order）：

总是优先归约最左边、最外层的 redex。

例如：

$(λ x . a) ((λ y . b) c)$

按照正规序，先归约外层，立刻得到：

$a$

正规序的重要性质是：

如果某个项存在 β-范式，那么正规序一定能找到它。

这使它在理论上非常重要。

4.5.2 另一种自然想法：先算参数

另一种很自然的想法是：

先把函数和参数都算好；
再执行函数应用。

这更接近许多实际编程语言的执行方式。

不过这里要先提醒一个边界：
下面这一小节里的例子，仍然只是为了说明“先算参数”这种一般归约直觉；它们未必已经满足后面 4.8 节里那套“封闭项 + 只把 Lambda 抽象当值”的传值调用小步语义。

例如：

$(λ x . x) ((λ y . y) z)$

如果先算参数，就得到：

$(λ x . x) ((λ y . y) z) ⟶ (λ x . x) z ⟶ z$

而如果先做外层 β-归约，则得到：

$(λ x . x) ((λ y . y) z) ⟶ ((λ y . y) z) ⟶ z$

两条路径都到达了 z，但中间步骤不同。

4.5.3 “策略不同”不等于“语义不同”

对于未类型化 Lambda 演算，策略的差异主要体现为：

中间步骤不同；
是否会多算一些本来不必算的部分；
是否更容易找到范式。

但由于 Church–Rosser 定理，若某项有范式，则不同策略不会把它带到两个不兼容的范式。

所以这里要区分：

归约关系本身：描述哪些步是允许的；
归约策略：在允许的步中实际优先选哪一步。

而到下一节，我们会进一步固定“值”的概念，并进入更接近编程语言语义的求值策略层面。

4.6 求值策略：传名调用与传值调用

在编程语言语义里，我们通常不使用“任意归约任意 redex”这种最自由的方式，而是定义一套更具体的求值策略（evaluation strategy）。

最常见的两种是：

传名调用（call-by-name）
传值调用（call-by-value）

为了讲清楚这两者，先引入“值”的概念。

这里也再次提醒层次区别：

本节仍然先用一些开放项例子说明策略直觉；
4.8 节开始，我们才会把这些直觉固定成更严格的小步语义规则；
因此本节的重点是“理解差异”，不是“给出最终正式定义”。

4.6.1 值（value）

在最小的未类型化 Lambda 演算里，通常把下面这种形式看作值：

$v ::= λ x . t$

也就是说，函数本身就是值。

变量一般不作为封闭程序的最终结果来讨论；但在开放项的例子里，我们有时仍会把它们当作无法继续归约的式子来看待。

4.6.2 传名调用（call-by-name）

传名调用的核心想法是：

调用函数时，不先把参数算成值，而是直接把参数项代入函数体。

例如：

$(λ x . x) ((λ y . y) z)$

传名调用会先做最外层应用：

$(λ x . x) ((λ y . y) z) ⟶ ((λ y . y) z) ⟶ z$

这里参数 ((\lambda y.y) z) 在代入前没有先被化简。

要注意，这里用的是开放项上的策略直觉示例：它说明“先代入、后继续算参数”的思路，但还没有切换到 4.8 节那套对值和一步关系的严格限定。

4.6.3 传值调用（call-by-value）

传值调用的核心想法是：

只有当参数已经是值时，才执行函数应用。

所以同一个例子：

$(λ x . x) ((λ y . y) z)$

在“先把参数算好再应用”的传值直觉下，会先算参数：

$(λ x . x) ((λ y . y) z) ⟶ (λ x . x) z ⟶ z$

不过同样要注意：这一段是在解释策略直觉，还不是后面 4.8 节那套严格的小步语义。
因为在 4.8 节里，我们会把值限定为 Lambda 抽象；在那套规则下，像 z 这样的自由变量不会被当作封闭程序求值的最终值来讨论。

4.6.4 一个能体现差异的例子

看这个项：

$(λ x . a) Ω$

其中：

$Ω = (λ x . x x) (λ x . x x)$

如果采用传名调用，由于函数体 a 不使用 x，我们直接有：

$(λ x . a) Ω ⟶ a$

但如果采用传值调用，就必须先把参数 \Omega 算成值，而 \Omega 会永远发散，因此整个式子也发散。

这说明：

不同求值策略不仅中间步骤不同，甚至会影响一个程序是否终止。

4.6.5 Haskell 与“惰性”

很多教材会把 Haskell 粗略类比为“传名调用”，这是为了抓住“不急着算参数”这个核心直觉。

但更准确地说：

Haskell 使用的是 按需求值（call-by-need）
它与传名调用关系很近
区别在于：按需求值会共享求值结果，避免同一参数被重复展开多次

在本章里，你只需要先记住：

传名调用：先代入，后计算；
传值调用：先把参数算成值，再代入。

而从 4.8 节开始，我们会把这里的直觉收束成一套固定的、可逐步执行的操作语义规则。

4.7 操作语义：把“如何计算”写成规则

到目前为止，我们已经有了很多直觉性描述：

什么是 β-归约；
什么是求值策略；
什么是值。

现在要做的是把“程序怎样执行”写成一套明确规则。这就是操作语义（operational semantics）。

最常见的两种写法是：

小步语义（small-step semantics）
大步语义（big-step semantics）

4.8 小步语义：一次只走一步

小步语义的目标是定义一个关系：

$t ⟶ t^{'}$

意思是：

项 $t$ 经过一步计算变成 $t^{'}$ 。

为了避免“任意 redex 任意归约”的非确定性，我们现在固定采用传值调用来举例。

4.8.1 传值调用下的值

在未类型化 Lambda 演算中，取：

$v ::= λ x . t$

4.8.2 小步规则

β-应用规则

$( λ x . t ) v ⟶ [ x \mapsto v ] t (E-AppAbs)$

这条规则说：

只有当参数已经是值 v 时，
才能执行函数应用。

函数位置先求值

$\frac{t _{1} ⟶ t _{1}^{'}}{t _{1} t _{2} ⟶ t _{1}^{'} t _{2}} (E-App1)$

这条规则说：

如果函数位置还能再算一步，
那么整个应用先跟着它往前走一步。

参数位置后求值

$\frac{t _{2} ⟶ t _{2}^{'}}{v _{1} t _{2} ⟶ v _{1} t _{2}^{'}} (E-App2)$

这条规则说：

如果函数位置已经是值，
那就开始求值参数位置。

这三条规则一起刻画了传值调用的顺序：

先算函数位置；
再算参数位置；
最后在两者都就绪时做 β-归约。

4.8.3 一个完整例子

为了和这里固定的传值调用小步语义完全一致，我们使用一个封闭项例子：

$((λ f . λ x . f x) (λ y . y)) (λ z . z)$

先看最左边的应用。函数位置和参数位置都已经是值，因此可用 E-AppAbs：

$((λ f . λ x . f x) (λ y . y)) (λ z . z) ⟶ (λ x . (λ y . y) x) (λ z . z)$

接着，外层应用再次满足 E-AppAbs：

$(λ x . (λ y . y) x) (λ z . z) ⟶ (λ y . y) (λ z . z)$

最后再归约一次：

$(λ y . y) (λ z . z) ⟶ λ z . z$

所以整体归约到：

$λ z . z$

这个例子和 4.6 节里那些“开放项上的策略直觉示例”不同：
这里每一步都严格符合本节给出的值定义与小步规则。

4.8.4 多步归约

如果一步关系记作 $⟶$ ，那么“经过零步或多步归约”记作：

$⟶^{*}$

例如：

$(λ x . x) ((λ y . y) z) ⟶^{*} z$

这表示它可以经过若干步，最终到达 z。

4.9 大步语义：直接描述最终结果

大步语义不关心中间每一步，而直接定义：

$t ⇓ v$

意思是：

项 $t$ 最终求值为值 $v$ 。

对于传值调用的未类型化 Lambda 演算，可写出如下规则。

4.9.1 值规则

$v ⇓ v (B-Value)$

值求值到它自己。

4.9.2 应用规则

$\frac{t _{1} ⇓ λ x . t t _{2} ⇓ v _{2} [ x \mapsto v _{2} ] t ⇓ v}{t _{1} t _{2} ⇓ v} (B-App)$

它的意思是：

先把函数位置求值为某个 Lambda 抽象；
再把参数求值为值；
然后把该值代入函数体继续求值；
最终得到结果值。

4.9.3 一个例子

仍然考虑：

$((λ f . λ x . f x) (λ y . y)) (λ z . z)$

按大步语义理解：

(\lambda f.\lambda x.f x) 已经是值；
(\lambda y.y) 也是值；
代入后得到 \lambda x.(\lambda y.y) x；
再把它应用到 \lambda z.z；
最终结果是 \lambda z.z。

所以：

$((λ f . λ x . f x) (λ y . y)) (λ z . z) ⇓ λ z . z$

4.9.4 小步与大步的差别

小步语义擅长描述“程序如何一步步运行”
大步语义擅长描述“程序最终得到什么结果”

各有侧重：

如果你想讨论中间状态、卡住、并发、异常传播等，小步语义通常更方便；
如果你只关心一个确定性语言的最终求值结果，大步语义更简洁。

本教程后面谈类型安全时，会更多依赖小步语义的视角，因为它更适合表达“要么继续走，要么已经是值”。

4.10 值、范式与卡住：先做一个概念区分

这一节先做概念澄清。严格意义上，在纯未类型化 Lambda 演算里：

我们通常讨论的是值（value）与 β-范式（β-normal form）；
“卡住状态（stuck term / stuck state）”这个概念在加入布尔值、自然数、条件表达式等扩展构造后会变得尤其清楚、尤其有教学意义。

4.10.1 值与范式不是同一个概念

范式：相对于某个归约关系，已经无法继续走；
值：相对于某个求值策略，被视为“计算完成”的形式。

在很多简单系统里，值往往也是范式；但这两个概念的定义来源不同，最好不要混为一谈。

4.10.2 “卡住”在扩展语言里最典型，但不是只能在那里出现

例如，在带有布尔值和应用的扩展语言里：

true 0

它既不是值，也没有任何求值规则适用，因此是“卡住”的。

这类例子之所以常被拿来讲“卡住”，是因为它非常直观：
程序表面上有某种“计算形状”，但语言规则根本不给它下一步。

不过更精确地说：

对纯 Lambda 演算的封闭项，在讨论完全 β-归约时，“卡住”通常不是最核心的组织概念；
但一旦你固定某种求值策略，特别是在讨论开放项时，也仍然可能出现“既不是值、又不能按当前策略前进”的情况。

因此，更稳妥的理解方式是：

“卡住”在扩展语言里最自然、最典型；而在纯 Lambda 演算里，我们本章更关心的仍然是归约、范式和值。

真正要把“良类型程序不会卡住”说严谨，要等到下一章引入类型规则之后再看才最自然。

所以本章先记住三点：

第四章前半主要在讨论归约与策略；
第四章后半把这些直觉收束成操作语义；
第五章才会把“卡住”正式接到类型安全上。

4.11 本章小结

这一章建立了 Lambda 演算中“计算”这一层的核心概念。

你应该已经掌握的主线

β-归约是 Lambda 演算的核心计算规则： $(λ x . t) s ⟶_{β} [x \mapsto s] t$
一个项里可能同时有多个 redex，因此需要讨论归约策略。
Church–Rosser 定理保证了：
- 若某项有范式，则其范式在 α-等价意义下唯一；
- 不同归约路径不会导致真正冲突的最终结果。
求值策略进一步规定：
- 到底先算函数位置还是参数位置；
- 是否要求参数先成为值。
操作语义把“程序如何运行”写成推导规则：
- 小步语义关注单步执行；
- 大步语义关注最终结果。

与下一章的关系

如果说本章回答的是：

“Lambda 项如何运行？”

那么下一章将回答：

“哪些 Lambda 项是被允许的？为什么它们不会在运行时出问题？”

也就是说：

本章是计算规则
下一章是类型规则

两者合在一起，才构成类型系统理论最核心的骨架。

回看导航

如果你读完本章后还觉得某些部分不够稳，可以按下面顺序回看：

若你对 FV(t)、替换、变量捕获、α-重命名仍然不稳，先回到第 3 章；
若你对“值 / 范式 / 卡住”“→ / →* / ⇓”这些术语或记号混淆，先查附录A和附录B；
若你想把“如何计算”和“为什么良类型程序不会卡住”连起来，再继续看第 5 章。

本章练习

逐步归约下列项，并写出每一步：
- $(λ x . x) y$
- $(λ x . λ y . x) a b$
- $(λ f . λ x . f x) (λ y . y) z$
解释为什么下面的归约不能直接做“无脑文本替换”： $(λ x . λ y . x) y$ 并给出正确结果。
对项 $(λ x . a) ((λ y . b) c)$ 分别先归约外层和先归约内层，观察结果。
比较下列项在传名调用和传值调用下的行为： $(λ x . a) Ω 其中 Ω = (λ x . x x) (λ x . x x)$ 说明为什么两种策略的终止性不同。
用小步语义规则证明： $((λ f . λ x . f x) (λ y . y)) (λ z . z) ⟶^{*} λ z . z$

Keyboard shortcuts

编程语言理论与类型系统入门