第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）从代数规范导出的重写规则（操作语义）。 前四节对泛代数的数学系统提供一个简明介绍，随后一节关于数据类型的代数理论的讨
论指出数学中传统的关注点和程序设计中代数数据类型使用之间的一些区别。最后一节考虑 在代数项上的归约，它有两个应用，分析等式规范的性质和为代数项上的计算建模。 在数据类型的代数理论中还有许多专题。本书所忽略的重要专题有：层次规范、参数化 规范、从一个规范到另一个规范的求精、代数规范的实现的正确性等。在讨论函数应用产生 错误引起的问题时，本书没有介绍诸如使用带部分函数的代数和有序类别代数等更复杂方 法。对这些专题，有兴趣的读者可以参考有关文献。 本章研究的是PC℉这样的函数式语言的代数数据类型部分，此时不会出现函数作为变 元或返回值的情况，因此对它的研究比入演算的研究要容易得多。先研究泛代数而后研究类 型化入演算的理由是，许多技术概念在这里以更简单和易于理解的形式出现，因而易于讲授 和学习。 2.2代数、基调和项 2.2.1代数 一个代数由叫做载体(carrier)的一个或多个集合、这些载体上的一组特征元素和一阶 函数（或叫做代数函数） :A1×.×As→A 组成。例如 W=W0,1,+,*) 其载体N是自然数集合，特征元素0,1W,函数+，*：N×W→N。一个载体的“特征”元 素和它的其他元素的区别是，在代数项语言中每个特征元素被给出一个名字。一种简单的做 法是把0,1∈W这样的特征元素叫做零元函数，以便把特征元素和函数统一。 多个载体的例子有代数 4gf=N尽0,1，+，true,fale,Eq?,…〉 其中W是自然数集合，B是布尔值集合，0,1，.是自然数，+是加法函数等等。它们是在写 PCF的基本数值和布尔表达式时通常想到的数学值。在研究代数时，将把PC℉的语法表达 式和在这个代数中的语义值精确地对应起来。 2.2.2代数项的语法 现在开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要。首 先从代数项的语法开始。 代数项的语法依赖于基本符号和它们的类型，这些信息收集起来后被叫做基调。前面己 提到，在代数中通常把基本类型的符号叫做类别。 基调（signature)Σ=(S,F)由下列两部分组成： (1)集合S,其元素叫做类别： (2)序对s1×…×s张→s的集合F,其中s1,,s%,3∈S并且f不出现在两个不同的 序对中。 在基调的定义中，出现在F中的符号∫叫做类型化的函数符号（或简称函数符号），并 且表达式s1×.×Sk→s叫做S上的一阶（或代数）函数类型。通常用f:代替，)∈F。 类别是代数载体的名称，函数符号f:S1×.×Sk→s是代数的一个k元函数的名称。允 许k=0,从而函数符号f:s也可以是对应类别s的载体的元素的名称，通常称它们为常量符 号。不允许有子：和f:,即任何一个常量符号或函数符号只有唯一的类别或类型。 例2.1一个简单的例子是∑v=(S,F月)，其中S={nal仅含一个类别。F包含0：na叫，1：nat, 2
2 论指出数学中传统的关注点和程序设计中代数数据类型使用之间的一些区别。最后一节考虑 在代数项上的归约，它有两个应用，分析等式规范的性质和为代数项上的计算建模。 在数据类型的代数理论中还有许多专题。本书所忽略的重要专题有：层次规范、参数化 规范、从一个规范到另一个规范的求精、代数规范的实现的正确性等。在讨论函数应用产生 错误引起的问题时，本书没有介绍诸如使用带部分函数的代数和有序类别代数等更复杂方 法。对这些专题，有兴趣的读者可以参考有关文献。 本章研究的是 PCF 这样的函数式语言的代数数据类型部分，此时不会出现函数作为变 元或返回值的情况，因此对它的研究比演算的研究要容易得多。先研究泛代数而后研究类 型化演算的理由是，许多技术概念在这里以更简单和易于理解的形式出现，因而易于讲授 和学习。 2.2 代数、基调和项 2.2.1 代数 一个代数由叫做载体（carrier）的一个或多个集合、这些载体上的一组特征元素和一阶 函数（或叫做代数函数） f : A1 … Ak A 组成。例如 , 0, 1, +, 其载体 是自然数集合，特征元素 0, 1，函数+, : 。一个载体的“特征”元 素和它的其他元素的区别是，在代数项语言中每个特征元素被给出一个名字。一种简单的做 法是把 0, 1这样的特征元素叫做零元函数，以便把特征元素和函数统一。 多个载体的例子有代数 pcf , , 0, 1, …, +, true, false, Eq ?, … 其中 是自然数集合，是布尔值集合，0, 1, …是自然数，+是加法函数等等。它们是在写 PCF 的基本数值和布尔表达式时通常想到的数学值。在研究代数时，将把 PCF 的语法表达 式和在这个代数中的语义值精确地对应起来。 2.2.2 代数项的语法 现在开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要。首 先从代数项的语法开始。 代数项的语法依赖于基本符号和它们的类型，这些信息收集起来后被叫做基调。前面已 提到，在代数中通常把基本类型的符号叫做类别。 基调（signature） S，F 由下列两部分组成： （1）集合 S，其元素叫做类别； （2）序对f, s1 … sk s的集合 F，其中 s1, …, sk, s S 并且 f 不出现在两个不同的 序对中。 在基调的定义中，出现在 F 中的符号 f 叫做类型化的函数符号（或简称函数符号），并 且表达式 s1 … sk s 叫做 S 上的一阶（或代数）函数类型。通常用 f : 代替f, F。 类别是代数载体的名称，函数符号 f : s1 … sk s 是代数的一个 k 元函数的名称。允 许 k 0，从而函数符号 f : s 也可以是对应类别 s 的载体的元素的名称，通常称它们为常量符 号。不允许有 f : 和 f : ，即任何一个常量符号或函数符号只有唯一的类别或类型。 例 2.1 一个简单的例子是 S，F，其中 S nat仅含一个类别。F 包含 0 : nat, 1: nat
+:nat×nal→nal和*：nal×nal→nal。描述基调的习惯写法如下： sorts nat fetns:0.1 nat +,*:1al×al→nal 在这种表示法中，通常把同样类型的函数符号写在同一行上。 口 定义基调的目的是用于写代数项，但还得考虑项中有变量的情况。假定有一个无穷的符 号集合V,其元素称为变量，并假定这些符号和所有常量符号、函数符号和类别符号都不一 样。变量未指定类型是没有意义的，因此还需要列出变量的类别。类别指派是变量与类别序 对的一个有限集合： 「={：S,,:Sk} 其中任何变量不会被指派多个类别。给定一个基调Σ=S,F)和类别指派T,∑和T上类别s 良形的代数项集合Terms(区，「)定义如下： (1)如果x:s∈「，那么x∈Terms(E,T): (2)如果∫：s1×.×sk→s并且M∈Trms(②，T)(t=1,,),那么fM…M ∈Terms(Σ，T)。 当k=0时，第二个子句应该解释成：如果f:s,那么fe Terms(区，T)。 例如，0∈Tmsa(Es),+01也是Terms"(Es)的项，因为+是Σv上的二元函数符号。 这两个项都不含变量，不含变量的项称为闭项。对任何类别指派T,+01总是Tms(E「) 的项。为了和PC℉一致，把0+1看成是+01的语法美化。如果只有一个类别，则总假定所 有的变量都属于这个类别，这时类别指派可以简化为列出所有的变量即可。下面用(M 表示出现在项M中的变量集合。 因为代数项中无约束变元，因此代换[Wx]M就是简单地把M中x的每个出现都用N代 替。很容易看出，如果项中的一个变量由适当类别的项代替的话，那么可以得到一个良形的 项，其类别和代换之前一样。这可由下面的引理精确地给出。下面用「，x:s表示类别指派 T.x:s=TUx:s 其中x在T中没有出现。 引理2.1如果M eTerms(E,T,x:s')并且N E Terms(E,T),那么[NIx]ME Terms(E,T)。 证明按Tems(区，「，x:s')中项的结构进行归纳。这是本章第一个归纳证明，因此叙述 得详细一些，以后的归纳证明仅给出要点。因为每个项都是变量、常量符号或者函数符号应 用到变元的形式，因此代数项上的归纳只有一种基本情况（变量）和一种归纳步骤（函数符 号)。对基本情况必须直接证明引理，而在归纳步骤中，假定引理对所有子项都成立。这个 假定叫做归纳假设。 对基本情况，考虑变量ye Terms(E,「，x:s)。如果y和x不同，那么[Nxy就是y。在 这种情况下肯定有y:s∈「，因此ye Terms(E,「)。如果项是变量x本身，那么[Nxx的结果 是项N。这时x一定有类别s,则N一定属于Terms(Σ，T)。这就证明了归纳的基本情况。 对于归纳步骤，假定[NWxM∈Trms(②，)(I≤i≤k),并且考察形式为fM.M的 项。在这个项中用N对x进行代换的结果可以写成fNx]MNx]M。因为已经假定fM 4∈Tems(②，「，x:s'),因此f必定有类型s1×.×sk→s。现在有[N/x]M,e Terms(②，T)(1≤ i≤k),因此f[N/x]M[N/xM∈Terms(区，T)。这就结束了该引理的归纳证明。读者应该检 验在归纳步骤中k=0的情况。 0 例2.2可以用基调∑：=S,F)来写自然数和栈表达式，其中S={nal,s1ack},F包含下列 函数符号。 sorts nat,stack fetns 0,1,2,...nat 3
3 : nat nat nat 和: nat nat nat。描述基调的习惯写法如下： sorts : nat fctns : 0, 1 : nat , : nat nat nat 在这种表示法中，通常把同样类型的函数符号写在同一行上。 定义基调的目的是用于写代数项，但还得考虑项中有变量的情况。假定有一个无穷的符 号集合 V，其元素称为变量，并假定这些符号和所有常量符号、函数符号和类别符号都不一 样。变量未指定类型是没有意义的，因此还需要列出变量的类别。类别指派是变量与类别序 对的一个有限集合： x1 : s1, …, xk : sk 其中任何变量不会被指派多个类别。给定一个基调 S，F和类别指派，和上类别 s 良形的代数项集合 Termss (, )定义如下： （1）如果 x : s ，那么 x Termss (, )； （2）如果 f : s1 … sk s 并且 Mi i s Terms (, ) (i 1, …, k)，那么 f M1 … Mk Termss (, )。 当 k 0 时，第二个子句应该解释成：如果 f : s，那么 f Termss (, )。 例如，0Termsnat(, )，01 也是 Termsnat(, )的项，因为是上的二元函数符号。 这两个项都不含变量，不含变量的项称为闭项。对任何类别指派，01 总是 Termsnat(, ) 的项。为了和 PCF 一致，把 01 看成是01 的语法美化。如果只有一个类别，则总假定所 有的变量都属于这个类别，这时类别指派可以简化为列出所有的变量即可。下面用 Var(M) 表示出现在项 M 中的变量集合。 因为代数项中无约束变元，因此代换NxM 就是简单地把 M 中 x 的每个出现都用 N 代 替。很容易看出，如果项中的一个变量由适当类别的项代替的话，那么可以得到一个良形的 项，其类别和代换之前一样。这可由下面的引理精确地给出。下面用, x : s表示类别指派 , x : s x : s 其中 x 在中没有出现。 引理 2.1 如果 M Termss (, , x : s)并且 N s Terms (, )，那么NxMTermss (, )。 证明 按 Termss (, , x : s)中项的结构进行归纳。这是本章第一个归纳证明，因此叙述 得详细一些，以后的归纳证明仅给出要点。因为每个项都是变量、常量符号或者函数符号应 用到变元的形式，因此代数项上的归纳只有一种基本情况（变量）和一种归纳步骤（函数符 号）。对基本情况必须直接证明引理，而在归纳步骤中，假定引理对所有子项都成立。这个 假定叫做归纳假设。 对基本情况，考虑变量 yTermss (, , x : s)。如果 y 和 x 不同，那么Nx y 就是 y。在 这种情况下肯定有 y : s ，因此 yTermss (, )。如果项是变量 x 本身，那么Nx x 的结果 是项 N。这时 x 一定有类别 s，则 N 一定属于 Termss (, )。这就证明了归纳的基本情况。 对于归纳步骤，假定NxMi i s Terms (, )（1 i k），并且考察形式为 f M1 … Mk的 项。在这个项中用 N 对 x 进行代换的结果可以写成 f NxM1…NxMk。因为已经假定 f M1… Mk Termss (, , x : s)，因此 f 必定有类型 s1 … sk s。现在有NxMi is Terms (, )（1 i k），因此 f NxM1 …NxMkTermss (, )。这就结束了该引理的归纳证明。读者应该检 验在归纳步骤中 k = 0 的情况。 例 2.2 可以用基调stk S, F来写自然数和栈表达式，其中 S nat, stack，F 包含下列 函数符号。 sorts : nat, stack fctns : 0, 1, 2, … : nat
+,*:1al×nal→nal empty:stack push:nal×stack→stack pop:sack→stack top:stack-→nalt push2(push1(push0emp))是该基调的项，在这个基调的标准解释中它表示有元素0,1 和2的栈。使用栈变量s:stack,表达式push1(push0s)定义把0和1压进s后的栈。口 2.2.3代数以及项在代数中的解释 确定了代数项的语法描述后，需要一种方式将代数项解释到相应代数上的元素。 代数是为代数项提供含义（指称语义）的数学结构。为了显式地表示从项到代数的映射， 需要先把基调的类别和函数符号映射到代数中。如果Σ是一个基调，那么代数A包含： (1)对每个s∈S,正好有一个载体A: (2)一个解释映射T把函数 I(f):A××A→ 指派给函数符号∫：S1×.×sk→s∈F,并且把T(f)eA指派给常量符号∫：s∈F。 如果Σ只有一个类别，那么称它为单类别(single-sorted)代数，否则为多类别(mamm-sorted, muli-sorted)代数。 如果A=〈{4xes,工)是一个Σ代数，并且∫是Σ的函数符号，为方便起见，通常把I) 写成。在函数符号是有限多或可数多的情况下，一般是列出所有的函数，像代数N和A 给出的那样。根据这两个约定，把Σ代数W写成 N=W0W,1N,+V,* 它给出了解释Σ上的项所需的全部信息，因为解释映射工己经由这个代数的函数命名方式给 出。 确定项M∈Trms(E,「)在Σ代数中的含义相对来说是简单的事情。可能唯一不太熟悉的 技术方法是对变量指派载体上的值。代数A的环境？是从变量集合到A的各载体集合的并集 的一个映射7：V→，。需要环境的原因是项M中可能含变量，在确定M的含义前必须 给变量一个值。当然，一个环境必须把每个变量映射到恰当载体上的值。如果对每个x:s∈ 「都有x)e4,就说环境n满足r。 为A给出一个满足T的环境n后，可以定义任何项M∈Trms(E,)在n下的含义AMn 如下（双括号[]在此用来表示求语法项的语义）： Ax]n=mx) A[Mn=f(A[M]n,...,A[Mn) 若∫：s是常量符号，则Af]n=f八。如果代数A在上下文中是清楚的，通常省略A而直 接写[M7。如果M是闭项，那么AM不依赖于7。此时可以省略环境，用AM表示M在 代数A中的含义。 例2.3例2.1的基调Σw有类别nal和函数符号0、1、+、*，可以把该基调上的项解释 到2.3.1节的Σv代数W上。 令是针对W的一个环境，x)=0心。x+1在n下的含义确定如下： x+1]n=+(,I川) =+(7x),1) =+N(0N,1N) =1W ◇ 例2.4例2.2的基调E=(S,F有类别nal与s1ack,有函数符号0、1、、+、*、empty、 4
4 , : nat nat nat empty : stack push : nat stack stack pop : stack stack top : stack nat push 2 (push 1 (push 0 empty) )是该基调的项，在这个基调的标准解释中它表示有元素 0，1 和 2 的栈。使用栈变量 s : stack，表达式 push 1 (push 0 s)定义把 0 和 1 压进 s 后的栈。 2.2.3 代数以及项在代数中的解释 确定了代数项的语法描述后，需要一种方式将代数项解释到相应代数上的元素。 代数是为代数项提供含义（指称语义）的数学结构。为了显式地表示从项到代数的映射， 需要先把基调的类别和函数符号映射到代数中。如果是一个基调，那么代数包含： （1）对每个 s S，正好有一个载体 As ； （2）一个解释映射把函数 (f ) : 1s A … k s A As 指派给函数符号 f : s1 … sk s F，并且把(f )As 指派给常量符号 f : s F。 如果只有一个类别，那么称它为单类别（single-sorted）代数，否则为多类别（many-sorted, multi-sorted）代数。 如果 As sS, 是一个代数，并且 f 是的函数符号，为方便起见，通常把 (f ) 写成 f 。在函数符号是有限多或可数多的情况下，一般是列出所有的函数，像代数和pcf 给出的那样。根据这两个约定，把代数 写成 , 0, 1, , 它给出了解释上的项所需的全部信息，因为解释映射 已经由这个代数的函数命名方式给 出。 确定项 M Termss (, )在代数中的含义相对来说是简单的事情。可能唯一不太熟悉的 技术方法是对变量指派载体上的值。代数的环境是从变量集合到的各载体集合的并集 的一个映射 : V s As 。需要环境的原因是项 M 中可能含变量，在确定 M 的含义前必须 给变量一个值。当然，一个环境必须把每个变量映射到恰当载体上的值。如果对每个 x : s 都有(x)As ，就说环境 满足。 为 给出一个满足的环境后，可以定义任何项 M Termss (, )在下的含义M 如下（双括号 在此用来表示求语法项的语义）： x (x) M f (M1, …, Mk) 若 f : s 是常量符号，则f f 。如果代数 在上下文中是清楚的，通常省略而直 接写M。如果 M 是闭项，那么M不依赖于。此时可以省略环境，用M表示 M 在 代数 中的含义。 例 2.3 例 2.1 的基调有类别 nat 和函数符号 0、1、、，可以把该基调上的项解释 到 2.3.1 节的 代数上。 令是针对 的一个环境，(x) 0。x 1 在下的含义确定如下： x 1 (x, 1) ((x), 1 ) (0, 1 ) 1 例 2.4 例 2.2 的基调stkS, F有类别 nat 与 stack，有函数符号 0、1、…、、、empty
push、pop和1op。这个基调的一个代数A以标准的方式解释自然数，并把栈解释成自然数 序列。为了描述栈上的函数，用n:s表示把自然数n加到序列s∈W的前面而形成的结果序 列。使用这种表示法，则 A=(N,N,04,14,...,+4,*A emptyA,push,pop,top) 栈函数的确定如下： empy=&,空序列 psh(n,s）=n:s pop(n:s）=s pop (s)=s top (n::s)=n top(s)=0 需要注意的是，因为pop(empy)是良形代数项，因此在这个代数中必须给予某种解释。 这个代数中没有“error”元素，因而让pop(e)等于空串。1op也有类似的情况，当栈为空 时，直接返回自然数0，这是一个随意的决定。 如果环境把变量x:nal映射到自然数3，把变量s:s1ack映射到自然数序列(2,1)，其 第一个元素是2，第二个元素是1，那么可以确定下面两个项的含义。 [pop(push x s)n=pop(push(x]n,s]n)) =pop(push(3,(2,1〉)) =p0p((3,2,1) =(2,1) top(push x s)n=top(push(x n,[s]n)) =1 op(push3,(2,1)) =1op(3,2,1〉) =3 从这些例子很容易看出，对于把x映射到自然数并把s映射到栈的任何环境，有 pop(push x s)n=时n [top(push x s)n=n 含义函数的一个重要性质用下面的引理表达，该引理表明项含义的定义是正确的。 引理2.2令A是一个Σ代数，MeTerms(区，)，并且n是满足T的环境，那么M7e。 证明这个证明根据Terms(区，「)中项的结构进行归纳。 对于基本情况，是要证明对任何变量x∈Trms(E,「)和满足T的环境n,有x)n∈A'。从 Tms(E,「)的定义可知x:s∈「。由含义的定义可知xn=x)。因为7满足T,因此(x)∈A。 这就证明了归纳的基本情况。 对于归纳步骤，假定对1≤i≤k,[Mn∈A,然后考虑形式为fM.M的项。根据前 面有关项的含义的定义，这个项的含义是 fM…Mn=f(IMh,,[M) 从Σ代数的定义和fMM∈Tems(区，「)这个事实，可以知道f是个函数，它把A×,.× A的k元组映射到载体上的一个元素。于是 f(Mn,…,Mm∈A 这就证明了该引理。读者应该检验在归纳步骤中当k=0的情况。 0 另一个直截了当的性质是，项的含义仅依赖于出现在其中的变量的值。 引理2.3令x1,,x是由出现在M∈Tems(②，「)中的所有变量构成的变量表，h和h 是满足T的两个环境，并且对i=1,,k有(x)=h(x,那么Mh=[Mh。 从这个引理可以知道，如果1和h对T中出现的每个变量都一致，那么对每个项M∈ 5
5 push、pop 和 top。这个基调的一个代数stk以标准的方式解释自然数，并把栈解释成自然数 序列。为了描述栈上的函数，用 n::s 表示把自然数 n 加到序列 s 的前面而形成的结果序 列。使用这种表示法，则 stk , , 0, 1, …, , , empty, push, pop, top 栈函数的确定如下： empty ，空序列 push (n, s) n :: s pop (n :: s) s pop () top (n :: s) n top () 0 需要注意的是，因为 pop (empty)是良形代数项，因此在这个代数中必须给予某种解释。 这个代数中没有“error”元素，因而让 pop ()等于空串。top 也有类似的情况，当栈为空 时，直接返回自然数 0，这是一个随意的决定。 如果环境把变量 x : nat 映射到自然数 3，把变量 s : stack 映射到自然数序列2, 1 ，其 第一个元素是 2，第二个元素是 1，那么可以确定下面两个项的含义。 pop(push x s) pop(push(x,s) ) pop(push(3, 2, 1 ) ) pop( 3, 2, 1 ) 2, 1 top(push x s) top(push(x, s) ) top(push(3, 2, 1 ) ) top( 3, 2, 1 ) 3 从这些例子很容易看出，对于把 x 映射到自然数并把 s 映射到栈的任何环境，有 pop(push x s) s top( push x s) x 含义函数的一个重要性质用下面的引理表达，该引理表明项含义的定义是正确的。 引理 2.2 令是一个代数，MTermss (, )，并且是满足的环境，那么MAs 。 证明 这个证明根据 Termss (, )中项的结构进行归纳。 对于基本情况，是要证明对任何变量 xTermss (, )和满足的环境，有x As 。从 Termss (, )的定义可知 x : s 。由含义的定义可知x (x)。因为满足，因此(x) As 。 这就证明了归纳的基本情况。 对于归纳步骤，假定对 1 i k，Mi i s A ，然后考虑形式为 f M1 … Mk的项。根据前 面有关项的含义的定义，这个项的含义是 f M1 … Mk f (M1, …, Mk) 从代数的定义和 f M1 … Mk Termss (, )这个事实，可以知道 f 是个函数，它把 1s A … k s A 的 k 元组映射到载体 As 上的一个元素。于是 f (M1, …, Mk) As 这就证明了该引理。读者应该检验在归纳步骤中当 k 0 的情况。 另一个直截了当的性质是，项的含义仅依赖于出现在其中的变量的值。 引理 2.3 令 x1, …, xk是由出现在 M Termss (, )中的所有变量构成的变量表，1 和2 是满足的两个环境，并且对 i 1, …, k 有1(xi) 2(xi)，那么M1 M2。 从这个引理可以知道，如果1 和2 对中出现的每个变量都一致，那么对每个项 M
ems(区，「)，都有[Mn1=IMh,因为M中的每个变量必定出现在T中。 证明该证明也是基于项结构的归纳。对x1,,x中的任何变量x有 h=1(x)=2(x)=xh 对任何项fM…M,假定该引理对每个M都成立，即对所有的i有[Mn=IMh。 然后证明fM…M,h=fM,Mh。该证明如下： fM…Mh=f'(M]n,,Mm) =f'(M]h,…,Mm) =fM.M倜h 这就证明了该引理。 0 2.2.4代换引理 代数、一阶逻辑和类型化)演算都有的一个非常重要的性质叫做代换引理。直观上，就 M的含义而言，用N代换项M中的x和改变环境使得x等于N的值，两者的效果是一样的。 换句话说，当用项代换变量时，被代换项的含义是本质的，而它的语法形式不是。这就使得 项中的子项可以用等价的项来替换。这是一个非常有用的性质，在推理中经常使用，它是代 数项的等式证明系统的中心。 在论述此引理时用记号x→表示这样一个环境：除了x映射到a外，该环境在其他 变量上和n一致。 引理2.4（代换引理）令M∈Terms(E,r,x:s)并且N ETerms(②，T),那么[NWx]M∈ Tems(②，「)。并且对任何环境n,有 INx]Mn=[M(r→a),其中a=[Mn是N在n下的含义 证明根据项M的结构进行归纳。如果M是变量，分两种情况，即M是否就是x。这 两种情况的证明是直截了当的，把它们留给读者。 对于归纳步骤，考虑形式为fM…M的项。该项的相应代换实例是fNWx]M[NxM。 从含义的定义知道 [f[NIx]Mi...[N/x]Ml n=f(I[NIx]Mi]n,...[[NIx]M]n) 由归纳假设，I[NWx]Mn=[M(x→)(I≤i≤k)。再次使用含义的定义，可得 fIM(x→a),,M(r→a)=fM…M(x→a) 于是引理得证。 0 2.3等式、可靠性和完备性 2.3.1等式 一个代数数据类型的公理语义由一个基调上项之间一组等式给出。一个基调和一组等式 合在一起称为代数规范（algebraic specification)。从一个代数规范，可以使用等式证明系统 去推导新的等式，或者调查什么样的代数满足这些等式强加的要求。这两个方面是紧密相关 的：从规范推导出的等式应该在任何满足该规范的代数中都成立。这个性质叫做代数证明系 统的可靠性(soundness)。反过来，在满足规范的所有代数中都成立的等式应该从该规范可 以证明，这叫做完备性(comple1 eness)。代数证明系统及其可靠性在2.3.3节给出，完备性 在2.3.5节证明。 本书对代数或一阶逻辑的一般分析方法所做的一个小小推广是允许空载体。考虑空载体 的原因是为了让每个规范都有初始代数（见2.4.2节），以及和类型化入演算允许空类型这一 点保持一致。和单类别一阶逻辑相比较时，值得一提的是，如果只有一个类别，假定该类别 6
6 Termss (, )，都有M1 M2，因为 M 中的每个变量必定出现在中。 证明 该证明也是基于项结构的归纳。对 x1, …, xk中的任何变量 xi 有 xi1 1(xi) 2(xi) xi2 对任何项 f M1 … Mk，假定该引理对每个 Mi 都成立，即对所有的 i 有Mi1 Mi2。 然后证明f M1 … Mk1 f M1 … Mk2。该证明如下： f M1 … Mk1 f (M11, …, Mk1) f (M12, …, Mk2) f M1 … Mk2 这就证明了该引理。 2.2.4 代换引理 代数、一阶逻辑和类型化演算都有的一个非常重要的性质叫做代换引理。直观上，就 M 的含义而言，用 N 代换项 M 中的 x 和改变环境使得 x 等于 N 的值，两者的效果是一样的。 换句话说，当用项代换变量时，被代换项的含义是本质的，而它的语法形式不是。这就使得 项中的子项可以用等价的项来替换。这是一个非常有用的性质，在推理中经常使用，它是代 数项的等式证明系统的中心。 在论述此引理时用记号xa表示这样一个环境：除了 x 映射到 a 外，该环境在其他 变量上和一致。 引理 2.4（代换引理）令 M Termss (, , x : s)并且 N s Terms (, )，那么NxM Termss (, )。并且对任何环境，有 NxM M(x a)，其中 a N是 N 在下的含义 证明 根据项 M 的结构进行归纳。如果 M 是变量，分两种情况，即 M 是否就是 x。这 两种情况的证明是直截了当的，把它们留给读者。 对于归纳步骤，考虑形式为 f M1 … Mk的项。该项的相应代换实例是 f NxM1 … NxMk。 从含义的定义知道 f NxM1 … NxMk f (NxM1, …, NxMk) 由归纳假设，NxMi Mi(x a)（1 i k）。再次使用含义的定义，可得 f (M1(x a), …, Mk(x a)) f M1 … Mk(x a) 于是引理得证。 2.3 等式、可靠性和完备性 2.3.1 等式 一个代数数据类型的公理语义由一个基调上项之间一组等式给出。一个基调和一组等式 合在一起称为代数规范（algebraic specification）。从一个代数规范，可以使用等式证明系统 去推导新的等式，或者调查什么样的代数满足这些等式强加的要求。这两个方面是紧密相关 的：从规范推导出的等式应该在任何满足该规范的代数中都成立。这个性质叫做代数证明系 统的可靠性（soundness）。反过来，在满足规范的所有代数中都成立的等式应该从该规范可 以证明，这叫做完备性（completeness）。代数证明系统及其可靠性在 2.3.3 节给出，完备性 在 2.3.5 节证明。 本书对代数或一阶逻辑的一般分析方法所做的一个小小推广是允许空载体。考虑空载体 的原因是为了让每个规范都有初始代数（见 2.4.2 节），以及和类型化演算允许空类型这一 点保持一致。和单类别一阶逻辑相比较时，值得一提的是，如果只有一个类别，假定该类别
非空是有意义的，否则任何逻辑公式在模型中都为真。 为什么说空载体提出一个技术问题？请回忆项M∈Terms'(Σ，T)的含义，它是对满足Γ的 环境定义的。如果x:s'∈「并且=⑦是空集，那么不可能有任何环境满足T。因而并不清 楚，应该说Terms'(Σ，『)中的任何两个项都相等（因为所有项都无含义），还是说这样的等式 没有什么意义。使得理论最简单的选择是：如果是空集，那么涉及x:S的任何两个项都 相等。本书采用按这种选择的理论。因为空载体会影响等式的真假，并且因为只有类别解释 到非空载体时变量才可能给出值，因此证明系统将显式地掌握变量和它们所属类别的情况。 后面将看到，掌握变量的情况将怎样影响命题2.7的证明。 等式是一个公式M=N[],其中对某个s,M,N ETerms(区，)。注意，一个等式有三 部分：两个项和一个类型指派「。如果7满足「，那么只要M7=Mn,就说代数A在环境7 下满足M=NT],写成 A,n卡M=N☐ 如果4在下满足一个等式，也可以说该等式在下成立。对于含变量的项，更感兴趣的是一 个等式是否在变量所有取值情况下都成立，而不是在一个特别的环境下成立。如果对满足「 的任何环境7，都有A,nFM=N[T],就可以说A满足M=N[T],写成 A卡M=Nr] 可满足性也可以扩大到一组等式或一组代数。令￡是一组Σ等式，如果A满足的所有等 式，就说A满足E。类似地，如果C是一类代数，并且对每个AEC,都有AFM=N[T],那么 写成C卡M=N[]. 例2.5令Σ是有两个类别a和b的基调，令A是一个Σ代数，其中4={0,1}并且A=☑。 由于A°有两个元素，则A不可能满足x=yx:a,y:a,即 AFx=yx:a,y:a可 不可能成立。例如，如果一个环境的映射是”→0和W→1，那么该等式不成立。但是，如果 在类型指派增加变量：：b,那么 AFx=y[x:a,y:a,三：b] 成立。即该等式无意义地成立，因为不可能在A上对变量：作出任何指派。 ◇ 逻辑中的一个标准概念是永真性。如果任何一个Σ代数都满足等式M=N[],就说该等 式是永真的(valid,也称有效的)，并写成 FM=N门 若等式x=xx:s是永真的，因为在包含类别s的基调的任何一个代数中，它都成立，因此， 即使s可以空也是这样。后面将看到，永真等式并非很有意义，能够引起兴趣的是在特定的 一个代数或一类代数中成立的等式。 如果A满足Σ上的所有等式，就说Σ代数A是平凡的(trivial)。平凡代数的特点见习题 2.6。 2.3.2项代数 关于代数项的一个有用事实是，任何基调Σ和变量类别指派T上的Terms(区，「)给出了一 个Σ代数，叫做项代数。在代数项的定义中，为每个类别s定义了一个项集rms(Σ，「)，在 项代数中，就把它作为s的载体。剩下的是给每个函数符号∫：S1×…×sSk→s一个精确的解 释。如果Σ=S,F),Σ和变量类别指派T上项代数 Terms(,I)=((Terms'(I)),I 的解释I为 I(f)(M1,...,M)=fM...M 个
7 非空是有意义的，否则任何逻辑公式在模型中都为真。 为什么说空载体提出一个技术问题？请回忆项 M Termss (, )的含义，它是对满足的 环境定义的。如果 x:s并且 As 是空集，那么不可能有任何环境满足。因而并不清 楚，应该说 Termss (, )中的任何两个项都相等（因为所有项都无含义），还是说这样的等式 没有什么意义。使得理论最简单的选择是：如果 As 是空集，那么涉及 x : s的任何两个项都 相等。本书采用按这种选择的理论。因为空载体会影响等式的真假，并且因为只有类别解释 到非空载体时变量才可能给出值，因此证明系统将显式地掌握变量和它们所属类别的情况。 后面将看到，掌握变量的情况将怎样影响命题 2.7 的证明。 等式是一个公式 M N ，其中对某个 s，M, N Termss (, )。注意，一个等式有三 部分：两个项和一个类型指派。如果满足，那么只要M N，就说代数在环境 下满足 M N ，写成 , M N 如果在下满足一个等式，也可以说该等式在下成立。对于含变量的项，更感兴趣的是一 个等式是否在变量所有取值情况下都成立，而不是在一个特别的环境下成立。如果对满足 的任何环境，都有, M N ，就可以说 满足 M N ，写成 M N 可满足性也可以扩大到一组等式或一组代数。令是一组等式，如果满足的所有等 式，就说满足。类似地，如果是一类代数，并且对每个，都有 M N ，那么 写成 M N 。 例 2.5 令是有两个类别 a 和 b 的基调，令是一个代数，其中 Aa {0,1}并且 Ab 。 由于 Aa 有两个元素，则不可能满足 x y[x : a, y : a]，即 x y[x : a, y : a] 不可能成立。例如，如果一个环境的映射是 x0 和 y1，那么该等式不成立。但是，如果 在类型指派增加变量 z : b，那么 x y[x : a, y : a, z : b] 成立。即该等式无意义地成立，因为不可能在 Ab 上对变量 z 作出任何指派。 逻辑中的一个标准概念是永真性。如果任何一个代数都满足等式 M N ，就说该等 式是永真的（valid，也称有效的），并写成 M N 若等式 x x[x : s]是永真的，因为在包含类别 s 的基调的任何一个代数中，它都成立，因此， 即使 s 可以空也是这样。后面将看到，永真等式并非很有意义，能够引起兴趣的是在特定的 一个代数或一类代数中成立的等式。 如果 满足上的所有等式，就说代数是平凡的（trivial）。平凡代数的特点见习题 2.6。 2.3.2 项代数 关于代数项的一个有用事实是，任何基调和变量类别指派上的 Terms(, )给出了一 个代数，叫做项代数。在代数项的定义中，为每个类别 s 定义了一个项集 Termss (, )，在 项代数中，就把它作为 s 的载体。剩下的是给每个函数符号 f : s1 … sk s 一个精确的解 释。如果 S, F，和变量类别指派上项代数 Terms(, ) Termss (, ), 的解释为 (f ) (M1, …, Mk) f M1 … Mk
这个定义很简单，也很容易看出Tems(公，T)是Σ代数，见习题2.8。因此，下面Termst(②，「) 既用来表示项集，也用来表示项代数。 在项代数Termst(Σ，「)中，项的含义很容易用代换描述。如果n是项代数的一个环境，那 么是从变量到项的映射，它也叫做一个代换（但可能涉及对多个变量的代换）。通常，如 果S是一个代换，则用SM表示同时把M中的各个变量x用Sx替换的结果。因为项代数的 环境是一个代换，因此也可以用M表示把代换应用于M的结果。 例2.6令∑是有类别u和函数符号f:u→u和g:u×u→u的基调.若T={a:4,b:4,c: w,则在项代数T=Terms(E,「)中，类别u的载体是基于变量a、b、c以及函数符号f和g 的所有项的集合，即： T"=(a,b,c,fa,fb,fc,gaa,gab,gac,gbb,...g (f(fa))(f(gbc)),.... 在该项代数中，函数符号∫的解释fT是把任何项M映射到项∫M的函数，g类似。如果环 境把变量x映射到a,把y映射到fb,那么有 T[g(fx)(fy)In=g(fa)(f(fb)) 口 下面的引理将含义和代换联系在一起。 引理2.5令M∈Terms((Σ，「)，并且n是满足T的项代数Termst(E,「)的环境，那么Mn= 7M。 证明对M进行结构归纳证明。对变量x,由定义，有xn=r。对项fM…M,由项 在代数中含义的定义，有 If M...Meln=ftrm(IMiln...,IMln) 由归纳假设，可以知道Mn=nM,并且因为Terms(E,「)是一个项代数，因此 [fM...Mn=f(nM)...(nM) 它正好是代换应用于M的结果。 ◇ 项代数给出了一种简单的方法表明，只有M和N是语法上相同的项时，等式M=N[门 才会永真。 2.3.3语义蕴涵和等式证明系统 序对Spec=(②，8)，包含一个基调Σ和一组等式E,叫做代数规范。通常把代数规范Spec =②，)看成是规定了一组代数，即一组满足的Σ代数。这就引出了语义蕴涵概念。 如果满足基调Σ上的一组等式的所有Σ代数A都满足等式M=W[T],那么就说语义上 蕴涵这个等式，写成 &=M=N[T] 很容易明白，在满足规范Spc=(②，8的所有代数中都成立的等式也就是由语义蕴涵的Σ等 式。 如果一组等式在语义蕴涵下封闭，那么称它为一个语义理论。更准确地说，如果￡卡M= N[T]蕴涵M=N[T]∈C,那么等式集合E叫做一个语义理论。一个代数A的理论T(A)是 在A中成立的所有等式的集合。很容易检查，一个代数的理论是一个语义理论。证明由习题 2.11完成。 本节剩余部分致力于讨论语义蕴涵的代数证明系统。前面己提到，一个证明系统的两个 重要性质是可靠性和完备性。用语义蕴涵来解释的话，可靠性是指，若一个等式从一组假设 ￡可证，那么￡语义上蕴涵该等式。完备性则相反，如果￡语义上蕴涵一个等式，那么该等 式从￡可证。本节证明代数证明系统的可靠性，2.3.5节证明完备性。 有关相等的某些性质是“泛”的，它们不依赖于代数的特别性质。具体说，语义相等是 个等价关系。即自反公理的每个实例 M=M[T] (ref) 8
8 这个定义很简单，也很容易看出 Terms(, )是代数，见习题 2.8。因此，下面 Terms(, ) 既用来表示项集，也用来表示项代数。 在项代数 Terms(, )中，项的含义很容易用代换描述。如果是项代数的一个环境，那 么是从变量到项的映射，它也叫做一个代换（但可能涉及对多个变量的代换）。通常，如 果 S 是一个代换，则用 SM 表示同时把 M 中的各个变量 x 用 Sx 替换的结果。因为项代数的 环境是一个代换，因此也可以用M 表示把代换应用于 M 的结果。 例 2.6 令是有类别 u 和函数符号 f : u u 和 g : u u u 的基调。若 {a : u, b : u, c : u}，则在项代数 Terms(, )中，类别 u 的载体是基于变量 a、b、c 以及函数符号 f 和 g 的所有项的集合，即： Tu a, b, c, fa, fb, fc, gaa, gab, gac, gbb, …, g (f ( fa ) ) (f (gbc) ), … } 在该项代数中，函数符号 f 的解释 f 是把任何项 M 映射到项 f M 的函数，g类似。如果环 境把变量 x 映射到 a，把 y 映射到 f b，那么有 g(f x) (f y) g(f a) (f (f b)) 下面的引理将含义和代换联系在一起。 引理 2.5 令 M Terms(, )，并且是满足的项代数 Terms(, )的环境，那么M M。 证明 对 M 进行结构归纳证明。对变量 x，由定义，有x x。对项 f M1 … Mk，由项 在代数中含义的定义，有 f M1 … Mk f Terms(M1, …, Mk) 由归纳假设，可以知道Mi Mi，并且因为 Terms(, )是一个项代数，因此 f M1 … Mk f (M1) … (Mk) 它正好是代换应用于 M 的结果。 项代数给出了一种简单的方法表明，只有 M 和 N 是语法上相同的项时，等式 M N 才会永真。 2.3.3 语义蕴涵和等式证明系统 序对 Spec , ，包含一个基调和一组等式，叫做代数规范。通常把代数规范 Spec , 看成是规定了一组代数，即一组满足的代数。这就引出了语义蕴涵概念。 如果满足基调上的一组等式的所有代数都满足等式 M N ，那么就说语义上 蕴涵这个等式，写成 M N 很容易明白，在满足规范 Spec , 的所有代数中都成立的等式也就是由语义蕴涵的等 式。 如果一组等式在语义蕴涵下封闭，那么称它为一个语义理论。更准确地说，如果 M N 蕴涵 M N ，那么等式集合 叫做一个语义理论。一个代数 的理论 Th( )是 在中成立的所有等式的集合。很容易检查，一个代数的理论是一个语义理论。证明由习题 2.11 完成。 本节剩余部分致力于讨论语义蕴涵的代数证明系统。前面已提到，一个证明系统的两个 重要性质是可靠性和完备性。用语义蕴涵来解释的话，可靠性是指，若一个等式从一组假设 可证，那么 语义上蕴涵该等式。完备性则相反，如果 语义上蕴涵一个等式，那么该等 式从 可证。本节证明代数证明系统的可靠性，2.3.5 节证明完备性。 有关相等的某些性质是“泛”的，它们不依赖于代数的特别性质。具体说，语义相等是 个等价关系。即自反公理的每个实例 M M (ref )
是永真的，并且语义相等是对称的和传递的。后两个性质可形式化为下面两条推理规则。 M=N[T] (sym) N=M[T] M=N[T]N=P[T] (trans) M=PT] 下一条推理规则允许在等式中增加类别指派。这条规则不是很重要，但它不可少。需要 这条规则的原因是，有了它就可以考虑没有在项中出现的变量。该规则是 M=N[T] x不在T中 (add var) M=NTx s] 它允许加一个变量到任何类别指派。重复使用该规则，可以加入有限个变量。很容易验证， 一个代数A满足这条规则的假设，那么它一定满足其结论。 最后一条规则叫做等价代换。如果不提及类别指派的话，该代换规则是说，如果M=N 并且P=Q,那么用P和Q分别代换M和N中的x,所得的两个结果相等。该规则形式表 达如下： M=NCx:P=O☐P,Q eTerms'(②，) (subst) [P/]M =[Q/]N [T] 该规则副条件给出的限制是说，不能代换含x的P和Q到等式M=N口，x:s]中，因为P= Q[]的类别指派T假定为不含x。但是从习题213可以看出，实际上这并不是一个问题。 如果从￡中的等式和公理(ef)及推理规则(sm小、(trans)、(subst)和(add var)可以推出 等式M=NT],那么就说该等式可证，并写成 E上M=Nr] 更形式地说，从￡到E的证明是一个等式序列，其中每个等式是公理、￡中的等式、或者是 序列中早先出现的一个或多个等式的一步推导的结果，序列的最后一个等式是￡。有关证明 的一种有用的推理形式是基于E的证明长度的归纳。 如果￡封闭于可证明性，那么就说￡是一个语法理论。换种说法，如果上M=N[T门 蕴涵M=N[T门∈E,那么￡是一个语法理论。￡的语法理论Th(E)也就是从￡可证的所有等 式的集合。通过下面关于可靠性和完备性的证明，可以得知语法上的代数理论和语义上的代 数理论是相同的。但是，目前仍保持两个定义是有用的。等式集合￡是语义一致的 (consistent),如果存在某个等式M=[T],它不是￡的语义蕴涵：等式集合￡是语法一致的， 如果存在某个等式M=N[T],它不能由E证明，否则称为不一致的。 例2.7（例2.2和2.4的继续）在基调Σ=(S,F)上增加等式 top (push x s)=x [s stack,x nat] pop (push x s)=s [s stack,x nat] 使用这些等式可以证明等式 top(push3empy）=3 其证明如下： top (push x s)=x [s:stack,x.nat] empty empty [x:nat] top (push x empty)=x [x:nat] 3=3[] top (push 3 empty)=3[] 9
9 是永真的，并且语义相等是对称的和传递的。后两个性质可形式化为下面两条推理规则。 [] [] M N N M (sym) [ ] [ ] [] MN NP M P (trans) 下一条推理规则允许在等式中增加类别指派。这条规则不是很重要，但它不可少。需要 这条规则的原因是，有了它就可以考虑没有在项中出现的变量。该规则是 [] [ , : ] M N M N xs x 不在中 (add var) 它允许加一个变量到任何类别指派。重复使用该规则，可以加入有限个变量。很容易验证， 一个代数满足这条规则的假设，那么它一定满足其结论。 最后一条规则叫做等价代换。如果不提及类别指派的话，该代换规则是说，如果 M N 并且 P Q，那么用 P 和 Q 分别代换 M 和 N 中的 x，所得的两个结果相等。该规则形式表 达如下： [ , : ] [ ] , ( , ) [ ] [ ] [] M N xs P Q s P Q Terms P/x M Q/x N (subst) 该规则副条件给出的限制是说，不能代换含 x 的 P 和 Q 到等式 M N , x : s 中，因为 P = Q []的类别指派假定为不含 x。但是从习题 2.13 可以看出，实际上这并不是一个问题。 如果从 中的等式和公理(ref )及推理规则 (sym)、(trans)、(subst) 和(add var) 可以推出 等式 M N，那么就说该等式可证，并写成 M N 更形式地说，从 到 E 的证明是一个等式序列，其中每个等式是公理、 中的等式、或者是 序列中早先出现的一个或多个等式的一步推导的结果，序列的最后一个等式是 E。有关证明 的一种有用的推理形式是基于 E 的证明长度的归纳。 如果 封闭于可证明性，那么就说 是一个语法理论。换种说法，如果 M N 蕴涵 M N ，那么 是一个语法理论。 的语法理论 Th( )也就是从 可证的所有等 式的集合。通过下面关于可靠性和完备性的证明，可以得知语法上的代数理论和语义上的代 数理论是相同的。但是，目前仍保持两个定义是有用的。等式集合 是语义一致的 (consistent)，如果存在某个等式 M N ，它不是 的语义蕴涵；等式集合 是语法一致的， 如果存在某个等式 M N ，它不能由 证明，否则称为不一致的。 例 2.7 （例 2.2 和 2.4 的继续）在基调stk S, F上增加等式 top (push x s ) = x [s : stack, x : nat] pop (push x s ) = s [s : stack, x : nat] 使用这些等式可以证明等式 top (push 3 empty ) = 3 其证明如下： ( ) [ : , : ] [ : ] ( ) [ : ] 3 3 [ ] ( 3 ) 3 [ ] top push x s x s stack x nat empty empty x nat top push x empty x x nat top push empty
该证明两次使用(e)公理，一次栈公理和两次(sbs1)。 一个证明系统的导出规则是一条推理规则 前提 结论 它满足：从该前提的任何实例，通过使用该证明系统的公理和其他证明规则，可以推导出该 结论的相应实例。例如， M=N T]N=P[T]P=O[T] M=OT] 是该代数证明系统的一个导出规则，因为从形式为M=N,N=P,P=Q的任意三个等式，两 次使用传递规则可以得到M=Q。 导出规则的另一个例子是下面的同余规则，直观上说，同余是指“相等的项应用于相等 的项时，产生相等的项”。 M=N[C].M4=N[]fs×.×s&→sand (cong） fM1.Mk=fN1Nk[C]M,N,∈Terms(②，T) (cong)规则可从(add var),(re)和(subs)推导。从这些假设，使用(add var),可以推导出k 个等式： M=N,x1:S1,,x1:sS](i=1,,k) 其中x1,,x是不出现在T中的新变量(i=1时的等式就是M=N[])。再由（阳功可得 fx1...x=fx1...x:S1,...,X&SA] 重复使用(sbs),第一步是先将上式两边的分别用M和N代换，最后一步将倒数第二步 代换结果中两边的x1分别用M和M代换。最终得到 fM...M=fN1...N&I 例2.8证明等式1op(pop(pushx(push3empy))=3[r:na叫 为证明该等式，从栈公理和(e)的实例开始，应用(subs),然后再用导出规则(cong)得 到 pop (push x s)=s [s:stack,x.nat]push 3 empty push 3 empty [x:nat] pop (push x(push 3 empty))=push 3 empty [x:nat] top (pop (push x(push 3 empty)))=top(push 3 empty)[x:nat] 再从上例的结果用(add var)得到 top(push 3 empty)=3 [x nat] 最后用(trans)得到 top(pop (push x (push 3 empty))=3 [x:nat] 0 例2.9下面的规则允许从任何等式的变量类别指派中删除多余变量。如果变量x在M 和N中都不出现，并且从其他信息知道s类别的项集Terms(Σ，「)非空，那么在等式M=NT, x:中，x:s没有什么作用，可以把它从T,x:s中删除，即推理规则 M N [T,x.s] M和N中没有x,Terms(E,T)非空 M=N[T] 有意义。 o
10 该证明两次使用 (ref)公理，一次栈公理和两次(subst)。 一个证明系统的导出规则是一条推理规则 结论 前提 它满足：从该前提的任何实例，通过使用该证明系统的公理和其他证明规则，可以推导出该 结论的相应实例。例如， [ ] [ ] [ ] [] M N N P PQ M Q 是该代数证明系统的一个导出规则，因为从形式为 M = N, N = P, P = Q 的任意三个等式，两 次使用传递规则可以得到 M = Q。 导出规则的另一个例子是下面的同余规则，直观上说，同余是指“相等的项应用于相等 的项时，产生相等的项”。 1 1 1 1 1 [ ] ... [ ] : ... and ... ... [ ] , ( , ) i k k k s k k i i MN M N fs s s fM M fN N M N Terms (cong) (cong)规则可从(add var), (ref)和(subst)推导。从这些假设，使用(add var)，可以推导出 k 个等式： Mi = Ni[, x1 : s1, …, xi-1 : si-1] （i = 1, …, k） 其中 x1, …, xk是不出现在中的新变量（i = 1 时的等式就是 M1= N1 []）。再由(ref)可得 f x1 … xk = f x1 … xk [,x1 : s1, …, xk : sk] 重复使用(subst)，第一步是先将上式两边的 xk分别用 Mk和 Nk代换，最后一步将倒数第二步 代换结果中两边的 x1 分别用 M1 和 N1 代换。最终得到 f M1 …Mk = f N1…Nk [] 例 2.8 证明等式 top(pop(push x(push 3 empty ))) = 3 [x : nat] 为证明该等式，从栈公理和(ref)的实例开始，应用(subst)，然后再用导出规则(cong)得 到 ( ) [ : , : ] 3 3 [ : ] ( ( 3 )) 3 [ : ] ( ( ( 3 ))) ( 3 ) [ : ] pop push x s s s stack x nat push empty push empty x nat pop push x push empty push empty x nat top pop push x push empty top push empty x nat 再从上例的结果用(add var)得到 top(push 3 empty) = 3 [x : nat] 最后用(trans)得到 top(pop (push x (push 3 empty))) = 3 [x : nat] 例 2.9 下面的规则允许从任何等式的变量类别指派中删除多余变量。如果变量 x 在 M 和N 中都不出现，并且从其他信息知道s类别的项集Termss (, )非空，那么在等式M = N [, x : s]中，x : s 没有什么作用，可以把它从[, x : s]中删除，即推理规则 [ , : ] [ ] M N xs M N M 和 N 中没有 x，Termss (, )非空 有意义