Practical Foundations for Programming Languages, Second Edition¶
本篇笔记大部分都是原书的翻译。仅引用块和 abstract 块是我自己的笔记内容。
第一部分：判断和规则¶
第一章：抽象语法¶
抽象语法（abstract syntax）也称为结构语法（structural syntax），考虑词组（phrase）的结构，它们如何有别的词组组成。在这一层次，词组是一棵树，节点是将多个词组组合在一起的操作符（operator）。
语法的绑定（binding）结构引入了标识符（identifier），考虑它们如何声明和使用。在这一层次，词组视为抽象绑定树（abstract binding tree）。
本节分两部分：
- 定义抽象语法树
- 介绍标识符绑定和作用域（scope）的规则
接下来将会在 ABT 上精确定义一些函数和关系，来阐明绑定和作用域的精确含义。这两个概念难以正确定义，通常是语言实现者产生错误的地方。
抽象语法树¶
Abstract
- 定义：
- 范畴 \(s\)、范畴集合 \(S\)、运算符 \(o\)、运算符集族 \(O\)、变量 \(x\)、变量集 \(X\)、变量集族 \(X_s\)
- 抽象语法树 \(a\)、抽象语法树家族 \(A[X]\)
- 添加范畴 \(X, x\)
- 替换 \([b/x]a\)
- 应用：
- 结构归纳法
- 定理：
- 替换的良定义
通常情况下，应用结构归纳原理时，会考虑将变量解释为合适范畴的抽象语法树 (AST) 的占位符。非正式地讲，在证明涉及变量的 AST 性质时，通常有用的是以变量满足某种性质为前提，来证明 AST 的某个性质。这样做的目的是预期这些变量将被具有该性质的 AST 替换，从而替换后的结果也会保持该性质。这相当于将结构归纳原理应用于某种形式的性质 \(P(a)\)，即“如果 \(a\) 包含变量 \(x_1, \dots, x_k\)，并且每个 \(x_i\) 都满足性质 \(Q\)，那么 \(a\) 也满足 \(Q\)”。因此，通过结构归纳证明所有 AST \(a\) 的 \(P(a)\)，实际上就是在假设 \(Q\) 对这些变量成立的情况下，证明 \(Q(a)\) 对所有 AST \(a\) 都成立。当没有变量时，不存在任何假设，证明 \(P\) 就是证明 \(Q\) 对所有封闭的 AST 都成立。另一方面，如果 \(a\) 中的变量 \(x\) 被满足性质 \(Q\) 的 AST \(b\) 替换，那么在 \(a\) 中将 \(x\) 替换为 \(b\) 的结果也将满足性质 \(Q\)。
为了精确起见，我们现在给出这些概念的准确定义。设 \(S\) 为一个有限的范畴集合。对于给定的范畴集合 \(S\)，一个算子的元数（arity）形式为 \((s_1, \dots, s_n)s\)，表示该算子取 \(n \geq 0\) 个参数，每个参数的范畴为 \(s_i \in S\)，且算子的范畴为 \(s \in S\)。令 \(O = \{ O_\alpha \}\) 为一组按元数 \(\alpha\) 索引的不交算子集 \(O_\alpha\)，其中每个算子具有元数 \(\alpha\)。如果 \(o\) 是元数为 \((s_1, \dots, s_n)s\) 的算子，我们称 \(o\) 的范畴为 \(s\)，且它有 \(n\) 个参数，其范畴分别为 \(s_1, \dots, s_n\)。
固定一个范畴集合 \(S\) 和一个按元数索引的运算符集族 \(O\)，每个运算符集对应不同的元数。令 \(X = \{ X_s \}_{s \in S}\) 为按范畴索引的变量集族，每个变量集 \(X_s\) 是一个属于范畴 \(s\) 的不相交有限变量集。当上下文清楚时，如果 \(x \in X_s\)，我们称变量 \(x\) 属于范畴 \(s\)。如果 \(x\) 对于 \(X\) 是新的，即 \(x \notin X_s\)（对任何范畴 \(s\) 都不在其变量集中），我们就说 \(x\) 对于 \(X\) 是“新鲜”的，或者在已知 \(X\) 的情况下，直接称 \(x\) 为“新鲜”的。如果 \(x\) 对于 \(X\) 是新鲜的且 \(s\) 是一个范畴，那么 \(X, x\) 表示通过将 \(x\) 添加到 \(X_s\) 中得到的变量集族。该符号具有一定的歧义性，因为范畴 \(s\) 没有明确给出，而是从上下文中确定的。
抽象语法树的定义
抽象语法树（AST）家族 \(A[X] = \{ A[X]_s \}_{s \in S}\) 是满足以下条件的最小集合：
- 属于范畴 \(s\) 的变量是范畴 \(s\) 的抽象语法树：如果 \(x \in X_s\)，则 \(x \in A[X]_s\)。
- 运算符可以组合抽象语法树：如果 \(o\) 是一个元数为 \((s_1, \dots, s_n)s\) 的运算符，并且 \(a_1 \in A[X]_{s_1}, \dots, a_n \in A[X]_{s_n}\)，则 \(o(a_1; \dots; a_n) \in A[X]_s\)。
根据这个定义，可以应用结构归纳原理来证明某个性质 \(P\) 对每个抽象语法树都成立。要证明 \(P(a)\) 对所有 \(a \in A[X]\) 成立，只需证明：
结构归纳法
- 如果 \(x \in X_s\)，则 \(P_s(x)\) 成立。
- 如果 \(o\) 的元数为 \((s_1, \dots, s_n)s\)，且 \(P_{s_1}(a_1)\)、\(\dots\)、\(P_{s_n}(a_n)\) 成立，则 \(P_s(o(a_1; \dots; a_n))\) 成立。
例如，通过结构归纳法很容易证明，当 \(X \subseteq Y\) 时，\(A[X] \subseteq A[Y]\)。
变量的意义通过替换来赋予。如果 \(a \in A[X, x]_{s'}\)，且 \(b \in A[X]_s\)，则 \([b/x]a \in A[X]_{s'}\) 表示将 \(b\) 替换 \(a\) 中每个出现的 \(x\) 的结果。此时，抽象语法树 \(a\) 被称为替换的目标，\(x\) 被称为替换的对象。替换由以下方程定义：
抽象语法树中替换的定义
- \([b/x]x = b\) 且 \([b/x]y = y\)（如果 \(x \neq y\)）。
- \([b/x]o(a_1; \dots; a_n) = o([b/x]a_1; \dots; [b/x]a_n)\)。
例如，我们可以验证：\([\text{num}[2]/x]\text{plus}(x; \text{num}[3]) = \text{plus}(\text{num}[2]; \text{num}[3])\)
我们可以通过结构归纳法证明抽象语法树上的替换是良定义的。
定理 1.1 替换的良定义
定理 1.1：如果 \(a \in A[X, x]\)，那么对于每个 \(b \in A[X]\)，存在唯一的 \(c \in A[X]\)，使得 \([b/x]a = c\)。
证明：通过对 \(a\) 进行结构归纳。如果 \(a = x\)，则根据定义 \(c = b\)；如果 \(a = y \neq x\)，则根据定义 \(c = y\)。否则，\(a = o(a_1, \dots, a_n)\)，根据归纳假设，存在唯一的 \(c_1, \dots, c_n\)，使得 \([b/x]a_1 = c_1\) 以及 \([b/x]a_n = c_n\)。因此，根据替换的定义，\(c\) 为 \(c = o(c_1; \dots; c_n)\)。
抽象绑定树¶
Abstract
- 定义：
- 绑定 \(\text{let}(a_1; x.a_2)\)
抽象绑定树（ABT）是在抽象语法树（AST）的基础上进行扩展的，用来引入新的变量和符号，这种引入称为绑定，并具有一个特定的作用范围，称为其作用域。绑定的作用域是一个 ABT，在该范围内被绑定的标识符可以被使用，或者作为占位符（在变量声明的情况下），或者作为某个运算符的索引（在符号声明的情况下）。因此，在 ABT 的某个子树中，活动标识符的集合可能比其外部树中的更大。此外，不同的子树可能引入具有不相交作用域的标识符。关键原则是，标识符的任何使用都应被理解为对其绑定的引用或抽象指针。由此产生的一个结果是，标识符的选择并不重要，只要我们始终可以将每次标识符的使用唯一地关联到其绑定即可。
作为一个激励性的例子，考虑表达式 \(\texttt{ let } x \texttt{ be } 7 \texttt{ in } x + x\)。这个表达式引入了一个变量 \(x\)，该变量在表达式 \(x + x\) 中表示 \(7\)。变量 \(x\) 由 \(\texttt{ let }\) 表达式绑定，仅在 \(x + x\) 内部使用；任何在 \(7\) 中对 \(x\) 的使用都指代一个不同的变量，即使它恰好具有相同的名称。另一方面，表达式 \(\texttt{ let } x \texttt{ be } x \times x \texttt{ in } x + x\) 中，乘法中的 \(x\) 指代的是 \(\texttt{ let }\) 引入的绑定，而加法中的 \(x\) 指代的是某个外部绑定（这里未展示）。
被绑定变量的名称并不重要，只要它们指向相同的绑定。
例如，表达式 \(\texttt{ let } x \texttt{ be } x \times x \texttt{ in } x + x\) 也可以写作 \(\texttt{ let } y \texttt{ be } x \times x \texttt{ in } y + y\)，而不会改变其含义。在前一种情况下，加法中的变量 \(x\) 被绑定，而在后一种情况下，被绑定的是变量 \(y\)，但“指针结构”保持不变。另一方面，表达式 \(\texttt{ let } x \texttt{ be } y \times y \texttt{ in } x + x\) 与前两者的含义不同，因为乘法中的变量 \(y\) 此时指向的是一个不同的外部变量。
重命名被绑定变量的约束在于，它不能改变表达式的引用结构。
例如，表达式 \(\texttt{ let } x \texttt{ be } 2 \texttt{ in } \texttt{ let } y \texttt{ be } 3 \texttt{ in } x + x\) 与表达式 \(\texttt{ let } y \texttt{ be } 2 \texttt{ in } \texttt{ let } y \texttt{ be } 3 \texttt{ in } y + y\) 含义不同，因为在第二个表达式中，加法中的 \(y + y\) 引用了内部的声明，而不像第一个表达式那样引用外部的声明。
抽象语法树（AST）的概念可以通过引入变量的绑定和作用域来进行扩展。这些扩展后的 AST 称为抽象绑定树（ABT）。ABT 扩展了 AST 的概念，通过允许一个运算符在每个参数中绑定任意数量（可能为零）的变量。
抽象器的定义
运算符的一个参数称为抽象器，其形式为 \(x_1, \dots, x_k .a\)。其中，变量序列 \(x_1, \dots, x_k\) 在 ABT \(a\) 中被绑定。（当 \(k\) 为零时，我们省略抽象器中的点，直接写作 \(a\)）。
绑定的 ABT 写法
以 ABT 的形式书写，表达式 \(\texttt{ let } x \texttt{ be } a_1 \texttt{ in } a_2\) 的形式是 \(\texttt{ let }(a_1; x.a_2)\)，这更清楚地指定了变量 \(x\) 是在 \(a_2\) 中绑定的，而不是在 \(a_1\) 中。我们常用 \(\vec{x}\) 来表示一个有限的、不同的变量序列 \(x_1, \dots, x_n\)，并用 \(\vec{x}.a\) 表示 \(x_1, \dots, x_n .a\)。
广义元数和价位的定义
为了处理绑定，运算符被赋予形式为 \((\nu_1, \dots, \nu_n)s\) 的广义元数，这表示范畴为 \(s\) 的运算符具有 \(n\) 个参数，每个参数的价位分别为 \(\nu_1, \dots, \nu_n\)。通常，价位 \(\nu\) 具有形式 \(s_1, \dots, s_k .s\)，这指定了一个参数的范畴以及在该参数中绑定的变量的数量和范畴。
我们说变量序列 \(\vec{x}\) 的范畴为 \(\vec{s}\)，意味着这两个序列的长度 \(k\) 相同，并且对于每个 \(1 \leq i \leq k\)，变量 \(x_i\) 的范畴为 \(s_i\)。
Example
因此，指定运算符 \(\texttt{let}\) 的元数为 \((\mathsf{Exp}, \mathsf{Exp}.\mathsf{Exp})\mathsf{Exp}\) 表示它是一个范畴为 \(\mathsf{Exp}\) 的运算符，其第一个参数的范畴为 \(\mathsf{Exp}\)，并且不绑定任何变量；第二个参数也是 \(\mathsf{Exp}\) 的范畴，并在其中绑定一个 \(\mathsf{Exp}\) 范畴的变量。非正式表达式 \(\texttt{let } x \texttt{ be } 2 \texttt{ in } x + x\) 可以写作 ABT 形式 \(\texttt{let}(\texttt{num}[2]; x.\texttt{plus}(x; x))\)。其中运算符 \(\texttt{let}\) 具有两个参数，第一个是表达式，第二个是一个抽象器，它绑定了一个表达式变量。
固定一个范畴集合 \(S\) 和一个按广义元数索引的互不相交的运算符集族 \(O\)。对于给定的互不相交的变量集族 \(X\)，抽象绑定树（ABT）家族 \(B[X]\) 的定义类似于 \(A[X]\)，但不同的是，\(X\) 在定义过程中不是固定不变的，而是随着进入抽象器的作用域而变化。
这个简单的概念在精确定义上意外地困难。对其定义的初步尝试是作为满足以下条件的最小集合族：
抽象绑定树的初步定义
- 如果 \(x \in X_s\)，则 \(x \in B[X]_s\)。
- 对于每个元数为 \((\vec{s_1}.s_1, \dots, \vec{s_n}.s_n)s\) 的运算符 \(o\)，如果 \(a_1 \in B[X, \vec{x_1}]_{s_1}, \dots, a_n \in B[X, \vec{x_n}]_{s_n}\)，则 \(o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n) \in B[X]_s\)。
绑定变量被附加到每个参数的活动变量集合中，每个变量的范畴由运算符的价位决定。
这个定义几乎是正确的，但未能正确处理绑定变量的重命名。按照这个定义，形如 \(\texttt{let } x \texttt{ be } 2 \texttt{ in } \texttt{let } x \texttt{ be } 3 \texttt{ in } x + x\) 的 ABT 是合法的，因为第一个 \(\texttt{let}\) 绑定的 \(x\) 与第二个 \(\texttt{let}\) 绑定的 \(x\) 是不同的。但是，这个 ABT 的意义是不明确的，因为两个绑定变量具有相同的名称，这可能会导致混淆。为了避免这种混淆，我们需要确保每个参数都是合法的，无论绑定变量名称的选择如何。这通过使用新的重命名来实现，新的重命名是变量序列之间的双射。
重命名的定义
具体来说，相对于 \(X\) 的一个有限变量序列 \(\vec{x}\) 的新的重命名是一个双射 \(\rho : \vec{x} \leftrightarrow \vec{x'}\)，其中 \(\vec{x'}\) 对 \(X\) 是新的。我们用 \(\hat{\rho}(a)\) 表示将 \(a\) 中每个 \(x_i\) 替换为其新的对应变量 \(\rho(x_i)\) 的结果。
这通过使用新的重命名来修改 ABT 定义的第二条规则实现，如下所示：
抽象绑定树的精确定义
对于每个元数为 \((\vec{s_1}.s_1, \dots, \vec{s_n}.s_n)s\) 的运算符 \(o\)，如果对于每个 \(1 \leq i \leq n\) 和每个新的重命名 \(\rho_i : \vec{x_i} \leftrightarrow \vec{x'_i}\)，我们有 \(\hat{\rho_i}(a_i) \in B[X, \vec{x'_i}]\)，则 \(o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n) \in B[X]_s\)。
重命名 \(\hat{\rho_i}(a_i)\) 确保了不会发生冲突，并且 ABT 对几乎所有的绑定变量的重命名都是有效的。
结构归纳原理可以扩展到抽象绑定树（ABT），这种扩展称为“结构归纳模新重命名”。它表明，为了证明 \(P[X](a)\) 对于每个 \(a \in B[X]\) 都成立，只需证明以下条件即可：
- 如果 \(x \in X_s\)，则 \(P[X]_s(x)\) 成立。
- 对于每个元数为 \((\vec{s_1}.s_1, \dots, \vec{s_n}.s_n)s\) 的运算符 \(o\)，如果对于每个 \(1 \leq i \leq n\)，对于每个新重命名 \(\rho_i : \vec{x_i} \leftrightarrow \vec{x'_i}\)（其中 \(\vec{x'_i} \notin X\)），有 \(P[X, \vec{x'_i}]_{s_i}(\hat{\rho_i}(a_i))\) 成立，则 \(P[X]_s(o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n))\) 也成立。
第二个条件确保归纳假设对所有新选择的绑定变量名称都成立，而不仅仅是 ABT 中实际给出的那些名称。
作为一个例子，我们定义判断 \(x \in a\)，其中 \(a \in B[X, x]\)，表示 \(x\) 在 \(a\) 中自由出现。非正式地，这意味着 \(x\) 在 \(a\) 外部某处被绑定，而不是在 \(a\) 本身内部。如果 \(x\) 在 \(a\) 内部被绑定，则这些 \(x\) 的出现与绑定外部的那些出现不同。以下定义确保了这一点：
判断 \(x \in a\) 的定义
- \(x \in x\)。
- \(x \in o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n)\) 如果存在 \(1 \leq i \leq n\)，对于每个新的重命名 \(\rho : \vec{x_i} \leftrightarrow \vec{z_i}\)，我们有 \(x \in \hat{\rho}(a_i)\)。
第一个条件声明 \(x\) 在 \(x\) 中是自由的，但在任何变量 \(y\)（除了 \(x\) 之外）中不是自由的。第二个条件声明，如果 \(x\) 在某个参数中是自由的，无论该参数中的绑定变量名称如何选择，那么它在整个 ABT 中也是自由的。
\(\alpha\)-等价的定义
关系 \(a =_\alpha b\)（称为 \(\alpha\)-等价，因历史原因）表示 \(a\) 和 \(b\) 在绑定变量名称选择上是相同的。\(\alpha\)-等价关系是包含以下两个条件的最强同余关系：
- \(x =_\alpha x\)。
- \(o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n) =_\alpha o(\vec{x'_1}.a'_1; \dots; \vec{x'_n}.a'_n)\) 如果对于每个 \(1 \leq i \leq n\)，\(\hat{\rho_i}(a_i) =_\alpha \hat{\rho'_i}(a'_i)\) 对于所有新的重命名 \(\rho_i : \vec{x_i} \leftrightarrow \vec{z_i}\) 和 \(\rho'_i : \vec{x'_i} \leftrightarrow \vec{z_i}\)。
这个想法是我们一致地重命名 \(\vec{x_i}\) 和 \(\vec{x'_i}\)，以避免混淆，并检查 \(a_i\) 和 \(a'_i\) 是否是 \(\alpha\)-等价的。如果 \(a =_\alpha b\)，则 \(a\) 和 \(b\) 是对方的 \(\alpha\)-变体。
在定义将一个 ABT \(b\)（其类型为 \(s\)）替换到另一个 ABT \(a\) 的某个变量 \(x\)（其类型为 \(s\)）的自由出现位置时（记作 \([b/x]a\)），需要小心。替换的部分定义如下：
ABT 中替换的定义
- \([b/x]x = b\)，而 \([b/x]y = y\)（如果 \(x \neq y\)）。
- \([b/x]o(\vec{x_1}.a_1; \dots; \vec{x_n}.a_n) = o(\vec{x_1}.a'_1; \dots; \vec{x_n}.a'_n)\)，其中，对于每个 \(1 \leq i \leq n\)，我们要求 \(\vec{x_i} \notin b\)，并且设置 \(a'_i = [b/x]a_i\) 如果 \(x \notin \vec{x_i}\)，否则 \(a'_i = a_i\)。
定义 \([b/x]a\) 是相当精细的，需要仔细考虑。
替换的一个问题是，如果 \(x\) 在 \(a\) 内部由抽象器绑定，则 \(x\) 在抽象器内部不会出现为自由变量，因此不会被替换。
例如，\([b/x] \text{let}(a_1; x.a_2) = \texttt{let}([b/x]a_1; x.a_2)\)，因为在 \(x.a_2\) 中没有 \(x\) 的自由出现。
另一个问题是替换过程中可能会捕获到 \(b\) 中的自由变量。
例如，如果 \(y \in b\) 且 \(x \neq y\)，则 \([b/x] \texttt{let}(a_1; y.a_2)\) 是未定义的，而不是 \(\texttt{let}([b/x]a_1; y.[b/x]a_2)\)，这可能在初看时会有所误解。
例如，给定 \(x \neq y\)，\([y/x] \texttt{let}(\text{num}[0]; y.\text{plus}(x; y))\) 是未定义的，而不是 \(\texttt{let}(\text{num}[0]; y.\text{plus}(y; y))\)，因为这混淆了两个不同的变量 \(y\)。
尽管避免捕获（capture avoidance）是替换的一个基本特征，但在某种意义上，它仅仅是一个技术上的麻烦。如果绑定变量的名称没有实际意义，那么可以通过首先重命名 \(a\) 中的绑定变量来避免 \(b\) 中的任何自由变量，从而总是能够避免捕获。在前面的例子中，如果我们将绑定变量 \(y\) 重命名为 \(y'\)，得到 \(a' = \texttt{let}(\text{num}[0]; y'.\text{plus}(x; y'))\)，那么 \([b/x]a'\) 是定义好的，且等于 \(\texttt{let}(\text{num}[0]; y'.\text{plus}(b; y'))\)。以这种方式避免捕获的代价是，替换仅在 \(\alpha\)-等价下确定，因此我们可能不再将替换视为一个函数，而只能视为一个适当的关系。
为了恢复替换的函数特性，采用以下识别约定是足够的：
识别约定
抽象绑定树（ABTs）总是按 \(\alpha\)-等价（\(\alpha\)-equivalence）来识别。
也就是说，\(\alpha\)-等价的 ABT 被视为相同。替换可以扩展到 ABT 的 \(\alpha\)-等价类，以避免捕获，通过选择 ABT 的等价类的代表，从而使得替换是定义良好的，然后形成结果的等价类。任何两个替换定义良好的代表选择都将给出 \(\alpha\)-等价的结果，因此替换变成一个定义明确的全函数。在本书中，我们将采用 ABT 的识别约定。
我们经常需要考虑那些其抽象语法不能通过固定的操作符集合来指定的语言，而是需要操作符对其出现的上下文敏感。
符号的定义
为了我们的目的，我们将考虑一组符号参数，或称为符号，这些符号索引操作符的家族，从而在符号集变化时，操作符集也会变化。一个索引操作符 \(o\) 是一个由符号 \(u\) 索引的操作符家族，当 \(u\) 是一个可用符号时，\(o[u]\) 是一个操作符。
如果 \(U\) 是一个有限的符号集，那么 \(B[U; X]\) 是按照之前的方式生成的按类型索引的 ABTs 家族，接受所有符号 \(u \in U\) 的索引操作符实例。
虽然变量是一个占位符，代表其类型的未知 ABT，但符号本身并不代表任何东西，也不是一个 ABT。符号的唯一意义在于它是否与另一个符号相同或不同；操作符实例 \(o[u]\) 和 \(o[u']\) 只有在 \(u\) 和 \(u'\) 相同时才相同，即当 \(u\) 和 \(u'\) 是相同的符号时，操作符实例才相同。
符号集通过在作用域内引入新的或“新鲜的”符号来扩展，这使用抽象符号 \(u.a\)，该抽象符号在 ABT \(a\) 中绑定了符号 \(u\)。抽象符号在某种意义上是“新”的，就像抽象变量一样：绑定符号的名称可以随意变化，只要不产生冲突。这种重命名属性确保了抽象符号在作用域内是唯一的。
符号与变量的区别
符号和变量之间的唯一区别在于对符号的唯一操作是重命名；对于符号，没有替换的概念。
最后，关于符号表示法的一点说明：为了提高可读性，我们通常会对操作符的参数进行“分组”和“分阶段”处理，使用圆括号和花括号来显示分组，并且一般认为阶段从右到左进行。所有在一个组中的参数被认为是在相同的阶段出现的，尽管它们的顺序是有意义的，而连续的组被认为是在顺序的阶段中出现的。分阶段和分组通常是一个有用的记忆工具，但没有根本意义。例如，ABT \(o\{a1; a2\}(a3; x.a4)\) 与 \(o(a1; a2; a3; x.a4)\) 是相同的，任何其他保持顺序的分组或分阶段方法也会得到相同的结果。
第二章：归纳定义¶
归纳定义是编程语言研究中不可或缺的工具。在本章中，我们将建立归纳定义的基本框架，并给出其一些应用实例。归纳定义由一组用于推导各种形式的判断或断言的规则组成。判断是关于某种抽象绑定树的一个或多个的陈述。这些规则规定了判断有效的必要和充分条件，从而完全确定了其含义。
判断¶
我们首先介绍关于抽象绑定树的判断（或断言）的概念。我们将使用多种形式的判断，其中包括以下示例：
- \(n \text{ nat}\) 表示 \(n\) 是一个自然数
- \(n_1 + n_2 = n\) 表示 \(n\) 是 \(n_1\) 和 \(n_2\) 的和
- \(\tau \text{ type}\) 表示 \(\tau\) 是一种类型
- \(e : \tau\) 表示表达式 \(e\) 的类型是 \(\tau\)
- \(e \Downarrow v\) 表示表达式 \(e\) 的值为 \(v\)
一个判断声明一个或多个抽象绑定树具有某种属性或彼此之间存在某种关系。属性或关系本身被称为判断形式，而对象具有该属性或存在该关系的判断则称为该判断形式的一个实例。判断形式也称为谓词，而构成实例的对象称为其主体。我们用 \(a \ J\) 或 \(J \ a\) 来表示断言判断 \(J\) 对抽象绑定树 \(a\) 成立。相应地，有时我们用 \(- J\) 或 \(J -\) 来表示判断形式 \(J\)，其中破折号表示 \(J\) 没有具体的参数。当判断的主体不重要时，我们用 \(J\) 来代表未指定的判断，即某个判断形式的实例。对于特定的判断形式，我们可以自由地使用前缀、后缀或混合表示法，如上例所示，以增强可读性。
推理规则¶
判断形式的归纳定义由一组形式为：
的规则组成，其中 \(J\) 和 \(J_1, \dots, J_k\) 都是所定义的判断形式。水平线以上的判断称为规则的前提，水平线以下的判断称为其结论。如果一个规则没有前提（即 \(k\) 为零），该规则称为公理；否则，称为适当的规则。
推理规则可以理解为前提对于得出结论是充分的：要证明 \(J\)，只需要证明 \(J_1, \dots, J_k\)。当 \(k\) 为零时，规则表示其结论无条件成立。请记住，通常可能存在多个具有相同结论的规则，每个规则都为结论提供充分条件。因此，如果某个规则的结论成立，并不意味着该规则的前提必须成立，因为它可能是由另一条规则推导出来的。
Example
例如，以下规则构成了判断形式 \(- \text{nat}\) 的归纳定义：
这些规则指定了当 \(a\) 为零，或 \(a\) 为 \(\text{succ}(b)\) 且 \(b\) 对于某个 \(b\) 满足 \(\text{nat}\) 时，\(a \text{ nat}\) 成立。将这些规则视为完整的，可以得出 \(a \text{ nat}\) 当且仅当 \(a\) 是一个自然数。
Example
类似地，以下规则构成了判断形式 \(- \text{tree}\) 的归纳定义：
这些规则表明，当 \(a\) 是 \(\text{empty}\)，或 \(a\) 是 \(\text{node}(a_1 ; a_2)\) 且 \(a_1 \text{ tree}\) 和 \(a_2 \text{ tree}\) 时，\(a \text{ tree}\) 成立。将这些规则视为完整的，它们表示 \(a\) 是一棵二叉树，即它要么是空树，要么是由两个子节点组成的节点，而每个子节点也是二叉树。
判断形式 \(a \text{ is } b\) 表示两个抽象绑定树 \(a\) 和 \(b\) 的相等性，其中 \(a \text{ nat}\) 且 \(b \text{ nat}\)，其归纳定义由以下规则给出：
在前面的例子中，我们使用了一种符号惯例，通过有限数量的模式或规则方案指定无限多的规则。例如，规则 (2.2b) 是一个规则方案，它为规则中的每个对象 \(a\) 确定了一条规则，称为规则方案的实例。我们将依赖上下文来判断一条规则是针对特定对象 \(a\) 还是作为一个规则方案，进而为规则中的每个对象提供相应的规则。
一组规则被认为定义了在这些规则下闭合或遵守这些规则的最强判断形式。对规则闭合意味着这些规则足以证明判断的有效性：如果有办法通过给定的规则得到 \(J\)，则 \(J\) 成立。作为最强判断形式，规则是必要的：\(J\) 仅当通过应用规则能够得到时才成立。规则的充分性意味着我们可以通过组合规则来推导出 \(J\) 的成立。而规则的必要性则意味着我们可以使用规则归纳对其进行推理。
推导¶
要证明一个归纳定义的判断成立，展示其推导过程就足够了。判断的推导是规则的有限组合，开始于公理，结束于该判断。可以将其看作一个树结构，其中每个节点代表一个规则，而其子节点是该规则前提的推导过程。我们有时会说，某个判断 \(J\) 的推导是该归纳定义的判断 \(J\) 成立的证据。
通常，我们将推导描绘成一棵树，结论位于底部，而规则的前提作为证据出现在该节点的上方。因此，如果
是一个推理规则，并且 \(\bigtriangledown_1, \dots, \bigtriangledown_k\) 是其前提的推导过程，那么
就是其结论的推导。特别地，当 \(k = 0\) 时，节点没有子节点。
Example
例如，以下是 \(\text{succ}(\text{succ}(\text{succ}(\text{zero}))) \text{ nat}\) 的一个推导过程：
Example
类似地，下面是 \(\text{node}(\text{node}(\text{empty}; \text{empty}); \text{empty}) \text{ tree}\) 的一个推导过程：
为了证明一个归纳定义的判断是可推导的，我们只需要找到一个推导过程。寻找推导的主要方法有两种，分别称为前向推导（或自下而上的构造）和后向推导（或自上而下的构造）。前向推导从公理开始，朝着所需的结论逐步推进，而后向推导则从目标结论出发，向后追溯到公理。
更具体地说，前向推导的搜索方法会维护一组可推导的判断，并通过添加所有前提已在该集合中的推理规则的结论，持续扩展这一集合。最初，该集合为空；当所需的判断出现在集合中时，过程结束。假设在每个阶段都考虑了所有规则，那么前向推导最终会找到任何可推导判断的推导过程，但通常无法通过算法确定何时应该停止扩展集合，并得出所需判断不可推导的结论。我们可能会不断地将更多判断添加到可推导集合中，却始终无法实现预期目标。要判断给定的判断是否不可推导，必须理解规则的全局特性。
前向推导是无目标指向的，因为在每一步决定如何继续时，它并不考虑最终目标。相比之下，后向推导是目标导向的。后向推导的搜索方法会维护一个当前目标的队列，这些是需要寻找推导过程的判断。最初，该队列仅包含我们希望推导的判断。在每个阶段，我们从队列中移除一个判断，并考虑所有以该判断为结论的推理规则。对于每个这样的规则，我们将该规则的前提添加到队列的末尾，然后继续。如果有多条符合条件的规则，这个过程必须为每个候选规则重复，使用相同的初始队列。该过程在队列为空时终止，所有目标都已实现；此过程中可以丢弃对候选规则的任何未完成的考虑。和前向推导一样，后向推导最终也会找到任何可推导判断的推导过程，但通常没有算法可以确定当前目标是否可推导。如果不可推导，我们可能徒劳地将更多判断添加到目标集合中，永远无法满足所有目标。
规则归纳¶
由于归纳定义指定了在一组规则下封闭的最强判断形式，我们可以通过规则归纳对它们进行推理。规则归纳原理表明，要证明某个性质 \( P \) 在 \( J \) 可导时成立，只需证明 \( P \) 在定义判断形式 \( J \) 的规则下是封闭的或遵守这些规则。
更具体地说，性质 \( P \) 遵守如下规则：
如果当 \( P(a_1), \dots, P(a_k) \) 成立时，\( P(a) \) 也成立。假设 \( P(a_1), \dots, P(a_k) \) 被称为归纳假设，而 \( P(a) \) 被称为推理的归纳结论。
规则归纳原理只是归纳定义的表达形式，它说明通过一组规则定义的判断形式是最强的、在这些规则下封闭的形式。因此，规则归纳定义的判断形式有两个特性：(a) 在这些规则下封闭，即通过规则推导出的结论是有效的；(b) 足以用于推理其他在规则下也封闭的性质。这意味着推导出的判断是判断有效性的证据，同时我们可以通过规则归纳推理关于归纳定义的判断形式。
对于规则 (2.2)，规则归纳原理表明，要证明 \( P(a) \) 在 \( a \) 为自然数时成立，只需证明：
- \( P(zero) \)。
- 对任意 \( a \)，如果 \( P(a) \) 成立，则 \( P(succ(a)) \) 也成立。
这些条件的充分性是我们熟悉的数学归纳法原理。同样，对于规则 (2.3)，规则归纳法表明，要证明 \( P(a) \) 在 \( a \) 为树时成立，只需证明：
- \( P(empty) \)。
- 对任意 \( a_1 \) 和 \( a_2 \)，如果 \( P(a_1) \) 和 \( P(a_2) \) 成立，则 \( P(node(a_1; a_2)) \) 也成立。
这些条件的充分性被称为树归纳原理。
我们还可以通过规则归纳证明，自然数的前驱也是自然数。尽管这看起来显而易见，但这个例子展示了如何从基本原则推导出这一结论。
引理 2.1：自然数的后继还是自然数
引理 2.1 如果 \( succ(a) \) 是自然数，则 \( a \) 也是自然数。
证明 我们只需证明性质 \( P(a) \)，即如果 \( a \) 是自然数且 \( a = succ(b) \)，则 \( b \) 是自然数，该性质遵守规则 (2.2)。
- 规则 (2.2a)：显然 \( zero \) 是自然数，且第二个条件空成立，因为 \( zero \) 不是 \( succ(-) \) 的形式。
- 规则 (2.2b)：归纳假设下，我们知道 \( a \) 是自然数，且如果 \( a \) 是 \( succ(b) \) 的形式，则 \( b \) 是自然数。我们要证明 \( succ(a) \) 是自然数，这是显然的；且如果 \( succ(a) \) 是 \( succ(b) \) 的形式，则 \( b \) 是自然数，根据归纳假设，\( b \) 是自然数。
通过规则归纳，我们还可以证明按照规则 (2.4) 定义的等式是自反的。
引理 2.2：自然数等于自身
引理 2.2 如果 \( a \) 是自然数，则 \( a = a \)。
证明 通过对规则 (2.2) 进行规则归纳：
- 规则 (2.2a)：应用规则 (2.4a)，我们得到 \( zero = zero \)。
- 规则 (2.2b)：假设 \( a = a \)，那么通过应用规则 (2.4b)，可以推导出 \( succ(a) = succ(a) \)。
类似地，我们可以证明后继运算是单射的。
引理 2.3：自然数的后继是单射的
引理 2.3 如果 \( succ(a_1) = succ(a_2) \)，则 \( a_1 = a_2 \)。
证明 类似于引理 2.1 的证明。
迭代和同时归纳定义¶
归纳定义通常是迭代进行的，意味着一个归纳定义是在另一个归纳定义的基础上构建的。在迭代归纳定义中，规则的前提：
可以是之前定义的判断形式的实例，也可以是正在定义的判断形式的实例。例如，以下规则定义了判断形式 \(- \text{list}\)，它表示 \(a\) 是一个自然数列表：
规则 (2.7b) 的第一个前提是之前定义的判断形式 \(a \text{ nat}\) 的实例，而前提 \(b \text{ list}\) 则是正在通过这些规则定义的判断形式的实例。
同时，归纳定义经常一次定义两个或更多的判断形式。一个同时归纳定义包含一组规则，用于推导多个不同判断形式的实例，任何判断形式都可以作为任何规则的前提。由于定义每个判断形式的规则可能涉及其他判断形式，因此这些判断形式没有一个是先于其他形式定义的。相反，我们必须理解，这些判断形式是由整组规则同时定义的。由这些规则定义的判断形式仍然是封闭在这些规则下的最强判断形式。因此，规则归纳的证明原则仍然适用，不过它要求我们同时证明每个定义的判断形式的某个性质。
Example
例如，以下规则构成了 \(a \text{even}\)（表示 \(a\) 是偶数）和 \(a \text{odd}\)（表示 \(a\) 是奇数）判断的同时归纳定义：
这些规则的规则归纳原理表明，要同时证明 \(P(a)\) 对于 \(a\) 是偶数时成立，且 \(Q(b)\) 对于 \(b\) 是奇数时成立，只需证明以下几点：
- \(P(\text{zero})\)；
- 如果 \(Q(b)\) 成立，则 \(P(\text{succ}(b))\) 成立；
- 如果 \(P(a)\) 成立，则 \(Q(\text{succ}(a))\) 成立。
例如，我们可以使用同时规则归纳来证明：（1）如果 \(a\) 是偶数，则 \(a\) 要么是 0，要么是 \( \text{succ}(b) \)，其中 \(b\) 是奇数；（2）如果 \(a\) 是奇数，则 \(a\) 是 \( \text{succ}(b) \)，其中 \(b\) 是偶数。
我们定义 \(P(a)\) 当且仅当 \(a\) 是 0 或 \(a\) 是 \( \text{succ}(b) \)，其中 \(b\) 是奇数时成立，并定义 \(Q(b)\) 当且仅当 \(b\) 是 \( \text{succ}(a) \)，其中 \(a\) 是偶数时成立。通过规则归纳可以证明：
- \(P(\text{zero})\) 成立，因为 \( \text{zero} \) 是 0；
- 如果 \(Q(b)\) 成立，则 \( \text{succ}(b) \) 是 \( \text{succ}(b') \)，其中 \(b' = b\)，并应用归纳假设；
- 如果 \(P(a)\) 成立，则 \( \text{succ}(a) \) 是 \( \text{succ}(a') \)，其中 \(a' = a\)，并应用归纳假设。
通过规则定义函数¶
归纳定义的一个常见用途是通过给定输入和输出之间的图的归纳定义来定义函数，然后证明该关系唯一地确定了给定输入的输出。例如，我们可以定义自然数上的加法函数为关系 \( \text{sum}(a; b; c) \)，其意图是表示 \(c\) 是 \(a\) 和 \(b\) 的和，定义如下：
这些规则定义了自然数 \(a\)、\(b\) 和 \(c\) 之间的三元关系 \( \text{sum}(a; b; c) \)。我们可以证明，在这个关系中，\(c\) 是由 \(a\) 和 \(b\) 唯一确定的。
定理 2.4: 和函数的存在性和唯一性
定理 2.4 对于每个自然数 \(a\) 和 \(b\)，存在唯一的自然数 \(c\)，使得 \( \text{sum}(a; b; c) \) 成立。
证明 该证明分为两部分：
- 存在性：如果 \(a\) 和 \(b\) 是自然数，则存在自然数 \(c\)，使得 \( \text{sum}(a; b; c) \) 成立。
- 唯一性：如果 \( \text{sum}(a; b; c_1) \) 和 \( \text{sum}(a; b; c_2) \) 都成立，则 \(c_1 = c_2\)。
对于存在性，我们令 \(P(a)\) 表示以下命题：如果 \(b\) 是自然数，则存在自然数 \(c\)，使得 \( \text{sum}(a; b; c) \) 成立。我们通过规则归纳来证明，如果 \(a\) 是自然数，则 \(P(a)\) 成立。我们有两个情况需要考虑：
- 规则 (2.2a)：我们要证明 \(P(\text{zero})\)。假设 \(b\) 是自然数，并令 \(c = b\)，根据规则 (2.9a)，我们得出 \( \text{sum(zero; b; c)} \)。
- 规则 (2.2b)：假设 \(P(a)\) 成立，我们要证明 \(P(\text{succ}(a))\)。也就是说，我们假设如果 \(b\) 是自然数，则存在自然数 \(c\)，使得 \( \text{sum}(a; b; c) \) 成立，并且要证明如果 \(b' \) 是自然数，则存在 \(c'\)，使得 \( \text{sum(succ}(a); b'; c') \) 成立。为此，假设 \(b' \) 是自然数。根据归纳假设，存在 \(c\) 使得 \( \text{sum}(a; b'; c) \) 成立。令 \(c' = \text{succ}(c)\)，并应用规则 (2.9b)，我们得出 \( \text{sum(succ}(a); b'; c') \)，如所需。
对于唯一性，我们证明，如果 \( \text{sum}(a; b; c_1) \) 成立，且 \( \text{sum}(a; b; c_2) \) 成立，则 \(c_1 = c_2\)，通过基于规则 (2.9) 的规则归纳来证明。
- 规则 (2.9a)：我们有 \(a = 0\) 且 \(c_1 = b\)。通过相同规则的内归纳，我们可以证明如果 \( \text{sum(zero; b; c_{2})} \) 成立，则 \(c_2 = b\)。根据引理 2.2，我们得出 \(b = b\)。
- 规则 (2.9b)：我们有 \(a = \text{succ}(a')\) 且 \(c_1 = \text{succ}(c'_1)\)，其中 \( \text{sum}(a'; b; c'_1) \) 成立。通过相同规则的内归纳，我们可以证明如果 \( \text{sum}(a; b; c_2) \) 成立，则 \(c_2 = \text{succ}(c'_2)\)，其中 \( \text{sum}(a'; b; c'_2) \) 成立。根据外归纳假设，\(c'_1 = c'_2\)，因此 \(c_1 = c_2\)。
第三章：假设判断与一般判断¶
假设判断表达了一个或多个假设与结论之间的蕴涵关系。我们将考虑两种蕴涵概念，分别是可导性和可接受性。两者都表示某种形式的蕴涵，但区别在于可导性在扩展新规则时是稳定的，而可接受性则不是。一般判断表达了判断的普遍性或泛化性。一般判断有两种形式：泛型和参数化。泛型判断表示相对于判断中变量的所有替换实例的泛化，而参数化判断表示相对于符号重命名的泛化。
假设判断¶
假设判断编纂了表达一个结论在一个或多个假设成立的条件下有效性的规则。假设判断有两种形式，区别在于结论在何种意义上依赖于假设。其中一种在扩展更多规则时是稳定的，另一种则不是。
可导性¶
对于给定的规则集合 \(R\)，我们定义可导性判断，记为 \(J_1, ..., J_k \vdash_R K\)，其中每个 \(J_i\) 和 \(K\) 是基本判断，意思是我们可以从将 \(R\) 扩展为 \(R \cup \{J_1, ..., J_k\}\) 的规则中推导出 \(K\)。我们将判断的假设或前提 \(J_1, ..., J_k\) 视为“临时公理”，并通过组合 \(R\) 中的规则推导出结论或后件。因此，假设判断的证据由使用 \(R\) 中的规则从假设推导出结论的推导过程组成。
我们用大写希腊字母（通常是 \(\Gamma\) 或 \(\Delta\)）表示一组有限的基本判断，并写作 \(R \cup \Gamma\) 表示 \(R\) 扩展为包含 \(\Gamma\) 中每个判断的公理的集合。判断 \(R \vdash \Gamma\) 表示从 \(R \cup \Gamma\) 中可以推导出 \(\Gamma\) 中的每个 \(J\)。一种等价的定义 \(J_1, ..., J_n \vdash_R J\) 的方式是说规则：
[ J_1, ..., J_n \ J ] （3.1）
是从 \(R\) 中可导出的，这意味着存在一个由 \(R\) 中的规则组成的 \(J\) 的推导过程，并将 \(J_1, ..., J_n\) 作为公理。例如，考虑相对于规则 (2.2) 的可导性判断：
对于任何对象 \(a\)，这个判断都是有效的，如推导所示：
这是通过组合规则 (2.2) 从 \(a \ \text{nat}\) 作为公理出发，最终得到 \( \text{succ(succ}(a)) \ \text{nat}\)。等价地，(3.2) 的有效性也可以通过表示规则
[ a \ \text{nat} \ \text{succ(succ}(a)) \ \text{nat} ] （3.4）
是从规则 (2.2) 可导出来表达。这直接源于可导性的定义，即它在扩展新规则时是稳定的。
定理 3.1（稳定性） 如果 \(R \vdash J\)，那么 \(R \cup R' \vdash J\)。
证明 从 \(R \cup \Gamma\) 中的任何推导也可以从 \(R \cup R' \cup \Gamma\) 中推导出来，因为 \(R\) 中的任何规则也是 \(R \cup R'\) 中的规则。
可导性具有许多结构性质，它们独立于所讨论的规则 \(R\) 而存在：
- 自反性 每个判断都是自己的后件：\(\Gamma, J \vdash_R J\)。每个假设都可以证明自己为结论。
- 弱化 如果 \(R \vdash J\)，那么 \(\Gamma, K \vdash_R J\)。未使用的选项不会影响蕴涵。
- 传递性 如果 \(\Gamma, K \vdash_R J\) 并且 \(R \vdash K\)，那么 \(R \vdash J\)。如果我们用一个推导替换掉一个公理，结果仍然是该后件的推导。
自反性直接源于可导性的定义。弱化直接来自可导性的定义。传递性通过对第一个前提进行规则归纳来证明。
可接受性¶
可接受性，记为 \(\Gamma \models_R J\)，是一种较弱的假设判断形式，表示 \(R\) 推导出 \(R \vdash J\)。也就是说，当假设可以从 \(R\) 中推导出时，结论 \(J\) 也可以从 \(R\) 中推导出。特别地，如果任何假设不能相对于 \(R\) 推导出来，那么判断是空真值。另一种定义 \(J_1, ..., J_n \models_R J\) 的等价方式是说规则：
[ J_1 \dots J_n \ J ] （3.5）
相对于 \(R\) 的规则是可接受的。也就是说，给定任何使用 \(R\) 中规则推导出的 \(J_1, ..., J_n\)，我们可以使用 \(R\) 中的规则推导出 \(J\)。
例如，可接受性判断：
是有效的，因为从规则 (2.8) 中推导出 \(\text{succ}(a) \ \text{even}\) 的任何推导都必须包含从相同规则中推导出 \(a \ \text{odd}\) 的子推导，这证明了结论。这个事实可以通过对规则 (2.8) 进行归纳证明。判断 (3.6) 的有效性也可以通过表示规则：
[ \text{succ}(a) \ \text{even} \ a \ \text{odd} ] （3.7）
相对于规则 (2.8) 是可接受的来表达。
与可导性不同，可接受性判断在扩展规则时并不稳定。例如，如果我们用公理：
扩展规则 (2.8)，则规则 (3.6) 就变得不可接受了，因为没有规则组合可以推导出 \( \text{zero odd}\)。可接受性对归纳定义中缺失或存在的规则都非常敏感。
定理 3.2 如果 \(R \vdash J\)，那么 \(\Gamma \models_R J\)。
证明 通过多次应用可导性的传递性，可以证明如果 \(R \vdash J\) 并且 \(R \vdash \Gamma\)，那么 \(R \vdash J\)。
反例说明了反过来的情况并不成立。例如，\(\text{succ(zero)} \ \text{even} \vdash_{(2.8)} \ \text{zero odd}\) 并不成立，因为在添加 \(\text{succ(zero)} \ \text{even}\) 作为公理时，无法推导出 \(\text{zero odd}\)。然而，相关的可接受性判断：
是有效的，因为假设是假的：根据规则 (2.8)，无法推导出 \(\text{succ(zero)} \ \text{even}\)。即便如此，可导性判断
是有效的，因为我们可以通过组合规则 (2.8) 从左边推导出右边。
可接受性的证据可以被视为一个数学函数，将假设的推导 \( \delta_1, \dots, \delta_n \) 转化为结论的推导 \( \delta \)。因此，可接受性判断享有与可导性相同的结构性质，因此也是一种假设判断：
- 自反性 如果 \( J \) 可以从原始规则中推导出，那么 \( J \) 也可以从原始规则中推导出：\( J \models_R J \)。
- 弱化 如果在假设每个判断 \( \Delta \) 都可以从这些规则中推导出的前提下 \( J \) 可导，那么在假设 \( \Delta \) 和 \( K \) 都可以从原始规则中推导出的前提下，\( J \) 也必须是可导的：如果 \( \Delta \models_R J \)，那么 \( \Delta, K \models_R J \)。
- 传递性 如果 \( \Delta, K \models_R J \) 且 \( \Delta \models_R K \)，那么 \( \Delta \models_R J \)。如果 \( \Delta \) 中的判断是可导的，那么 \( K \) 也是可导的，因此 \( \Delta, K \) 中的判断也是可导的，进而 \( J \) 也是可导的。
定理 3.3 可接受性判断 \( \Delta \models_R J \) 享有蕴涵的结构性质。
证明 这一结论直接来源于可接受性的定义，即假设相对于规则 \( R \) 是可导的，那么结论也是可导的。
如果一个规则 \( r \) 对于规则集合 \( R \) 是可接受的，那么 \( R, r \vdash J \) 等价于 \( R \vdash J \)。因为如果 \( R \vdash J \)，那么显然 \( R, r \vdash J \)，只需忽略 \( r \) 即可。反之，如果 \( R, r \vdash J \)，那么我们可以用 \( r \) 在 \( R \) 规则中的展开替代对 \( r \) 的任何使用。通过对 \( R, r \) 进行规则归纳，可以得出从扩展后的规则集合 \( R, r \) 推导出的任何推导都可以转化为仅从 \( R \) 中推导出的推导。因此，如果我们想要证明从 \( R, r \) 推导出的判断的某一性质，而 \( r \) 对 \( R \) 是可接受的，只需证明该性质在 \( R \) 规则下是闭合的即可，因为 \( r \) 的可接受性表明 \( r \) 的结果隐含于 \( R \) 的结果之中。
假设性归纳定义¶
将归纳定义的概念拓展为允许包含推导性判断作为前提和结论的规则是非常有用的。这样做可以让我们引入仅适用于某个特定前提推导过程的局部假设，同时也允许我们在规则应用的点约束基于有效全局假设的推理。
一个假设性归纳定义由以下形式的一组假设性规则组成：
其中，\( \Gamma \) 是规则的全局假设，而 \( \Gamma_i \) 是第 \( i \) 个前提的局部假设。非正式地，这条规则表明，当每个 \( J_i \) 都是 \( \Gamma \)，并扩展了对应的局部假设 \( \Gamma_i \) 时，可以从 \( \Gamma \) 推导出 \( J \)。因此，证明 \( J \) 可以从 \( \Gamma \) 推导的方式之一是依次证明每个 \( J_i \) 都可以从 \( \Gamma_i \) 推导出。每个前提的推导涉及一种“上下文切换”，我们在该前提的推导中，将全局假设扩展为包括局部假设。
我们要求假设性归纳定义中的所有规则都是一致的，即这些规则在所有全局上下文中都适用。一致性确保规则可以以隐含或局部形式呈现：
在这里，全局上下文被隐含忽略，并默认规则适用于任意全局假设的选择。
假设性归纳定义应被视为形式推导判断 \( \Gamma \vdash J \) 的普通归纳定义，推导过程由一组有限的基本判断 \( \Gamma \) 和一个基本判断 \( J \) 构成。一组假设性规则 \( R \) 定义了最强的形式推导判断，该判断具有结构性并在一致规则 \( R \) 下封闭。结构性意味着形式推导判断必须在以下规则下封闭：
- \( \Gamma, J \vdash J \) \quad (3.11a)
- \( \Gamma, K \vdash J \Rightarrow \Gamma \vdash J \) \quad (3.11b)
- \( \Gamma \vdash K \quad \Gamma, K \vdash J \Rightarrow \Gamma \vdash J \) \quad (3.11c)
这些规则确保形式推导行为像假设性判断一样。我们写作 \( \Gamma \vdash_R J \) 来表示 \( J \) 是从规则 \( R \) 中推导出来的。
假设性规则归纳的原则仅是形式假设性推导判断上的规则归纳原则。因此，若要证明 \( P(\Gamma \vdash J) \)，只需证明 \( P \) 在规则 \( R \) 和结构规则下封闭。因此，对于每条形式如 (3.9) 的规则（无论是结构性的还是 \( R \) 中的），我们必须证明：
如果 \( P(\Gamma_1 \vdash J_1) \)、……以及 \( P(\Gamma_n \vdash J_n) \) 成立，那么 \( P(\Gamma \vdash J) \) 也成立。
但这只是第二章中规则归纳原则的重新表述，专门针对形式推导判断 \( \Gamma \vdash J \)。
在实践中，我们通常通过 3.1.2 节中描述的方法省略结构规则。通过证明结构规则是可接受的，任何基于规则归纳的证明都可以将注意力限制在 \( R \) 中的规则上。如果假设性归纳定义的所有规则都是一致的，那么结构规则 (3.11b) 和 (3.11c) 显然是可接受的。通常，规则 (3.11a) 必须显式地作为一条规则提出，而不是基于其他规则来证明其可接受性。
一般判断¶
一般判断编纂了处理判断中的变量的规则。与数学中类似，变量被视为一个未知量，范围在指定的对象集内。一个泛化判断表明，对于替换判断中指定变量的任何对象，判断都成立。另一种形式的泛化判断编纂了符号参数的处理。一个参数化判断表示对于指定符号的任何新的重命名，判断都成立。
为了跟踪推导中的活动变量和符号，我们写作 \( U;X \vdash_R J \)，表示在符号 \( U \) 和变量 \( X \) 构成的 abt（抽象绑定树）对象上，\( J \) 可以根据规则 \( R \) 被推导出来。
规则的一致性概念必须扩展，要求规则在变量的重命名和替换下封闭，并且在参数的重命名下封闭。更精确地说，如果 \( R \) 是包含类型为 \( s \) 的自由变量 \( x \) 的规则集，那么它必须包含所有可能的替换实例，将类型为 \( s \) 的 abt \( a \) 替换为 \( x \)，包括那些包含其他自由变量的 abt。同样，如果 \( R \) 包含带有参数 \( u \) 的规则，那么它必须包含通过将类型为 \( u \) 的参数重命名为同类型的其他 \( u \) 而获得的所有规则实例。一致性排除了只为某个变量声明规则而不为该变量的所有实例声明规则的情况，也排除了只为某个参数声明规则而不为该参数的所有可能重命名声明规则的情况。
泛化推导判断定义如下：
其中，\( Y.X \) 是通用的。泛化推导的证据由涉及变量 \( X, Y \) 的泛化推导 \( \delta \) 构成。只要规则是一致的，选择 \( Y \) 并无区别，原因将在后面解释。
例如，以下泛化推导：
可以作为判断 \( X \vdash x \vdash \text{nat} \quad (2.2) \quad \text{succ}(\text{succ}(x)) \vdash \text{nat} \) 的证据，只要 \( x \notin X \)。只要所有规则是一致的，其他任何 \( x \) 的选择都同样有效。
只要 \( R \) 是一致的，泛化推导判断享有以下结构性质，这些性质约束了变量的行为：
- 增生：如果 \( Y \vdash_R J \)，那么 \( Y, y \vdash_R J \)。
- 重命名：如果 \( Y, y \vdash_R J \)，那么 \( Y, y \vdash_R J[y'/y] \) 对于任意 \( y' \notin XY \)。
- 替换：如果 \( Y, y \vdash_R J \) 且 \( a \in B[XY] \)，那么 \( Y \vdash_R J[a/y] \)。
增生由规则模式的解释保证，它涵盖了宇宙的所有扩展。重命名内置于泛化判断的意义中。替换原则中隐含的是，替换的 abt 与被替换的变量类型相同。
参数化推导类似于泛化推导，只是其泛化对象是符号而非变量。参数化推导定义如下：
其中，\( V.U \) 是通用的。参数化推导的证据由涉及符号 \( V \) 的推导 \( \delta \) 构成。规则的一致性确保了参数名称的任意选择都同样有效；推导在重命名下是稳定的。
第二部分：静态与动态¶
第四章：静态¶
第五章：动态¶
第六章：类型安全¶
第七章：动态类型推导¶
第三部分：全函数¶
第八章：函数定义和值¶
第九章：高阶递归的 \(T\) 系统¶
第四部分：有限数据类型¶
第十章：乘积类型¶
第十一章：和类型¶
第五部分：类型和提议¶
第十二章：构造逻辑¶
第十三章：经典逻辑¶
第六部分：无限数据类型¶
第十四章：泛型编程¶
第十五章：归纳与协归纳类型¶
第七部分：变量类型¶
第十六章：多态类型的 \(F\) 系统¶
第十七章：抽象类型¶
第十八章：更高种类¶
第八部分：部分和递归类型¶
第十九章：递归函数的 \(PCF\) 系统¶
第二十章：递归类型的 \(FPC\) 系统¶
第九部分：动态类型¶
第二十一章：无类型 \(\lambda\) 演算¶
第二十二章：动态类型¶
第二十三章：混合类型¶
编程语言原理课内部分到此为止。