归纳定义

在学习编程语言的过程中，归纳定义是必不可少的工具。一个归纳定义是由各种各样 判断 的推导过程形成的 规则 集合组成的。判断是某个特定类别的语法对象的表达式。规则表述了一条判断有效的充分必要条件。

判断

判断是一个语法对象的表达式，举例来说：

一条判断表示语法对象具有某种性质或者几个语法对象直接有某种关系。这种性质或者关系被称为 判断式，这里的语法对象称为这种判断形式的 实例。判断式也被称为 谓语，对应的实例被称为 主语。我们用 $ a ~ J $ 表示断言 $ J $ 对 $ a $ 成立。不需要关心判断的主语时，用 $ J $ 来表示不确定的判断。为了能够更直观地表达，可能会使用前缀，中缀或混合词缀表示一条特定的判断。

推理规则

一个判断式的 归纳定义 由一组规则组成。一条 规则 可以表示为

$$ \frac{J_1…J_k}{J} $$

在横线以上的称为这条规则的 假设，横线以下的称为它的 结论。如果一条规则没有假设，那么这条规则被称为 公理。一条规则所表示的意思是它的假设是它的结论的 充分条件：要证明 $ J $ ，只需要证明 $ J_1…,J_k $ 。当 $ k $ 为 $ zero $ 时，它的结论永远都是成立的。一般地，可能会有多条规则拥有同样的结论，因此一条规则的结论成立不一定意味着它的假设也成立，结论可能可以由其它的规则推导出来。

举例来说，以下规则是一条判断 $ a ~ \text{nat} $ 的归纳定义：

$$ \frac{}{\text{zero} ~ \text{nat}} \tag{2.2a} $$

$$ \frac{a ~ \text{nat}}{succ(a) ~ \text{nat}} \tag{2.2b} $$

这两条规则说明了当 $ a $ 是 $ \text{zero} $ 或者是另一个自然数的后继时，是一个自然数。类似地，也可以给出一棵二叉树的定义：

$$ \frac{}{\text{empty} ~ \text{tree}} \tag{2.3a} $$

$$ \frac{a_1 ~ \text{tree} \quad a_2 ~ \text{tree}}{node(a_1;a_2) ~ \text{tree}} \tag{2.3b} $$

这两条规则说明一棵二叉树要么为空，要么两个节点都是一棵二叉树。

表示自然数 $ a $ 和 $ b $ 相等的判断 $ a = b $ 可以定义为：

$$ \frac{}{\text{zero} = \text{zero} ~ \text{nat}} \tag{2.4a} $$

$$ \frac{a = b ~ \text{nat}}{succ(a) = succ(b) ~ \text{nat}} \tag{2.4b} $$

在这些例子中我们都使用有限的形式声明了无限个规则。

如果有一些规则，通过这些规则可以推导出一条判断，就说这条判断 $ J $ 闭合与这些规则。如果这些规则同时还是必要 的，称判断 $ J $ 强闭合于这些规则。

推导过程

要证明一条归纳定义的判断成立，只需要列出它的 推导过程。推导过程从公理开始，结束于要证明的判断。它可以被看成是一棵树，一个节点的子树就是它的假设的推导过程。如果

$$ \frac{J_1…J_k}{J} $$

且 $ \Delta_1,…,\Delta_k $ 分别是这些假设的推导过程，可以将 $ J $ 的推导过程写为

$$ \frac{\Delta_1…\Delta_k}{J} $$

例如， $ succ(succ(succ(\text{zero}))) ~ \text{nat} $ 的推导过程写为

$$ \frac{\frac{\frac{\text{zero} ~ \text{nat}}{succ(\text{zero}) ~ \text{nat}}}{succ(succ(\text{zero})) ~ \text{nat}}}{succ(succ(succ(\text{zero}))) ~ \text{nat}} \tag{2.5} $$

要证明一条判断能被推导出来，只需要找到一个推导过程。主要有两种方法用于得到推导过程。一个是 正向查询，从公理出发，直到推导出最终结论。另一个是 反向查询，是从结论出发直到顶层的假设都为公理。正向查询维护一个判断的集合，初始为空，然后找到所有假设都在该集合中的规则，将它的结论也加入集合，直到需要推导的判断出现在这个集合中。如果一条判断是可推导的，那么这个方法总是可以找到它的推导过程，但是如果一条判断无法被推导，那么运算永远不会终止，此时无法判断它是否可以推导。反向查询则维护一个队列，初始时只有这条需要推导的判断，随后每一次操作都移除队列中的一条判断，将它的假设加入队列中，如果有多条规则可以推导出这条判断，那么需要分别执行这个过程，知道队列为空。如果一条判断是可推导的，这个方法也能找到它的推导过程，但是同样地，如果一条判断不可被推导，那么可能会有无限条规则加入到队列中，永远不会被清空。

规则归纳

如果当 $ P(J_1),…,P(J_k) $ 成立时， $ P(J) $ 也成立，那么称 $ P $ 闭合于规则

$$ \frac{J_1…J_k}{J} $$

规则归纳表示如果 $ P $ 闭合于一些规则，那么 $ P $ 对于任何由这些规则定义的判断 $ J $ 是成立的。例如对于规则 $ (2.2) $ 要证明 $ P(a ~ \text{nat}) $ ，只要证明：

1. $ P(\text{zero} ~ \text{nat}) $
2. 对于任意 $ a $ ，如果 $ a ~ \text{nat} $ 且 $ P(\text{zero} ~ \text{nat}) $ ，那么 $ succ(a) ~ \text{nat} $ 且 $ P(succ(a) ~ \text{nat}) $

这个与数学归纳法很像，它是规则归纳的一个特例。

类似地对于规则 $ (2.3) $ ，要证明 $ P(a ~ \text{tree}) $ 对于任何 $ a ~ \text{tree} $ 成立，只需要证明：

1. $ P(\text{empty} ~ \text{tree}) $
2. 对于任意 $ a_1 $ 和 $ a_2 $ ，如果 $ a_1 ~ \text{tree} $ ，$ P(a_1 ~ \text{tree}) $ 且 $ a_2 ~ \text{tree} $ ，$ P(a_2 ~ \text{tree}) $ ，那么可以得出 $ node(a_1;a_2) ~ \text{tree} $ 与 $ P(node(a_1;a_2) ~ \text{tree}) $

这被称为树形归纳，也是规则归纳的一种形式。

用这种方法可以证明很多性质，比如：

引理. 如果 $ a ~ \text{nat} $ ，那么 $ a = a ~ \text{nat} $

证明：根据规则 $ (2.4a) $ ，$ \text{zero} = \text{zero} ~ \text{nat} $ 。假设 $ a = a ~ \text{nat} $，那么根据规则 $ (2.4b) $ ， $ succ(a) = succ(a) ~ \text{nat} $ 成立。

类似地也能证明如果 $ succ(a_1) = succ(a_2) $ ，则 $ a_1 = a_2 ~ \text{nat} $ 。

迭代归纳与相互归纳

归纳定义经常是迭代定义的，即一条归纳定义是在另一条的基础上构成的。在迭代归纳定义中，一条规则的假设即可能是之前有定义的判断，也可以是当前定义的判断，例如定义一个自然数列表 [公式] 为 [公式] ：

$$ \frac{}{nil ~ \text{list}} \tag{2.7a} $$

$$ \frac{a ~ \text{nat} \quad b ~ \text{list}}{cons(a;b) ~ \text{list}} \tag{2.7b} $$

第一条假设 $ a ~ \text{nat} $ 是前面定义过的判断，而第二条 $ b ~ \text{list} $ 则是当前正在定义的。

很多时候，有两条或者更多判断使用相互归纳的方式同时定义。相互归纳定义推导出多条判断，其中每一条判断都可能出现在其中一些规则的假设中。因为它们在定义的时候彼此依赖，所以只能同时给出它们的定义。例如定义一个自然数是奇数或者偶数：

$$ \frac{}{\text{zero} ~ \text{even}} \tag{2.8a} $$

$$ \frac{a ~ \text{odd}}{succ(a) ~ \text{even}} \tag{2.8b} $$

$$ \frac{a ~ \text{even}}{succ(a) ~ \text{odd}} \tag{2.8c} $$

类似地根据规则归纳，如果要证明对于任意 $ a ~ \text{even} $ 有 $ P(a ~ \text{even}) $ ，对于任意 $ a ~ \text{odd} $ 有 $ P(a ~ \text{odd}) $ ，只需要证明：

1. $ P(\text{zero} ~ \text{odd}) $
2. 如果 $ P(a ~ \text{odd}) $ 那么 $ P(succ(a) ~ \text{even}) $
3. 如果 $ P(a ~ \text{even}) $ 那么 $ P(succ(a) ~ \text{odd}) $

举一个最简单的例子，证明 (1) 如果 $ a ~ \text{even} $ 则 $ a ~ \text{nat} $ ，(2) 如果 $ a ~ \text{odd} $ 则 $ a ~ \text{nat} $ ：

1. 根据 $ (2.2a) $ 显然 $ \text{zero} ~ \text{nat} $
2. 根据 $ (2.2b) $ ，如果 $ a ~ \text{odd} $ 时有 $ a ~ \text{nat} $ 则 $ succ(a) ~ \text(nat) $
3. 根据 $ (2.2b) $ ，如果 $ a ~ \text{even} $ 时有 $ a ~ \text{nat} $ 则 $ succ(a) ~ \text(nat) $

因此得证。

用规则定义函数

归纳定义也经常被用来定义函数，这时只需要给出输入与输出的对应关系，并且证明输出是由输入唯一确定的即可。例如定义一个自然数的加法 $ sum(a;b;c) $，表示 $c$ 为 $a$ 与 $b$ 的和：

$$ \frac{b ~ \text{nat}}{sum(\text{zero};b;b)} \tag{2.9a} $$

$$ \frac{sum(a;b;c)}{sum(succ(a);b;succ(c))} \tag{2.9b} $$

这两条规则定义了一个自然数的三元关系，我们需要证明 $ c $ 是由 $ a $ 和 $ b $ 确定的。

定理. 对于任意的 $ a ~ \text{nat} $ 和 $ b ~ \text{nat} $ 都存在唯一的 $ c $ 符合 $ sum(a;b;c) $ 。

证明：这里的证明分为两个部分：

1. （存在性）如果 $ a ~ \text{nat} $ 且 $ b ~ \text{nat} $ ，存在 $ c $ 使得 $ sum(a;b;c) $
2. （唯一性）如果 $ sum(a;b;c) $ 且 $ sum(a;b;c’) $ ，则 $ c = c’ $

存在性：设 $ P(a ~ \text{nat}) $ 的含义为 对于任意 $ b ~ \text{nat} $ 存在 $ c $ 使得 $ sum(a;b;c) $。

1. 当 $ a $ 为 $ \text{zero} $ 时，根据 $ (2.9a) $ 显然成立，此时 $ c = b $ 。
2. 假设 $ P(a ~ \text{nat}) $ 成立，需要证明 $ P(succ(a) ~ \text{nat}) $ 成立，即对于任意 $ b ~ \text{nat} $ 存在 $ c $ 使得 $ sum(succ(a);b;c) $ 。因为 $ P(a ~ \text{nat}) $ ，因此对于这个 $ b $ 存在 $ c’ $ 使得 $ sum(a;b;c’) $ 。根据 $ (2.9b) $ 有 $ sum(succ(a);b;succ(c’)) $ ，因此可令 $ c = succ(c’) $ 。

唯一性：我们证明如果 $ sum(a;b;c_1) $ 与 $ sum(a;b;c_2) $ ，则 $ c_1 = c_2 ~ \text{nat} $ 。

1. 当 $ a = \text{zero} $ 时，根据 $ (2.9a) $ 有 $ c_1 = b $ 与 $ c_2 = b $ 。根据前面的引理可得 $ c_1 = c_2 $ 。
2. 设 $ sum(a’;b;c_1’) $ ， $ a = succ(a’) $ ， $ c_1 = succ(c_1’) $ 。如果 $ sum(a;b;c_2) $ ，根据 $ (2.9b) $ 有 $ sum(succ(a’);b;succ(c_1’)) $ ，即 $ sum(a;b;c_1) $ ，因为它们来源于同一条规则所以 $ c_1 = c_2 $ 。

模式

在一条判断中，一些参数是由另外参数决定的，这被称为判断的 模式声明。例如自然数加法 $ sum(a;b;c) $ 具有模式 $ (\forall, \forall, \exists) $ 。它表示对于任意 $ a ~ \text{nat} $ 与任意 $ b ~ \text{nat} $ 都存在 $ c $ 使得 $ sum(a;b;c) $ 。如果要说明 $ c $ 是唯一确定的，就写为 $ (\forall, \forall, \exists!) $ 。如果 $ c $ 不一定存在，写为 $ (\forall, \forall, \exists^{\leq1}) $ ，意为对于任意 $ a ~ \text{nat} $ 与任意 $ b ~ \text{nat} $ 最多存在一个 $ c $ 使得 $ sum(a;b;c) $ 。

可以看到，一条判断可能同时满足多个模式声明。一般来说，全称量词修饰的参数被当做是输入，而存在量词修饰的参数当做输出。但是一般会有一个我们希望的主要的模式，一般使用等号来表达输入和输出的关系，例如重新定义加法：

$$ \frac{a ~ \text{nat}}{a + \text{zero} = a ~ \text{nat}} \tag{2.10a} $$

$$ \frac{a + b = c ~ \text{nat}}{a + succ(b) = succ(c) ~ \text{nat}} \tag{2.10b} $$

用这种方式表示等号右侧的参数是由左边的参数决定的。当 $ a + b = c ~ \text{nat} $ 时，可以直接使用 $ a + b $ 来表示 $ c $ 。

总结

这部分介绍了归纳定义以及它的一些使用。我们不仅可以使用归纳的方法定义一些判断，同时还可以使用归纳的方法证明它们的一些性质。其中基于自然数定义的归纳方法就是通常情况下所说的数学归纳法，另外还可以通过类似的方法把归纳法推广到任何拥有类似结构的定义，如上面提到的树形归纳和相互归纳。归纳定义也可以用来定义函数，一条判断中的一些参数可能由另一些参数决定，它们分别可以看成函数的输入与输出，这些性质决定了它符合哪些模式声明。