泛代数和代数数据类型(编辑修改稿)

泛代数和代数数据类型(编辑修改稿)内容摘要：

u的所有项的集合，即： Tu a, b, c, fa, fb, fc, gaa, gab, gac, gbb, …, g (f ( fa ) ) (f (gbc) ), … } 在该项代数中，函数符号 f的解释 f T 是把任何项 M映射到项 f M 的函数， g T类似。 如果环境 把 变量 x 映射到 a，把 y 映射到 f b，那么有 T g(f x) (f y)   g(f a) (f ( f b) )  下面的引理将含义和代换联系在一起。 引理 令 M  Terms(, )，并且 是满足 的项代数 Terms(, )的环境，那么 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才会永真。 语义蕴涵和一个等式证明系统 二元组 Spec  , E，包含一个基调 和一组等式 E，叫做 代数规范。 通常把代数规范Spec  , E看成是说明了一组代数，即一组满足 E 的 代数。 这就引出了语义蕴涵概念。 如果满足基调 上的一组等式 E的所有 代数 A都满足等式 M  N，那么就说 E 语义上蕴涵这个等式 M  N，写成 E M  N 很容易明白，在满足规范 Spec  , E的 所有代数中都成立的等式也就是由 E语义蕴涵的 等式。 如果一组等式在语义蕴涵下封闭，那么把它叫做一个语义理论。 更准确地说，如果 E M  N蕴涵 M  N  E，那么等式集合 E叫做一个 语义理论。 一个代数 A的理论 Th(A)是在 A 中成立的所有等式的集合。 读者很容易检查，一个代数的理论是一个语义理论。 证明见习题。 本节剩余部分致力于讨论语义蕴涵的代数证明系统。 前面已提到，一个证明系统的两个重要性质是 可靠性 和 完备性。 可靠性的意思是，若一个等式 从一组假设 E 是可证明的，那么 E 语义上蕴涵该等式。 完备性相反，如果 E 语义上蕴涵一个等式，那么该等式可从 E 证明。 本节证明代数证明系统的可靠性， 节证明完备性。 9 有关相等的某些性质是“泛”的，它们不依赖于代数的特别性质。 具体说，语义相等是个等价关系。 这就是说，自反公理的每个实例 M  M (ref ) 是永真的，并且语义相等是对称的和传递的。 后两个性质可形式化为下面两条推理规则。 ][ ][ MN NM (sym) ][ ][],[   PM PNNM (trans) 下一条推理规则允许在等式中增加类别指派。 这条规则不是很重要，但它不可少。 需要这条规则的原因是，有了它就可以考虑没有在项中出现的变量。 该规则是 ] : ,[ ][ sxNM NM  x 不在 中 (add var) 它允许加一个变量到任何类别指派。 重复使用该规则，可以加入有限个变量。 很容易验证，一个代数 A 满足这条规则的假设，那么它一定满足其结论。 最后一条规则叫做 等价代换。 如果不提及 类别指派的话，该代换规则是说，如果 M  N 并且 P  Q，那么用 P 和 Q分别 代换 M 和 N中的 x，所得到的两个结果相等。 该规则形式化表达如下： )( ,][][][ ][ ], : ,[   ,/ sT e r m sQPNxQMP / x QPsxNM (subst) 这条规则的一个明显限制是，不能代换含 x 的 P 和 Q 到等式 M  N, x : s 中，因为 P = Q[]的类别指派 假定为不含 x。 但是从习题 可以看出，实际上这并不是一个问题。 如果从 E中的等式和公理 (ref )及推理规则 (sym)、 (trans)、 (subst) 和 (add var) 可以推出等式 M  N，那么就说该等式是 可证明的 ，并写成 E M  N 更形式地说，从 E 到 E 的证明是一个等式序列，使得每个等式是公理、 E 中的等式、或者是序列中早先出现的一个或多个等式的一步推导的结果。 有关证明的一种有用的推理形式是基于 E 的证明长度的归纳。 如果 E 封闭于可证明性，那么就说 E是一个 语法理论。 换种说法，如果 E M  N蕴涵 M  N  E，那么 E是一个语 法理论。 E 的语法理论 Th(E)也就是从 E 可证明的所有等式的集合。 通过下面关于可靠性和完备性的证明，可以得知语法上的代数理论和语义上的代数理论是相同的。 但是，目前仍保持两个定义是有用的。 等式集合 E 是 语义一致的(consistent)，如果存在某个等式 M  N，它不是 E 的语义蕴涵；等式集合 E是 语法一致的 ，如果存在某个等式 M  N，它不能由 E 证明。 例 （例 和 的继续）在基调 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 其证明如下： 10 ] [ 3 ) 3 ( ] [ 3 3 ]:[ ) ( ]:[ ],: ,:[ ) (  e m p t yp u s ht o pnatxxe m p t yxp u s ht o p natxe m p t ye m p t ynatxs t a c ksxsxp u s ht o p 该证明两次使用 (ref)公理，一次栈公理和两次 (subst)。  一个证明系统的 导出规则 是一个推理规则 结论前提 使得从该前提的任何实例，通过使用该证明系统的公理和其它证明规则，可以推导出该结论的相应实例。 例如， ][ ][ ],[ ],[   QM QPPNNM 是该代数证明系统的一个 导出规则，因为 从形式为 M = N, N = P, P = Q的任意三个等式，两次使用传递规则可以得到 M = Q。 导出规则的另一个例子是下面的同余规则，直观上说，同余是指“相等的项作用于相等的项时，产生相等的项”。 ),(, a nd ... :][... ... ][ ..., ],[ 111 11    isii kkk kk T e r m sNM sssfNfNMfM NMNM （ cong） (cong)规则可从 (add var), (ref)和 (subst)推导。 从这些假设，使用 (add var)，可以推导 k个等式（下面 i = 1 时的等式就是 M1= N1 []）： Mi = Ni[, x1 : s1, …, xi1 : si1] （ i = 1, …, k） 其中 x1, …, xk 是不出现在 中的新变量。 再由 (ref)可得 f x1 … xk = f x1 … xk [,x1 : s1, …, xk : sk] 重复使用 (subst)，第一步是先将上式两边的 xk分别用 Mk 和 Nk代换，最后一步将倒数第二步代换结果中两边的 x1分别用 M1和 N1代换。 最终得到 f M1 … Mk = f N1… Nk[] 例 证明等式 top(pop(push x(push 3 empty ))) = 3[x : nat] 为证明该等式，从栈公理和 (ref)的实例开始，应用 (subst)，然后再用导出规则 (cong)得到 ]:)[ 3 ( ))) 3 ( ( ( ]:[ 3 )) 3 ( ( ]:[ 3 3 ],: ,:[ ) ( natxe m p t yp u s ht o pe m p t yp u s hxp u s hpopt o pnatxe m p t yp u s he m p t yp u s hxp u s hpopnatxe m p t yp u s he m p t yp u s hnatxs t a c ksssxp u s hpop 再从上例的结果用 (add var)得， top(push 3 empty) = 3[x : nat] 最后用 (trans) top(pop (push x (push 3 empty))) = 3[x : nat]  例 下面的规则 允许从任何等 式的变量类别指派中删除多余变量。 如果变量 x 在 M和 N 中都不出现，并且从其它信息知道 s 类别的项集 Termss (, )非空，那么在等式 M = N [, x : s]中， x : s 没有什么作用，可以把它从 [, x : s]中删除，即推理规则 11 ][ ]: ,[   NM sxNM M 和 N 中没有 x， Termss (, )非空 有意义。 很容易证明这是一个导出规则。 因为 Termss (, )非空，则存在某个 PTermss (, )，使得 P = P []。 结合假设 M = N [, x : s]，用 (subst)可以证明 [Px]M = [Px]N []。 因为变量 x在 M 和 N 中不出现，代换没有影响，因此 M = N []。  本节主要定理如下： 定理 （ 可靠性 ）如果 E E，那么 E E。 证明 可以根据该证明的长度进行归纳，即根据 E E 的证明长度来证明 E E。 归纳 基础是长度为 1 的证明，它是公理或 E 的一个等式。 不管哪一种情况，很容易看出，任何满足 E 的代数一定满足该等式。 对于归纳步骤，假定证明 E 的最后一步是从 E1, …, En得到，并且 E1, …, En是由更短的证明得到。 从归纳假设可以假定，如果 A E，那么 A 满足 E1, …, En。 要证明的是，如果A 满足最后一条规则的这些前提，那么 A 满足 E。 这就导致根据证明规则的集合，对各种情况进行分析。 下面仅给出对代换规则的证明。 假定 A M = N [, x : s]，并且 A P = Q []。 必须证明 A [Px]M = [Qx]N []。 令 是满足 的任意一个环境，必须证明 [Px]M  = [Qx]N 。 令 a = P  = Q ，并且注意 [x  a]满足 , x : s。 由代换引理： [Px]M  = M ([x  a]) 并 且 [Qx]N  = N ([x  a]) 因为 A M = N [, x : s]，因此 M ([x  a]) ＝ N ([x  a]) 从而 [Px]M 和 [Qx]N 相等。 这就完成了本定理的证明。  使用这个定理，通过下面的命题可以说明为什么在等式中掌握变量的情况是重要的。 命题 存在一个代数理论 E 和不含 x 的项 M 和 N，使得 E M=N, x : s，但是 E M=N 。 证明 令 是一个基调，它有类别 a 和 b，函数符号 f : a  b 和 c, d : b。 令 E 是包含能从 f x = c[x : a]和 f x = d [x : a]证明的所有等式，并且考虑等式 c = d [x : a]。 很清楚，从 E 的等式通过传递性可以得到它。 但是从下面的语义讨论可以看到，等式 c = d[]是不可证明的。 考虑一个 代数，其对应 a的载体是空集，但是 c 和 d分 别 指称对应 b 的非空载体上的两个不同元素。 等式 f x = c [x : a]和 f x = d [x : a]在这个模型中为真，因为 x 没有任何可能的值。 但是等式 c = d []在此模型中不成立。 因此，由等式证明系统的可靠性， c = d []是不可能从 E 证明的。  可靠性定理不仅表明证明系统是语义正确的，而且可以知道，如果能找出一个代数满足E 而不满足某个等式 E，即 E从语义上并不蕴涵 E，那么从 E 不可能证明 E。 在不知等式 E是否由等式集合 E 语义蕴涵时，可以作两种尝试：从 E 证明 E，或 者找出一个满足 E 而不满足 E 的代数。 原则上，根据完备性定理，这两者之间总有一个是可能的。 但是应该认识到，在寻找一个证明和寻找一个代数以表明不存在这样的证明这两者之间有一。