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

附录E：Church 编码（进阶选读）

本附录适合在读完第 3 章和第 4 章之后阅读。它不是理解后续类型系统章节的前置条件，但非常适合用来体会一个重要事实：
即使语言极端简化到只剩变量、抽象和应用，也仍然能够表示我们熟悉的数据与计算。

同时，这一附录也可以和第 6 章“一阶类型系统：基本类型构造”对照着看：
第 6 章把 Bool、Nat、if 等构造当作语言的原生部分来引入，是为了让类型规则与类型安全主线更清楚；而本附录展示的是：即使不把这些构造当作原生语法，未类型化 Lambda 演算也仍然可以通过编码方式表示出相应行为。

在前面的章节里，我们一直强调 Lambda 演算的“极简”：

• 没有内置数字
• 没有内置布尔值
• 没有内置 if
• 没有内置列表、元组、树

这时一个自然问题就出现了：

如果什么都没有，Lambda 演算到底拿什么来“编程”？

Church 编码（Church encoding）给出的答案是：

用函数来表示数据。

也就是说，我们不再把“布尔值”“数字”“数据结构”看成语言的原始成分，而是把它们都编码成某种 Lambda 项。

这件事之所以重要，不是因为实际编程语言真的会让你手写这些编码，而是因为它展示了 Lambda 演算的表达能力：
即使语法极度贫瘠，只要函数和应用还在，很多看似“必须内置”的概念都可以被表示出来。

E.1 为什么布尔值可以编码成函数？

先从最简单的对象开始：布尔值。

如果你仔细想想，布尔值最核心的用途是什么？
不是“它长得像 true 或 false 这两个单词”，而是：

它能帮助我们在两个分支之间做选择。

例如：

• if true then a else b 的结果是 a
• if false then a else b 的结果是 b

所以，从行为角度看：

• true 就是“选第一个”
• false 就是“选第二个”

而“从两个候选里选一个”这件事，本来就可以用函数表达。

E.2 Church 布尔值

按照上面的想法，我们定义：

$$\begin{array}{rl}\mathbf{true}& =\lambda t.\lambda f.t\\ \mathbf{false}& =\lambda t.\lambda f.f\end{array}$$

这两个定义的行为分别是：

• true 接收两个参数，返回第一个
• false 接收两个参数，返回第二个

这和“真假控制分支”的直觉完全一致。

E.2.1 条件表达式

既然 true 和 false 已经能“选分支”，那么条件表达式也可以编码为：

$$\mathbf{if}=\lambda b.\lambda x.\lambda y.bxy$$

它的含义是：

• 先给一个布尔值 b
• 再给两个候选 x 和 y
• 然后让 b 决定选哪一个

也就是说，if 不再是语言内置语法，而只是一个普通函数。

不过这里必须立刻补一个重要边界：

Church 编码里的布尔值与 if，最自然地表现为“分支选择行为”；但它并不自动等同于现实严格语言里的原生条件表达式。

原因是：
在第四章讨论过的不同求值策略下，编码后的 if 行为会有差异。

• 在更接近传名调用 / 正规序的语境里，b x y 的“先选哪一支、再继续算那一支”的直觉最自然；
• 但在传值调用语境里，若把 x 和 y 都当作普通实参传入，那么它们往往会在进入 b x y 之前就先被求值；
• 这样一来，Church 编码得到的 if 就不再像很多语言内置的条件语句那样，天然具有“只计算被选中分支”的效果。

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

Church 布尔值准确编码的是“二选一的控制接口”；至于它在某种求值策略下是否表现得像原生条件语句，还要结合具体求值规则一起看。

E.3 一个完整演算：为什么 if true a b 会得到 a？

我们来验证：

$$\mathbf{if}\mathbf{true}ab{⟶}^{\ast }a$$

把定义展开：

$$\begin{array}{rl}\mathbf{if}\mathbf{true}ab& =(\lambda b.\lambda x.\lambda y.bxy)(\lambda t.\lambda f.t)ab\\ & ⟶(\lambda x.\lambda y.(\lambda t.\lambda f.t)xy)ab\\ & ⟶(\lambda y.(\lambda t.\lambda f.t)ay)b\\ & ⟶(\lambda t.\lambda f.t)ab\\ & ⟶(\lambda f.a)b\\ & ⟶a\end{array}$$

同理：

$$\mathbf{if}\mathbf{false}ab{⟶}^{\ast }b$$

所以，这套编码确实实现了“真假控制分支”。

E.3.1 这里真正发生了什么？

从表面上看，我们好像“发明了布尔值”。
但更准确地说，我们做的是：

• 不再把布尔值当成“某种原始数据”
• 而是只保留它最核心的行为
• 再用函数把这种行为表示出来

这就是 Church 编码的基本精神：

数据不由“长相”定义，而由“可观察行为”定义。

E.4 为什么自然数也可以编码成函数？

接下来是数字。

布尔值的关键行为是“二选一”；
而自然数的关键行为是什么？

一种很自然的答案是：

一个自然数表示“把某个操作重复多少次”。

例如：

• 0：做 0 次
• 1：做 1 次
• 2：做 2 次
• 3：做 3 次

这个想法非常适合函数编码，因为“重复应用某个函数若干次”本来就是高阶函数能表达的事情。

E.5 Church 数

据此，我们定义：

$$\begin{array}{rl}{c}_0& =\lambda f.\lambda x.x\\ c_1& =\lambda f.\lambda x.fx\\ c_2& =\lambda f.\lambda x.f(fx)\\ c_3& =\lambda f.\lambda x.f(f(fx))\end{array}$$

一般地：

$$c_n=\lambda f.\lambda x.\underset{n\text{ 次}}{\underbrace{f(f(\cdots (f}}x)\cdots ))$$

它们的含义是：

• c0：把 f 作用 0 次，直接返回 x
• c1：把 f 作用 1 次
• c2：把 f 作用 2 次
• c3：把 f 作用 3 次

所以 Church 数并不是“看起来像数字的值”，而是：

一个接收函数 f 和初始值 x，并把 f 重复应用若干次的高阶函数。

E.6 一个直觉例子：c_2 为什么像 2？

来看：

$$c_2=\lambda f.\lambda x.f(fx)$$

如果你给它一个函数 f 和一个起点 x，它会产生：

$$f(f(x))$$

也就是“做两次 f”。

因此，c_2 并不是“符号 2 的替身”，而是“二次迭代器”。

这就是 Church 数最应该记住的直觉：

自然数被编码成“迭代次数”。

E.7 后继函数：如何把 n 变成 n+1？

如果一个 Church 数表示“重复应用 $n$ 次”，那么“后继”最自然的定义就是：

先做原来的 $n$ 次，再额外做一次。

因此定义：

$$\mathbf{succ}=\lambda n.\lambda f.\lambda x.f(nfx)$$

它的含义非常直观：

• n f x 先做 n 次 f
• 外面再套一个 f
• 总共就做了 n+1 次

E.7.1 验证 succ c_1 = c_2

我们来算：

$$\begin{array}{rl}\mathbf{succ}{c}_1& =(\lambda n.\lambda f.\lambda x.f(nfx))c_1\\ & ⟶\lambda f.\lambda x.f(c_{1}fx)\end{array}$$

再展开 c_1 = \lambda f.\lambda x.f x：

$$\begin{array}{rl}\lambda f.\lambda x.f(c_{1}fx)& ⟶\lambda f.\lambda x.f(fx)\end{array}$$

这正是 c_2。

E.8 加法：为什么“先做 n 次，再做 m 次”就是加法？

如果数字表示“重复应用次数”，那么：

• m + n 就应该表示：
• 先做 n 次
• 再做 m 次

因此定义：

$$\mathbf{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$$

读法是：

1. 先计算 n f x
2. 再把 f 额外做 m 次

总计就是 m+n 次。

E.8.1 例子：plus c_1 c_2

展开：

$$\begin{array}{rl}\mathbf{plus}{c}_1{c}_2& =(\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx))c_1{c}_2\\ & ⟶\lambda f.\lambda x.c_{1}f(c_{2}fx)\end{array}$$

而：

• c_2 f x = f(f x)
• c_1 f y = f y

所以整体变成：

$$\lambda f.\lambda x.f(f(fx))$$

这正是 c_3。

E.9 乘法：为什么“n 次地做 m 次”就是乘法？

如果一个数字表示“迭代”，那么乘法自然可以理解成：

把“做 $n$ 次”这个过程本身，再重复做 $m$ 次。

因此定义：

$$\mathbf{times}=\lambda m.\lambda n.\lambda f.m(nf)$$

直觉是：

• n f 是“做 n 次 f”的新函数
• 然后 m (n f) 表示“把这个 n 次迭代器再做 m 次”
• 总效果就是 m \times n 次

这一定义初看有点抽象，但一旦抓住“Church 数 = 迭代器”的核心，乘法就会自然很多。

E.10 Church 编码真正展示了什么？

到这里为止，我们已经看到：

• 布尔值可以编码成函数
• 条件表达式可以编码成函数
• 自然数可以编码成高阶函数
• 后继、加法、乘法也都可以定义出来

这说明了一个重要事实：

许多你以为必须由语言原生提供的数据和操作，其实都可以由函数组织出来。

这并不意味着真实语言不该提供数字和布尔值。
真实语言当然应该内置这些东西，因为：

• 更高效
• 更直观
• 更适合工程实现

Church 编码的意义不在于“替代真实语言实现”，而在于展示：

1. Lambda 演算的表达能力极强；
2. “数据”与“行为”之间可以有非常深的联系；
3. 极简语言依然可以成为严肃的计算模型。

如果把它和第 6 章放在一起看，可以更清楚地理解两种写法的分工：

• 第 6 章的写法是：把 Bool、Nat、和类型等当作语言原生构造，以便直接讨论类型规则与类型安全；
• 本附录的写法是：退回到更极简的未类型化 Lambda 演算，只保留函数与应用，再展示这些“看似必须内建”的对象其实也能被编码出来。

因此，这两部分不是互相冲突，而是分别服务于两条不同目标：

• 正文主线强调：怎样建立清楚、可证明的类型系统骨架；
• 本附录强调：极简计算模型本身具有多强的表达能力。

E.11 Church 编码的边界

看到这里，也要避免把结论说得太满。

更稳妥的说法是：

• 在适当编码下，未类型化 Lambda 演算可以表示许多熟悉的数据和计算过程；
• 这与它作为通用计算模型的地位一致；
• 但“能表示”不等于“适合实际工程实现”。

此外，Church 编码在不同求值策略下的行为细节也可能不同；某些编码在理论上很优雅，但在实际求值时未必高效。
特别是前面提到的 Church 布尔值与编码后的 if：它们在“分支选择”意义上非常清楚，但在严格求值语言里，并不应直接被理解成对原生条件表达式的逐字替代。

所以更好的理解方式是：

Church 编码是一种理论展示：它说明函数足以承担比你第一眼想象更多的表达任务。

E.12 本附录小结

这一附录最重要的内容只有三点：

1. 布尔值可以看作“在两个候选中选一个”的函数

   • true 选第一个
   • false 选第二个

2. 自然数可以看作“重复应用多少次”的迭代器

   • 0 是做 0 次
   • 1 是做 1 次
   • 2 是做 2 次
   • 以此类推

3. 一旦接受“数据由行为定义”这个视角，许多熟悉的数据结构都可以编码成函数

   • 布尔值
   • 数字
   • 条件表达式
   • 算术运算

如果把这一附录压缩成一句话，那就是：

Church 编码告诉我们：在 Lambda 演算里，函数不仅能表示计算过程，也能表示数据本身。

练习

1. 验证： $$\mathbf{if}\mathbf{false}ab{⟶}^{\ast }b$$

2. 验证： $$\mathbf{succ}{c}_2{⟶}^{\ast }{c}_3$$

3. 用自然语言解释为什么： $$\mathbf{plus}=\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$$ 确实表示加法。

4. 试着说明为什么 Church 数最自然的直觉不是“数字长什么样”，而是“它让某个操作重复多少次”。