是永真的，并且语义相等是对称的和传递的。后两个性质可形式化为下面两条推理规则。 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[] 99 是永真的，并且语义相等是对称的和传递的。后两个性质可形式化为下面两条推理规则。 [] [] 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     