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

第一章 数学基础

阅读提示

本章会频繁使用“集合”“关系”“归纳定义”“结构归纳法（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。