这个定义很简单，也很容易看出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) 88 这个定义很简单，也很容易看出 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 )