第2章 泛代数和代数数据类型 2.1引 言 第2章到第4章提出一种用于对可计算函数进行编程的语言，叫做PC℉语言。它是基 于类型化入演算的函数式语言。该语言的设计目的是便于后面各章的分析和讨论，而不是把 它作为编写大程序的实际语言。PC℉语言可以看成由三部分组成：包括自然数类型和布尔类 型的基本数据类型，带函数类型、积类型与和类型等的纯类型化入演算，涉及递归函数的不 动点算子。这三章分别对像PC℉这样语言的三个组成部分进行透彻的研究，以达到全面系 统了解这样的语言。本章研究像自然数类型和布尔类型这样的代数数据类型。 如果用其他的基本数据类型，如字符类型和串类型，来代替PC℉语言的自然数类型和 布尔类型，则可以得到有类似类型构造（函数和序对等）的语言，但面向的是不同种类的数 据的求值。如果想对PC℉作这样的修改，则必须确定命名基本字符和串的一种方式，就像 用0,1,2，·命名自然数那样，并选择以字符和串作为操作对象的基本函数，代替自然 数上的+和相等比较等运算以及布尔值上的运算。有了这些就可以定义这些基本数据类型的 项语言的语法，然后写一组项之间的等式作为公理来刻画这些函数的性质，即给出该项语言 的公理语义。一旦有了项的语法和公理语义，就可以进一步选择归约公理，编写程序，研究 指称语义。 一个代数数据类型包括一个或多个值集，如自然数集、布尔值集、字符集或串集，再加 上一组在这些集合上的函数。对代数数据类型的一个基本限制是其函数不能有函数变元，这 就是“代数的”的含义。需要说明的一点是，对于属于一个代数的若干个集合，本章使用泛 代数的标准术语。因此，基本“类型”符号，如nal,bool,char和string等，当它们用于 代数项时，叫做类别(so)。这样做的目的是，既维护和代数方面的文献的一致性，同时又 强调由集合和相关函数组成的代数数据类型和单纯的集合是有区别的。在代数数据类型理论 中，类型和类别的区别在于类型有一组运算而类别没有。 泛代数(niversal algebra),也叫做等式逻辑（equational logic),是用于定义和研究代 数数据类型的一般数学框架。在泛代数中，一个代数数据类型的公理语义由项之间的一组等 式给出。代数数据类型的指称语义涉及的结构叫做代数，它由一组集合和一组函数组成，对 应每个类别有一个集合，对应项中使用的每个函数符号有一个函数。代数项的操作语义由有 向的代数等式（即归约公理）给出，习惯上称它们为重写规则。可以用泛代数定义和研究的 数据类型有自然数、布尔值、表、有限集合、多重集合、栈、队列和树等。 本章研究泛代数和它在程序设计中定义常用数据类型时的作用，主要关心公理语义（一 组等式)和指称语义（代数）之间的联系，并另用单独一节研究操作语义。本章虽只研究代 数，但覆盖了大多数逻辑系统的一些公共议题。本章的主要内容有： (1)代数项和它们在多类别代数中的解释： (2)等式规范（也叫代数规范）和等式证明系统： (3)等式证明系统的可靠性和完备性（公理语义和指称语义的等价）： (4)代数之间的同态关系和初始代数： (5)数据类型的代数理论： (6)从代数规范导出的重写规则（操作语义）。 前四节对泛代数的数学系统提供一个简明介绍，随后一节关于数据类型的代数理论的讨1 第 2 章 泛代数和代数数据类型 2.1 引 言 第 2 章到第 4 章提出一种用于对可计算函数进行编程的语言，叫做 PCF 语言。它是基 于类型化演算的函数式语言。该语言的设计目的是便于后面各章的分析和讨论，而不是把 它作为编写大程序的实际语言。PCF 语言可以看成由三部分组成：包括自然数类型和布尔类 型的基本数据类型，带函数类型、积类型与和类型等的纯类型化演算，涉及递归函数的不 动点算子。这三章分别对像 PCF 这样语言的三个组成部分进行透彻的研究，以达到全面系 统了解这样的语言。本章研究像自然数类型和布尔类型这样的代数数据类型。 如果用其他的基本数据类型，如字符类型和串类型，来代替 PCF 语言的自然数类型和 布尔类型，则可以得到有类似类型构造（函数和序对等）的语言，但面向的是不同种类的数 据的求值。如果想对 PCF 作这样的修改，则必须确定命名基本字符和串的一种方式，就像 用 0，1，2，… 命名自然数那样，并选择以字符和串作为操作对象的基本函数，代替自然 数上的和相等比较等运算以及布尔值上的运算。有了这些就可以定义这些基本数据类型的 项语言的语法，然后写一组项之间的等式作为公理来刻画这些函数的性质，即给出该项语言 的公理语义。一旦有了项的语法和公理语义，就可以进一步选择归约公理，编写程序，研究 指称语义。 一个代数数据类型包括一个或多个值集，如自然数集、布尔值集、字符集或串集，再加 上一组在这些集合上的函数。对代数数据类型的一个基本限制是其函数不能有函数变元，这 就是“代数的”的含义。需要说明的一点是，对于属于一个代数的若干个集合，本章使用泛 代数的标准术语。因此，基本“类型”符号，如 nat，bool，char 和 string 等，当它们用于 代数项时，叫做类别（sort）。这样做的目的是，既维护和代数方面的文献的一致性，同时又 强调由集合和相关函数组成的代数数据类型和单纯的集合是有区别的。在代数数据类型理论 中，类型和类别的区别在于类型有一组运算而类别没有。 泛代数（universal algebra），也叫做等式逻辑（equational logic），是用于定义和研究代 数数据类型的一般数学框架。在泛代数中，一个代数数据类型的公理语义由项之间的一组等 式给出。代数数据类型的指称语义涉及的结构叫做代数，它由一组集合和一组函数组成，对 应每个类别有一个集合，对应项中使用的每个函数符号有一个函数。代数项的操作语义由有 向的代数等式（即归约公理）给出，习惯上称它们为重写规则。可以用泛代数定义和研究的 数据类型有自然数、布尔值、表、有限集合、多重集合、栈、队列和树等。 本章研究泛代数和它在程序设计中定义常用数据类型时的作用，主要关心公理语义（一 组等式）和指称语义（代数）之间的联系，并另用单独一节研究操作语义。本章虽只研究代 数，但覆盖了大多数逻辑系统的一些公共议题。本章的主要内容有： （1）代数项和它们在多类别代数中的解释； （2）等式规范（也叫代数规范）和等式证明系统； （3）等式证明系统的可靠性和完备性（公理语义和指称语义的等价）； （4）代数之间的同态关系和初始代数； （5）数据类型的代数理论； （6）从代数规范导出的重写规则（操作语义）。 前四节对泛代数的数学系统提供一个简明介绍，随后一节关于数据类型的代数理论的讨