第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
gJoInleft=f并且f,g]oInright=g,其中余配对函数[fg:X+Y→Z的定义如下： [f(x)如果w=0,x)》 [fg]w)兰 g(y)如果w=1,y〉 从图6.1可以看出，(a)和b)两个图的区别在于代表函数的所有有向边的方向相反，这正 体现积与和的对偶性。上面有关二元积和二元和的性质很容易推广到多元的场合。 Z Z (1 g) g Proji X×Y Proj2 Inlef +Y Inright (a) (b) 图6.1积与和的交换图表 所有的集合和它们之间的函数构成一个范畴，称为集合范畴。在这个范畴中，每个集合 是范畴的一个对象（表示为图表上的一个节点），每个函数是相应两个对象之间的射（表示 为图表上的一条有向边)。所有这些对象（集合）加上这些对象之间的所有射（函数）满足 作为一个范畴的4个条件： (1)射是可以合成的（函数可以复合）： (2)射的合成满足结合律（函数复合有性质(hog)of=ho(go): (3)每个对象都有一个恒等射（每个集合都有一个恒等函数）： (4)如果f:A→B是对象A到B的射，id4和idB分别表示A和B的恒等射，o表示射 的合成运算，那么foid4=idBof=∫（显然恒等函数满足该性质）。 函子是范畴之间保结构的映射，在此只关心集合范畴到它自身的映射。集合范畴到它自 身的映射F由Fo和F两部分构成：Fo将集合映射到集合，F,将函数映射到函数。映射F 若满足下面3个条件则称为函子： (1)若∫：A→B在集合范畴中，则F(f):F(A)→Fo(B)也在集合范畴中： (2)对任何集合A,F(idA)=id( (3)若f:A→B和g:B→C都在集合范畴中，则F(go)=Fi(g)oF(f) 下面不再使用F和F,而是直接使用F,若它的变元是集合或函数，则F分别代表F0 或F1。 下面可以基于函子来定义代数，只考虑单类代数的情况。令F是函子，F的一个代数（简 称F代数)是一个序对U,a),其中U是集合，称为该代数的载体，a是函数a:F(U)→U, 称为该代数的代数结构（也称为运算）。 例6.6自然数上的零和后继函数0：1→W和S:W→W(其中1在这里代表对应nit类 型的单元素集合)形成函子F)=1+X的一个F代数(1+W,0,):1+W→W)。 以集合A的元素标记节点的二叉树的集合用tree(4)表示，则空树nil可用函数nil:1→ tree(A)表示，node:ree(4)×A×tree(A)→tree(A)表示从两棵子树和一个节点标记构造一棵 树。nil和node形成函子F)=l+(X×A×)的一个代数 F(f) [nil,node]:1+(tree(A)x Ax tree(A))->tree(A). F(U) →F( 基于函子和交换图表可以给出代数同态的另一种表 0 b 示。令F是函子，a:F(U)→U和b:F)→'是两个函 数。F代数U,a)到W,b)的同态是一个函数f:U→V,满 f 足foa=boF0,其交换图表在图6.2。 图6.2代数同态的交换图表 6
6 g]DInleft = f 并且[f, g]DInright = g，其中余配对函数[f, g] : X + Y → Z 的定义如下： [f, g](w) ( ) 0, ( ) 1, f x wx gy w y ⎧ = 〈 〉 ⎨ ⎩ = 〈 〉 如果 如果 从图 6.1 可以看出，(a)和(b)两个图的区别在于代表函数的所有有向边的方向相反，这正 体现积与和的对偶性。上面有关二元积和二元和的性质很容易推广到多元的场合。 所有的集合和它们之间的函数构成一个范畴，称为集合范畴。在这个范畴中，每个集合 是范畴的一个对象（表示为图表上的一个节点），每个函数是相应两个对象之间的射（表示 为图表上的一条有向边）。所有这些对象（集合）加上这些对象之间的所有射（函数）满足 作为一个范畴的 4 个条件： （1）射是可以合成的（函数可以复合）； （2）射的合成满足结合律（函数复合有性质(h D g) D f = h D (g D f)）； （3）每个对象都有一个恒等射（每个集合都有一个恒等函数）； （4）如果 f : A → B 是对象 A 到 B 的射，idA和 idB分别表示 A 和 B 的恒等射，D表示射 的合成运算，那么 f D idA = idB D f = f（显然恒等函数满足该性质）。 函子是范畴之间保结构的映射，在此只关心集合范畴到它自身的映射。集合范畴到它自 身的映射 F 由 F0 和 F1 两部分构成：F0 将集合映射到集合，F1 将函数映射到函数。映射 F 若满足下面 3 个条件则称为函子： （1）若 f : A → B 在集合范畴中，则 F1(f ) : F0(A) → F0(B)也在集合范畴中； （2）对任何集合 A，F1(idA) = 0 F A( ) id ； （3）若 f : A → B 和 g : B → C 都在集合范畴中，则 F1(g D f ) = F1(g) D F1(f )。 下面不再使用 F0 和 F1，而是直接使用 F，若它的变元是集合或函数，则 F 分别代表 F0 或 F1。 下面可以基于函子来定义代数，只考虑单类代数的情况。令 F 是函子，F 的一个代数（简 称 F 代数）是一个序对〈U, a〉，其中 U 是集合，称为该代数的载体，a 是函数 a : F(U) →U， 称为该代数的代数结构（也称为运算）。 例 6.6 自然数上的零和后继函数 0 : 1→N 和 S : N →N（其中 1 在这里代表对应 unit 类 型的单元素集合）形成函子 F(X) =1+ X 的一个 F 代数〈1+N , [0, S] : 1+N →N〉。 以集合 A 的元素标记节点的二叉树的集合用 tree(A)表示，则空树 nil 可用函数 nil : 1→ tree(A)表示，node : tree(A) × A × tree(A) → tree(A)表示从两棵子树和一个节点标记构造一棵 树。nil 和 node 形成函子 F(X) =1+ (X × A × X)的一个代数 [nil, node] : 1 + (tree(A) × A × tree(A)) → tree(A)。 基于函子和交换图表可以给出代数同态的另一种表 示。令 F 是函子，a : F(U) →U 和 b : F(V) →V 是两个函 数。F 代数〈U, a〉到〈V, b〉的同态是一个函数 f : U → V，满 足 f D a = b D F(f)，其交换图表在图 6.2。 图 6.1 积与和的交换图表 Z 〈f, g〉 X X × Y Y Proj1 f g (a) Proj2 Z [f, g] X X + Y Y Inlef f g Inright (b) 图 6.2 代数同态的交换图表 F(f ) F(U) U V a b f F(V)
可以进一步定义初始代数。F代数(U,a)是初始的，如果对任意的F代数(W,b),都存在 从(U,a)到(W,b)的唯一同态f。 现在基于函子来定义余代数。令F是函子，F的一个余代数（简称F余代数）是一个 序对U,c),其中U是集合，称为该余代数的载体，c是函数c:U→F(U),称为该余代数的 余代数结构（也称为运算）。由于余代数经常描述动态系统，载体也叫做状态空间。 F(U)→U的代数和U→F(U)的余代数有什么区别？本质上这是构造和观察之间的区 别。一个代数由载体集合U和射入U的一个函数a:FU)→U组成，它告知怎样构造U的 元素。而一个余代数由载体集合U和一个逆向的函数c:U→F(U)组成。此时不知道怎样形 成U的元素，仅有作用在U上的操作，它给出关于U的某些信息。 基于函子和交换图表也可以给出余代数同态的一种 F() FU)← F 表示。令F是函子，a:U→F(U)和b:V→F(O是两个 函数.F余代数(W,b)到(U,a)的同态是一个函数f:V→U, a 满足aof=F0ob,其交换图表在图6.3。 也可以进一步定义终结代数。F代数(U,a)是终结的， 如果对任意的F代数(V,b),都存在从(V,b)到(U,)的唯 图6.3余代数同态的交换图表 一同态f。 例6.7考虑有两个按键value和next的机器。按value键时，它不影响机器内部状态， 并且产生数据集A的某个元素，该元素代表机器内部状态的某个可见属性。因此，连续按 value键两次则产生同样的结果。按next键，则机器转移到另一个状态，该状态的性质也可 以通过按valu键来观察。抽象地说，该机器可以用状态空间U上的余代数 (value,nex:U→A×UU 来描述，该余代数的函数(value,nex)由两个函数value:UA和next:U→U组成。在状 态u∈U下，连续地交替按next键和value键，可以产生无限序列(a,a2,),它可以看成 N→A上的一个函数，其中a,=value(nexf()∈A。该序列就是状态u引发的可观察结果。 若1,2∈U给出同样的可观察序列，则称山和2从可观察角度是不可区分的。 口 6.3递归类型 6.3.1递归类型总揽 在类型表达式的语法中增加类型变量，s,1,,再增加一种形式为.o的类型表达式， 由此可以把递归定义的类型加到PC℉，或加到其它基于演算的语言中。在类型定义1=σ中， 若1出现在σ中，则该类型等式相当于1的一个递归定义式。可以像为递归定义的项引入不 动点算子那样，也为递归定义的类型引入不动点算子，fx(1.o用来表示等式1=σ的一个解。 递归类型是指类型等式系统的解，就像递归函数是项等式系统的解一样。第7章介绍多态类 型时，类型表达式的抽象用记号Ⅱ而不是入，以避免同项的抽象发生混淆，本章由于两种抽 象表达式不会同时出现一个式子中，因而暂时用同一个记号。第7章还会讨论1.σ中1所属 集合，目前暂时忽略它。习惯上用l.σ作为x(1.σ)的语法美化，并且把看成基本符号。在 .o中4约束1：类型表达式和项一样，也是既可以有约束变量又可以有自由变量。若在PC℉ 中把单位类型、和类型及递归类型加入，PC℉的类型表达式则是由文法 g:=b|1|1niσ+go×og→gl.g 产生的闭表达式，其中b代表基本类型，【代表类型变量。一个项，若其类型表达式含自由 变量，则会导致多态性，多态性要等到第7章讨论，因此这里将类型表达式限制到闭表达式。 在此看到，合法的类型表达式己经难以用纯文法来表示了，这个问题也等到第7章解决。仅 1
7 可以进一步定义初始代数。F 代数〈U, a〉是初始的，如果对任意的 F 代数〈V, b〉，都存在 从〈U, a〉到〈V, b〉的唯一同态 f。 现在基于函子来定义余代数。令 F 是函子，F 的一个余代数（简称 F 余代数）是一个 序对〈U, c〉，其中 U 是集合，称为该余代数的载体，c 是函数 c : U → F(U)，称为该余代数的 余代数结构（也称为运算）。由于余代数经常描述动态系统，载体也叫做状态空间。 F(U) → U 的代数和 U → F(U)的余代数有什么区别？本质上这是构造和观察之间的区 别。一个代数由载体集合 U 和射入 U 的一个函数 a : F(U) →U 组成，它告知怎样构造 U 的 元素。而一个余代数由载体集合 U 和一个逆向的函数 c : U → F(U)组成。此时不知道怎样形 成 U 的元素，仅有作用在 U 上的操作，它给出关于 U 的某些信息。 基于函子和交换图表也可以给出余代数同态的一种 表示。令 F 是函子，a : U → F(U)和 b : V → F(V)是两个 函数。F 余代数〈V, b〉到〈U, a〉的同态是一个函数 f : V → U， 满足 a D f = F(f) D b，其交换图表在图 6.3。 也可以进一步定义终结代数。F 代数〈U, a〉是终结的， 如果对任意的 F 代数〈V, b〉，都存在从〈V, b〉到〈U, a〉的唯 一同态 f。 例 6.7 考虑有两个按键 value 和 next 的机器。按 value 键时，它不影响机器内部状态， 并且产生数据集 A 的某个元素，该元素代表机器内部状态的某个可见属性。因此，连续按 value 键两次则产生同样的结果。按 next 键，则机器转移到另一个状态，该状态的性质也可 以通过按 value 键来观察。抽象地说，该机器可以用状态空间 U 上的余代数 〈value, next〉 : U → A × U 来描述，该余代数的函数〈value, next〉由两个函数 value : U → A 和 next : U → U 组成。在状 态 u ∈U 下，连续地交替按 next 键和 value 键，可以产生无限序列(a1, a2, …)，它可以看成 N → A 上的一个函数，其中 ai = value(next(i) (u)) ∈A。该序列就是状态 u 引发的可观察结果。 若 u1, u2∈U 给出同样的可观察序列，则称 u1和 u2 从可观察角度是不可区分的。 6.3 递归类型 6.3.1 递归类型总揽 在类型表达式的语法中增加类型变量 r, s, t, …，再增加一种形式为μt.σ的类型表达式， 由此可以把递归定义的类型加到 PCF，或加到其它基于λ演算的语言中。在类型定义 t = σ中， 若 t 出现在σ中，则该类型等式相当于 t 的一个递归定义式。可以像为递归定义的项引入不 动点算子那样，也为递归定义的类型引入不动点算子，fix(λt.σ) 用来表示等式 t = σ的一个解。 递归类型是指类型等式系统的解，就像递归函数是项等式系统的解一样。第 7 章介绍多态类 型时，类型表达式的抽象用记号Π而不是λ，以避免同项的抽象发生混淆，本章由于两种抽 象表达式不会同时出现一个式子中，因而暂时用同一个记号。第 7 章还会讨论λt.σ中 t 所属 集合，目前暂时忽略它。习惯上用μt.σ作为 fix(λt.σ)的语法美化，并且把μ看成基本符号。在 μt.σ中μ 约束 t；类型表达式和项一样，也是既可以有约束变量又可以有自由变量。若在 PCF 中把单位类型、和类型及递归类型加入，PCF 的类型表达式则是由文法 σ ::= b | t | unit | σ +σ | σ ×σ | σ → σ | μt.σ 产生的闭表达式，其中 b 代表基本类型，t 代表类型变量。一个项，若其类型表达式含自由 变量，则会导致多态性，多态性要等到第 7 章讨论，因此这里将类型表达式限制到闭表达式。 在此看到，合法的类型表达式已经难以用纯文法来表示了，这个问题也等到第 7 章解决。仅 图 6.3 余代数同态的交换图表 F(f ) F(U) U V a b f F(V)
约束变量的名字不同的类型表达式在此也被看成是等价的。 有递归类型时，需要仔细考虑类型相等问题。虽然从直观上讲，山.σ代表等式1=o的一 个解，但是对这个类型等式有两种可能的解释。第一种解释是，等式左右两边是真正不可区 分的类型。在这种观点下，类型相等变得相当复杂，因为1=o意味着1=[o1]o。使用语法， 则有等式 ut.=[ut.o/t o 并且许多其它等式都可以由此得出。虽然类型相等的观点有些吸引力，但它使得确定项良类 型与否变得更加困难。具体说，必须考虑项的类型相等问题，以便把某类型的一个项用到要 求它具有相等类型（语法上可以有区别）的场合。本章不用这种观点，而用下面的观点。 第二种观点把等式1=o看成要找到类型，它和σ同构。这里用 .o≥[l.ol川o 表达这个意思。其中≥表示同构。在同构观点下，类型.σ并不等于类型[.o川o,但是存在 把.σ的项“转换”成[l.o/川o的项的函数，反之亦然。对于递归类型，用同构代替相等后， 可以继续用语法上的等式来表示类型相等（除了用于约束类型变量的改名以外）。对于类型 同构情况，所要付的代价是，必须给出项在类型山.σ和[.σ川σ之间变化的转换函数，使得 可以准确知道每个项的类型的语法形式。 递归类型理论中最中心的问题是对类型等式1三σ有解和无解的情况进行分类，即1.σ 在什么情况下有不动点。这个问题在6.4节介绍。因此在形式为Ⅲ.σ的递归类型中，本节没 有讨论对σ的限制。 下面在PC℉语言中通过增加定型规则，来为递归类型同时给出新增项的形式及其类型。 由于涉及递归类型的项的形式允许把类型.o的项转换成类型[Ⅲ.σ川o的项并且反之亦然， 因此有下面两个定型规则 M:lut.o/t]a (u Intro) fold M:ut.o M:ut.o (u Elim) unfold M:Jut.o/t]o 其中函数fold和unfold互逆，满足下面的等式公理 unfold(fold M)=M fold(unfold M)=M (foldlunfold) 4 Intro规则根据l.o的展开类型的元素来引入l.o类型的元素，而消去形式unfold M 从该递归类型的一个元素给出其展开类型的相应元素。项fold M和unfold M处于递归类型 .o和它的展开类型[l.o川o之间，是联系它们的桥梁。 基于急切归约策略，PC℉语言所增加的递归类型的归约规则见表6.1。采用惰性归约策 略的归约规则也很容易设计。 表6.1PCF的急切归约 值 如果V是值，则fold V也是值。 公理 unfold(fold)caer→V V是值 子项规则 Mcar→M Masr→M 函数 fold M-eager >fold M unfold Mcager >unfold M
8 约束变量的名字不同的类型表达式在此也被看成是等价的。 有递归类型时，需要仔细考虑类型相等问题。虽然从直观上讲，μt.σ代表等式 t = σ的一 个解，但是对这个类型等式有两种可能的解释。第一种解释是，等式左右两边是真正不可区 分的类型。在这种观点下，类型相等变得相当复杂，因为 t = σ意味着 t = [σ /t]σ。使用μ语法， 则有等式 μt.σ = [μt.σ /t]σ 并且许多其它等式都可以由此得出。虽然类型相等的观点有些吸引力，但它使得确定项良类 型与否变得更加困难。具体说，必须考虑项的类型相等问题，以便把某类型的一个项用到要 求它具有相等类型（语法上可以有区别）的场合。本章不用这种观点，而用下面的观点。 第二种观点把等式 t = σ看成要找到类型 t，它和σ同构。这里用 μt.σ ≅ [μt.σ /t]σ 表达这个意思。其中≅表示同构。在同构观点下，类型μt.σ并不等于类型[μt.σ /t]σ，但是存在 把μt.σ的项“转换”成[μt.σ /t]σ的项的函数，反之亦然。对于递归类型，用同构代替相等后， 可以继续用语法上的等式来表示类型相等（除了用于约束类型变量的改名以外）。对于类型 同构情况，所要付的代价是，必须给出项在类型μt.σ和[μt.σ /t]σ之间变化的转换函数，使得 可以准确知道每个项的类型的语法形式。 递归类型理论中最中心的问题是对类型等式 t ≅ σ有解和无解的情况进行分类，即λt.σ 在什么情况下有不动点。这个问题在 6.4 节介绍。因此在形式为μt.σ的递归类型中，本节没 有讨论对σ的限制。 下面在 PCF 语言中通过增加定型规则，来为递归类型同时给出新增项的形式及其类型。 由于涉及递归类型的项的形式允许把类型μt.σ的项转换成类型[μt.σ /t]σ的项并且反之亦然， 因此有下面两个定型规则 : [ . / ] fold : . M μt σ t σ M μt σ (μ Intro) : . unfold :[ . / ] M μt σ M μt σ t σ (μ Elim) 其中函数 fold 和 unfold 互逆，满足下面的等式公理 unfold(fold M) = M fold(unfold M) = M (fold/unfold) μ Intro 规则根据μt.σ的展开类型的元素来引入μt.σ类型的元素，而消去形式 unfold M 从该递归类型的一个元素给出其展开类型的相应元素。项 fold M 和 unfold M 处于递归类型 μt.σ和它的展开类型[μt.σ /t]σ之间，是联系它们的桥梁。 基于急切归约策略，PCF 语言所增加的递归类型的归约规则见表 6.1。采用惰性归约策 略的归约规则也很容易设计。 表 6.1 PCF 的急切归约 值 如果 V 是值，则 fold V 也是值。 公理 unfold(fold V) ⎯eager ⎯ →⎯ V V 是值 子项规则 函数 eager eager eager eager ' ' fold fold ' unfold unfold ' MM MM M MM M ⎯⎯⎯→ ⎯⎯⎯→ ⎯⎯⎯→ ⎯⎯⎯→
通常仅把foldlunfold的第一个公理用作从左向右的归约公理。虽然运算fold和unfold 能消去项的类型歧义，但写起来是非常麻烦的。在后面的章节中，有时会省略fold和unfold, 以增强可读性。 对增加递归类型的PCF语言，很容易证明下面的安全性定理。 定理6.1(1)保持性若TPM:o并且Mr→M,则TDM:o (2)前进性若©>M:o且σ是可观测类型，则M是闭范式，或者存在程序M,使 得Mr→M. 6.3.2递归的数据结构 递归类型在程序设计语言中有很多应用，包括： (1)表示像表和树这样的无界数据结构： (2)表示像循环图这样的带环数据结构： (3)支持动态定型和动态类型派遣(pe dispatch): (4)支持协同例程和类似的控制结构。 本小节举例说明在递归数据结构方面的应用。 递归类型的一个重要应用是表示像表和树这样的数据结构，它们的大小和内容在程序的 执行过程中确定。例如自然数表的类型可以想象成类型等式1三mit+(nal×)的一个解。该 解是函数中的一个不动点fix(Ds),D的定义如下： par兰1.unit+(nal×t) 其不动点o满足同构o三心(o)。这时的fold和unfold函数的类型是 fold:unit+(nat×t)→t 和 unfold:t→unit+(nal×t) 它们是该类型等式的解和它的定义条件之间的见证。（删除） 类似地，对于二叉树，中ee的定义如下： Dee≌入t.unit+(t×t） 需要寻找o三mc(o)的一个解，即pee的一个不动点fix(pee)。 下面详细介绍自然数类型的例子。在PCF语言中自然数类型作为一种基本类型。引入 单位类型、和类型以及递归类型定义后，可以用它们来定义n1类型、数码0,1,2，、 后继函数、前驱函数和判零函数。于是可以把任何PC℉表达式翻译到只含递归类型定义、 单位类型、积类型与和类型的表达式（因为另一个基本类型b00l可以用单位类型与和类型 来定义，见3.24节)。 自然数的一个显著特征是，如果加一个元素到自然数集合，所得集合和自然数集合一一 对应，即同构。因为和m+x比x仅多一个元素，因此期望na1满足下面的同构： nat三nil+nal 这就导致下面把na1作为递归类型的一个定义： nal≌l.nil+t 直观上，可以通过下面的同构来理解这个定义： nat三lnit+nat 三umit+(2umit+nat) unit (unit (unit nat)) 三… 三mit+(mit+(nit+(nit+(unil+..+nal)..)）)） 9
9 通常仅把 fold/unfold 的第一个公理用作从左向右的归约公理。虽然运算 fold 和 unfold 能消去项的类型歧义，但写起来是非常麻烦的。在后面的章节中，有时会省略 fold 和 unfold， 以增强可读性。 对增加递归类型的 PCF 语言，很容易证明下面的安全性定理。 定理 6.1 （1）保持性 若Γ M :σ并且 M ⎯eager ⎯ →⎯ M′，则Γ M′:σ。 （2）前进性 若∅ M :σ 且σ是可观测类型，则 M 是闭范式，或者存在程序 M′，使 得 M ⎯eager ⎯ →⎯ M′。 6.3.2 递归的数据结构 递归类型在程序设计语言中有很多应用，包括： （1）表示像表和树这样的无界数据结构； （2）表示像循环图这样的带环数据结构； （3）支持动态定型和动态类型派遣（type dispatch）； （4）支持协同例程和类似的控制结构。 本小节举例说明在递归数据结构方面的应用。 递归类型的一个重要应用是表示像表和树这样的数据结构，它们的大小和内容在程序的 执行过程中确定。例如自然数表的类型可以想象成类型等式 t ≅ unit + (nat × t)的一个解。该 解是函数Φlist的一个不动点 fix(Φlist)，Φlist 的定义如下： Φlist λt.unit + (nat × t) 其不动点σ满足同构σ ≅Φlist(σ)。这时的 fold 和 unfold 函数的类型是 fold : unit + (nat × t) → t 和 unfold : t → unit + (nat × t) 它们是该类型等式的解和它的定义条件之间的见证。（删除） 类似地，对于二叉树，Φtree的定义如下： Φtree λt.unit + (t × t) 需要寻找σ ≅Φtree(σ)的一个解，即Φtree的一个不动点 fix(Φtree)。 下面详细介绍自然数类型的例子。在 PCF 语言中自然数类型作为一种基本类型。引入 单位类型、和类型以及递归类型定义后，可以用它们来定义 nat 类型、数码 0，1，2，…、 后继函数、前驱函数和判零函数。于是可以把任何 PCF 表达式翻译到只含递归类型定义、 单位类型、积类型与和类型的表达式（因为另一个基本类型 bool 可以用单位类型与和类型 来定义，见 3.2.4 节）。 自然数的一个显著特征是，如果加一个元素到自然数集合，所得集合和自然数集合一一 对应，即同构。因为和 unit+τ 比τ 仅多一个元素，因此期望 nat 满足下面的同构： nat ≅ unit + nat 这就导致下面把 nat 作为递归类型的一个定义： nat μt.unit + t 直观上，可以通过下面的同构来理解这个定义： nat ≅ unit + nat ≅ unit + (unit + nat) ≅ unit + (unit + (unit + nat)) ≅ … ≅ unit + (unit + (unit + (unit + (unit + … + nat)…) ) )
这个展开过程可以按照需要一直继续，然后把na1想象成这无数个单位类型的可区分的并。 其中自然数0由这个和的第一个mil类型的元素*表示，若写成项Inlefts*,则它成为上面和 类型的元素，再写成项fold(nleft*),则被转换成该递归类型的一个元素：自然数1由这个 和的第二个umil类型的元素*表示，项fold(nright fold(nleft*)表示它被转换成该递归类型 的一个元素；其余自然数依此类推。 为了避免自然数和用于代表自然数的项之间的混淆，在这里用「l表示代表自然数n的 数码（项）。根据上面的同构式，就有 「0]≌fold(Inleft*) 对任何自然数n>0,可以类似地定义如下： [n]fold(Inright fold(Inright...fold(Inleft*)...)) 其中Inright出现n次，并且hold应用有t1次。 后继函数正好使用fold和Inright: succ≌入r:nal.fold(Inrightx) 该表达式有正确的类型，因为如果x:nal,那么Inrightx属于nit什nal,fold(nright x)属于 nal。读者可以检验，对任何自然数有succ[nl=「n+1l。 判零测试的定义如下： zero?natCase(unfoldx(y:unittrue)(nat false) 读者很容易检查，zero?「0l=true并且对n>0,ero?「nl=alse。 最后一个操作是前驱算子。注意，0虽然没有前驱，但是为了便利起见，取pd0=0。 这样，前驱函数的定义如下，它类似于判零测试。 pred :nat.Casem a bool(unfoldx(y:unit.[)(nat=) 读者可以检验，对任意x:nal,有pred(succ x)=x。 作为另一个例子，自然数表的类型可以由递归类型l.nil+(nal×)来表示，即有同构 lisl三unit+(nal×list 表的两种构造形式，空表nil和非空表consx 1,由下面的定义给出： nil≌fold(Inleft*) consx1 fold(Inright (x,D) 根据表的形式进行分支的函数listcase定义如下： listcasex:list.y:)flistCase(unfold x)(w:unity)(f) 其中第1个参数x是s类型的项，若x是空表，该表达式的结果是o类型的项，即等于第 2个参数：若x是非空表，则该表达式的结果由类型为is1→o的第三个参数f应用到该非空 表得到。 6.4归纳类型和余归纳类型 6.4.1归纳类型和余归纳类型总揽 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到某个类型同构等式的最 小解，也叫初始解：余归纳类型对应到它们的最大解，也叫终结解。直观地说，归纳类型被 看成是包含它们引入形式的“最小”类型：而其消去形式是在这引入形式上的一种递归形式。 对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型：而其引入形式是一种在这 消去形式需要时提供元素的方法。 推动归纳类型研究的一个例子是自然数类型。它是包含引入形式0和scc()的最小类 型，其中M也是引入形式。为了进行以一个自然数为参数的计算，可以定义一个递归函数， o
10 这个展开过程可以按照需要一直继续，然后把 nat 想象成这无数个单位类型的可区分的并。 其中自然数 0 由这个和的第一个 unit 类型的元素∗表示，若写成项 Inleft∗，则它成为上面和 类型的元素，再写成项 fold(Inleft∗)，则被转换成该递归类型的一个元素；自然数 1 由这个 和的第二个 unit 类型的元素∗表示，项 fold(Inright fold(Inleft∗))表示它被转换成该递归类型 的一个元素；其余自然数依此类推。 为了避免自然数和用于代表自然数的项之间的混淆，在这里用⌈n⌉表示代表自然数 n 的 数码（项）。根据上面的同构式，就有 ⌈0⌉ fold(Inleft∗) 对任何自然数 n > 0，可以类似地定义如下： ⌈n⌉ fold(Inright fold(Inright … fold(Inleft∗) … )) 其中 Inright 出现 n 次，并且 hold 应用有 n+1 次。 后继函数正好使用 fold 和 Inright： succ λx:nat. fold(Inright x) 该表达式有正确的类型，因为如果 x:nat，那么 Inright x 属于 unit+nat，fold(Inright x)属于 nat。读者可以检验，对任何自然数有 succ⌈n⌉ =⌈n +1⌉。 判零测试的定义如下： zero? λx:nat.Caseunit, nat, bool(unfold x) (λy:unit.true) (λz:nat.false) 读者很容易检查，zero? ⌈0⌉ = true 并且对 n > 0，zero? ⌈n⌉ = false。 最后一个操作是前驱算子。注意，0 虽然没有前驱，但是为了便利起见，取 pred 0 = 0。 这样，前驱函数的定义如下，它类似于判零测试。 pred λx:nat.Caseunit, nat, bool(unfold x) (λy:unit.⌈0⌉) (λz:nat.z) 读者可以检验，对任意 x : nat，有 pred (succ x) = x。 作为另一个例子，自然数表的类型可以由递归类型μt.unit + (nat × t)来表示，即有同构 list ≅ unit + (nat × list) 表的两种构造形式，空表 nil 和非空表 cons x l，由下面的定义给出： nil fold(Inleft ∗) cons x l fold(Inright 〈x, l〉) 根据表的形式进行分支的函数 listcase 定义如下： listcase λx:list.λy:σ.λf:list→σ.Caseunit, list, σ (unfold x) (λw:unit.y) (f ) 其中第 1 个参数 x 是 list 类型的项，若 x 是空表，该表达式的结果是σ类型的项 y，即等于第 2 个参数；若 x 是非空表，则该表达式的结果由类型为 list→σ的第三个参数 f 应用到该非空 表得到。 6.4 归纳类型和余归纳类型 6.4.1 归纳类型和余归纳类型总揽 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到某个类型同构等式的最 小解，也叫初始解；余归纳类型对应到它们的最大解，也叫终结解。直观地说，归纳类型被 看成是包含它们引入形式的“最小”类型；而其消去形式是在这引入形式上的一种递归形式。 对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型；而其引入形式是一种在这 消去形式需要时提供元素的方法。 推动归纳类型研究的一个例子是自然数类型。它是包含引入形式 0 和 succ(M)的最小类 型，其中 M 也是引入形式。为了进行以一个自然数为参数的计算，可以定义一个递归函数