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

  在2021年最开始看 Types and Programming Languages 的时候，前面一直看的都非常顺利，结果到了 Recursive Type 对应的章节直接傻了眼，由于缺乏相关内容的熟练度，再加上个人感觉这一章设计的着实不是太好，结果导致我根本没看懂。前几天在南京和朋友讨论逻辑的时候突然想起来了这么一茬，决定把当时整理的笔记发出来，顺便把书里书外的内容都整理的更清楚一些。

  要了解如何 reasoning about 有限以及无限的内容，我们至少需要知道什么是归纳，与高中学习到的不同，归纳法不仅可以应用在自然数上，而是可以应用在任何 well-founded 的关系上，其中一个例子是 structural induction，我们可以认为 structural induction 是对 well-founded induction 的一个 instantiation，其中某个节点和它的 immediate substructure 构成了一个 well-founded relation，因此我们可以对一个树状或者图状的任何拥有一些拓扑意义上的序的结构进行归纳论证。
  几个自然而然的问题是：为什么归纳能行？为什么归纳是正确的？我们能对归纳法本身做些什么 generalization？

为什么归纳是一种可行的证明技巧？

  这个问题实际上有些莫名其妙，归纳的概念多多少少是作为公理存在的，在解释归纳的直觉之前，我们可以先一种比较常规的办法来证明归纳法

令 \N 是自然数集，P(n) 是一个 \N 上的归纳属性，由归纳属性的定义，有 P(0) 成立，令 S = \lbrace n\in \N\ | \ \neg P(n)\rbrace，则 S\subseteq \N，由 well-ordering principle，存在 s=\min(S) 且 s\neq 0，则 s-1\notin S，这意味着 P(s-1) 成立，则由归纳属性的定义，P(s) 同样成立，与 S 的定义矛盾，因此 P(n) 对所有 n\in\N 都成立。

这个证明很简单，但是如果对归纳法有一些了解的话，就会发现我们也能用归纳法来证明 well-ordering principle，这就让这么一个证明多多少少变得有些像是循环论证。事实上，与其被理解成一种需要和自然数有关的定理，归纳法更适合被当成一个对自然数的 reformulation，描述归纳法的过程正是描述自然数集的过程。或者可以说，实际上归纳法就是对自然数的定义的一部分。首先，根据定义，我们知道自然数满足 \N= 0\ |\ S(\N)¹，这就允许我们把归纳论证想象成一个“尝试构造自然数集的过程”，令 P(n) 是一个归纳命题，归纳论证背后的直觉如下：

令 S=\lbrace n\in \N \ |\ P(n)\rbrace 是一个被 P(n) 所确定的集合，由于 P(n) 是一个归纳属性，显然有 1\in S，同理，有 2\in S，且对于任意 n\in S，都有 n+1\in S，这意味着 S 符合自然数的定义，即 S=\N

从上面的论证可以看出，归纳论证的过程实际上是说 P(n) 的外延是 \N，因此 P(n) 对所有 \N 成立，这意味着某种程度上归纳论证可以被看做是对自然数定义的另外一种描述。
  接下来，让我们从集合的角度来审视一下归纳，令 F: \mathcal{P}(U) \rightarrow \mathcal{P}(U) 是一个函数，如果对于 A, B\in \mathcal{P}(U) 且 A\subseteq B，有 F(A)\subseteq F(B)，则称 F 为单调的，令 X\in \mathcal{P}(U)，如果 F(X)\subseteq X，则 X 是 F-closed 的；如果 X\subseteq F(X)，则 X 是 F-consistent 的，如果 F(X)=X，则说 X 是 F 的一个 不动点。
  这样的单调函数 F 可以被当作是一个“推理函数”，它的参数是一组逻辑语句，而 F 负责“看看由这一组逻辑语句能推出什么新的语句”，F-closed 集合意味着这些定理是 self-contained 的，无法再推导出什么新的定理，而 F-consistent 意味着这个集合中的所有定理都是由同样在这个集合中的定理推出来的：假设 A, B\vdash C, 则 F(\lbrace A, B \rbrace)=\lbrace A, B, C\rbrace，也即证明新定理 C 的所有定理都已经在 \lbrace A, B\rbrace 中。从这个角度来理解，为什么 F 是单调的也就很显然了，因为推理关系 \vdash 可以被当作一个序关系，直觉上，可以把 F 理解成一个“从较小的元素产生较大的元素的生成函数”，例如在上面的例子中，如果将 \vdash 比做一个序关系，那么 A, B 显然是 C 的 predecessor，而 F 则从 \lbrace A, B\rbrace 生成了他们的 successor C，此时如果 F 不是单调的，就会出现 derivation tree 中的 premise 被 conclusion 所推导出来的荒谬情况。

例如，如果令 F(\lbrace A, B\rbrace)=\lbrace A, B, C\rbrace，F(\lbrace A, B, C\rbrace)=\lbrace A, B\rbrace，则 F 不是单调的，而从我们把 F 解释为 \vdash 的语义来看，这显然是荒谬的。

在之后我们将 F 解释为其他函数时，无论是解释为自然数的 succ 函数、逻辑的 implication，还是解释为序关系上的小于等于，语义上也处于同一原因同样满足这个单调性的特点，即从作为 predecessor 的元素，生成作为 successor 的元素。
  让我们首先看一下这样的 F 是如何和归纳扯上关系的

Knaster-Tarski 定理: 令 U 是一个集合，F:\mathcal{P}(U)\rightarrow\mathcal{P}(U) 是一个 U 上的单调函数，则 F 的最小不动点 \mu F 是所有 F-closed 集合的交集，而 F 的最大不动点 \nu F 是所有 F-consistent 集合的并集。

因此，可以很直观的推导出：

1. （Principle of Induction）对于所有的 F-closed 集合 X，\mu F\subseteq X
2. （Principle of Coinduction）对于所有的 F-consistent 集合 X，X\subseteq \nu F

先放开第二条不管，只看第一条，第一条告诉我们，如果要证明 \mu F\subseteq X，只需要证明 X 是一个 F-closed 的集合，这意味着什么呢？注意到，我们将 F 当做一个生成函数来对待（你可以把 F 想象成一个对应了 inference rules 的函数），又因为 \mu F 本身是 F-closed 的，这意味着 \mu F 是一个 inductive set（任何 F-closed 集合都可以通过先选择其中的一部分元素作为 generator，然后递归的调用 F 得到）。现在，结合上面所提到的，归纳的证明过程本质上是证明某个归纳命题 P 的外延是 \N²，而 \N 就是一个 inductively defined set，因此，我们可以令 \mu F=\N 并且使用如下设置：

令 U=\N，S: \mathcal{P}(\N)\rightarrow \mathcal{P}(\N) 是自然数的 succ 函数，也即 S(X)=\lbrace 0\rbrace\cup \lbrace x+1\ |\ x\in X\rbrace，则 \mu S 显然是 \N，令 P 是 \N 上任意归纳属性的外延（或者说 P 是 \N 上的任意 inductive set），则如果 S(P)\subseteq P，也即 P 是 S-closed 的，则 \N\subseteq P，又因为 P 是 \N 上的 inductive set，因此 P 至多等于 \N，即如果 P 是 S-closed 的，则 P=\N。

回顾一下之前说过的“归纳法背后的直觉”，里面提到了归纳法的本质基本上是定义了一个 \N，或者说证明某个归纳命题的外延是 \N，而这就正是我们上面所描述的，通过引用 Principle of Induction，要证明某个属性 P 对所有 n\in \N 都成立，我们只需要证明这个属性 P 的外延是 S-closed 的，也即 S(P)\subseteq P，这意味换句话说，只需要证明

对于所有的 x\in\ N，如果 x\in P，那么 S(x)\in P。

如果将 S(x) 的定义展开，这蕴含了

0\in P，且对于对于所有的 x\in\N，如果 x\in P，那么 x+1\in P

而这恰好是对归纳法的描述。

  在本文中，我们将 Induction 作为一种证明技巧来对待，并且通过取对偶提出了 Coinduction 这一种证明技巧，同时还对这两种技巧进行了数学上的 formulation 和合适的 generalization。，在本文的下一个章节中，我们会从类型的视角了解 Inductive Type 和 Coinductive Type，以及他们之间、尤其是在 finiteness 上的异同。