开始之前：如何使用本教程

本教程面向这样一类读者：你已经写过一些程序，知道变量、函数、条件分支这些基本概念，但还没有系统学习过编程语言理论和类型系统。如果你读过一些函数式编程资料，或者听说过 Lambda 演算（Lambda Calculus）、类型推断（type inference）、子类型（subtyping）、线性类型（linear type）这些词，却总觉得概念零散、彼此之间缺少一条主线，那么这份教程就是为你准备的。

本教程的目标不是把所有高级主题一次讲完，而是建立一条适合自学的入门路径：

• 先学会用形式化的方式描述语言；
• 再理解 Lambda 演算这个最小计算模型；
• 然后在这个基础上引入类型系统；
• 最后逐步扩展到多态、子类型、类型推断和子结构类型等主题。

主要参考材料是：

• Benjamin C. Pierce，《Types and Programming Languages》（TAPL）
• Luca Cardelli，《Type Systems》
• Pierce 编，《Advanced Topics in Types and Programming Languages》（ATAPL）的相关章节

不过，这份教程并不是这些材料的逐章翻译或摘抄，而是按“先建立直觉，再进入形式化”的思路重新组织的学习材料。

本教程与参考材料的关系

为了帮助你建立稳定主线，本教程对参考材料做了有意识的重组，而不是按原书目录逐章平移：

• 第 0–6 章主要围绕 TAPL 前半部分的核心路线展开，并吸收 Cardelli 对“类型系统是什么、它在防什么错误”的经典表述；
• 第 7–10 章继续引入多态、子类型、类型推断和子结构类型系统，但目标仍然是建立可自学的整体框架，而不是完整覆盖 TAPL、ATAPL 或 PFPL 的全部技术细节；
• 附录部分则承担三类任务：
  • 统一术语与记号；
  • 提供自检与学习建议；
  • 展示若干值得了解、但不必作为正文前置条件的进阶主题。

因此，更准确地说，本教程是：

以经典教材为基础、按“语法 → 语义 → 类型 → 元理论”主线重新组织的一份入门教程。

你需要具备哪些基础？

编程基础

最低要求并不高。你只需要：

• 用过任意一门编程语言；
• 能看懂简单的函数定义和函数调用；
• 知道什么是变量、返回值、条件分支。

如果你完全没有编程经验，建议先补一个非常基础的入门教程。Python、JavaScript、TypeScript、Java、C、OCaml 都可以，语言本身并不重要，重要的是你对“函数接受输入并产生输出”这件事已经不陌生。

数学基础

本教程主要依赖离散数学里最基础的部分：

• 集合
• 函数
• 命题逻辑中的“且 / 或 / 蕴含”
• 简单的归纳法

不要求你先学完高等数学，也不要求你有逻辑学背景。第一章会把后续真正要用到的数学工具重新梳理一遍。

建议怎样阅读本教程？

本教程大致分成四个层次。

第一层：形式化工具

• 第零章：为什么需要类型系统
• 第一章：数学基础
• 第二章：形式文法与 BNF

这一部分的任务，是让你先接受一种思维方式：

讨论语言和类型系统时，我们不能只靠“差不多能懂”的自然语言描述，而要学会用明确的语法、规则和证明来表达。

第二层：计算模型

• 第三章：Lambda 演算基础
• 第四章：Lambda 演算中的计算

这一部分建立“程序如何计算”的最小模型。后面的大多数类型系统，都是在某种 Lambda 演算之上扩展出来的。

第三层：核心类型系统

• 第五章：类型系统核心概念
• 第六章：一阶类型系统

这一部分会回答最关键的问题：

• 什么叫“一个项具有某个类型”？
• 类型规则究竟在说什么？
• 为什么类型系统可以排除某些运行时错误？

第四层：重要扩展

• 第七章：二阶类型系统
• 第八章：子类型
• 第九章：类型推断
• 第十章：子结构类型系统

这里的主题彼此有关，但并不要求你一次完全掌握。第一次阅读时，建议把注意力放在每章的核心动机和最基本规则上；形式细节可以在第二遍阅读时慢慢回看。

阅读时应该重点抓什么？

每一章里通常会同时出现三类内容：

1. 直觉：为什么要引入这个概念？它解决了什么问题？
2. 形式化定义：它的语法、规则、定理是什么？
3. 语言对照：在真实语言里，大概有什么相似做法？

如果你是第一次接触这类内容，建议优先确保自己能回答下面三个问题：

• 这个概念想解决什么问题？
• 它的最小形式定义是什么？
• 我能否手动做一个最基本的例子？

比如：

• 学 Lambda 演算时，能否自己算自由变量和替换？
• 学类型规则时，能否自己画一个简单的推导树？
• 学类型推断时，能否跟着一个例子生成约束并做合一？

和“看懂了”相比，能亲手做一个最小例子往往更重要。

本教程常用的记号与约定

完整的术语说明见附录A，完整的符号表见附录B。建议把这两个附录当作阅读时的常驻参考：

• 正文中首次引入的重要术语，通常会在括号中给出英文原文；
• 如果你一时忘了某个术语的边界，优先查附录A；
• 如果你一时忘了某个记号的读法和语境，优先查附录B；
• 如果你一时分不清“值 / 范式 / 卡住”“类型检查 / 类型推断”“Church 风格 / Curry 风格”这类术语差别，优先查附录A；
• 如果你一时忘了 $\Gamma \vdash t : T$、$\longrightarrow$、$\forall$、$S <: T$ 这些记号怎么读、怎么用，优先查附录B。

这里先列出最常见、最值得提前熟悉的几个。

其中要特别注意两点：

• $\mapsto$ 的字面意思是“映射到”；在不同上下文里，它可能表示替换、环境中的绑定，或更一般的映射关系。
• $\vdash$ 常读作“推出”或“可判断为”；它通常不是普通的逻辑蕴含，而是在某套规则系统内部的可推导关系。

最后一点建议

第一次读这类材料时，遇到公式多、符号多是正常的。不要把目标设成“第一次就完全掌握所有形式细节”，而是先建立下面这条主线：

语法定义了程序长什么样；语义定义了程序怎么计算；类型系统定义了哪些程序被允许；元理论则说明这些规则为什么可靠。

如果你能沿着这条主线把各章串起来，后面的细节就有落脚点了。

接下来，从第零章开始，我们先回答一个最自然的问题：

为什么程序语言需要类型系统？

第零章 导论：为什么需要类型系统

第零章 导论：为什么需要类型系统

阅读提示

本章是全书主线的起点。阅读时如果你想快速确认“卡住”“类型安全”“类型判断”“静态 / 动态”“安全 / 不安全”等术语，建议配合：

• 附录A《术语表》
• 附录B《符号速查表》

这一章不急着进入公式和推导规则，而是先回答一个更根本的问题：

为什么我们需要类型系统？

如果不先回答这个问题，后面学到的类型判断、类型安全、子类型、类型推断，很容易变成一堆彼此孤立的技术名词。导论的任务，就是先把整本教程的主线建立起来。

0.1 从一个简单错误开始

考虑下面这个 JavaScript 函数：

function add(a, b) { return a + b; }
add(3, "hello")

这段程序在语法上完全合法，但它的行为未必符合你的意图：

• 如果你想做数值加法，那么这里出了问题；
• 问题并不是在写代码时立刻暴露的，而是在运行时才表现出来。

类型系统最直观的价值，就是把一部分这类问题提前到运行之前发现。

function add(a: number, b: number): number { return a + b; }
add(3, "hello")

在这个版本里，编译器会直接报告：第二个参数不是 number。程序甚至不必真正运行，错误就已经被指出来了。

这就是类型系统最常见的第一印象：

它试图在程序运行之前，排除某些本来会在运行时才出现的错误。

当然，这个说法还是比较粗糙的。下面我们把它说得更精确一点。

0.2 类型系统是什么？

Cardelli 对类型系统有一个经典定义：

类型系统是一种可判定的语法方法，通过对程序短语按其计算值的种类进行分类，来证明程序的某些行为不会发生。

这个定义里的每个词都很重要。

这里最值得强调的是最后一点：类型系统保证的从来不是“程序绝对正确”，而是“程序不会发生我们选定的那类错误”。

例如，一个程序即使类型完全正确，也仍然可能：

• 返回了错误的业务结果；
• 进入死循环；
• 因为算法太慢而不可用；
• 因为逻辑漏洞而做出不合预期的事。

所以学习类型系统时，最重要的心态之一是：

类型系统很重要，但它解决的是程序可靠性中的一部分问题，而不是全部问题。

0.3 为什么类型系统必须“保守”？

你可能会问：

既然目标是排除运行时错误，为什么类型系统不直接精确分析程序的所有行为？

直观上的答案是：那通常做不到，或者代价太高。

更深层的背景来自可判定性理论。Rice 定理告诉我们：关于程序语义行为的很多非平凡性质，一般来说是不可判定的。你可以把它理解为一种“坏消息”：

• 如果我们要求类型系统精确预测程序所有有意义的行为，
• 那它往往就不再是一个总能结束的检查过程。

因此，类型系统通常采取一种折中策略：

• 不去精确模拟程序所有运行行为；
• 而是只根据程序结构做一种保守近似。

“保守”意味着两件事：

1. 它宁可拒绝一些其实运行时没有问题的程序；
2. 也要尽量避免放过那些会落入禁止错误的程序。

例如，下面这段代码从运行角度看其实没有问题：

if (true) { 42 } else { "hello" }

但如果某个极其简单的类型系统只允许 if 的两个分支具有相同类型，那么它就会拒绝这段程序。原因不是程序真的会出错，而是这个类型系统太粗糙，只能用“两个分支类型一致”这种简单规则来换取可判定性和实现简洁性。

所以“被类型系统拒绝”并不一定意味着“运行时一定出错”；它也可能意味着：

这个类型系统选择了一种更简单、更安全、也更保守的近似方式。

0.4 类型系统到底在防什么错误？

在本教程里，我们会频繁使用一个词：卡住（stuck）。

先给一个工作直觉：

一个程序如果既不是一个被当前求值规则视为“计算完成”的结果，又无法按照语言的求值规则继续走下去，我们就说它“卡住”了。

这里先故意说得比较直觉。更严格地说，后面我们会区分：

• 值（value）：相对于某个求值策略，被视为“计算完成”的项；
• 范式（normal form）：相对于某个归约关系，已经无法继续归约的项；
• 卡住（stuck）：既不是值，又不能继续前进的项。

更稳妥地说，本章这里只给出“卡住”的工作定义；第 4 章会把它放回具体求值关系中说明，第 5 章再把它和“类型安全”正式连起来。若你想先快速确认这些术语，也可以配合附录A“术语表”和附录B“符号速查表”一起看。

例如，把布尔值当函数调用，就是一种典型的卡住情形：

true 0

这个式子不是一个正常结果，也没有任何合理的“下一步计算规则”。后面几章我们会把这种现象形式化，并把它和类型安全联系起来。

Cardelli 还区分了不同种类的执行错误。用最粗略的方式说，可以把错误分成两类：

• 程序显式报错并终止：例如除零异常、断言失败；
• 程序进入未预期状态：例如类型混淆、非法内存访问、协议顺序错误。

不同语言、不同语义模型，会把“什么算错误”画在不同边界上。因此更稳妥的说法不是“类型系统保证绝不出错”，而是：

相对于我们选定的语义和错误模型，良类型程序不会发生那类被禁止的错误。

这就是后面“类型安全”要表达的核心思想。

0.5 静态类型、动态类型与安全性

在日常讨论里，人们常把“静态 / 动态”和“安全 / 不安全”混在一起，但它们其实是两个不同维度。

静态 vs 动态

• 静态类型：主要在运行之前检查程序；
• 动态类型：主要在运行过程中检查程序。

安全 vs 不安全

• 安全：语言设计会阻止某类未定义或不可接受的错误行为；
• 不安全：某些错误行为可能直接暴露给程序员，语言不保证彻底拦住它们。

这两个维度并不完全重合。

• 一个语言可以是静态而安全的；
• 也可以是动态而安全的；
• 还可以是静态但仍允许某些不安全操作的；
• 更可以是把很多责任交给程序员自己承担的。

因此，下面这种说法就太粗糙了：

“静态类型语言一定更安全。”

更准确的说法是：

• 静态类型系统常常能在运行前排除更多错误；
• 但完整的安全性往往还依赖运行时检查、内存模型、异常机制、边界检查、模块系统等其他设计；
• 而动态语言也完全可以通过运行时检查来维持某种安全保证。

这也是为什么本教程后面会区分：

• 类型规则本身在保证什么；
• 整个语言运行时系统在保证什么。

本教程后文主要关心的是：静态类型系统如何与操作语义配合，建立可证明的安全保证；至于完整语言实现中的所有安全机制，则只在需要时点到为止。

0.6 本教程接下来会怎样推进？

既然类型系统的目标是“排除某些不良运行行为”，那么我们就需要按顺序解决四个问题：

1. 程序长什么样？

   • 需要语法工具
   • 对应第1章和第2章的一部分准备工作

2. 程序怎么计算？

   • 需要求值规则、操作语义
   • 对应第3章和第4章的 Lambda 演算

3. 程序为什么算是“有类型”？

   • 需要类型判断和类型规则
   • 对应第5章

4. 这些规则为什么可靠？

   • 需要先在第4章明确“程序怎样前进”，再在第5章讨论类型安全、进展性与保持性，并在第6–10章继续扩展
   • 对应第4章、第5章后半以及第6–10章；其中第 9 章还会回到一个新问题：如果项里不显式写出类型，系统如何自动恢复这些类型信息？

换句话说，本教程的大主线其实很简单：

先定义语言，再定义计算，再定义类型，最后证明这些定义彼此匹配。

如果你读到后面一时忘了术语或符号，可以随时回查：

• 附录A：术语表
• 附录B：符号速查表

它们并不替代正文，但很适合在阅读第 4 章“计算”与第 5 章“类型安全”时来回对照。

这条主线会在后面的章节里反复出现。

0.7 本章小结

这一章先建立了三个最关键的认识：

1. 类型系统的任务不是证明程序“绝对正确”，而是排除某类被禁止的错误行为。
2. 类型系统之所以保守，是因为程序语义的精确分析通常不可判定或代价过高。
3. 后续所有形式化工作——语法、语义、类型规则和安全性证明——都是为了把“良类型程序不会卡住”这类直觉命题说清楚。

如果你读完这一章，已经能清楚地区分下面几件事，那就达成目标了：

• 静态类型和动态类型不是一回事；
• 安全和不安全也不是同一个维度；
• 类型系统是“程序可靠性的一部分”，不是“程序正确性的全部”。

回看导航

如果你读完本章后还觉得有些概念只是“听懂了大意”，但还没形成稳定主线，建议按下面顺序回看：

1. 先回看本章的 0.2、0.4、0.5 三节，重新确认：
   • 类型系统到底在防什么错误；
   • 什么叫“卡住”；
   • 为什么“静态 / 动态”和“安全 / 不安全”不是同一个维度。
2. 若你对术语边界仍然模糊，回查附录A《术语表》。
3. 若你读到后面章节时忘了本章埋下的主线，可以把本章和第 4 章“计算”、第 5 章“类型系统核心概念”连起来重看。

思考题

1. 为什么“程序能运行”并不等于“程序没有类型问题”？
2. 如果一个类型系统很保守，它可能拒绝哪类实际上运行正常的程序？
3. “静态类型”和“安全”为什么不能简单画等号？

第一章 数学基础

第一章 数学基础

阅读提示

本章会频繁使用“集合”“关系”“归纳定义”“结构归纳法（structural induction）”“推导规则（inference rule）”“推导树（derivation tree）”等概念。若你在阅读时想快速回查术语与记号，建议配合：

• 附录A《术语表》中的 A.9“逻辑与元理论相关术语”
• 附录B《符号速查表》中的“逻辑与判断相关记号”

后面的章节会频繁出现集合、关系、归纳定义、推导规则这些概念。它们不是为了“让材料看起来更数学”，而是因为：

• 语法需要精确定义；
• 类型判断需要规则化表达；
• 类型安全需要证明。

这一章的目标不是系统讲授全部离散数学，而是把后续真正会用到的最小工具建立起来。

1.1 为什么类型系统需要数学工具？

学习类型系统时，你会不断遇到三类问题：

1. 如何定义一个语言？

   • 这需要归纳定义和形式文法。

2. 如何说明一个判断是成立的？

   • 这需要推导规则和推导树。

3. 如何证明一个性质对所有程序成立？

   • 这需要归纳法。

所以这一章的核心不是“数学知识本身”，而是下面这套工作流：

定义对象 → 写出规则 → 对规则与结构做证明。

1.2 集合：最基本的直觉工具

集合是类型理论里最常见的背景语言之一。

在很多入门场景下，我们会用“值的集合”来帮助理解类型。例如：

• Bool 可以直觉地理解成集合 $\{\text{true},\text{false}\}$；
• 一个积类型可以直觉地理解成两个集合的笛卡尔积；
• 一个和类型可以直觉地理解成两个集合的带标签并集。

要注意，这是一种有帮助的语义直觉，但它并不是所有类型理论中的统一定义。随着系统变复杂，类型未必总能简单等同于某个朴素集合。

1.2.1 常见集合操作

例如，若 $A=\{1,2\}$，$B=\{2,3\}$，则：

$$\begin{array}{rl}A\cup B& =\{1,2,3\}\\ A\cap B& =\{2\}\\ A\setminus B& =\{1\}\\ A\times B& =\{(1,2),(1,3),(2,2),(2,3)\}\end{array}$$

在后面的章节里：

• 笛卡尔积会帮助我们理解积类型；
• 集合包含会帮助我们直觉化地理解某些子类型关系；
• 幂集会在更高级的语义讨论里再次出现。

在某些语义模型中，子类型常可以用集合包含来直觉理解；但这是一种语义视角，不应直接当作所有类型系统中的定义。

1.3 关系与函数

仅仅有集合还不够。类型理论更关心的是：

对象之间怎样相互关联？

例如：

• “这个类型是不是那个类型的子类型？”
• “这个项能不能一步归约到那个项？”
• “这两个项是否等价？”

这些都属于关系。

1.3.1 关系

集合 $A$ 与 $B$ 之间的一个二元关系 $R$，就是笛卡尔积 $A\times B$ 的一个子集：

$$R\subseteq A\times B$$

若 $(a,b)\in R$，我们常记作：

$$aRb$$

1.3.2 常见性质

不同性质的组合，会得到不同种类的关系：

这些名字在后文都不是摆设：

• α-等价（alpha-equivalence）是一种等价关系；
• 子类型关系（subtyping relation）通常至少希望具备前序性质；
• 归约关系（reduction relation）则是另一类重要关系。

1.3.3 一个例子：模 3 等价

在整数集合上定义关系：

$$a\equiv b(\mathrm{mod}3)\text{当且仅当}3\mid (a-b)$$

这个关系是一个等价关系：

• 自反：$a-a=0$，而 $3\mid 0$
• 对称：若 $3\mid (a-b)$，则也有 $3\mid (b-a)$
• 传递：若 $3\mid (a-b)$ 且 $3\mid (b-c)$，则 $3\mid (a-c)$

因此它会把整数划分成三个等价类：

• $\{\dots ,-6,-3,0,3,6,\dots \}$
• $\{\dots ,-5,-2,1,4,7,\dots \}$
• $\{\dots ,-4,-1,2,5,8,\dots \}$

这个例子的重要性不在于模运算本身，而在于它帮助你建立“等价关系把对象按某种意义上的相同划分成类”的直觉。后面讲 α-等价（alpha-equivalence）时，这种直觉会再次出现（见第 3 章；若你只想先查术语，可配合附录A“术语表”中的“α-等价”条目）。

1.3.4 函数

函数可以看作一种特殊关系：

• 每个输入都有输出；
• 每个输入至多对应一个输出。

写作：

$$f:A\to B$$

根据是否“对所有输入都有定义”，可以区分：

• 全函数：对每个输入都给出结果；
• 部分函数：只对某些输入有定义。

这里要特别小心一个常见混淆。

• 类型判断本身首先是一个关系：$\Gamma ⊢t:T$；
• 在某些语法制导（syntax-directed）的系统中，这个关系可以实现成一个检查算法；
• 这个算法通常是一个总函数，返回“类型”或“错误”。

所以，更准确的说法不是“类型判断就是部分函数”，而是：

类型关系在某些系统里可以被实现为一个总会终止的检查过程。

后面几章里，这种“关系先于算法”的视角会不断出现：

• 第 4 章会把“程序如何计算”写成归约关系与求值关系；
• 第 5 章会把“项具有某类型”写成类型判断关系；
• 第 8 章会再引入子类型关系 <:，讨论什么叫安全替换。

1.4 归纳定义：如何定义无限对象族？

编程语言的语法、类型、推导树，往往都是无限的对象族。我们不可能把它们一个个列出来，所以需要一种“有限地定义无限”的方法：归纳定义。

归纳定义通常由两部分构成：

1. 基础情况：先给出最简单的对象；
2. 构造规则：说明如何从已知对象构造新对象。

1.4.1 例子：自然数

自然数可以归纳地定义为：

1. $0$ 是自然数；
2. 如果 $n$ 是自然数，那么 $S(n)$ 也是自然数。

通过不断使用第二条规则，我们得到：

• $0$
• $S(0)$
• $S(S(0))$
• $S(S(S(0)))$
• ……

这个定义告诉我们两件事：

• 哪些对象属于自然数；
• 除了按这些规则构造出来的对象，别的都不算自然数。

这类“最小闭包”思想，在后面定义项、类型、推导树时都会出现。

1.4.2 例子：算术表达式

可以把只含加法和乘法的表达式定义为：

1. 数字 $n$ 是表达式；
2. 如果 $e_1$ 和 $e_2$ 是表达式，那么 $e_1+e_2$ 是表达式；
3. 如果 $e_1$ 和 $e_2$ 是表达式，那么 $e_1\times e_2$ 是表达式。

这也是后面定义语法的基本方式。

对本教程中的语法对象来说，第二章的 BNF 记法可以看作归纳定义的一种常见写法；而第 3 章对 Lambda 项的定义，就是这一点最直接的实例。

1.5 归纳法：如何证明“对所有对象都成立”？

归纳定义告诉我们对象是怎样长出来的；归纳法则告诉我们，怎样对它们做普遍证明。

1.5.1 自然数归纳法

要证明性质 $P(n)$ 对所有自然数成立，通常分两步：

1. 证明 $P(0)$；
2. 假设 $P(n)$ 成立，证明 $P(S(n))$ 成立。

这种证明方法之所以有效，是因为自然数正是按“从 0 出发、不断取后继”归纳生成的。

1.5.2 结构归纳法

对于语法树、项、类型等归纳定义出来的对象，更常见的是结构归纳法（structural induction）：

• 对每个基础构造分别证明；
• 对每个复合构造，假设性质对其子结构成立，再证明对整体成立。

1.5.3 一个简单示例

假设算术表达式的深度定义如下：

• $depth(n)=1$
• $depth(e_1+e_2)=\max (depth(e_1),depth(e_2))+1$
• $depth(e_1\times e_2)=\max (depth(e_1),depth(e_2))+1$

我们想证明：每个算术表达式的深度都是有限的。

证明方法就是对表达式结构归纳：

• 若表达式是数字，深度显然是 1，因此有限；
• 若表达式是加法或乘法，则由归纳假设，其两个子表达式深度有限，因此最大值再加 1 仍然有限。

这类证明在后面的类型安全证明中会反复出现。

1.5.4 推导归纳法

除了对“项的结构”做归纳，我们还常对“推导树的结构”做归纳，这叫推导归纳法（induction on derivations）。

它的模式是：

• 看一个判断是通过哪条规则最后推出的；
• 对该规则的前提对应的子推导使用归纳假设；
• 再证明结论成立。

第五章证明保持性时，就会用到这种方法；而替换引理、进展性、保持性这些术语，也都可以在附录A“术语表”中快速回查。

1.6 推导规则：怎样把判断写成统一格式？

类型系统里最常见的书写形式是推导规则：

$$\frac{前{提}_1前{提}_2\cdots 前{提}_n}{结论}\text{(规则名)}$$

意思是：

如果上面的前提都成立，那么下面的结论成立。

如果一个规则没有前提，就叫公理。

1.6.1 一个小例子：自然数上的“小于”

我们可以用下面两条规则定义“$<$”：

$$\frac{}{0<S(n)}\text{(Zero)}$$

$$\frac{n<m}{S(n)<S(m)}\text{(Succ)}$$

用它们可以推出 $1<3$：

$$\frac{\frac{}{0<S(S(0))}\text{(Zero)}}{S(0)<S(S(S(0)))}\text{(Succ)}$$

这里最重要的不是这个例子本身，而是要熟悉这样一种表达方式：

• 一个判断是否成立，
• 取决于它能否被某些规则一步步推出。

后面的类型规则、子类型规则、操作语义规则，都会以同样的形式出现。

1.6.2 推导树的意义

当多条规则叠加使用时，就会形成一棵推导树：

• 叶子通常是公理或无需再展开的事实；
• 中间节点对应规则的应用；
• 根节点是我们最终想得到的判断。

这也是为什么“一个判断成立”常常等价于“存在一棵以它为根的合法推导树”。

这条视角在后续几章中会不断复现：

• 第 3 章里，我们会先定义 Lambda 项及其变量结构；
• 第 4 章里，我们会用规则描述归约与求值；
• 第 5 章里，我们会正式写出类型判断与类型推导树；
• 第 8 章里，我们还会把同样的规则化思路用于子类型关系。

1.7 本章小结

这一章建立了后续最常用的四种工具：

1. 集合与关系：帮助我们表达“元素属于什么”“对象之间如何关联”。
2. 归纳定义：帮助我们有限地定义无限对象族。
3. 归纳法：帮助我们证明某个性质对所有语法对象或所有推导都成立。
4. 推导规则：帮助我们把“何时能推出一个判断”写成精确统一的形式。

如果把本章压缩成一句话，那就是：

后面所有形式化内容，都会围绕“定义、规则、归纳证明”这三件事展开。

1.8 回看导航

如果你读到后面章节时，发现自己开始对形式化规则“看得懂但推不动”，最值得优先回看的通常就是本章。建议按下面顺序复习：

1. 回看本章的“关系”“归纳定义”“结构归纳”“推导规则”。
2. 配合附录A确认术语：尤其是“推导规则”“推导树”“结构归纳法”“推导归纳法”。
3. 配合附录B确认记号：尤其是 \vdash、\forall、\Rightarrow 等。
4. 再回到第 3–5 章看它们怎样把这些数学工具真正用在语法、归约和类型判断上。

下一章里，这些工具会立刻派上用场：我们将用形式文法和 BNF 来精确定义语言语法。

本章练习

1. 设 $A=\{1,2,3,4\}$，$B=\{3,4,5,6\}$，计算 $A\cup B$、$A\cap B$、$A\setminus B$、$A\times B$。
2. 用归纳定义的方式定义“合法的括号字符串”。
3. 用推导规则定义自然数上的“小于等于”关系，并尝试推出 $2\le 4$。
4. 用结构归纳法证明：每个算术表达式的大小（节点数）至少为 1。

第二章 形式文法与 BNF

第二章 形式文法与 BNF

阅读提示

本章会频繁使用“终结符（terminal）/ 非终结符（nonterminal）”“具体语法（concrete syntax）/ 抽象语法（abstract syntax）”“抽象语法树（abstract syntax tree, AST）”“BNF（Backus–Naur Form）”等概念。若你在阅读时想快速回查术语与记号，建议配合：

• 附录A《术语表》中的相关条目；
• 附录B《符号速查表》中的元变量与常见记号说明。

第一章介绍了推导规则和归纳定义，现在我们把这些工具真正用在“语言本身”上：

怎样精确地说明：什么样的程序是合法的？

这件事如果只靠自然语言描述，往往不够稳定，也不够适合后续的数学推理。于是我们需要形式文法（formal grammar）。

在阅读本章时，建议同时记住两条线索：

• 本章主要处理“程序在表面上如何写出来”与“它在结构上如何被分析”；
• 下一章开始，我们会把这里的语法工具真正用于 Lambda 演算，并更多地站在抽象语法而不是源代码表面写法的层面讨论问题。

如果你在术语或记号上感到不确定，可以配合附录A“术语表”和附录B“符号速查表”一起阅读。

2.1 为什么自然语言不够？

假设我们这样描述一个简单表达式语言：

算术表达式由数字、加号、乘号和括号组成，乘法优先级高于加法。

这段话对人类读者来说已经“差不多能懂”，但对于形式化讨论来说还不够。

例如：

1 + 2 * 3

它到底应该理解成：

• $(1+2)\ast 3$，还是
• $1+(2\ast 3)$？

人类会说：“当然是后者，因为乘法优先级更高。”

但如果你要把这件事交给编译器、解释器，或者要在这个语言上定义类型规则，就不能只说“当然”。你必须把优先级和结合性直接体现在语法规则中。

这就是形式文法的作用：

• 明确什么字符串是合法程序；
• 明确它们应该如何解析；
• 为后续的抽象语法和类型规则打基础。

2.2 BNF：最常见的语法表示法

类型系统文献里最常见的语法记法是 BNF（Backus–Naur Form）。

它的基本形式是：

<非终结符> ::= 定义

其中：

• ::= 表示“定义为”；
• | 表示“或”；
• 尖括号里的名字表示一个语法类别，称为非终结符（nonterminal）；
• 真正出现在程序里的字面符号，称为终结符（terminal）。

这里先提醒一个后文会反复用到的区分：

• 当我们用 BNF 讨论源代码表面写法时，重点通常是具体语法（concrete syntax）；
• 当我们在后续章节里写 t ::= ...、T ::= ... 这类生成式时，重点往往已经转向抽象语法（abstract syntax）的归纳定义。

例如：

<expr> ::= <expr> + <term> | <term>
<term> ::= <term> * <factor> | <factor>
<factor> ::= ( <expr> ) | <number>

这里：

• <expr>、<term>、<factor>、<number> 是非终结符；
• +、*、(、) 以及数字字符属于终结符。

BNF 的价值不在于记号本身，而在于它把“合法程序长什么样”变成了一组可以机械检查的规则。

2.3 优先级与结合性如何写进文法？

回到前面的算术表达式例子。为什么要分成 expr / term / factor 三层？

因为这恰好把优先级写进了语法：

• expr 对应较低优先级的加法层；
• term 对应较高优先级的乘法层；
• factor 对应最基本的原子层。

于是 1 + 2 * 3 只能被解析成：

• 一个 expr
• 其左边是 1
• 其右边是一个 term
• 而那个 term 再展开为 2 * 3

这就自然得到：

$$1+(2\ast 3)$$

一个简单推导示例

<expr>
→ <expr> + <term>
→ <term> + <term>
→ <factor> + <term>
→ <number> + <term>
→ 1 + <term>
→ 1 + <term> * <factor>
→ 1 + <factor> * <factor>
→ 1 + 2 * 3

这个推导过程说明：

• 2 * 3 先在 term 层形成；
• 然后整个式子才回到 expr 层；
• 因而乘法天然绑定得更紧。

左结合与右结合

除了优先级，文法也常用来表达结合性。

例如：

<expr> ::= <expr> + <term> | <term>

这是一种典型的左递归写法，它对应左结合：

1 + 2 + 3  读作  (1 + 2) + 3

后面第三章讲 Lambda 项时，我们同样会用“左结合”和“向右延伸”这样的书写约定来消歧义。到那时你会看到：很多看起来像“BNF 规则”的写法，真正服务的对象其实已经是抽象语法层面的结构表示。

2.4 形式文法的四元组表示

从更抽象的角度看，一个形式文法通常写成四元组：

$$G=(N,\Sigma ,P,S)$$

其中：

对于前面的算术表达式文法，可以理解为：

• $N=\{⟨expr⟩,⟨term⟩,⟨factor⟩,⟨number⟩\}$
• $\Sigma =\{+,\ast ,(,),0,1,2,\dots \}$
• $P$ 是所有产生式规则
• $S=⟨expr⟩$

四元组写法的好处是：

• 你可以精确讨论“这是哪一类文法”；
• 也可以把“语法”当成一个标准数学对象来研究。

一个简短的 Chomsky 层级说明

本教程主要用的是上下文无关文法。它的特征是：

每条产生式左侧都是一个单独的非终结符。

这正好就是 BNF 最常见的写法。

对本书来说，你不需要深入掌握整个 Chomsky 层级。只要记住：

• 编程语言的核心语法，通常适合用上下文无关文法描述；
• 而“变量必须先声明后使用”这类约束，往往不属于纯语法层，而要交给后续的语义分析或类型系统处理。

2.5 具体语法与抽象语法

真正编程时，你写下的是具体语法（concrete syntax）；

而类型系统和解释器更关心的是：

去掉无关书写细节之后，程序的核心结构是什么？

这就是抽象语法（abstract syntax）。

这一点对后文非常重要。因为从第三章开始，本教程虽然仍会沿用类似 BNF 的紧凑写法，但默认更关心的是：

• 哪些对象属于语言的抽象语法；
• 它们如何按归纳方式生成；
• 后续的自由变量、替换、归约和类型规则如何定义在这些结构上。

也就是说，后文很多看起来像“文法”的写法，主要服务于抽象语法对象的定义，而不是完整源代码语法的刻画。

例如，下面这些写法在具体语法上不同：

1 + 2 * 3
1+2*3
(1) + ((2) * 3)

但它们都对应同一个抽象语法树（AST）：

      Add
     /   \
   Num    Mul
   1     /   \
       Num   Num
        2     3

这就是为什么后面定义语义和类型规则时，我们通常直接面向 AST，而不是面向源代码表面的括号和空格。

第三章的 Lambda 项语法就是第一个完整例子：虽然表面上仍会写成类似 BNF 的形式，但那时我们真正关心的已经是“变量、抽象、应用”这三类抽象语法构造，而不是某门具体语言里的排版细节。

一个重要提醒

很多入门材料会说：“BNF 的每个分支都对应一个 AST 节点。”

这句话作为直觉有帮助，但不能说得太绝对。更准确的说法是：

• 抽象语法构造子通常来自我们对文法的整理；
• 具体语法里的某些产生式只是为了优先级、结合性或书写方便服务；
• 它们未必都会在 AST 中保留下来。

比如括号就是典型例子：

• 它在具体语法里非常重要；
• 但在 AST 里通常不会单独形成一个“括号节点”。

因此，后面如果你看到教程把某个语法写成

t ::= ...

这样的形式，最稳妥的理解通常不是“这里在讨论完整源代码语法”，而是“这里在用一种紧凑记法描述抽象语法对象的生成方式”。

这也是为什么本章虽然从 BNF 讲起，但它真正要为后文准备的，不只是“怎么写文法”，更是：

怎样把语言对象写成可归纳定义、可做推理、可接上语义与类型规则的抽象结构。

2.6 词法层与语法层

还有一个常见细节值得提早说明：

• 词法层负责把字符流切成记号（token），如标识符、数字、关键字；
• 语法层负责把这些记号组织成树状结构。

因此，如果你在 BNF 里看到类似：

<number> ::= <digit> | <digit> <number>
<digit> ::= 0 | 1 | 2 | ... | 9

这只是为了教学清楚，把数字的内部结构也显式写出来。

但到了 AST 层，解释器或类型检查器往往只关心：

Num(123)

也就是说：

词法细节在 AST 中常被折叠。

这点后面非常重要。因为类型规则通常对应的是 AST 构造，而不是字符级别的文法细节。

2.7 本书中的常见元变量

类型系统文献喜欢使用固定的元变量约定。熟悉这些记号，会让后面的公式更容易读。

这里的“项”可以理解成“形式化语言中的表达式对象”。例如：

• 在第三章，Lambda 项就是用语法规则生成出来的项；
• 在第五章，类型规则判断的对象也是项。

2.8 本章小结

这一章最重要的不是记住某种特定文法，而是理解下面几件事：

1. 形式文法的任务是精确定义“什么样的程序合法”。
2. BNF 是最常见的语法书写方式，尤其适合描述上下文无关语法。
3. 优先级与结合性并不是语法之外的注释，而是可以直接写进文法结构里的。
4. 类型系统真正操作的对象通常是抽象语法，而不是源代码的表面写法。
5. 从第三章开始，本教程中的许多生成式写法都应优先理解为抽象语法的归纳定义，而不是完整 concrete syntax 的逐字描述。

下一章开始，我们就会把这些工具用在一个真正重要的对象上：

Lambda 演算。

届时你会看到，本章区分的几件事会立刻变得具体起来：

• 什么是语法对象；
• 什么是抽象语法层面的构造；
• 为什么后续的自由变量、替换、β-归约和类型规则，都更自然地定义在 AST 结构上。

如果你想提前做准备，建议特别回顾本章中的“优先级 / 结合性”“具体语法 vs 抽象语法”“元变量约定”这三部分。

回看导航

如果你读完本章后仍觉得“文法看着都懂，但不知道它和后面章节有什么关系”，建议这样回看：

• 回看本章中的“优先级 / 结合性”和“具体语法 vs 抽象语法”；
• 配合附录A确认“终结符、非终结符、抽象语法、AST”这些术语；
• 配合附录B确认本章使用的元变量记法；
• 然后再进入第 3 章，看这些语法工具如何真正落到 Lambda 项上。

本章练习

1. 用 BNF 定义一个简单的布尔表达式语言，包含 true、false、not、and、or，并体现 not 的优先级高于 and，and 高于 or。
2. 用你定义的文法推导字符串 true and (false or true)。
3. 为表达式 1 + 2 * 3 画出对应的 AST。
4. 解释“具体语法”和“抽象语法”的区别，并说明类型系统主要工作在哪一层。

第三章 Lambda 演算基础

第三章 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 演算如何真正“跑起来”。

第四章 Lambda 演算中的计算

第四章 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 项到底如何计算？

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

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

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

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

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

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

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

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

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

$$(\lambda x.t)s{⟶}_{\beta }[x\mapsto s]t$$

它的直觉非常简单：

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

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

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

4.1.1 最简单的例子

例 1：恒等函数

$$(\lambda x.x)y{⟶}_{\beta }y$$

因为：

$$[x\mapsto y]x=y$$

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

例 2：常函数

$$(\lambda x.\lambda y.x)ab$$

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

$$((\lambda x.\lambda y.x)a)b$$

先归约最左边的应用：

$$(\lambda x.\lambda y.x)a{⟶}_{\beta }\lambda y.a$$

于是整体变成：

$$(\lambda y.a)b{⟶}_{\beta }a$$

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

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

考虑下面这个项：

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

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

$$\lambda y.y$$

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

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

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

然后再归约：

$$(\lambda x.\lambda z.x)y{⟶}_{\beta }\lambda z.y$$

所以更准确地说：

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

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

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

4.2.1 可归约表达式（redex）

形如

$$(\lambda 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 项都能归约到范式。

最经典的例子是：

$$\Omega =(\lambda x.xx)(\lambda x.xx)$$

归约一步：

$$(\lambda x.xx)(\lambda x.xx){⟶}_{\beta }(\lambda x.xx)(\lambda x.xx)$$

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

$$\Omega {⟶}_{\beta }\Omega {⟶}_{\beta }\Omega {⟶}_{\beta }\cdots$$

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

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

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

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

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

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

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

例如：

$$(\lambda x.a)((\lambda y.b)c)$$

这里有两个 redex：

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

于是会出现一个问题：

应该先归约哪一个？

我们可以先归约外层：

$$(\lambda x.a)((\lambda y.b)c)⟶a$$

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

也可以先归约内层：

$$(\lambda x.a)((\lambda y.b)c)⟶(\lambda x.a)b⟶a$$

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

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

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

这就引出下面的合流性。

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

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

直观上，合流性说的是：

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

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

如果 $t{⟶}_{\beta }^{\ast }{t}_1$ 且 $t{⟶}_{\beta }^{\ast }{t}_2$，那么存在某个项 $u$，使得
$t_1{⟶}_{\beta }^{\ast }u$ 且 $t_2{⟶}_{\beta }^{\ast }u$。

其中：

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

图形上可以画成：

        t
       / \
      *   *
     /     \
   t1      t2
     \     /
      *   *
       \ /
        u

4.4.1 这个定理意味着什么？

它最重要的推论是：

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

也就是说：

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

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

4.4.2 需要注意的边界

Church–Rosser 定理说的是：

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

例如对某些项：

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

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

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

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

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

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

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

4.5.1 正规序：最左最外优先

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

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

例如：

$$(\lambda x.a)((\lambda y.b)c)$$

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

$$a$$

正规序的重要性质是：

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

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

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

另一种很自然的想法是：

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

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

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

例如：

$$(\lambda x.x)((\lambda y.y)z)$$

如果先算参数，就得到：

$$(\lambda x.x)((\lambda y.y)z)⟶(\lambda x.x)z⟶z$$

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

$$(\lambda x.x)((\lambda y.y)z)⟶((\lambda 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::=\lambda x.t$$

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

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

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

传名调用的核心想法是：

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

例如：

$$(\lambda x.x)((\lambda y.y)z)$$

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

$$(\lambda x.x)((\lambda y.y)z)⟶((\lambda y.y)z)⟶z$$

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

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

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

传值调用的核心想法是：

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

所以同一个例子：

$$(\lambda x.x)((\lambda y.y)z)$$

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

$$(\lambda x.x)((\lambda y.y)z)⟶(\lambda x.x)z⟶z$$

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

4.6.4 一个能体现差异的例子

看这个项：

$$(\lambda x.a)\Omega$$

其中：

$$\Omega =(\lambda x.xx)(\lambda x.xx)$$

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

$$(\lambda x.a)\Omega ⟶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^{\prime }$$

意思是：

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

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

4.8.1 传值调用下的值

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

$$v::=\lambda x.t$$

4.8.2 小步规则

β-应用规则

$$\frac{}{(\lambda x.t)v⟶[x\mapsto v]t}\text{(E-AppAbs)}$$

这条规则说：

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

函数位置先求值

$$\frac{t_1⟶t_1^{\prime }}{t_1{t}_2⟶t_1^{\prime }{t}_2}\text{(E-App1)}$$

这条规则说：

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

参数位置后求值

$$\frac{t_2⟶t_2^{\prime }}{v_1{t}_2⟶v_1{t}_2^{\prime }}\text{(E-App2)}$$

这条规则说：

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

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

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

4.8.3 一个完整例子

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

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

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

$$((\lambda f.\lambda x.fx)(\lambda y.y))(\lambda z.z)⟶(\lambda x.(\lambda y.y)x)(\lambda z.z)$$

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

$$(\lambda x.(\lambda y.y)x)(\lambda z.z)⟶(\lambda y.y)(\lambda z.z)$$

最后再归约一次：

$$(\lambda y.y)(\lambda z.z)⟶\lambda z.z$$

所以整体归约到：

$$\lambda z.z$$

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

4.8.4 多步归约

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

$${⟶}^{\ast }$$

例如：

$$(\lambda x.x)((\lambda y.y)z){⟶}^{\ast }z$$

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

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

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

$$t\Downarrow v$$

意思是：

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

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

4.9.1 值规则

$$\frac{}{v\Downarrow v}\text{(B-Value)}$$

值求值到它自己。

4.9.2 应用规则

$$\frac{t_1\Downarrow \lambda x.t{t}_2\Downarrow v_2[x\mapsto v_2]t\Downarrow v}{t_1{t}_2\Downarrow v}\text{(B-App)}$$

它的意思是：

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

4.9.3 一个例子

仍然考虑：

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

按大步语义理解：

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

所以：

$$((\lambda f.\lambda x.fx)(\lambda y.y))(\lambda z.z)\Downarrow \lambda 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 演算里，我们本章更关心的仍然是归约、范式和值。

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

所以本章先记住三点：

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

4.11 本章小结

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

你应该已经掌握的主线

1. β-归约是 Lambda 演算的核心计算规则： $$(\lambda x.t)s{⟶}_{\beta }[x\mapsto s]t$$

2. 一个项里可能同时有多个 redex，因此需要讨论归约策略。

3. Church–Rosser 定理保证了：

   • 若某项有范式，则其范式在 α-等价意义下唯一；
   • 不同归约路径不会导致真正冲突的最终结果。

4. 求值策略进一步规定：

   • 到底先算函数位置还是参数位置；
   • 是否要求参数先成为值。

5. 操作语义把“程序如何运行”写成推导规则：

   • 小步语义关注单步执行；
   • 大步语义关注最终结果。

与下一章的关系

如果说本章回答的是：

“Lambda 项如何运行？”

那么下一章将回答：

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

也就是说：

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

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

回看导航

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

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

本章练习

1. 逐步归约下列项，并写出每一步：

   • $(\lambda x.x)y$
   • $(\lambda x.\lambda y.x)ab$
   • $(\lambda f.\lambda x.fx)(\lambda y.y)z$

2. 解释为什么下面的归约不能直接做“无脑文本替换”： $$(\lambda x.\lambda y.x)y$$ 并给出正确结果。

3. 对项 $$(\lambda x.a)((\lambda y.b)c)$$ 分别先归约外层和先归约内层，观察结果。

4. 比较下列项在传名调用和传值调用下的行为： $$(\lambda x.a)\Omega \text{其中 }\Omega =(\lambda x.xx)(\lambda x.xx)$$ 说明为什么两种策略的终止性不同。

5. 用小步语义规则证明： $$((\lambda f.\lambda x.fx)(\lambda y.y))(\lambda z.z){⟶}^{\ast }\lambda z.z$$

第五章 类型系统核心概念

第五章 类型系统核心概念

前两章建立了形式化工具，第 3–4 章建立了计算模型。现在终于可以进入本教程的核心问题：

我们怎样在程序运行之前，排除某些运行时错误？

本章要回答的问题是：

1. 什么叫“一个项有某个类型”？
2. 类型规则到底在检查什么？
3. 为什么这些规则能阻止程序“卡住”？

阅读提示

本章会频繁使用 Γ ⊢ t : T、进展性（progress）、保持性（preservation）、类型安全（type safety）等术语。若你一时记不清它们的定义，可随时回查：

• 附录A《术语表》中的 A.3“类型系统核心术语”；
• 附录B《符号速查表》中的“逻辑与判断相关记号”“类型系统相关记号”。

同时，本章直接依赖：

• 第 3 章中的自由变量、替换（substitution）与避免捕获的替换；
• 第 4 章中的值（value）、小步语义（small-step semantics）与“卡住”。

这一章的任务，就是把这个问题形式化。我们会在一个最小而经典的语言上完成这件事：简单类型 Lambda 演算（Simply Typed Lambda Calculus，简称 STLC）。

不过这里要先固定一个本章约定：

本章的对象语言不是“只有函数的最纯 STLC 片段”，而是“以 STLC 为核心、加入布尔值与条件表达式的最小扩展语言”。

这样做的原因很简单：

• 纯函数片段当然足以建立类型判断的基本骨架；
• 但加入 Bool 与 if 之后，“把布尔值当函数用”这类卡住例子会更直观；
• 因而更适合在入门阶段把“类型系统到底在防什么”讲清楚。

和前几章一样，本章的重点不是一下子记住所有规则，而是先抓住主线：

1. 什么叫“一个项有某个类型”？
2. 类型规则到底在检查什么？
3. 为什么这些规则能阻止程序“卡住”？

5.1 从“卡住”到“有类型”

第四章里我们已经见过“卡住状态”（stuck term / stuck state）这个概念。直观地说：

一个项如果既不是一个正常结果，又无法继续按照求值规则前进，那么它就卡住了。

例如，在一个同时含有布尔值和函数的语言里，下面这样的项就是典型的卡住项：

$$\mathbf{true}(\lambda x.x)$$

问题不在于它“语法不合法”，而在于它没有合理的计算规则：

• true 不是函数；
• 因此不能把它应用到参数上；
• 这个项不是值，也不能继续求值。

这正是类型系统想排除的情形。它的基本思路可以概括为：

• 先给项分类；
• 分类的名字就叫类型；
• 然后只允许那些符合规则的组合方式出现。

于是，像“把布尔值当函数用”这种错误，就能在运行前被识别出来。

5.2 什么是类型系统？

Cardelli 的经典定义是：

类型系统（type system）是一种可判定的语法方法，通过对程序短语按其计算值的种类进行分类，来证明程序的某些行为不会发生。

把它放到这一章的语境里，可以读成：

• 可判定：存在一种检查过程，能够在有限时间内判断程序是否符合类型规则；
• 语法方法：主要根据程序结构来检查，而不是先运行程序；
• 分类：把项分成“布尔值”“函数”“积类型值”等不同种类；
• 某些行为不会发生：类型系统不是万能的，它只保证排除我们关心的那类错误。

因此，Milner 的著名口号：

Well-typed programs cannot go wrong.

更适合被理解为：

在选定的语言和错误模型下，良类型程序不会发生被类型系统禁止的那类错误。

这句话很重要，但也要克制理解。它并不意味着：

• 良类型程序一定得到你想要的业务结果；
• 良类型程序一定终止；
• 良类型程序一定高效。

类型系统保证的是一种受限但有力的可靠性。

5.3 本章使用的对象语言：带布尔值与条件表达式的 STLC 扩展

为了讨论类型系统，我们需要一门足够小、又足够能体现“卡住问题”的语言。

如果只看最纯粹的 STLC 函数片段，很多“明显的类型错误”其实没那么直观；因此本章采用一个带布尔值和条件表达式的 STLC 扩展。这样一来：

• 我们有函数；
• 也有基础类型 Bool；
• 还可以明确展示“把布尔值当函数”之类的错误。

因此，后文若无特别说明：

“本章对象语言”都应理解为“以 STLC 为核心、加入 Bool 与 if 的最小扩展语言”。

5.3.1 类型、项和值

类型定义为：

$$T::=\text{Bool}\mid T_1\to T_2$$

项定义为：

$$t::=x\mid \lambda x:T.t\mid tt\mid \mathbf{true}\mid \mathbf{false}\mid \mathbf{if}t\mathbf{then}t\mathbf{else}t$$

值定义为：

$$v::=\lambda x:T.t\mid \mathbf{true}\mid \mathbf{false}$$

也就是说，在这一章里我们只考虑两类类型：

• Bool
• 函数类型 $T_1\to T_2$

对应地，项包含：

• 变量
• 函数抽象
• 函数应用
• 布尔常量
• 条件表达式

5.3.2 为什么要有类型注解？

注意这里的抽象写成：

$$\lambda x:T.t$$

而不是：

$$\lambda x.t$$

这意味着我们采用的是 Church 风格（Church-style）：函数参数的类型直接写在项里。这样做的好处是：

• 类型检查更直接；
• 规则更容易写成语法制导（syntax-directed）形式；
• 也更适合作为本教程入门阶段的对象语言。

第九章讲类型推断时，我们会再回头看不显式标注类型的 Curry 风格（Curry-style）。

5.4 类型判断：形式上到底在说什么？

类型系统的核心判断叫做类型判断（type judgment），写作：

$$\Gamma ⊢t:T$$

读作：

在类型环境 $\Gamma$ 下，项 $t$ 的类型是 $T$。

如果你对这个记号的读法还不熟，可以同时回看：

• 附录A中的“类型判断”“类型环境”条目；
• 附录B中的 Γ ⊢ t : T 与 ⊢ 记号说明。

这里有三个组成部分：

• $\Gamma$：类型环境
• $t$：项
• $T$：类型

5.4.1 类型环境

类型环境（type context / typing environment）是“变量到类型”的有限映射，通常写成：

$$\Gamma =x_1:T_1,x_2:T_2,\dots ,x_n:T_n$$

它的作用很直观：
当你在函数体里遇到一个变量时，必须知道它被假定成什么类型。

例如：

• 在环境 $x:\text{Bool}$ 下，变量 x 的类型就是 Bool
• 在环境 $f:\text{Bool}\to \text{Bool},x:\text{Bool}$ 下，项 f x 应该能判断成 Bool

可以把环境理解为一种形式化的“作用域上下文”。

5.4.2 一个直观例子

判断

$$x:\text{Bool}⊢x:\text{Bool}$$

表示：

• 假设变量 x 被赋予类型 Bool
• 那么项 x 的类型就是 Bool

而判断

$$⊢\lambda x:\text{Bool}.x:\text{Bool}\to \text{Bool}$$

表示：

• 在空环境下
• 恒等函数 λx:Bool.x
• 的类型是 Bool → Bool

这种“环境下的判断”形式，会在后面所有类型规则里反复出现。

5.5 STLC 的类型规则

现在进入本章最核心的部分：类型规则。

5.5.1 变量规则

$$\frac{}{\Gamma ⊢x:T}\text{(Var)}\text{若 }\Gamma (x)=T$$

这条规则的意思是：

• 如果环境里记着 x 的类型是 T
• 那么就可以判断 x : T

这是一条公理式规则，没有前提。

5.5.2 抽象规则

$$\frac{\Gamma ,x:T_1⊢t:T_2}{\Gamma ⊢\lambda x:T_1.t:T_1\to T_2}\text{(Abs)}$$

这条规则表达了函数的最基本思想：

• 假设参数 x 的类型是 $T_1$
• 如果在这个假设下，函数体 t 的类型是 $T_2$
• 那么整个函数的类型就是 $T_1\to T_2$

也就是说，函数类型来自两部分：

• 参数类型
• 返回类型

5.5.3 应用规则

$$\frac{\Gamma ⊢t_1:T_1\to T_2\Gamma ⊢t_2:T_1}{\Gamma ⊢t_1{t}_2:T_2}\text{(App)}$$

它的意思是：

• 若 $t_1$ 是一个从 $T_1$ 到 $T_2$ 的函数；
• 且 $t_2$ 恰好是一个 $T_1$ 类型的参数；
• 那么把 $t_1$ 应用于 $t_2$ 的结果类型就是 $T_2$。

这是整章最重要的一条规则之一。
它精确表达了“函数调用必须类型匹配”。

5.5.4 布尔常量规则

$$\frac{}{\Gamma ⊢\mathbf{true}:\text{Bool}}\text{(True)}$$

$$\frac{}{\Gamma ⊢\mathbf{false}:\text{Bool}}\text{(False)}$$

这两条规则很简单：

• true 的类型是 Bool
• false 的类型也是 Bool

5.5.5 条件表达式规则

$$\frac{\Gamma ⊢t_1:\text{Bool}\Gamma ⊢t_2:T\Gamma ⊢t_3:T}{\Gamma ⊢\mathbf{if}{t}_1\mathbf{then}{t}_2\mathbf{else}{t}_3:T}\text{(If)}$$

这条规则说：

• 条件位置必须是布尔类型；
• 两个分支必须具有同一个类型；
• 整个 if 表达式的类型就是那个共同的类型。

最后这一点非常关键。因为程序运行时会走哪一个分支，取决于条件真假；所以如果两个分支类型不同，整个表达式就无法有一个统一的类型。

5.6 如何读类型规则？

对初学者来说，最容易出问题的地方不是规则本身，而是不知道应该从哪里看起。

一个实用方法是：

• 从下往上看：这条规则允许我推出什么结论？
• 从上往下看：为了得到这个结论，我需要先满足哪些前提？

例如看应用规则：

$$\frac{\Gamma ⊢t_1:T_1\to T_2\Gamma ⊢t_2:T_1}{\Gamma ⊢t_1{t}_2:T_2}\text{(App)}$$

你可以这样读：

• 想证明 t1 t2 的类型是 $T_2$
• 我就必须先证明：
  • t1 是一个函数，类型为 $T_1\to T_2$
  • t2 是它期望的参数类型 $T_1$

这就是“按规则反向构造推导”的基本思路。

5.7 一个完整的推导树示例

我们来证明：

$$⊢\lambda x:\text{Bool}.\lambda y:\text{Bool}.x:\text{Bool}\to \text{Bool}\to \text{Bool}$$

这个项的直觉含义是：

• 接收一个布尔值 x
• 再接收一个布尔值 y
• 返回第一个参数 x

5.7.1 证明思路

最外层是一个抽象，所以最后一步一定使用 (Abs)：

• 若要证明整个项的类型是 Bool → Bool → Bool
• 就需要在环境 x:Bool 下证明内层函数的类型是 Bool → Bool

内层仍然是抽象，再用一次 (Abs)：

• 若要证明 $\lambda y:\text{Bool}.x$ 的类型是 Bool → Bool
• 就需要在环境 x:Bool, y:Bool 下证明 x : Bool

最后这个结论由 (Var) 直接得到。

5.7.2 推导树

$$\frac{\frac{\frac{}{x:\text{Bool},y:\text{Bool}⊢x:\text{Bool}}\text{(Var)}}{x:\text{Bool}⊢\lambda y:\text{Bool}.x:\text{Bool}\to \text{Bool}}\text{(Abs)}}{⊢\lambda x:\text{Bool}.\lambda y:\text{Bool}.x:\text{Bool}\to \text{Bool}\to \text{Bool}}\text{(Abs)}$$

这个例子很重要，因为它展示了：

• 类型判断不是“拍脑袋决定”；
• 而是严格由规则一步步推出；
• 一棵推导树，就是“这个项确实有这个类型”的正式证据。

5.8 为什么有些项无法通过类型检查？

类型系统的力量，恰恰体现在它拒绝某些项。

来看这个项：

$$\mathbf{true}(\lambda x:\text{Bool}.x)$$

如果想用 (App) 规则给它判类型，就必须满足：

• 函数位置 true 的类型必须是某个函数类型 $T_1\to T_2$
• 参数位置 λx:Bool.x 的类型必须是 $T_1$

但问题在于：

$$\mathbf{true}:\text{Bool}$$

而不是某个函数类型。

所以这个项没有办法构造出合法的类型推导树。也就是说：

它在类型系统里根本不是良类型项。

这就是类型系统排除“把布尔值当函数使用”的方式。它不是等程序运行出错后再抱怨，而是在构造推导树这一步就卡住了。

5.9 从类型规则到类型检查

目前为止，我们写出的都是声明式规则（declarative typing rules）：

• 它们说明什么样的判断成立；
• 但还没有明确告诉你，编译器应当如何实现检查。

这里的“声明式规则”和“语法制导”也是后续章节会反复使用的关键词；若你想快速确认定义，可回查附录A中的“类型规则”“语法制导”“类型检查”等条目。

对 STLC 来说，这个实现过程相当直接，因为它的规则是语法制导（syntax-directed）的：

• 遇到变量，就查环境；
• 遇到抽象，就扩展环境并递归检查函数体；
• 遇到应用，就分别检查函数和参数，再判断是否匹配；
• 遇到 if，就检查条件是不是 Bool，并确认两个分支类型一致。

也就是说，这里要区分两层东西：

• 声明式规则回答“什么情况下判断成立”；
• 语法制导检查过程回答“编译器怎样沿语法树把这个判断算出来”。

在本章这个最小系统里，这两层非常接近；但到后面更复杂的系统中，它们未必总是完全重合。

这就是为什么 STLC 的类型检查是可判定的。它不是通过复杂搜索得到的，而是沿着语法树递归进行。

更准确地说：

STLC 的类型判断关系可以被实现为一个总会终止的检查算法。

这和后面第九章的“类型推断”不同。
本章是在已知注解的前提下做类型检查；第九章则会讨论在没有显式注解时，如何自动推断类型。

5.10 类型安全：本章真正要到达的地方

写出类型规则还不够。我们还要回答一个更重要的问题：

为什么这些规则真的能阻止程序卡住？

类型理论里最经典的答案是：类型安全 = 进展性 + 保持性。

5.10.1 进展性（Progress）

进展性（progress）说的是：

一个良类型的封闭项，要么已经是值，要么还可以继续求值。

形式上可写为：

$$\text{若 }⊢t:T\text{，则 }t\text{ 是值，或存在 }{t}^{\prime }\text{ 使得 }t⟶t^{\prime }$$

它排除了什么？
它排除的是“既不是值，又走不动”的情况，也就是卡住状态。

5.10.2 保持性（Preservation）

保持性（preservation）说的是：

如果一个项在求值前有类型 $T$，那么它求值一步之后，类型仍然是 $T$。

形式上可写为：

$$\text{若 }\Gamma ⊢t:T\text{ 且 }t⟶t^{\prime }\text{，则 }\Gamma ⊢t^{\prime }:T$$

它说明：

• 求值不会把一个良类型项“算坏”；
• 计算过程保持类型结构的一致性。

5.10.3 两者合起来意味着什么？

• 进展性保证：良类型程序不会卡住；
• 保持性保证：良类型程序在每一步计算后仍然良类型。

合起来就得到：

从一个良类型程序出发，整个计算过程始终不会掉进被类型系统禁止的坏状态。

这才是“良类型程序不会出错”这句话在形式化里的真正内容。

5.11 为什么保持性会依赖替换？

保持性的核心难点，其实来自第四章的 β-归约：

$$(\lambda x:T.t)v⟶[x\mapsto v]t$$

也就是说，函数应用真正做的事是：

• 把参数 v
• 替换进函数体 t
• 然后继续计算

因此，第五章的类型安全证明并不是凭空开始的，而是直接建立在：

• 第 3 章的替换与避免捕获的替换；
• 第 4 章的小步语义与“前进一步”的定义

之上。

因此，要证明保持性，通常需要一个关键引理：替换引理。

替换引理（substitution lemma）

$$\text{若 }\Gamma ,x:T_1⊢t:T_2\text{ 且 }\Gamma ⊢v:T_1\text{，则 }\Gamma ⊢[x\mapsto v]t:T_2$$

它的直觉含义是：

如果 t 在假设 x : T1 时是良类型的，而 v 本身确实是一个 T1 类型的值，那么把 v 替换给 x 之后，整体仍然保持原来的类型。

这正是第三章为什么要严肃定义“避免捕获的替换”的原因：
替换不仅是计算规则的一部分，也是类型安全证明的一部分。

5.12 一个小例子：类型安全如何发挥作用？

看下面这个项：

$$(\lambda x:\text{Bool}.x)\mathbf{true}$$

它显然是良类型的，类型为 Bool。

求值一步：

$$(\lambda x:\text{Bool}.x)\mathbf{true}⟶\mathbf{true}$$

此时：

• 原项类型是 Bool
• 求值后的结果仍然是 Bool

这体现了保持性。

同时，原项也不是卡住的：

• 它不是值；
• 但它可以继续归约一步。

这体现了进展性。

反过来看：

$$\mathbf{true}(\lambda x:\text{Bool}.x)$$

这个项没有类型，因此不在“类型安全”定理的适用范围内。类型安全不是说“所有项都不会卡住”，而是说：

所有良类型项都不会卡住。

这个限定一定要记住。

5.13 Church 风格、Curry 风格与本章的定位

前面已经提到，本章采用的是 Church 风格（Church-style）：

• 项里直接写类型注解；
• 我们做的是“检查”。

而在 Curry 风格（Curry-style）中：

• 项本身不携带类型注解；
• 需要依靠推断或外部规则给项指派类型。

例如：

• Church 风格：$\lambda x:\text{Bool}.x$
• Curry 风格：$\lambda x.x$

两者的差别，不只是“写没写注解”，更关系到：

• 类型检查是否直接；
• 是否需要类型推断；
• 能否得到最一般类型。

本章故意选择 Church 风格，不是因为它“更高级”，而是因为：

对入门阶段来说，它最能清楚展示“类型规则如何工作”。

第九章再讨论 Curry 风格和 Hindley–Milner 推断，会更自然。

5.14 Curry–Howard：为什么函数类型像逻辑蕴含？（选读）

这一节不是本章主线，但值得知道它的直觉。

在合适的构造性逻辑系统里，存在一种深刻对应：

• 类型对应命题；
• 项对应证明；
• 函数类型 $A\to B$ 对应逻辑蕴含 $A\Rightarrow B$。

为什么？

看抽象规则：

$$\frac{\Gamma ,x:T_1⊢t:T_2}{\Gamma ⊢\lambda x:T_1.t:T_1\to T_2}$$

它可以被读成：

• 假设 $T_1$ 成立；
• 在这个假设下构造出 $T_2$；
• 因而得到一个从 $T_1$ 到 $T_2$ 的函数。

这和逻辑里证明蕴含的结构非常像：

• 假设前件成立；
• 在此基础上推出后件；
• 因而得到“前件蕴含后件”。

最经典的例子是恒等函数：

$$\lambda x:A.x:A\to A$$

它对应逻辑中的平凡命题：

$$A\Rightarrow A$$

不过这里仍要保持边界感：
Curry–Howard 对应不是一句“所有类型系统都等于逻辑系统”就能概括完的。它成立于特定的形式系统中，而且具体对应关系依赖于所选语言与逻辑。

所以把它当作一种非常重要的理论视角是合适的，但不应在入门阶段把它说得过满。

5.15 本章小结

这一章真正建立起来的，是一条完整链条：

1. 程序可能卡住，而类型系统的目标是排除某类卡住状态。
2. 类型判断写作 $\Gamma ⊢t:T$，表示在某个环境下，项具有某种类型。
3. 本章对象语言是以 STLC 为核心、加入 Bool 与 if 的最小扩展语言。
4. 良类型项不等于“绝对正确”，但它们满足一个关键的安全保证。
5. 这个安全保证通常被分解为：
   • 进展性：不会卡住；
   • 保持性：求值不破坏类型。
6. 保持性之所以成立，核心之一在于第三章已经准备好的替换理论。

如果把本章压缩成一句话，那就是：

先用类型规则给项做静态分类，再用进展性与保持性说明：良类型程序不会落入被本系统禁止的坏状态。

如果你读完本章，已经能清楚回答下面三个问题，就说明抓住主线了：

• Γ ⊢ t : T 到底是什么意思？
• 为什么 (App) 规则能防止“把布尔值当函数用”？
• 为什么“类型安全”要拆成进展性和保持性？

回看导航

如果你读完本章后，想把这一章重新挂回全书主线，最推荐的回看顺序是：

1. 回看第 3 章：重新确认自由变量、替换、变量捕获与 α-重命名，因为保持性与替换引理都建立在这套基础之上。
2. 回看第 4 章：重新确认“值 / 范式 / 卡住”“小步语义 / 大步语义”的区别，因为类型安全正是建立在“程序如何前进”这层定义之上。
3. 配合附录A：重点查看“类型判断”“类型环境”“进展性”“保持性”“类型安全”“替换引理”等条目。
4. 配合附录B：重点确认 Γ ⊢ t : T、\vdash、函数类型箭头等记号。
5. 若你准备继续读第 6 章，可以带着一个问题往下看：
   • 当语言不只包含函数和布尔值，而开始加入积类型、和类型、递归类型、引用类型时，这套类型规则骨架会怎样扩展？

本章向后输出的核心内容是：

• Γ ⊢ t : T 这类类型判断的基本读法；
• 类型规则、类型检查与语法制导之间的关系；
• “类型安全 = 进展性 + 保持性”这条后续各章都会反复依赖的主线。

本章练习

1. 构造推导树，证明： $$f:\text{Bool}\to \text{Bool},x:\text{Bool}⊢fx:\text{Bool}$$

2. 说明为什么下面这个项无法通过类型检查： $$\mathbf{true}(\lambda x:\text{Bool}.x)$$

3. 构造推导树，证明： $$⊢\lambda x:\text{Bool}.\mathbf{if}x\mathbf{then}\mathbf{false}\mathbf{else}\mathbf{true}:\text{Bool}\to \text{Bool}$$

4. 用自然语言解释进展性和保持性的区别，并说明它们如何一起排除卡住状态。

5. 试着说明为什么下面这个说法不准确：
   “良类型程序一定不会出任何问题。”

下一章，我们会在 STLC 的基础上继续扩展语言，加入更丰富的类型构造，如积类型、和类型、递归类型和引用类型。到那时，你会看到：类型规则的基本思想并没有变，只是它所处理的语言构造变得越来越丰富。

第六章 一阶类型系统：基本类型构造

第六章 一阶类型系统：基本类型构造

阅读提示

本章会频繁使用“基础类型（base type）”“积类型（product type）”“和类型（sum type）”“记录类型（record type）”“递归类型（recursive type）”“引用类型（reference type）”等术语。若你在阅读时想快速回查定义与记号，建议配合：

• 附录A《术语表》中的 A.4“一阶类型构造相关术语”
• 附录B《符号速查表》中的“类型系统相关记号”

同时，本章直接建立在第 5 章的类型判断 Γ ⊢ t : T 之上；若你对“类型规则”“语法制导”“类型安全”的基本骨架还不稳，建议先回看第 5 章。

第五章建立了简单类型 Lambda 演算（STLC）的最小核心：变量、函数抽象、函数应用，以及最基本的类型判断与类型安全性质。但如果只停留在函数类型，语言的表达能力仍然非常有限——我们还不能自然地表示布尔值、数字、二元组、记录、列表、树，甚至也还没有办法讨论可变存储。

这一章的任务，就是在 STLC 的基础上逐步加入这些更接近真实语言的类型构造。

这里说的一阶类型系统（first-order type system），主要是指：

• 还没有引入对类型本身的量化（如 $\forall X.T$、$\exists X.T$）；
• 因而还没有进入参数化多态或存在类型；
• 但已经可以表达很多常见的数据结构与程序构造。

换句话说，这一章研究的是：

在不引入“类型层面的抽象与量化”之前，一个类型系统能扩展到什么程度？

在阅读本章时，还需要先固定一个形式化层级上的约定：

本章的重点是建立一阶类型构造的统一直觉与最小规则骨架，而不是把所有扩展都写成同一精度的完整形式系统。

更具体地说：

• 基础类型、积类型、引用类型会给出较直接的规则形状；
• 和类型会同时提示“教学上的简写”和“更严格的 Church 风格写法”之间的区别；
• 记录类型会以最小形式骨架为主，为第 8 章的结构子类型做准备；
• 递归类型会明确采用同构递归（iso-recursive）视角，而不是把递归展开直接并入类型相等。

本章既延续第 5 章“类型规则如何工作”的主线，也为第 7–10 章埋下几个关键伏笔：

• 第 7 章会继续讨论“对类型本身做抽象”；
• 第 8 章会回到记录与引用，讨论子类型与变化方向；
• 第 10 章则会进一步讨论：类型不仅描述“值是什么”，还描述“值怎样被使用”。

6.1 为什么要超出函数类型？

在 STLC 中，最核心的类型构造是函数类型：

$$T_1\to T_2$$

这当然很重要，因为函数是整个类型理论的核心对象。但如果一个语言只有函数类型，就会立刻遇到很多实际问题：

• 我们如何表示“真 / 假”？
• 如何表示“两个值的组合”？
• 如何表示“要么是这个，要么是那个”？
• 如何定义列表、树这样的递归结构？
• 如何讨论带状态的程序？

因此，从 STLC 走向更实际的类型系统，第一步通常不是“先加高级多态”，而是先加入这些最基本的数据构造。

这一章会按下面的顺序展开：

1. 基础类型
2. 积类型
3. 和类型
4. 记录类型
5. 递归类型
6. 可变引用

这些构造虽然看起来彼此分散，但它们背后有一条清晰主线：

类型系统不仅要给函数分类，还要给程序中出现的各种数据形态分类。

6.2 基础类型

最自然的扩展，是加入一些“原子性的”基础类型（base types），例如布尔值、自然数和单位类型。

6.2.1 基础类型的直觉

在 STLC 里，函数类型告诉我们：

• 一个项如果类型是 $T_1\to T_2$，
• 那么它应该接收一个 $T_1$ 类型的输入，
• 并产生一个 $T_2$ 类型的结果。

但现实程序里还有很多根本不是“函数”的值，例如：

• true、false
• 0、1、2
• “什么信息都不携带，只表示操作完成了”的值

因此，常见的一阶类型系统通常会引入如下基础类型：

其中最容易误解的是 Unit。
它不是“空值”，而是“恰好只有一个值的类型”。

你可以把它理解成：

• 这个值本身不携带有趣信息；
• 但“返回了一个 Unit 值”仍然是一件事情。

这和很多语言中的“过程调用完成了，但没有返回有用结果”的情况很接近。

6.2.2 一个简单的布尔系统

如果给 STLC 加上布尔值和条件表达式，可以得到如下语法扩展：

$$\begin{array}{rl}T& ::=\dots \mid \text{Bool}\\ t& ::=\dots \mid \text{true}\mid \text{false}\mid \text{if }{t}_1\text{ then }{t}_2\text{ else }{t}_3\end{array}$$

相应的类型规则是：

$$\frac{}{\Gamma ⊢\text{true}:\text{Bool}}\text{(T-True)}$$

$$\frac{}{\Gamma ⊢\text{false}:\text{Bool}}\text{(T-False)}$$

$$\frac{\Gamma ⊢t_1:\text{Bool}\Gamma ⊢t_2:T\Gamma ⊢t_3:T}{\Gamma ⊢\text{if }{t}_1\text{ then }{t}_2\text{ else }{t}_3:T}\text{(T-If)}$$

这里最重要的是 if 的规则：

• 条件部分必须是 Bool；
• 两个分支必须有相同类型；
• 整个 if 表达式的类型就是这个共同类型。

这条规则体现了一个非常典型的类型系统思想：

表达式的类型必须在运行前就能确定，而不能取决于运行时到底走了哪个分支。

如果你读到这里时，想快速确认 Bool、Nat、Unit、类型判断 Γ ⊢ t : T 等记号的含义，也可以顺手回查附录A和附录B中的对应条目。

6.2.3 关于 Nat 与机器整数

理论里的 Nat 一般表示数学意义上的自然数。
它和真实语言里的 int、i32、u64 并不完全一样。

更准确地说：

• Nat 常被用作一个理想化的、无限的自然数类型；
• 而真实语言里的机器整数通常是有位宽限制的；
• 因此它们会涉及溢出、符号位、底层表示等额外问题。

所以，把 Nat 理解成“和真实语言整数很像的理论近似”是可以的；但不要把二者完全等同。

6.2.4 与真实语言的对照

如果一定要做编程语言类比，更稳妥的说法是：

• Unit 在直觉上接近某些语言里的“无有趣返回值”；
• 但它不应简单等同于 null；
• 某些语言里的 void、某些函数式语言里的 unit，通常更接近这个概念。

6.3 积类型：把两个值放在一起

基础类型解决了“原子值”的分类问题，但程序里经常还需要把多个值组合在一起。例如：

• 一个人的名字和年龄；
• 一个函数返回两个结果；
• 一个节点保存一个值和一个子结构。

这就引出积类型（product type）。

6.3.1 直觉

积类型 $T_1\times T_2$ 表示：

一个值同时包含一个 $T_1$ 类型的部分和一个 $T_2$ 类型的部分。

最简单的例子就是二元组：

$$(t_1,t_2)$$

如果：

• $t_1$ 的类型是 $T_1$
• $t_2$ 的类型是 $T_2$

那么整个二元组的类型就是：

$$T_1\times T_2$$

6.3.2 语法与规则

语法可以扩展为：

$$\begin{array}{rl}T& ::=\dots \mid T_1\times T_2\\ t& ::=\dots \mid (t_1,t_2)\mid t.1\mid t.2\end{array}$$

对应的类型规则：

$$\frac{\Gamma ⊢t_1:T_1\Gamma ⊢t_2:T_2}{\Gamma ⊢(t_1,t_2):T_1\times T_2}\text{(T-Pair)}$$