第6章 递归类型 6.1引 言 在某些程序设计语言中，类型可以递归地定义。例如ML,它有递归的datatype声明。 递归类型是类型等式系统的解，就像递归函数是项等式系统的解一样。例如，自然数表的类 型可以想象成类型等式1三mit+(nal×)的一个解，二叉树的类型可以想象成类型等式1三 i1+(1×)的一个解。“=”表示一个类型等式系统的解是要使等式两边的类型表达式同构， 而不是要使它们相等。 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到类型同构等式的最小 解，也叫做初始解；余归纳类型对应到它们的最大解，也叫做终结解。直观地说，归纳类型 被看成是包含它们引入形式的“最小”类型：而其消去形式是在这引入形式上的一种递归形 式。对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型：而其引入形式是一种 在这消去形式需要时提供元素的方法。推动归纳类型研究的一个例子是自然数类型，而推动 余归纳类型研究的一个例子是自然数流类型，它们在6.3和6.4节介绍。 归纳的概念比较熟悉，相应地理解归纳类型也比较容易。而要想理解余归纳类型，则必 须首先了解余归纳概念，包括余归纳定义和余归纳证明原理等，以及它们和归纳的相应概念 的对偶关系。对形式受到一定约束的递归类型等式，在不止一个解的情况下，某个初始代数 对应它的最小解，而某个终结余代数对应它的最大解。因此还需要了解余代数以及代数和余 代数的对偶性。 代数是数学中很好地确立了的一部分，涉及带有运算的集合，这些运算满足一定的性质， 这样的集合有群、环、向量空间等等。泛代数则在更高一个抽象层次上研究代数结构，研究 它们之间的同态、子代数和同余等。 概括地说，程序处理数据。在上世纪七八十年代就己经逐步清楚的是，这些数据的抽象 描述有望保证一个程序不依赖于它所操作数据的具体表示。这样的抽象也方便了正确性证 明。这种期望导致了代数方法在计算机科学中的使用，形成称为代数规范或抽象数据类型理 论的一个分支。它用代数中熟知的概念和技术来研究计算机科学中使用的数据类型。第2 章己经介绍了这方面的知识。 通常的代数技术己经展示出在捕捉计算机科学所用数据结构的本质方面是非常有用的。 但是，在试图代数地描述计算过程中出现的天性地动态的结构时，却遇到了困难。这样的结 构通常包括状态概念，状态可以按不同的方式进行变换。对于这样基于状态的动态系统，形 式方法一般利用自动机或迁移系统。上世纪九十年代，对这样基于状态的系统的深刻认识逐 步形成，它们不应该描述成代数，而应该是余代数。余代数是代数的对偶，这是本章需要介 绍的概念。代数中初始性的对偶性质（即终结性）对余代数来说是关键的，并且这样的终结 余代数所需的逻辑推理原理不是归纳，而是余归纳。在计算机科学中，代数方法是从“构造 的”角度研究抽象数据类型的语义，而余代数方法是从“观察的”的角度描述诸如对象、自 动机、进程、软件构件等基于状态的系统。 本章的主要内容有： (1)直观地介绍余归纳的定义、余归纳的证明原理和余代数。 (2)形式地介绍递归类型。 (3)形式地介绍归纳类型和余归纳类型。 11 第 6 章 递归类型 6.1 引 言 在某些程序设计语言中，类型可以递归地定义。例如 ML，它有递归的 datatype 声明。 递归类型是类型等式系统的解，就像递归函数是项等式系统的解一样。例如，自然数表的类 型可以想象成类型等式 t ≅ unit + (nat × t)的一个解，二叉树的类型可以想象成类型等式 t ≅ unit + (t × t)的一个解。“≅”表示一个类型等式系统的解是要使等式两边的类型表达式同构， 而不是要使它们相等。 归纳类型和余归纳类型是两类重要的递归类型。归纳类型对应到类型同构等式的最小 解，也叫做初始解；余归纳类型对应到它们的最大解，也叫做终结解。直观地说，归纳类型 被看成是包含它们引入形式的“最小”类型；而其消去形式是在这引入形式上的一种递归形 式。对偶地，余归纳被看成是和它们的消去形式一致的“最大”类型；而其引入形式是一种 在这消去形式需要时提供元素的方法。推动归纳类型研究的一个例子是自然数类型，而推动 余归纳类型研究的一个例子是自然数流类型，它们在 6.3 和 6.4 节介绍。 归纳的概念比较熟悉，相应地理解归纳类型也比较容易。而要想理解余归纳类型，则必 须首先了解余归纳概念，包括余归纳定义和余归纳证明原理等，以及它们和归纳的相应概念 的对偶关系。对形式受到一定约束的递归类型等式，在不止一个解的情况下，某个初始代数 对应它的最小解，而某个终结余代数对应它的最大解。因此还需要了解余代数以及代数和余 代数的对偶性。 代数是数学中很好地确立了的一部分，涉及带有运算的集合，这些运算满足一定的性质， 这样的集合有群、环、向量空间等等。泛代数则在更高一个抽象层次上研究代数结构，研究 它们之间的同态、子代数和同余等。 概括地说，程序处理数据。在上世纪七八十年代就已经逐步清楚的是，这些数据的抽象 描述有望保证一个程序不依赖于它所操作数据的具体表示。这样的抽象也方便了正确性证 明。这种期望导致了代数方法在计算机科学中的使用，形成称为代数规范或抽象数据类型理 论的一个分支。它用代数中熟知的概念和技术来研究计算机科学中使用的数据类型。第 2 章已经介绍了这方面的知识。 通常的代数技术已经展示出在捕捉计算机科学所用数据结构的本质方面是非常有用的。 但是，在试图代数地描述计算过程中出现的天性地动态的结构时，却遇到了困难。这样的结 构通常包括状态概念，状态可以按不同的方式进行变换。对于这样基于状态的动态系统，形 式方法一般利用自动机或迁移系统。上世纪九十年代，对这样基于状态的系统的深刻认识逐 步形成，它们不应该描述成代数，而应该是余代数。余代数是代数的对偶，这是本章需要介 绍的概念。代数中初始性的对偶性质（即终结性）对余代数来说是关键的，并且这样的终结 余代数所需的逻辑推理原理不是归纳，而是余归纳。在计算机科学中，代数方法是从“构造 的”角度研究抽象数据类型的语义，而余代数方法是从“观察的”的角度描述诸如对象、自 动机、进程、软件构件等基于状态的系统。 本章的主要内容有： （1）直观地介绍余归纳的定义、余归纳的证明原理和余代数。 （2）形式地介绍递归类型。 （3）形式地介绍归纳类型和余归纳类型