2.3等式、可靠性和完备性 代数规范 一个基调+一组等式 -调查什么样的代数满足这些等式强加的要求 使用等式证明系统可推导的新的等式 可靠性：从规范可证明的等式在任何满足该规范 的代数中都成立 完备性：在满足规范的所有代数中都成立的等式 都可从该规范证明 代数规范是描述代数数据类型公理语义的工具
2.3 等式、可靠性和完备性 • 代数规范 一个基调 + 一组等式 – 调查什么样的代数满足这些等式强加的要求 – 使用等式证明系统可推导的新的等式 – 可靠性：从规范可证明的等式在任何满足该规范 的代数中都成立 – 完备性：在满足规范的所有代数中都成立的等式 都可从该规范证明 – 代数规范是描述代数数据类型公理语义的工具
2.3等式、可靠性和完备性 2.3.1等式 公式M=N[T],对某个s,M,N∈Ters②，) -若满足T，并且还有 M7= N 7,则认为 代数A在环境n下满足M=N[T],写成 A,7 M=NT] -若A在任何环境下都满足该等式，则写成 A M=NI] -若代数类C中的任何代数A都满足该等式，写成 C M=NT] -若任何一个Σ代数都满足等式M=N[T],则写成 M=NT] (永真的、有效的)
2.3 等式、可靠性和完备性 2.3.1 等式 公式 M = N ，对某个s，M, N Termss (, ) – 若满足，并且还有 M = N ，则认为 代数A在环境下满足M = N ，写成 A, M = N – 若A在任何环境下都满足该等式，则写成 A M = N – 若代数类C中的任何代数A都满足该等式，写成 C M = N – 若任何一个代数都满足等式M = N ，则写成 M = N (永真的、有效的 )
2.3等式、可靠性和完备性 平凡的代数 若A满足Σ上所有等式，就说Σ代数A是平凡的 例 令Σ有两个类别a和b,令A是一个Σ代数，其中 Aa={0,1}并且Ab=⑦ A不可能满足x=yx:a,y:a,即下式不成立 A x=yx:a,y:a -但是Ax=yx:a,y:,乙：b]无意义地成立
2.3 等式、可靠性和完备性 • 平凡的代数 若A满足上所有等式，就说代数A是平凡的 • 例 – 令有两个类别a和b，令A是一个代数，其中 Aa={0,1}并且Ab= – A不可能满足x = y [x : a, y : a]，即下式不成立 A x = y [x : a, y : a] – 但是A x = y [x : a, y : a, z : b]无意义地成立
2.3等式、可靠性和完备性 2.3.2项代数 项代数Ters②，) -类别s的载体：集合Terms②，T 函数符号f:S1×.×Sk→S的解释 I(f)(Mi...,M)=fM...M 项代数Terms(2,T)的环境n也叫做一个代换 如果S是代换，则用SM表示同时把M中的各个变 量x用Sx替换的结果 因此用7M表示把代换作用于M的结果
2.3 等式、可靠性和完备性 2.3.2 项代数 • 项代数Terms(, ) – 类别s的载体：集合Termss (, ) – 函数符号f : s1 … sk → s的解释 I (f ) (M1 , …, Mk ) = f M1 … Mk – 项代数Terms(, )的环境也叫做一个代换 – 如果S是代换，则用SM表示同时把M中的各个变 量x用Sx替换的结果 – 因此用M表示把代换作用于M的结果
2.3等式、可靠性和完备性 例 类别w - 函数符号f:w→u和g:u×u→u -T=fa:u,b:u,c:u Tu={a,b,c,fa,fb,fc,gaa,gab,gac,gbb,... g (f(fa))(fgbc)),.. 若环境把变量x映射到a,把y映射到fb,则 T g(fx)(fy) n=gf)f(fb)
2.3 等式、可靠性和完备性 • 例 – 类别u – 函数符号f : u → u和g : u u → u – = {a : u, b : u, c : u} – Tu= a, b, c, fa, fb, fc, gaa, gab, gac, gbb, …, g (f (fa)) (f(gbc)), … } – 若环境把变量x映射到a，把y映射到f b，则 T g(f x) (f y) = g(fa) (f (f b))