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

第三章 Lambda 演算基础

阅读提示

本章会频繁使用“项”“自由变量 / 绑定变量”“α-等价”“替换”“新鲜变量”“变量捕获”等术语。若你在阅读时想快速回查定义与记号，建议配合：

• 附录A《术语表》中的 A.1“Lambda 演算与语法相关术语”
• 附录B《符号速查表》中的“Lambda 演算相关记号”“正文中常见的元变量约定”

我们已经学会了如何用 BNF 和抽象语法来定义一门语言。现在可以把这些工具真正用起来：定义一个极简、却足以支撑整个类型系统理论的核心语言——Lambda 演算（Lambda Calculus）。

阅读本章时，建议把附录A“术语表”和附录B“符号速查表”放在手边。
如果你一时分不清 FV(t)、[x \mapsto s]t、\equiv_\alpha 这些记号，它们都可以在附录中快速查到。

Lambda 演算（Lambda Calculus）之所以重要，不是因为它像真实编程语言那样“功能丰富”，恰恰相反，是因为它极简。整个语言只有三种基本构造：

• 变量（variable）
• 函数抽象（abstraction）
• 函数应用（application）

它没有数字、没有字符串、没有布尔值、没有 if、没有循环。但令人惊讶的是，在适当的编码方式下，未类型化 Lambda 演算具有与图灵机等价的计算表达能力。

这也是为什么它会成为类型系统理论的出发点：
真实语言太复杂，不适合直接做数学分析；Lambda 演算足够小，我们可以先在这个最小核心上定义语法、变量作用域、替换和计算规则，再把这些思想推广到更丰富的语言中。

Lambda 演算之于类型系统，犹如集合论之于数学：它是一个小而稳固的形式化基础。

3.1 为什么学习 Lambda 演算？

学习 Lambda 演算，主要有四个原因：

• 它是函数式编程的理论基础
• 它提供了极简但完整的计算模型
• 类型系统通常建立在某种 Lambda 演算之上
• 现代语言（如 Haskell、ML、Scala）的许多核心概念都可以追溯到这里

如果你后续要读《Types and Programming Languages》（TAPL），那几乎一定会反复遇到 Lambda 演算。
可以把它理解为：类型系统研究中的“牛顿力学模型”——现实世界远比它复杂，但许多基础原理都要先在这里建立。

3.2 语法：只有三种构造

先用一句话概括 Lambda 演算：

Lambda 演算是一门只有“变量、函数定义、函数调用”三种构造的极简语言。

你可以先把它和熟悉的语言对应起来。比如在 Python 里：

f = lambda x: x
f(3)

第一行定义了一个匿名函数，第二行调用它。
Lambda 演算做的事情完全一样，只不过它更纯粹——连数字和 + 都还没有：

λx.x

这个项读作：“一个函数，接收参数 x，返回 x 本身。”
它通常叫做恒等函数（identity function）。

3.2.1 抽象语法的定义

按照第 2 章的区分，这里更准确地说是在给出 Lambda 项的抽象语法；它常用 BNF 风格记号写成：

$$t::=x\mid \lambda x.t\mid tt$$

这表示一个项 $t$ 只能是以下三种情况之一：

1. 一个变量（variable） $x$
2. 一个抽象（abstraction） $\lambda x.t$
3. 一个应用（application） $tt$

其中：

• $x$ 表示变量名
• $\lambda x.t$ 表示“参数为 $x$、函数体为 $t$ 的函数”
• $t_1{t}_2$ 表示“把函数 $t_1$ 应用于参数 $t_2$”

通常我们默认变量名来自一个可数无限集合，例如 $x,y,z,x_1,x_2,\dots$。
这样做的好处是：当后面需要“换一个没用过的新变量名”时，总能找到一个。

3.2.2 三种构造的直观含义

例如：

• $\lambda x.x$：恒等函数
• $\lambda x.\lambda y.x$：接收两个参数，返回第一个
• $\lambda f.\lambda x.fx$：接收函数 f 和参数 x，把 f 应用于 x

3.2.3 括号与书写约定

上面的核心语法里没有把括号写进 BNF，但在实际书写时我们会大量使用括号来消除歧义。这里的括号只是元语言中的辅助记法，不是在给 Lambda 演算增加新的核心构造。

有两个非常重要的约定：

• 应用左结合：
  $stu$ 读作 $((st)u)$
• 抽象体尽量向右延伸：
  $\lambda x.\lambda y.xyx$ 读作 $\lambda x.(\lambda y.((xy)x))$

因此：

• $abc$ 表示 ((a b) c)
• $\lambda x.xyz$ 表示 λx.((x y) z)
• $\lambda x.x(\lambda y.y)$ 表示 “一个函数，其函数体是 x (λy.y)”

如果没有这些约定，很多式子都会变得难以阅读。

3.2.4 一些基本例子

λx.x
λx.λy.x
λx.λy.y
λf.λx.f (f x)

它们分别表示：

• λx.x：恒等函数 I
• λx.λy.x：返回第一个参数的函数 K
• λx.λy.y：返回第二个参数
• λf.λx.f (f x)：把函数 f 连用两次

对应到熟悉的语言中，大致可以写成：

fun x -> x
fun x -> fun y -> x

lambda x: x
lambda x: (lambda y: x)

3.2.5 与抽象语法树（AST）的关系

按照第 2 章的思路，这里的三种抽象语法构造分别对应三类 AST 节点。因此 Lambda 演算的 AST 只有三种节点：

• 变量节点
• 抽象节点
• 应用节点

例如项 $\lambda x.xy$ 的抽象语法结构可以画成：

λx.
  └── @
      ├── x
      └── y

这里的 @ 只是图示中的一个记号，表示“应用节点”，不是 Lambda 演算本身的语法符号。

3.3 变量、作用域与自由变量

变量是 Lambda 演算里最微妙的部分。
真正困难的地方不是“函数定义”本身，而是：一个变量出现时，到底是被哪个 λ 绑定的？

3.3.1 绑定变量与自由变量

在项 $\lambda x.t$ 中：

• λx 引入一个绑定
• 函数体 $t$ 中由这个 λ 管辖的那些 x，叫做绑定变量出现（bound occurrence）
• 若一个变量出现不受任何 λ 绑定，它就是自由变量（free variable）
• 这个绑定生效的语法范围，叫做作用域（scope）

例如：

• 在 $\lambda x.x$ 中，x 是绑定的
• 在 $\lambda x.xy$ 中，x 是绑定的，y 是自由的
• 在 $xy$ 中，x 和 y 都是自由的

可以把自由变量理解成“依赖外部环境的名字”。

3.3.2 自由变量集合的递归定义

我们用 $FV(t)$ 表示项 $t$ 的自由变量集合。这个记号也收录在附录A与附录B中。定义如下：

$$FV(x)=\{x\}$$

$$FV(\lambda x.t)=FV(t)\setminus \{x\}$$

$$FV(t_1{t}_2)=FV(t_1)\cup FV(t_2)$$

这三条规则非常自然：

• 一个单独的变量 x，它的自由变量就是自己
• 在 λx.t 里，x 被绑定了，所以要从 FV(t) 中删掉
• 在应用 t1 t2 中，自由变量来自左右两个子项的并集

3.3.3 例子

我们来逐步计算最后一个：

$$FV(\lambda x.\lambda y.xyz)$$

先根据抽象规则：

$$FV(\lambda x.\lambda y.xyz)=FV(\lambda y.xyz)\setminus \{x\}$$

再计算内层：

$$FV(\lambda y.xyz)=FV(xyz)\setminus \{y\}$$

由于应用左结合，$xyz$ 就是 $((xy)z)$，所以它的自由变量是：

$$FV(xyz)=\{x,y,z\}$$

因此：

$$FV(\lambda y.xyz)=\{x,y,z\}\setminus \{y\}=\{x,z\}$$

最后：

$$FV(\lambda x.\lambda y.xyz)=\{x,z\}\setminus \{x\}=\{z\}$$

3.3.4 封闭项

如果一个项没有任何自由变量，就称它是封闭项（closed term）。

例如：

• $I=\lambda x.x$
• $K=\lambda x.\lambda y.x$
• $S=\lambda x.\lambda y.\lambda z.xz(yz)$

这些都是封闭项。

有些文献也会把没有自由变量的 Lambda 项叫做组合子（combinator），尤其在讨论 S、K、I 等经典例子时更常见。不过在初学阶段，记住“封闭项 = 没有自由变量的项”就足够了；后面若无特别说明，本教程优先使用“封闭项”这一说法。

3.4 α-等价：绑定变量名不重要

接下来要处理一个关键问题：
如果我把函数参数名从 x 改成 y，函数还是不是原来的那个函数？

直觉上当然是。比如下面两个 Python 函数，参数名不同，但行为一样：

def f(x): return x
def g(y): return y

在 Lambda 演算里，这种“只改了绑定变量名字、不改含义”的关系叫做 α-等价（alpha-equivalence）。

3.4.1 基本思想

例如：

• $\lambda x.x$
• $\lambda y.y$
• $\lambda z.z$

这三个项的含义完全一样，因此它们 α-等价：

$$\lambda x.x{\equiv }_{\alpha }\lambda y.y{\equiv }_{\alpha }\lambda z.z$$

再比如：

$$\lambda x.\lambda y.xy{\equiv }_{\alpha }\lambda a.\lambda b.ab$$

这里改的只是绑定变量名；变量之间的绑定关系没有变，所以意义也没有变。

3.4.2 什么样的改名才是合法的？

并不是随便改名都可以。改名必须保持原来的绑定结构，并且不能引发变量捕获。

例如：

• $\lambda x.y$ 可以改成 $\lambda z.y$
• 但不能把它改成某个会让原本自由变量变成绑定变量的形式

更准确地说：

α-等价允许我们把某个抽象 λx.t 中由这个 λ 绑定的 x，统一改成一个新的变量名 y，前提是这个改名不会改变自由变量和绑定变量的结构。

这件事通常叫做 α-重命名 或 α-转换。

3.4.3 为什么 α-等价重要？

因为后面定义替换时，我们会遇到“变量捕获”问题。
而 α-转换正是避免变量捕获的关键工具：

• 如果一个替换会导致捕获
• 那就先把冲突的绑定变量改名
• 再进行替换

所以你可以把 α-等价理解为：

“绑定变量的名字只是局部占位符，真正重要的是绑定结构，而不是字面上的名字。”

在形式化处理中，通常会把 α-等价的项视为“同一个项的不同写法”。

如果你读到这里时，已经对“绑定变量 / 自由变量 / α-等价”的关系有些混淆，建议先回看附录A中的对应条目，再继续读替换。

3.5 替换：把参数代入函数体

替换（substitution）是 Lambda 演算最重要的操作之一。
直观上，它就是“把一个项代入另一个项里的某个变量位置”。

我们记：

$$[x\mapsto s]t$$

表示：把项 $t$ 中自由出现的 x 替换成项 $s$。

之所以强调“自由出现”，是因为被 λx 绑定住的那些 x，并不表示外部那个变量，不能替换。后面真正需要的，是避免捕获的替换（capture-avoiding substitution）。

3.5.1 直觉：替换就是“代入”

先用普通算术式来理解：

• 把 x 换成 3：x + 1 变成 3 + 1
• 把 x 换成 3：y + 1 不变，因为里面没有 x
• 把 x 换成 3：x + y 变成 3 + y

Lambda 演算里的替换本质上也是一样的。

最简单的两条规则是：

$$[x\mapsto s]x=s$$

$$[x\mapsto s]y=y(y\ne x)$$

也就是：

• 遇到目标变量 x，就换成 s
• 遇到别的变量，就保持不变

对于应用项，递归处理左右两边：

$$[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$$

到这里为止，一切都很自然。

3.5.2 关键难点：变量捕获

问题出在抽象上。

考虑这个替换：

$$[x\mapsto y](\lambda y.x)$$

如果“无脑替换”，你可能会得到：

$$\lambda y.y$$

但这其实是错的。

为什么？
原来的 $\lambda y.x$ 表示：“接收一个参数 y，但不返回它，而是返回外部的 x。”
这里的 x 是自由变量。

如果把 x 直接换成 y，变成 $\lambda y.y$，那这个 y 就不再是“外部的 y”，而是被 λy 绑定住的参数了。也就是说：

• 原本自由的 y
• 被新的 λy 意外“吃掉”了
• 含义彻底改变

这种现象就叫做变量捕获（variable capture）。

可以把它和自然语言中的误解类比：

• 原句：“把张三的电话告诉我”
• 错听成：“把你的电话告诉我”

只是因为同一个词碰巧重名，意思就变了。

3.5.3 抽象的三种情况

为了避免变量捕获，抽象项的替换必须分情况讨论。

情况一：绑定变量正好就是 x

$$[x\mapsto s](\lambda x.t)=\lambda x.t$$

因为这个 λx 已经把函数体里的 x 绑定住了。
替换只作用于自由出现的 x，而这里这些 x 都不是自由的，所以什么都不做。

情况二：绑定变量不是 x，而且不会捕获

如果 $y\ne x$，并且 $y\notin FV(s)$，那么可以安全地往里替换：

$$[x\mapsto s](\lambda y.t)=\lambda y.[x\mapsto s]t$$

这里的条件 $y\notin FV(s)$ 非常重要。
它保证了：当我们把 s 放进 t 里时，s 中的自由变量 y 不会被外面的 λy 捕获。

情况三：绑定变量不是 x，但会发生捕获

如果 $y\ne x$，同时 $y\in FV(s)$，那么直接替换就危险了。
这时必须先做 α-重命名，把 λy 改成一个新鲜变量 z，再继续：

$$[x\mapsto s](\lambda y.t)=\lambda z.[x\mapsto s]([y\mapsto z]t)$$

其中 z 必须是一个新鲜变量。更准确地说，它必须新鲜到足以避免新的名字冲突：至少不能与当前这一步中会产生影响的那些自由变量或已有绑定混淆。直觉上，可以把它理解为：

• 不等于当前正在讨论的绑定变量与被替换变量；
• 不出现在将要代入的项的自由变量中；
• 也不应引入新的捕获或歧义。

在实际推导里，你可以把它理解成：“选一个当前语境里没被相关部分使用过的名字”。
你不必把“新鲜”理解成“宇宙中从未出现过”，而应理解成：

对当前这一步替换来说，它足够新，因此不会改变原来的自由 / 绑定结构。

你可以把这个规则理解为：

如果将要发生“重名冲突”，先改名，再代入。

3.5.4 替换规则汇总

把前面的规则合起来，得到替换的完整定义：

$$[x\mapsto s]x=s$$

$$[x\mapsto s]y=y(y\ne x)$$

$$[x\mapsto s](t_1{t}_2)=([x\mapsto s]t_1)([x\mapsto s]t_2)$$

$$[x\mapsto s](\lambda x.t)=\lambda x.t$$

$$[x\mapsto s](\lambda y.t)=\lambda y.[x\mapsto s]t(y\ne x,y\notin FV(s))$$

$$[x\mapsto s](\lambda y.t)=\lambda z.[x\mapsto s]([y\mapsto z]t)(y\ne x,y\in FV(s),z\text{ 新鲜})$$

这六条规则共同定义了避免捕获的替换（capture-avoiding substitution）。

这一套规则会在下一章立刻进入中心位置，因为 β-归约的本质就是避免捕获的替换。
如果你觉得这里已经有些抽象，不必急着一次把每个边角都记死；先抓住下面这条主线即可：

自由变量决定一个项依赖什么外部名字，α-重命名保证绑定名字可安全改写，而替换则是在不破坏这种结构的前提下进行代入。

3.5.5 一个最重要的例子：如何避免捕获

回到前面那个危险例子：

$$[x\mapsto y](\lambda y.x)$$

由于替换项 y 的自由变量集合是：

$$FV(y)=\{y\}$$

而抽象绑定的也是 y，所以直接替换会发生捕获。
因此必须先做 α-重命名，把 λy 改成 λz：

$$\lambda y.x{\equiv }_{\alpha }\lambda z.x$$

然后再替换：

$$[x\mapsto y](\lambda z.x)=\lambda z.y$$

最终结果是：

$$[x\mapsto y](\lambda y.x)=\lambda z.y$$

这个结果才是正确的。它表示：“接收一个参数 z，返回外部的 y。”

对照一下：

• 错误结果：$\lambda y.y$ —— 恒等函数
• 正确结果：$\lambda z.y$ —— 常函数，返回外部 y

两者含义完全不同。

3.5.6 完整计算示例

下面计算：

$$[x\mapsto \lambda z.z](\lambda y.xy)$$

第一步：判断外层抽象是否安全

外层是 $\lambda y.(xy)$。
替换项是 $s=\lambda z.z$。

先算它的自由变量：

$$FV(\lambda z.z)=\varnothing$$

因为 $y\notin FV(s)$，所以属于“不会捕获”的安全情况，可以直接进入函数体：

$$[x\mapsto \lambda z.z](\lambda y.xy)=\lambda y.[x\mapsto \lambda z.z](xy)$$

第二步：处理应用项

$$[x\mapsto \lambda z.z](xy)=([x\mapsto \lambda z.z]x)([x\mapsto \lambda z.z]y)$$

第三步：处理变量

$$[x\mapsto \lambda z.z]x=\lambda z.z$$

$$[x\mapsto \lambda z.z]y=y$$

所以：

$$[x\mapsto \lambda z.z](xy)=(\lambda z.z)y$$

代回去得到：

$$[x\mapsto \lambda z.z](\lambda y.xy)=\lambda y.(\lambda z.z)y$$

这就是最终结果。

3.5.7 替换为什么这么重要？

因为 Lambda 演算的核心计算规则——β-归约（beta-reduction）——本质上就是：

函数应用时，把实参代入函数体

形式上，下一章我们会看到类似这样的规则：

$$((\lambda x.t)s)⟶[x\mapsto s]t$$

所以本章认真定义替换，并不是为了形式化而形式化，而是在为“函数如何计算”打基础。

3.6 本章小结

到这里，我们已经建立了 Lambda 演算最关键的静态基础。

这一章中，不同概念各自回答了不同的问题：

• 语法：什么样的式子是合法的 Lambda 项？
• 作用域与自由变量：一个变量出现时，它依赖外部环境，还是被某个 λ 绑定？
• α-等价：如果只改绑定变量名，项的意义是否不变？
• 替换：把一个项代入另一个项时，如何避免变量捕获？

如果把这一章和下一章联系起来，可以这样理解：

• 本章解决“式子长什么样，以及变量是什么意思”
• 下一章解决“式子如何计算”

也就是说，本章是静态结构，下一章将进入动态行为。

回看导航

如果你读完本章后，觉得“概念大致懂了，但一动手就容易乱”，建议按下面顺序回看：

1. 先回看本章正文中的三个核心主线

   • 项的抽象语法只有三种构造：变量、抽象、应用；
   • 自由变量与绑定变量决定名字在项中的语义角色；
   • α-等价与避免捕获的替换，为后面的 β-归约奠定基础。

2. 再查附录A《术语表》

   • 重点回看：
     • 项
     • 自由变量 / 绑定变量
     • α-等价
     • 替换
     • 新鲜变量
     • 变量捕获

3. 再查附录B《符号速查表》

   • 重点回看：
     • FV(t)
     • [x \mapsto s]t
     • \equiv_\alpha
     • \lambda x.t
     • t_1\ t_2

4. 最后再做本章练习

   • 如果自由变量集合和替换还能独立算出来，就说明这一章已经真正站稳了；
   • 如果一到替换就混乱，通常不是“不会算”，而是“自由 / 绑定结构还没完全内化”。

本章练习

1. 书写 Lambda 项
   用 Lambda 演算写出下列函数：

   • 接收参数 $x$，返回 $x$ 的函数
   • 接收参数 $x$，返回一个接收 $y$ 并返回 $y$ 的函数
   • 接收参数 $f$ 和 $x$，将 $f$ 应用于 $x$ 的函数

2. 分析自由变量
   计算以下项的自由变量集合：

   • $\lambda x.xyz$
   • $(\lambda x.x)y$
   • $\lambda x.\lambda y.xz$

3. 判断是否 α-等价
   判断下列各对项是否 α-等价，并说明理由：

   • $\lambda x.x$ 与 $\lambda y.y$
   • $\lambda x.\lambda y.x$ 与 $\lambda a.\lambda b.a$
   • $\lambda x.y$ 与 $\lambda y.y$

4. 替换练习
   计算下列替换，并写出每一步依据的规则：

   • $[x\mapsto y](\lambda z.xz)$
   • $[x\mapsto y](\lambda y.x)$
   • $[x\mapsto \lambda z.zw](\lambda y.xy)$，其中 $w$ 是自由变量

5. 理解捕获问题
   解释为什么下面这个“无脑替换”是错误的： $$[x\mapsto y](\lambda y.x)=\lambda y.y$$ 并给出正确结果。

在下一章，我们将正式引入 β-归约，看到 Lambda 演算如何真正“跑起来”。