中国科学技术大学：《程序设计语言理论》课程教学资源（参考教材）第2章 泛代数和代数数据类型

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 (, )，都有M1  M2，因为 M 中的每个变量必定出现在中。 证明 该证明也是基于项结构的归纳。对 x1, …, xk中的任何变量 xi 有 xi1  1(xi) 2(xi)  xi2 对任何项 f M1 … Mk，假定该引理对每个 Mi 都成立，即对所有的 i 有Mi1  Mi2。 然后证明f M1 … Mk1  f M1 … Mk2。该证明如下： f M1 … Mk1  f  (M11, …, Mk1)  f  (M12, …, Mk2)  f M1 … Mk2 这就证明了该引理。 ￾ 2.2.4 代换引理 代数、一阶逻辑和类型化演算都有的一个非常重要的性质叫做代换引理。直观上，就 M 的含义而言，用 N 代换项 M 中的 x 和改变环境使得 x 等于 N 的值，两者的效果是一样的。 换句话说，当用项代换变量时，被代换项的含义是本质的，而它的语法形式不是。这就使得 项中的子项可以用等价的项来替换。这是一个非常有用的性质，在推理中经常使用，它是代 数项的等式证明系统的中心。 在论述此引理时用记号xa表示这样一个环境：除了 x 映射到 a 外，该环境在其他 变量上和一致。 引理 2.4（代换引理）令 M Termss (, , x : s)并且 N  s Terms  (, )，那么NxM  Termss (, )。并且对任何环境，有 NxM M(x a)，其中 a N是 N 在下的含义 证明 根据项 M 的结构进行归纳。如果 M 是变量，分两种情况，即 M 是否就是 x。这 两种情况的证明是直截了当的，把它们留给读者。 对于归纳步骤，考虑形式为 f M1 … Mk的项。该项的相应代换实例是 f NxM1 … NxMk。 从含义的定义知道 f NxM1 … NxMk  f (NxM1, …, NxMk) 由归纳假设，NxMi 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] 不可能成立。例如，如果一个环境的映射是 x0 和 y1，那么该等式不成立。但是，如果 在类型指派增加变量 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 (, )非空 有意义