第2章：无类型 lambda 演算（计算的基础）The Untyped Lambda Calculus — Foundations of Computation

一、导读

1.1 学习目标

本章深入探讨无类型 lambda 演算，这是研究编程语言语义和类型系统的数学基础。通过本章的学习，读者将达成以下目标：

掌握 lambda 项的语法定义和三种基本构造形式
理解 alpha 等价和自由变量/约束变量的概念
熟练掌握 beta 归约规则及其不同归约策略
掌握 Church 编码技术，能用纯 lambda 项表示数据和逻辑运算
理解不动点组合子的原理及其在递归中的作用
认识 lambda 演算作为图灵完备计算模型的意义

1.2 重要性

无类型 lambda 演算是 Alonzo Church 在 1932 年提出的形式系统，其初衷是为数学和逻辑学提供一个基础框架。虽然 Church 最初的系统因为不一致性而被放弃，但 lambda 演算的核心思想——用函数抽象和应用来描述计算——被证明是极其深刻的。

lambda 演算与 Turing 机是等价的计算模型，两者都能表达所有可计算函数（Church-Turing 论题）。然而，lambda 演算的语法更加简洁优雅：整个系统只需要三种语法构造——变量、抽象和应用。这种极简性使得 lambda 演算成为研究计算本质的理想工具，也是理解类型系统的前提。

现代函数式编程语言（Lisp、ML、Haskell）的核心语义都直接源自 lambda 演算。理解 lambda 演算有助于我们深入认识函数调用的本质、变量绑定的语义、以及求值策略的选择对程序行为的影响。

1.3 核心问题

仅用函数抽象和应用能否表达所有计算？
在没有数据类型的情况下，如何表示数字、布尔值和数据结构？
在没有显式递归机制的情况下，如何实现递归计算？
lambda 演算的归约是否总会终止？如果不终止，我们如何理解这种非终止性？

二、核心概念详解

2.1 lambda 项的语法

lambda 项（lambda term）是无类型 lambda 演算的基本语法单元，由以下三条规则递归定义：

变量（Variable）：x 是一个 lambda 项，其中 x 是任意变量名

抽象（Abstraction）：如果 M 是一个 lambda 项，则 λx.M 也是一个 lambda 项，表示一个以 x 为参数的匿名函数

应用（Application）：如果 M 和 N 都是 lambda 项，则 M N 也是一个 lambda 项，表示将函数 M 应用于参数 N

这三种简单的构造足以表达任何可计算的函数。例如，恒等函数表示为 λx.x，它接受一个参数并原样返回。应用结合性约定为左结合，即 M N P 表示 (M N) P。抽象的作用域向右延伸到末尾，即 λx.λy.x y 表示 λx.(λy.(x y))。

2.2 alpha 等价与替换

自由变量与约束变量：在 lambda 项 λx.M 中，变量 x 在 M 中是约束的（bound），而出现在 M 中但不在任何包含它的抽象中的变量是自由的（free）。例如在 λx.x y 中，x 是约束变量，y 是自由变量。自由变量的集合 FV(M) 递归定义为：FV(x) = {x}，FV(λx.M) = FV(M) \ {x}，FV(M N) = FV(M) ∪ FV(N)。

alpha 等价：两个 lambda 项如果仅在约束变量的名称上不同，则它们是 alpha 等价的。例如 λx.x 和 λy.y 是 alpha 等价的，都表示恒等函数。形式化地，λx.M alpha 等价于 λy.M[y/x]，前提是 y 不在 M 中自由出现。alpha 等价提醒我们：变量的名称不重要，重要的是变量的绑定结构。

替换操作：替换 M[x := N] 表示将 M 中所有自由出现的 x 替换为 N。替换操作需要小心处理变量捕获（variable capture）问题。例如 (λy.x y)[x := λz.z] 应该得到 λy.(λz.z) y，而不是让 z 被外层的 λy 捕获。为避免捕获，必要时需要对约束变量进行 alpha 重命名。

2.3 beta 归约

beta 归约是 lambda 演算的核心计算规则。它描述了函数应用的意义：将函数 λx.M 应用于参数 N 的结果是将 M 中所有自由出现的 x 替换为 N，记为 (λx.M) N →β M[x := N]。

例如，(λx.x + 1) 2 →β 2 + 1 = 3（这里借用算术符号辅助理解）。在纯 lambda 演算中，(λx.λy.x) a b →β (λy.a) b →β a，这个项总是返回第一个参数，丢弃第二个参数。

归约策略的选择对计算行为有重要影响：

正规序（Normal Order）：优先归约最左最外层的 redex。如果存在范式（不可再归约的项），正规序一定能找到它（标准性定理）。
应用序（Applicative Order）：优先归约最左最内层的 redex，即先计算参数再应用函数。这是大多数编程语言的求值策略（严格求值）。
惰性求值（Lazy Evaluation）：Haskell 采用的策略，只在需要时才计算参数，且每个参数最多计算一次（通过记忆化）。

应用序可能陷入无限循环而正规序能找到范式。例如 (λx.y) ((λx.x x)(λx.x x))，应用序会先计算参数导致无限循环，而正规序直接归约得到 y。

2.4 Church 编码

Church 编码展示了如何用纯 lambda 项表示所有数据和逻辑运算。这是 lambda 演算作为通用计算模型的关键证据。

Church 布尔值：true = λx.λy.x（选择第一个），false = λx.λy.y（选择第二个）。条件语句 if b then M else N 编码为 b M N。当 b 为 true 时，选择 M；当 b 为 false 时，选择 N。逻辑运算如 and = λp.λq.p q p，or = λp.λq.p p q，not = λp.λx.λy.p y x。

Church 自然数：自然数 n 编码为将函数 f 应用 n 次的高阶函数。zero = λf.λx.x，one = λf.λx.f x，two = λf.λx.f (f x)，three = λf.λx.f (f (f x))。后继函数 succ = λn.λf.λx.f (n f x)，加法 plus = λm.λn.λf.λx.m f (n f x)，乘法 mult = λm.λn.λf.m (n f)。

Church 序对：pair = λx.λy.λf.f x y，fst = λp.p (λx.λy.x)，snd = λp.p (λx.λy.y)。序对将两个值打包在一起，fst 和 snd 分别提取第一个和第二个分量。

2.5 不动点组合子与递归

在无类型 lambda 演算中没有显式的递归机制，但可以通过不动点组合子实现递归。一个函数 f 的不动点是满足 f(x) = x 的值 x。在 lambda 演算中，Y 组合子是一个神奇的项，它对任何函数 F 都能找到不动点：Y = λf.(λx.f (x x)) (λx.f (x x))。

验证：Y F = (λx.F (x x)) (λx.F (x x)) →β F ((λx.F (x x)) (λx.F (x x))) = F (Y F)。因此 Y F 是 F 的不动点。

利用 Y 组合子可以实现递归函数。例如阶乘函数：fact = Y (λf.λn.if (iszero n) 1 (mult n (f (pred n))))。展开后，每次递归调用都通过 Y 组合子的不动点性质自然产生。

另一个常用的不动点组合子是 Turing 的 Θ 组合子：Θ = (λx.λf.f (x x f)) (λx.λf.f (x x f))，它满足 Θ F →β F (Θ F)（直接归约一步即得，不需要像 Y 组合子那样需要两步）。

三、深入分析

3.1 Church-Rosser 定理

Church-Rosser 定理（也称为合流性定理或菱形性质）是 lambda 演算最重要的元定理之一。它指出：如果一个 lambda 项 M 可以通过不同的归约路径分别到达 N1 和 N2，那么一定存在一个 lambda 项 P，使得 N1 和 N2 都能归约到 P。

形式化地：如果 M →>* N1 且 M →>* N2，则存在 P 使得 N1 →>* P 且 N2 →>* P。

这个定理的直接推论是：如果一个 lambda 项有范式，那么范式是唯一的（在 alpha 等价意义下）。无论采用什么归约策略，只要最终到达范式，结果都是一样的。这为 lambda 演算的确定性语义提供了保证。

Church-Rosser 定理还意味着 beta 归约关系具有弱规范化性质：如果两个项可以互相归约到达，则它们在 beta 等价关系下是等价的。这为程序变换和优化提供了理论基础——只要变换保持 beta 等价，程序的行为就不会改变。

3.2 不可判定性与停机问题

无类型 lambda 演算的表达能力也带来了根本性的限制。Church 在 1936 年证明了 lambda 演算中的等价性问题是不可判定的：不存在通用算法能判定两个 lambda 项是否 beta 等价。

这个结果与 Turing 的停机问题等价。给定一个 lambda 项 M，判定 M 是否有范式（即对应的计算是否终止）是不可判定的。这意味着不存在通用算法能判定任意程序是否会终止。

这个不可判定性结果对类型系统的设计有深远影响。正是为了避免这种不可判定性，Church 引入了简单类型 lambda 演算——通过类型约束限制 lambda 项的构造，使得所有有类型的项都能保证终止。这揭示了类型系统的一个核心价值：通过限制表达能力来换取可判定性保证。

3.3 求值策略的语言学体现

不同的编程语言选择了不同的求值策略，这些选择直接影响了语言的语义和性能特征。

严格求值语言（如 C、Java、Python）采用应用序，在函数调用前先计算所有参数的值。优点是语义简单直观，容易推理程序的执行顺序。缺点是可能计算不需要的参数，浪费计算资源。

惰性求值语言（如 Haskell）采用正规序的优化版本（按需调用，call-by-need），只在需要时才计算参数，且通过记忆化确保每个参数最多计算一次。优点是可以处理无限数据结构、避免不必要的计算、支持更灵活的组合模式。缺点是运行时开销较大（需要维护 thunk），且难以推理程序的时空行为。

混合策略：一些语言支持混合策略。例如 Scheme 提供 delay 和 force 原语让程序员显式控制惰性求值。OCaml 默认严格求值但通过 lazy 关键字支持惰性求值。这些设计体现了求值策略在语言设计中的核心地位。

四、实践案例

4.1 案例一：用 Church 编码实现递归数据结构

让我们用 Church 编码实现一个完整的列表数据结构。列表可以用两种方式编码：

方式一：基于序对的嵌套

nil  = λz.λf.z                          -- 空列表
cons = λh.λt.λz.λf.f h (t z f)          -- 构造列表
head = λl.l (error) (λh.λt.h)           -- 取第一个元素
tail = λl.λz.λf.(l (pair nil nil)       -- 取剩余部分
           (λh.λt.pair t (cons h (snd t))))

方式二：基于 fold 的编码

nil  = λc.λn.n                          -- 空列表
cons = λh.λt.λc.λn.c h (t c n)          -- 构造列表
foldr = λf.λz.λl.l f z                  -- 折叠操作

这种 fold 编码直接对应函数式编程中的 fold 操作，展示了 Church 编码与函数式编程模式之间的深刻联系。

4.2 案例二：Y 组合子在实际语言中的应用

虽然大多数编程语言提供了原生的递归机制，但 Y 组合子的思想在实际编程中仍有体现。JavaScript 中可以用 Y 组合子实现匿名递归：

javascript

const Y = f => (x => f(v => x(x)(v)))
                   (x => f(v => x(x)(v)));

const factorial = Y(f => n => n === 0 ? 1 : n * f(n - 1));
// factorial(5) = 120

这个模式在需要匿名递归或延迟绑定时非常有用。在某些函数式编程库中，类似的技巧用于实现递归的解析器组合子、递归的流处理管道等。理解 Y 组合子有助于我们深入认识递归的本质——递归不需要语言层面的特殊支持，只需要函数抽象和应用就足够了。

五、常见误区

5.1 误区一：lambda 演算太简单，不实用

lambda 演算的语法虽然极简，但其计算能力是图灵完备的——它能表达所有可计算函数。所有的编程语言特性（条件分支、循环、递归、数据结构）都可以在 lambda 演算中编码。lambda 演算的价值不在于直接使用，而在于它揭示了计算的本质结构。

5.2 误区二：归约策略不影响最终结果

虽然 Church-Rosser 定理保证了范式的唯一性，但不同的归约策略可能导致完全不同的计算行为。应用序可能不终止而正规序能终止；不同的策略可能导致截然不同的计算路径和中间步骤。在实际语言实现中，选择求值策略是一个关键的设计决策。

5.3 误区三：Church 编码只是理论玩具

Church 编码不仅是理论工具，它直接影响了函数式编程的实践。fold 操作、continuation-passing style（CPS）变换、build/fold 融合优化等技术都源自 Church 编码的思想。理解 Church 编码有助于写出更优雅、更组合化的函数式程序。

5.4 误区四：变量名称不重要，所以可以随意命名

虽然 alpha 等价告诉我们约束变量的名称不影响语义，但在实际编写和阅读 lambda 项时，选择合适的变量名对于可读性至关重要。此外，替换操作中的变量捕获问题提醒我们：变量名称在避免冲突方面仍然扮演着重要角色。

六、本章小结

本章系统讲解了无类型 lambda 演算的基本概念和核心机制。lambda 项通过变量、抽象和应用三种简单构造表达了完整的计算能力，证明了极简语法也能实现图灵完备的计算。beta 归约规则定义了函数应用的语义，Church-Rosser 定理保证了归约结果的一致性。

Church 编码技术展示了如何用纯函数表示所有数据和逻辑运算——布尔值、自然数、序对、列表都可以编码为高阶函数。不动点组合子（Y 组合子）为递归提供了理论支持，证明了即使没有显式递归机制，lambda 演算也能实现任意递归计算。

然而，无类型 lambda 演算的不可判定性也暴露了无约束计算的局限。这为下一章引入类型系统埋下了伏笔：通过类型约束，我们既能保持计算的表达能力，又能获得终止性保证和类型安全保障。理解 lambda 演算的这些基础知识，是深入理解类型系统本质的必要前提。

七、思考题

请用 Church 编码写出前驱函数 pred，使得 pred n 归约到 n-1（当 n > 0 时）。提示：可以利用序对来追踪相邻的两个数。

证明 Y 组合子确实是任意函数 F 的不动点，即展示 Y F →β F (Y F) 的完整归约过程。

考虑 lambda 项 Ω = (λx.x x)(λx.x x)，它没有范式。请解释为什么应用序和正规序都无法使 Ω 终止。

请用 Church 编码实现一个判断自然数是否为零的函数 iszero，并验证 iszero zero →β true 且 iszero one →β false。

思考题：如果我们在 lambda 演算中加入一个不动点组合子 Y 作为原语，这对类型系统的设计有什么影响？为什么简单类型 lambda 演算不能包含 Y 组合子？