第6章 递归类型 6.1引 言 在某些程序设计语言中，类型可以递归地定义。例如ML,它有递归的datatype声明。 递归类型是类型等式系统的解，就像递归函数是项等式系统的解一样。例如，自然数表的类 型可以想象成类型等式1三mit+(nal×)的一个解，二叉树的类型可以想象成类型等式1三 i1+(1×)的一个解。“=”表示一个类型等式系统的解是要使等式两边的类型表达式同构， 而不是要使它们相等。 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到类型同构等式的最小 解，也叫做初始解；余归纳类型对应到它们的最大解，也叫做终结解。直观地说，归纳类型 被看成是包含它们引入形式的“最小”类型：而其消去形式是在这引入形式上的一种递归形 式。对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型：而其引入形式是一种 在这消去形式需要时提供元素的方法。推动归纳类型研究的一个例子是自然数类型，而推动 余归纳类型研究的一个例子是自然数流类型，它们在6.3和6.4节介绍。 归纳的概念比较熟悉，相应地理解归纳类型也比较容易。而要想理解余归纳类型，则必 须首先了解余归纳概念，包括余归纳定义和余归纳证明原理等，以及它们和归纳的相应概念 的对偶关系。对形式受到一定约束的递归类型等式，在不止一个解的情况下，某个初始代数 对应它的最小解，而某个终结余代数对应它的最大解。因此还需要了解余代数以及代数和余 代数的对偶性。 代数是数学中很好地确立了的一部分，涉及带有运算的集合，这些运算满足一定的性质， 这样的集合有群、环、向量空间等等。泛代数则在更高一个抽象层次上研究代数结构，研究 它们之间的同态、子代数和同余等。 概括地说，程序处理数据。在上世纪七八十年代就己经逐步清楚的是，这些数据的抽象 描述有望保证一个程序不依赖于它所操作数据的具体表示。这样的抽象也方便了正确性证 明。这种期望导致了代数方法在计算机科学中的使用，形成称为代数规范或抽象数据类型理 论的一个分支。它用代数中熟知的概念和技术来研究计算机科学中使用的数据类型。第2 章己经介绍了这方面的知识。 通常的代数技术己经展示出在捕捉计算机科学所用数据结构的本质方面是非常有用的。 但是，在试图代数地描述计算过程中出现的天性地动态的结构时，却遇到了困难。这样的结 构通常包括状态概念，状态可以按不同的方式进行变换。对于这样基于状态的动态系统，形 式方法一般利用自动机或迁移系统。上世纪九十年代，对这样基于状态的系统的深刻认识逐 步形成，它们不应该描述成代数，而应该是余代数。余代数是代数的对偶，这是本章需要介 绍的概念。代数中初始性的对偶性质（即终结性）对余代数来说是关键的，并且这样的终结 余代数所需的逻辑推理原理不是归纳，而是余归纳。在计算机科学中，代数方法是从“构造 的”角度研究抽象数据类型的语义，而余代数方法是从“观察的”的角度描述诸如对象、自 动机、进程、软件构件等基于状态的系统。 本章的主要内容有： (1)直观地介绍余归纳的定义、余归纳的证明原理和余代数。 (2)形式地介绍递归类型。 (3)形式地介绍归纳类型和余归纳类型。 1
1 第 6 章 递归类型 6.1 引 言 在某些程序设计语言中，类型可以递归地定义。例如 ML，它有递归的 datatype 声明。 递归类型是类型等式系统的解，就像递归函数是项等式系统的解一样。例如，自然数表的类 型可以想象成类型等式 t ≅ unit + (nat × t)的一个解，二叉树的类型可以想象成类型等式 t ≅ unit + (t × t)的一个解。“≅”表示一个类型等式系统的解是要使等式两边的类型表达式同构， 而不是要使它们相等。 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到类型同构等式的最小 解，也叫做初始解；余归纳类型对应到它们的最大解，也叫做终结解。直观地说，归纳类型 被看成是包含它们引入形式的“最小”类型；而其消去形式是在这引入形式上的一种递归形 式。对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型；而其引入形式是一种 在这消去形式需要时提供元素的方法。推动归纳类型研究的一个例子是自然数类型，而推动 余归纳类型研究的一个例子是自然数流类型，它们在 6.3 和 6.4 节介绍。 归纳的概念比较熟悉，相应地理解归纳类型也比较容易。而要想理解余归纳类型，则必 须首先了解余归纳概念，包括余归纳定义和余归纳证明原理等，以及它们和归纳的相应概念 的对偶关系。对形式受到一定约束的递归类型等式，在不止一个解的情况下，某个初始代数 对应它的最小解，而某个终结余代数对应它的最大解。因此还需要了解余代数以及代数和余 代数的对偶性。 代数是数学中很好地确立了的一部分，涉及带有运算的集合，这些运算满足一定的性质， 这样的集合有群、环、向量空间等等。泛代数则在更高一个抽象层次上研究代数结构，研究 它们之间的同态、子代数和同余等。 概括地说，程序处理数据。在上世纪七八十年代就已经逐步清楚的是，这些数据的抽象 描述有望保证一个程序不依赖于它所操作数据的具体表示。这样的抽象也方便了正确性证 明。这种期望导致了代数方法在计算机科学中的使用，形成称为代数规范或抽象数据类型理 论的一个分支。它用代数中熟知的概念和技术来研究计算机科学中使用的数据类型。第 2 章已经介绍了这方面的知识。 通常的代数技术已经展示出在捕捉计算机科学所用数据结构的本质方面是非常有用的。 但是，在试图代数地描述计算过程中出现的天性地动态的结构时，却遇到了困难。这样的结 构通常包括状态概念，状态可以按不同的方式进行变换。对于这样基于状态的动态系统，形 式方法一般利用自动机或迁移系统。上世纪九十年代，对这样基于状态的系统的深刻认识逐 步形成，它们不应该描述成代数，而应该是余代数。余代数是代数的对偶，这是本章需要介 绍的概念。代数中初始性的对偶性质（即终结性）对余代数来说是关键的，并且这样的终结 余代数所需的逻辑推理原理不是归纳，而是余归纳。在计算机科学中，代数方法是从“构造 的”角度研究抽象数据类型的语义，而余代数方法是从“观察的”的角度描述诸如对象、自 动机、进程、软件构件等基于状态的系统。 本章的主要内容有： （1）直观地介绍余归纳的定义、余归纳的证明原理和余代数。 （2）形式地介绍递归类型。 （3）形式地介绍归纳类型和余归纳类型
6.2 归纳和余归纳 6.2.1余归纳现象 本节先通过例子直观地介绍余归纳的数据、余归纳的函数和余归纳的证明。先介绍余归 纳的数据。 归纳法是构造主义的方法，用归纳法定义数据时，可以把它分解成几个基本步骤：基础 情况、迭代规则和最小化条件。归纳法从本质上来讲是封闭的。归纳法是定义字符串集合、 形式系统和可计算函数等的基础。 例61数据集A上的有限表集可归纳地定义如下： (1)基础情况：nil是有限表； (2)迭代规则：如果aeA,并且o是有限表，则cons(a,o)是有限表： (3)最小化条件：除此之外，有限表集中不含其它元素。 最小化规则是指所定义的集合是满足(1)和(2)两条约束的最小集合，没有任何垃圾 在其中。 ◇ 余归纳也分成几个基本步骤：迭代规则和最大化条件。与归纳法相比，余归纳删去了基 础情况，修改了迭代规则，称之为循环条件，并用最大化条件替换了最小化条件。 例62数据集A上的无限表集（称为流）可余归纳地定义如下： (1)迭代规则：如果a∈A,并且o是无限表，则cons(a,o)是无限表： (2)最大化条件：数据集A上的无限表集是满足迭代规则的最大集合。 和归纳不一样，最大化条件表示所有未被(1)排除的元素都被包含在所定义的集合中， 即该集合中的任何无限表都可以通过应用规则(1)若干次（可能是无限次）而得到。 有限表和无限表都有观察算子head和运算算子tail。它们满足的等式是 head(cons(a,))=a tail(cons(a,o))=o 这两个算子合在一起又称为有限表和无限表的解构子(destructor)。 ◇ 交互计算是在两个层次上余归纳的：余归纳定义的静态值域和余归纳定义的动态下一步 动作。 现在考虑在余归纳定义的集合上定义函数。在归纳定义的数据上通常定义的是递归函 数，在这样的函数中，需要定义它在所有构造子上的值。例如对于有限表集，计算表长的函 数length的定义如下： length(nil)=0 length(cons(a,o))=1+length(o) 在上述等式的左边，构造子出现在所定义的函数“里面”。 在一个函数的余归纳定义中，需要定义所有解构子在每个∫()上的值。仍以无限表集合 为例，如果有函数f:A→A,那么首先可以定义的一个拓展函数xf),它通过把应用到无 限表o的每个元素而得到新的无限表ex(f)(o),然后需要定义解构子head和1ail应用到无限表 exf)(o)的值： head(exi(f)()=f(head()) tail(exi(f)()=exi(f)(tail(o)) 在上述等式的左边，所定义的函数出现在解构子的“里面”。 例6.3仍以无限表为例，假定想定义一个运算odd,它应用到一个无限表上，忽略其所 有偶数位置上的元素，将其剩余元素按原来次序形成一个新的无限表。略加思考可得到如下 2
2 6.2 归纳和余归纳 6.2.1 余归纳现象 本节先通过例子直观地介绍余归纳的数据、余归纳的函数和余归纳的证明。先介绍余归 纳的数据。 归纳法是构造主义的方法，用归纳法定义数据时，可以把它分解成几个基本步骤：基础 情况、迭代规则和最小化条件。归纳法从本质上来讲是封闭的。归纳法是定义字符串集合、 形式系统和可计算函数等的基础。 例6.1 数据集A上的有限表集可归纳地定义如下： （1）基础情况：nil是有限表； （2）迭代规则：如果a∈A，并且σ是有限表，则cons(a, σ)是有限表； （3）最小化条件：除此之外，有限表集中不含其它元素。 最小化规则是指所定义的集合是满足（1）和（2）两条约束的最小集合，没有任何垃圾 在其中。 余归纳也分成几个基本步骤：迭代规则和最大化条件。与归纳法相比，余归纳删去了基 础情况，修改了迭代规则，称之为循环条件，并用最大化条件替换了最小化条件。 例6.2 数据集A上的无限表集（称为流）可余归纳地定义如下： （1）迭代规则：如果a∈A，并且σ是无限表，则cons(a, σ)是无限表； （2）最大化条件：数据集A上的无限表集是满足迭代规则的最大集合。 和归纳不一样，最大化条件表示所有未被（1）排除的元素都被包含在所定义的集合中， 即该集合中的任何无限表都可以通过应用规则（1）若干次（可能是无限次）而得到。 有限表和无限表都有观察算子head和运算算子tail。它们满足的等式是 head(cons(a, σ)) = a tail(cons(a, σ)) = σ 这两个算子合在一起又称为有限表和无限表的解构子（destructor）。 交互计算是在两个层次上余归纳的：余归纳定义的静态值域和余归纳定义的动态下一步 动作。 现在考虑在余归纳定义的集合上定义函数。在归纳定义的数据上通常定义的是递归函 数，在这样的函数中，需要定义它在所有构造子上的值。例如对于有限表集，计算表长的函 数length的定义如下： length(nil) = 0 length(cons(a, σ)) = 1 + length(σ) 在上述等式的左边，构造子出现在所定义的函数“里面”。 在一个函数f的余归纳定义中，需要定义所有解构子在每个f (x)上的值。仍以无限表集合 为例，如果有函数f : A → A，那么首先可以定义f的一个拓展函数ext(f )，它通过把f应用到无 限表σ的每个元素而得到新的无限表ext(f )(σ)，然后需要定义解构子head和tail应用到无限表 ext(f )(σ)的值： head(ext(f )(σ)) = f (head(σ)) tail(ext(f )(σ)) = ext(f )(tail(σ)) 在上述等式的左边，所定义的函数出现在解构子的“里面”。 例6.3 仍以无限表为例，假定想定义一个运算odd，它应用到一个无限表上，忽略其所 有偶数位置上的元素，将其剩余元素按原来次序形成一个新的无限表。略加思考可得到如下
的定义： head(odd())=head(o) tail(odd(=odd(tail(tail() 第一个等式说，oddo)的第一个元素是o的第一个元素：oddo)的第二个元素是head(tail (oddo),用等式演算可得： head(tail(odd(o)))=head(odd(tail(tail(o)))=head(tail(tail(o))) 因此odd(o)的第二个元素是o的第三个元素。这正是所需要的。不难证明，对所有的自然数n, head(taiNm(oddo)和head(tail2m(o)一样。 这两个等式是纯数学规范。若要从计算的角度来看这两个等式，则必须用惰性计算的观 点。 O 最后考虑余归纳的证明。余归纳定义的数据和函数的某些性质可以用归纳法来证明，例 如例6.3中的对所有的自然数n,head(tail"(odd(o)和head(tai(σ)一样。余归纳证明的一种 专用方法基于互模拟(bisimulation)的概念。互模拟从数学上刻画系统（如对象、进程等） 行为等价这个直观概念，它是指两个系统从观测者角度看可以互相模拟对方的行为，即从观 测者角度，两个系统对同样的输入会产生同样的输出，系统内部可能有的状态不同是观察不 到的。还是以无限表为例，来解释基于互模拟的证明方法。 例6.4先余归纳地定义函数even,,它应用到一个无限表上，忽略其所有奇数位置上的元 素，将其剩余元素按原来次序形成一个新的无限表。显然ven可以这样定义： even odd o tail 再定义应用到两个无限表o和的归并函数merge。.merge依次从o和轮流取元素，形成 一个新的无限表。同样，merge的余归纳定义需要解构子head和tail在merge(o,)上的结果： head(merge(o,t))=head(o) tail(merge(o,T))=merge(t,(tail()) 下面基于互模拟证明nergel(oddo),even(o)=o。无限表集合上的互模拟是满足下面条 件的二元关系R: 若(a,t)∈R,则head)=head)并且(ailo,tail(》∈R。 在无限表集合上基于互模拟的余归纳证明原理是： 对互模拟关系R,若(c,)∈R,则o=t。 国 R={(merge(odd(o),even(o),lo是一个无限表} 根据该余归纳证明原理，为了证明merge(oddσ)，even(σ)=o,只要证明R是互模拟关系就可 以了，也就是要证明互模拟关系的两个必要条件。 对于第一个条件，有 head(merge(odd(o),even(G)))=head(odd(G))=head(o) 对第二个条件，若有merge(oddo),even(o),o)∈R,则把1ail应用到该序对的两元时，产生 的新序对组tail(merge(oddo),even(o),tail(》也在R中，因为tail(merge(oddo),even(》= merge(odd1ail(oj,even(tail(o))。利用even=oddotail,该等式的证明如下： tail(merge(odd(o),even()))=merge(even(o),tail(odd()) =nerge(odd(tail(σ)，odd(tail(tail(o)) =merge(odd(tail(o)),even(tail())) 利用归纳和等式演算，也可以证明nerge(oddo),even(o)=o,但是没有这么简单。可 以对所有的自然数，用归纳法先证明下面几个等式： head(tail"(odd())=head(tai() head(tailm(merge(o,))=head(taikm()) 3
3 的定义： head(odd(σ)) = head(σ) tail(odd(σ)) = odd(tail(tail(σ))) 第一个等式说，odd(σ)的第一个元素是σ的第一个元素；odd(σ)的第二个元素是head(tail (odd(σ)))，用等式演算可得： head(tail(odd(σ))) = head(odd(tail(tail(σ)))) = head(tail(tail(σ))) 因此odd(σ)的第二个元素是σ的第三个元素。这正是所需要的。不难证明，对所有的自然数n， head(tail(n) (odd(σ)))和head(tail(2n) (σ))一样。 这两个等式是纯数学规范。若要从计算的角度来看这两个等式，则必须用惰性计算的观 点。 最后考虑余归纳的证明。余归纳定义的数据和函数的某些性质可以用归纳法来证明，例 如例6.3中的对所有的自然数n，head(tailn (odd(σ)))和head(tail2n (σ))一样。余归纳证明的一种 专用方法基于互模拟（bisimulation）的概念。互模拟从数学上刻画系统（如对象、进程等） 行为等价这个直观概念，它是指两个系统从观测者角度看可以互相模拟对方的行为，即从观 测者角度，两个系统对同样的输入会产生同样的输出，系统内部可能有的状态不同是观察不 到的。还是以无限表为例，来解释基于互模拟的证明方法。 例6.4 先余归纳地定义函数even，它应用到一个无限表上，忽略其所有奇数位置上的元 素，将其剩余元素按原来次序形成一个新的无限表。显然even可以这样定义： even = odd D tail 再定义应用到两个无限表σ和τ的归并函数merge。merge依次从σ和τ轮流取元素，形成 一个新的无限表。同样，merge的余归纳定义需要解构子head和tail在merge(σ, τ)上的结果： head(merge(σ, τ)) = head(σ) tail(merge(σ, τ)) = merge(τ, (tail(σ)) 下面基于互模拟证明merge(odd(σ), even(σ)) = σ。无限表集合上的互模拟是满足下面条 件的二元关系R： 若〈σ, τ〉 ∈R，则head(σ) = head(τ)并且〈tail(σ), tail(τ)〉 ∈R。 在无限表集合上基于互模拟的余归纳证明原理是： 对互模拟关系R，若〈σ, τ〉 ∈R，则σ = τ。 令 R = {〈merge(odd(σ), even(σ)), σ〉 | σ是一个无限表} 根据该余归纳证明原理，为了证明merge(odd(σ), even(σ)) = σ，只要证明R是互模拟关系就可 以了，也就是要证明互模拟关系的两个必要条件。 对于第一个条件，有 head(merge(odd(σ), even(σ))) = head(odd(σ)) = head(σ) 对第二个条件，若有〈merge(odd(σ), even(σ)), σ〉 ∈R，则把tail应用到该序对的两元时，产生 的新序对组〈tail(merge(odd(σ), even(σ))), tail(σ)〉也在R中，因为tail(merge(odd(σ), even(σ))) = merge(odd(tail(σ)), even(tail(σ)))。利用even = odd D tail，该等式的证明如下： tail(merge(odd(σ), even(σ))) = merge(even(σ), tail(odd(σ)) = merge(odd(tail(σ)), odd(tail(tail(σ)))) = merge(odd(tail(σ)), even(tail(σ))) 利用归纳和等式演算，也可以证明merge(odd(σ), even(σ)) = σ，但是没有这么简单。可 以对所有的自然数n，用归纳法先证明下面几个等式： head(tail(n) (odd(σ))) = head(tail(2n) (σ)) head(tail(2n) (merge(σ, τ))) = head(tail(n) (σ))
head(tail2m+(merge(a,t》=head1aim(t》 然后利用等式演算证明 head(tailm(merge(odd(),even()))=head(taim()) 显然这个证明比用余归纳原理的证明要复杂得多。 6.2.2归纳和余归纳指南 本节从集合论角度介绍余归纳定义和余归纳证明原理。 令U是某个泛集(niversal set),并且F:P(U)→P(U)(P(U)表示U的幂集)是一个单 调函数（即Xc蕴涵F)∈F())。归纳和余归纳是对偶的证明原理，它们分别衍生于作为 形式为X=F)方程的最小解或最大解的集合的定义。 首先给出一些定义。一个集合XcU是F封闭的，当且仅当F)CX。对偶地，一个集合 XcU是F致密(dense)的，当且仅当X∈F)。F的不动点是方程X=F)的解。令KF) 和XF)分别是满足下面条件的U的子集： Y.FX)≌∩{XIF)∈S XF)≌U{XIX∈F)} 引理6.1 (1)XF)是最小的F封闭集合。 (2)XFX)是最大的F致密集合。 证明仅证明(2)，(1)可以由对偶地论述得到。由XF)的定义知道，它包含每一 个F致密集合，因此仅需要证明它本身是致密的就可以了。这只要证明下面的引理就足够 了： 如果每个X都是F致密的，那么它们的并札UX也是。 因为对每个有X∈F(X),那么U,X,∈U,FX)。因为F是单调的，那么对每个有FX)S FUX。由此可得UFX)cFUX)。再由传递性，UXEFU,X),即UX是F致密的。口 定理6.2 (1)XFX)是F的最小不动点。 (2)XFX)是F的最大不动点。 证明再次仅证明(2)，(1)可以由对偶地论述得到。令v=XFX)。由引理6.1，y 是致密的，因此VSF()。由F的单调性，F(WsF(F(),因此F(也是致密的。由的定义 知道F()∈。由和F()之间的这两个不等式得v=F()。是最大不动点，因为任何其他不 动点都是致密的，因而都包含在中。 0 XFX)是X=F)的最小解，被称为是由F归纳地定义的集合：对偶地，XF)是X= F)的最大解，被称为是由F余归纳地定义的集合。这样就得到和这些定义相关联的两个对 偶的证明原理： (1)归纳：如果X是F封闭的，那么XF)cX。 (2)余归纳：如果X是F致密的，那么XcXF)。 自然数归纳是该一般框架的一种特殊情况。假定存在一个元素0∈U,并且存在一个内射 函数S:U→U。若单调函数FP(U)→P(U)由下式定义： FX)≌{0}U{Sx)|xeX3 令集合W≌XF),那么上述归纳原理告知： 若F)∈X,那么W∈X。 换句话说， 若0eX,并且只要x∈X,则S(x)EX,那么W∈X。 这样，要想证明所有的自然数满足某个性质，可以假定X是满足该性质的所有元素集合， 4
4 head(tail(2n + 1) (merge(σ, τ))) = head(tail(n) (τ)) 然后利用等式演算证明 head(tail(2n) (merge(odd(σ), even(σ)))) = head(tail(n) (σ)) 显然这个证明比用余归纳原理的证明要复杂得多。 6.2.2 归纳和余归纳指南 本节从集合论角度介绍余归纳定义和余归纳证明原理。 令U是某个泛集（universal set），并且F : P(U) → P(U)（P(U)表示U的幂集）是一个单 调函数（即X⊆Y蕴涵F(X) ⊆ F(Y)）。归纳和余归纳是对偶的证明原理，它们分别衍生于作为 形式为X = F(X)方程的最小解或最大解的集合的定义。 首先给出一些定义。一个集合X⊆U是F封闭的，当且仅当F(X) ⊆X。对偶地，一个集合 X⊆U是F致密（dense）的，当且仅当X ⊆ F(X)。F的不动点是方程X = F(X)的解。令μX.F(X) 和νX.F(X)分别是满足下面条件的U的子集： μX.F(X) ∩ {X | F(X) ⊆ X} νX.F(X) ∪ { X | X ⊆ F(X)} 引理6.1 （1）μX.F(X)是最小的F封闭集合。 （2）νX.F(X)是最大的F致密集合。 证明 仅证明（2），（1）可以由对偶地论述得到。由νX.F(X)的定义知道，它包含每一 个F致密集合，因此仅需要证明它本身是F致密的就可以了。这只要证明下面的引理就足够 了： 如果每个Xi都是F致密的，那么它们的并∪i Xi也是。 因为对每个i有Xi ⊆ F(Xi)，那么∪i Xi ⊆ ∪i F(Xi)。因为F是单调的，那么对每个i有F(Xi) ⊆ F(∪i Xi)。由此可得∪iF(Xi) ⊆ F(∪i Xi)。再由传递性，∪i Xi ⊆ F(∪i Xi)，即∪i Xi是F致密的。 定理6.2 （1）μX.F(X)是F的最小不动点。 （2）νX.F(X)是F的最大不动点。 证明 再次仅证明（2），（1）可以由对偶地论述得到。令ν = νX.F(X)。由引理6.1，ν 是致密的，因此ν ⊆ F(ν)。由F的单调性，F(ν) ⊆ F(F(ν))，因此F(ν)也是致密的。由ν的定义 知道F(ν) ⊆ ν。由ν和F(ν)之间的这两个不等式得ν = F(ν)。ν是最大不动点，因为任何其他不 动点都是致密的，因而都包含在ν中。 μX.F(X)是X = F(X)的最小解，被称为是由F归纳地定义的集合；对偶地，νX.F(X)是X = F(X)的最大解，被称为是由F余归纳地定义的集合。这样就得到和这些定义相关联的两个对 偶的证明原理： （1）归纳： 如果X是F封闭的，那么μX.F(X) ⊆ X。 （2）余归纳：如果X是F致密的，那么X⊆νX.F(X)。 自然数归纳是该一般框架的一种特殊情况。假定存在一个元素0∈U，并且存在一个内射 函数S:U →U。若单调函数F:P(U) →P(U)由下式定义： F(X) {0} ∪ {S(x) | x∈X} 令集合N μX.F(X)，那么上述归纳原理告知： 若F(X) ⊆ X，那么N ⊆ X。 换句话说， 若0∈X，并且只要x∈X，则S(x)∈ X，那么N ⊆ X。 这样，要想证明所有的自然数满足某个性质，可以假定X是满足该性质的所有元素集合
然后证明X满足不等式 {O}U{Sx)lx∈XcX 若能证明，则N二X,即所有自然数都满足该性质。这就是自然数归纳。 计算机学科中熟悉的结构归纳和规则归纳等证明原理都是从某个特定的归纳定义得到 的归纳原理。 对偶地，一个集合是余归纳定义的，若它是某种形式的不等式的最大解。下面以不终止 的项重写系统为例来解释。 例6.5用T表示某个项重写系统的项集。按某种确定的归约策略，不终止的项集可以如 下定义： Tnm≌{MN:T.(M→→N)→N不是范式)} 可以根据无界的归约来余归纳地刻画不终止性。令D:P(T)→P(T)并且T聊是如下定义的T 的子集： D)≌{M3N:T.(M→N)AN∈X} T兰XDX) 很容易看出D是单调的，因此由余归纳定义知道，T聊是最大的D致密集合并且T斯=D(T)。 下面证明Tnom=T聊。首先证明TsTnon。假定M∈T物，则必须证明每当M→yN,则 N不是范式，即证明Me Tnons。因为MeT,则存在M使得M→M并且M∈T。显然由归 纳可知，若MN,则N不是范式。 再证明TmcT即。由余归纳的定义，只要证明Tm是D致密的就可以了，因为T即是最 大的D致密集合。假定ME Thon。因为M→，M,因此M不是范式，即存在N使得M→N。 因为只要N→N',则也有M→yW”,并且W也不是范式，因为Me Tnon。于是有NeTm 即MED(T,mom)。从ME Tnon得到MED(Tomn)就可以知道Tnom是D致密的。 6.2.3代数和余代数 从普通算法到交互计算的转变在数学上表现为一系列的扩展：从归纳到余归纳的扩展、 从良基集到非良基集的扩展、从代数到余代数的扩展。从归纳到余归纳的扩展表达了从字符 串到流的转变，这是从算法到交互的转变的基础：非良基集作为流的行为的形式模型被引进： 余代数则为流的演算提供工具，它在交互计算模型中的地位相当于入演算在图灵计算模型中 的地位。本小节简要介绍余代数以及它和代数之间的对偶性，所用到的范畴论初步知识尽量 用比较通俗的文字来阐述。 从第3章已经知道，对两个集合X和Y,它们的笛卡儿积是如下的序对集合： X×Y≌{K,y)xEXAYEY} 并且射影函数Proju:X×Y→X和Pro2:X×Y→Y满足等式Projr(c,y)=x和Proj(x,y)=ya 还有，对函数f:Z→X和g:Z→Y,存在唯一的“配对”函数5，g〉：Z→X×Y使得Proj1o g〉=∫并且Proj2og〉=g,即对zeZ,gXe)=f(e),ge)》∈X×Y。 二元积的这些性质在范畴论中可以用交换图表表示，如图6.1()所示。交换图表中每个 节点都表示一个集合，有向边表示相应的两个集合之间的一个函数。若从交换图表一个节点 到另一个节点有两条路径，则这两条路径上的函数分别复合的结果相等。图6.l()表示的就 是Proj1o,g〉=f并且Proj2of8)=g 从第3章己经知道，对两个集合X和Y,它们的和（又称可区分并、余积）是如下的序 对集合： X+Y≌{0，x)Ix∈X}U{L,y)川yeY} 其中序对中第一个成员0和1用来使并可区分。内射函数（又称余射影函数）Inleft::X→X +Y和Inright:Y→X+Y以及它们满足的性质可以用6.l(b)的交换图表表示。即具有性质/ 5
5 然后证明X满足不等式 {0} ∪ {S(x) | x∈X} ⊆ X 若能证明，则N ⊆ X，即所有自然数都满足该性质。这就是自然数归纳。 计算机学科中熟悉的结构归纳和规则归纳等证明原理都是从某个特定的归纳定义得到 的归纳原理。 对偶地，一个集合是余归纳定义的，若它是某种形式的不等式的最大解。下面以不终止 的项重写系统为例来解释。 例6.5 用T表示某个项重写系统的项集。按某种确定的归约策略，不终止的项集可以如 下定义： Tnon { M | ∀N:T.((M →→ N) ⇒ N 不是范式) } 可以根据无界的归约来余归纳地刻画不终止性。令 D : P(T) → P(T)并且 Tgfp 是如下定义的 T 的子集： D(X) { M | ∃N:T.((M → N) ∧ N ∈ X } Tgfp νX.D(X) 很容易看出D是单调的，因此由余归纳定义知道，Tgfp是最大的D致密集合并且Tgfp = D(Tgfp)。 下面证明 Tnon = Tgfp。首先证明 Tgfp⊆Tnon。假定 M∈Tgfp，则必须证明每当 M →→ N，则 N 不是范式，即证明 M∈Tnon。因为 M∈Tgfp，则存在 M′使得 M → M′并且 M′∈Tgfp。显然由归 纳可知，若 M →→ N，则 N 不是范式。 再证明 Tnon⊆Tgfp。由余归纳的定义，只要证明 Tnon 是 D 致密的就可以了，因为 Tgfp 是最 大的 D 致密集合。假定 M∈Tnon。因为 M →→ M，因此 M 不是范式，即存在 N 使得 M → N。 因为只要 N →→ N′，则也有 M →→ N′，并且 N′也不是范式，因为 M∈Tnon。于是有 N∈Tnon， 即 M∈D(Tnon)。从 M∈Tnon得到 M∈D(Tnon)就可以知道 Tnon 是 D 致密的。 6.2.3 代数和余代数 从普通算法到交互计算的转变在数学上表现为一系列的扩展：从归纳到余归纳的扩展、 从良基集到非良基集的扩展、从代数到余代数的扩展。从归纳到余归纳的扩展表达了从字符 串到流的转变，这是从算法到交互的转变的基础；非良基集作为流的行为的形式模型被引进； 余代数则为流的演算提供工具，它在交互计算模型中的地位相当于λ演算在图灵计算模型中 的地位。本小节简要介绍余代数以及它和代数之间的对偶性，所用到的范畴论初步知识尽量 用比较通俗的文字来阐述。 从第 3 章已经知道，对两个集合 X 和 Y，它们的笛卡儿积是如下的序对集合： X × Y {〈x, y〉 | x∈X ∧ y∈Y } 并且射影函数 Proj1: X × Y → X 和 Proj2: X × Y → Y 满足等式 Proj1 (x, y) = x 和 Proj2(x, y) = y。 还有，对函数 f : Z → X 和 g : Z → Y，存在唯一的“配对”函数〈f, g〉 : Z → X × Y 使得 Proj1D 〈f, g〉 = f 并且 Proj2D 〈f, g〉 = g，即对 z∈Z，〈f, g〉(z) = 〈f (z), g(z)〉 ∈ X × Y。 二元积的这些性质在范畴论中可以用交换图表表示，如图 6.1(a)所示。交换图表中每个 节点都表示一个集合，有向边表示相应的两个集合之间的一个函数。若从交换图表一个节点 到另一个节点有两条路径，则这两条路径上的函数分别复合的结果相等。图 6.1(a)表示的就 是 Proj1D 〈f, g〉 = f 并且 Proj2D 〈f, g〉 = g。 从第 3 章已经知道，对两个集合 X 和 Y，它们的和（又称可区分并、余积）是如下的序 对集合： X + Y {〈0, x〉 | x∈X } ∪ {〈1, y〉 | y∈Y } 其中序对中第一个成员 0 和 1 用来使并可区分。内射函数（又称余射影函数）Inleft: X → X + Y 和 Inright: Y → X + Y 以及它们满足的性质可以用 6.1(b)的交换图表表示。即具有性质[f