论递归类型，章节二

套盾：本文用到的英文术语皆是本人实在不知道如何翻译、觉得翻译过来意思实在是不对、或者干脆是觉得翻译过来理解起来比不翻译更麻烦（例如“结构归纳法是对良基归纳法的一个实例化”这种句子放在中文里实在是有些狗屁不通了），不是为了故意装逼，这些术语都可以在 Wikipedia 上查到。

  在上一个章节中，我讲到了对归纳法的 generalization，即证明 Principle of Induction 蕴含了常见的数学归纳法，既然是对数学归纳法的一种 generalization，我们也可以轻易的将 Principe of Induction 中的 $\mu F$ 设定为除了 $\N$ 以外的其他归纳集合（例如可以将某个递归数据结构的所有层级作为 $\mu F$，我们就得到了 structural induction），不仅如此，通过取 Principle of Induction 的对偶，我们同样可以得到 Principle of Coinduction。令 $F:\mathcal{P}(U)\rightarrow \mathcal{P}(U)$，注意到在上一篇文章中提到了 $\mu F$ 是 $F$ 的最小不动点，而最小不动点对应 Principle of Induction，很容易就可以发现 $\mu F$ 实际上包含了所有可以由递归的应用 $F$ 得到的有限大的数据，以 $U=\N$ 为例，定义 $F: \mathcal{P}(\N)\rightarrow \mathcal{P}(\N) := X\mapsto \lbrace 0\rbrace \cup \lbrace x + 1\ |\ x\in X\rbrace$，则显然 $\mu F=\N$，也即所有有限大的自然数集合（当然了，没有无限大的自然数，除非我们对自然数集进行一些扩充，在此仅仅是举一个例子）：首先，$\N$ 是一个 $F$-closed 集合，所以 $\mu F\subseteq \N$；其次，我们用归纳法证明 $\forall n\in \N. n\in\mu F$，也即 $\N\subseteq \mu F$：首先，$0$ 显然属于 $\mu F$，其次由不动点的定义，有 $F(\mu F)=\mu F$，因为 $F(\mu F)= \lbrace 0\rbrace \cup \lbrace x + 1\ |\ x\in \mu F\rbrace$，如果 $n\in\mu F$，则显然 $n+1\in F(\mu F)=\mu F$，也即 $n+1\in \mu F$。以上论证适用于各种归纳定义得到的结构，例如读者可以轻松发现，如果将 $\N$ 换成 $\sf list = nil\ |\ cons(\mathrm{\Sigma}, list)$，其中 $\Sigma$ 是任意一个字母表，上面的论证一样成立。如果使用一些更加抽象的设定，我们应该可以证明该属性不仅仅是对 $\N$ 或 $\sf list$，而是对所有 inductive set 都成立，只是笔者才疏学浅，加上这部分内容超出了本文的主旨，因此不再就具体如何证明加一赘述，而仅仅给出一个思路供参考：

一种“更抽象的设定”可以由如下的思路给出：每个 inductive set $I$ 都可以被一组 inference rules 所 唯一确定（uniquely determined），因此，我们可以选择不去吧 $I$ 想象成一个具体数学对象的集合，而是想象成一个由这些 inference rules 的 derivation tree 所构成的集合，每一个 derivation tree 唯一的对应着其所 derive 出的数学对象，比如在 $\N$ 中，$3$ 可以对应如下的 derivation tree： $$ \cfrac{\cfrac{\cfrac{\cfrac{}{0}}{0+1}}{0+1+1}}{0+1+1+1} $$ 通过这种办法，我们将所有 inductive set 中的每个元素都变成了一个树状的结构，此时，我们可以用一个函数 $T(s)$ 来编码这个树，具体方法如下：假设这颗 derivation tree 至多有 $n$ 个分支，那么令 $s=\lbrace 1, …, N \rbrace^{\ast}$ 是一个由从 1 到 $N$ 的数字构成的字符串，其逻辑是 T(s) 会返回 derivation tree 中的某个节点，令 $\epsilon$ 是空字符串，则 $T(\epsilon)$ 为跟节点，而如果 $s\neq \epsilon$，则 $s$ 中的每个数字告诉了选择当前节点从左往右数的第几个子节点，例如，令 $s=121$，这意味这选择根节点的第一个子节点的第二个子节点的第一个子节点，通过这种方法，我们可以用 $T(s)$ 来编码任意的 derivation tree，又因为 $T(s)$ 唯一的特征就是 $s$，我们也就实现了一个用字符串 $s=\lbrace 1, …, N \rbrace^{\ast}$ 来编码任意 inductive set 的任意元素的方法（注意，这也意味着可能存在不同 inductive set 的不同元素有着相同的特征字符串 $s$ 的可能，但是这不要紧，因为我们只关注这样的一个元素是否是有限大的，而这是由 inference rules 的层数是否有限，也即 $s$ 的长度是否有限决定的，与元素本身以及 derive 出该元素的 inference rules 究竟长什么样子没有关系），此时，通过对 $s$ 的长度做归纳即可进行证明。

因为 $\mu F$ 对应所有有限大的结构，因此与 $\mu F$ 相关联的 Principle of Induction 自然也就告诉了如何论证有关所有 有限大 ¹的结构的命题。相对应的，通过对 Principle of Induction 中的所有内容取对偶，我们就得到了 Principle of Coinduction，通过取对偶，不难得知 $F$ 的最大不动点 $\nu F$ 对应了所有有限大以及无限大的结构，而与 $\nu F$ 相关的 Principle of Coinduction 告诉了我们如何论证有关任意无限大的结构的命题。   一个自然的落入 Coinduction 范畴的例子是 $\sf Stream$，在很多编程语言中，也叫做 infinite list 或者 lazy list，$\sf Stream$ 对应一个无限的数据列表。我们都知道 $\sf list$ 是一个 Inductive Type，不难发现，对于 $\sf list$ 来说，我们可以通过重复组合 $\sf nil$ 和 $\sf cons$ 来一步一步构建出任何 $\sf list$；但是对于 $\sf Stream$ 来说，由于所有 $\sf Stream$ 默认都是无限大的，我们不可能能想办法去构造一个 $\sf Stream$，我们所能做到的，仅仅是观察一下这个 $\sf Stream$ 的头部是什么元素，也就是说，$\sf Stream$ 会包含两个操作，$\sf head$ 和 $\sf tail$，其中 $\sf head$ 返回一个 $\sf Stream$ 的头部元素，而 $\sf tail$ 返回 $\sf Stream$ 去掉头部元素的剩余部分，也即一个新的无限的数据列表，不难发现，与 $\sf list$ 的 $\sf nil$ 以及 $\sf cons$ 都是用于构造的 constructor 不同，一个无限大的 $\sf Stream$ 只能拥有 destructor $\sf head$ 和 $\sf tail$，这样的一个类型就叫做一个 Coinductive Type。   对于 Inductive Type，我们使用递归函数来 分解它，例如，对于一个 $\sf len(list)$，其定义大概率将会是

$$ \begin{aligned} \sf len(nil) &= 0 \end{aligned} $$

$$ \sf len(cons(\pi, \tau)) = 1 + \sf len(\tau) $$

这样的一个算法非常典型的展示了我们是如何使用递归来处理一个 Inductive Type 的，类似的，对于 Coinductive，我们也需要 Corecursion 来处理 Coinductive Type，与 Coinduction 一样，Corecursion 是通过对普通的递归取对偶得到的，普通的递归通过分解 Inductive Type 来分析它，Corecursion 则反过来，从头开始 构建一个 Coinductive Type 的实例，例如在 C# 中，IEnumerable<T> 可以被看做是一个 Coinductive Type，而一个典型的 Corecursion 算法就是使用 yield 的斐波那契数列生成器：

public static IEnumerable<int> Fib() {
    var a = 0;
    var b = 1;
    while (true) {
        yield return a;
        (a, b) = (b, a + b);
    }
}

注意到在这样的一个算法是如何 生成一个 Coinductive Type IEnumerable<int> 的。   值得一提的是，Inductive Type 和 Coinductive Type 这一组对偶的概念并非完全对立，一个函数 $F: X\times A\rightarrow X$ 可以被看做是一个 Inductive Type 的生成函数，例如，如果取 $X=\sf list$，$A=\N$，令

$$ F(list, n) = \mathsf{cons}(n, list) $$

则 $F$ 显然是一个 $\sf list$ 的生成函数，这个函数的签名 $X\times A\rightarrow X$ 告诉我们，给出一个 Inductive Type 的结构 $x: X$，和一个新的元素 $a: A$，会返回一个将 $a$ 与 $x$ 按照 $X$ 的 constructor 结合起来的新的 $X$。但是，如果我们将 $F$ 柯里化，就得到了 $F: X \rightarrow A\rightarrow X$，或者说 $F: X\rightarrow (A\rightarrow X)$，则 $F$ 又可以看做是一个 Coinductive Type 的 observer，其中 $X$ 是初始的值，而 $A$ 代表当前的状态，或者迭代的次数（例如上文 Fib 函数中的 a 和 b 变量就是状态变量），而 $A\rightarrow X$ 是一个状态转移函数，告诉我们在某个特定的输入 $A$，会产出什么样、或者说观察到什么样的 $X$（例如 Fib 函数中根据当前的状态 a 和 b 产出 $X$ 中对应的下一个元素 a + b），这告诉了我们某些函数既可以被当做是 Inductive Type 上的操作（我们说这样的操作是 algebraic 的），也可以被当作是 Coinductive Type 上的操作（我们说这样的操作是 coalgebraic 的），不难发现，algebraic operation 与 coalgebraic operation 的区别就在于一个在表现上是 construction，而另一个则在表现上是 destruction/observation：通过取出 $X$ 的第一个元素来观察 $X$ 的内容。对于了解状态机的人，可以在这里将 $X$ 想象作状态空间，而将 $A$ 想象成状态机的字母表。

  在本篇文章中，我们解释了 Induction 为什么能够论证和构造有限大的数据，而 Coinduction 为什么能够论证和构造无限大的数据。在本系列的下一篇文章中，我们将会介绍 Induction 与 Coinduction 在证明技巧上的区别。