【教学课件】第十章代数语义学.ppt

第十章第十章 代数语义学代数语义学代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。代数规格说明成为语法、语义一体化描述的形式基础。10.1 代数基础代数基础定义定义10.1 代数是形如(A，OP)的对偶，其中A是承载子(carrier)集合，OP代表了操作符的有限集。OPi(a1，a2，an)=as:AA(ai，as A，i =1n)具体代数(true，false，)/布尔代数 (N，+，*)/整数代数 (S，gcd，lcm)/S-代数抽象代数 只给出一抽象的A集合和(组合)算子o，以及在构造中某些必需满足的公理、定理。抽象代数从更高的层次上研究构造子和承载子之间的关系，它不规定具体的值集和操作集，只给出一抽象的A集合和(组合)算子o，以及在构造中某些必需满足的公理、定理。抽象代数中对构造子不同的约定(即应满足的性质)得到不同的抽象代数:群:(A，o)/o不满足任何定理 半群:(A，o)/o必需满足结合律:x o(y o z)=(x o y)o z 独导半群满足恒等定律:x o(i(a)=x =(i(a)o x /其中(A，o)是一个半群,i是恒等操作(函数)i(a)为A的单位元。若o是+，A是整数集，i(a)=0。同样若o是*，i(a)=1。单位元是相对o而言的。每一群(A，o,i)中都有一逆操作i-1的独异(A，o，i-1)满足逆定律:x o i-1 =i(a)=i-1 o x 更为抽象的是泛代数(universal algebra)它把具体代数看作是具有某种操作性质的“对象”去研究各“对象”的“关系”。这些“关系”被抽象为态射(morphism)。定义定义10-2(子代数子代数)设(A，OP)是一个代数，(B，OP)也是一代数且(A，OP)，则称(B，OP)是(A，OP)的子代数，写为(B，OP)(A，OP)。定义定义10-3(范畴范畴category)范畴C是(ob(C)，morp(C)的二元组。其中ob(C)为集合对象X，Y，Z，等的象元集合，morp(C)为C(X,Y)，C(Y,Z)，C(X,Z)，组成的态射集合。C(X,Y)为X到Y的态射(morphism)集合，也可以写作f:XY，fC(X,Y)。X为态射函子f（function）的域(domain)，Y为f的协域(codomain)。公理保证这种映射总是有效。对于每个态射函数的对偶(f，g)，若一态射函数的域是另一态射函数的协域，即f:XY;g:YZ，则可利用组合算子o形成新的态射f o g:XZ。组合算子服从结合律。若f:XY，g:YZ，h:ZW，则有:(h o g)o f =h o(g o f):XW对于范畴每一对象X均存在着恒等(identity)态射idx:XX。因此，对任何态射有:idx o f:(XX)o(XY)=XY:f g o idy f:(YZ)o(YY)=YZ:g态射是表达两代数的结构相似性的有力工具。定义定义10-4(单射，满射，双射单射，满射，双射)若有态射函子f:AB，对于任意两对象a1，a2A，且a1a2，都有f(a1)f(a2)，(f(a1)，f(a2)B)，则f称为单射(injective)函子。对于任意bB都可以找到一个aA，使得b|=|f(a)，则f称为满射(surjective)函子。若f:AB的f既是单射又是满射，则f是可逆的，即存在 f-1:BA。f称为双射(bijective)函子。定义定义10-5(同态映射同态映射homomorphism)若态射函子f:AB是从代数(A，OP)到(B，OP，)的映射。如果对任意opOP，a1，a2，anA有:f(op(a1，a2，an)=op(f(a1)，f(a2)，f(an)(10-1)其中opOP，f(a1)，f(a2)，f(an)B，n=0，1 k。意即代数A中某k目操作op，若将其k个变元先映射到代数B中，总可以找到同目的操作op，以映射后的变元作变元，其结果和op运算后再映射的结果一致。(A，OP)，(B，OP，)是同态的。同理。若f:AB中f是单射的且满足(10-1)，则称单同态(monomorphism)。若f是满射的且满足式(10-1)，则称满同态(epimorphism)。若f是双射的且满足式(10-1)，则称同构(isomorphism)。同态保持两代数结构的相似性，同构即两代数结构相等，仅管其中值集不相同。同态保持两代数结构的相似性，同构即两代数结构相等，仅管其中值集不相同。BOOLEAN =(true，false，not)not(true)=false not(false)=true A =(0,1，flip)flip(0)=1 flip(1)=0 B(yes,no,maybe，change)change(yes)=no change(no)=yes change(maybe)=maybe C(any，same)same(any)=any 若有态射函子h:BOOLEANA。具体定义是:h(true)=1，h(false)=0 我们验证(10-1)式，先看右侧:h(not(true)=h(flase)=0 再看右侧:flip(h(true)=flip(1)=0 因此，代数BOOLEAN和代数A是同态的，且对于0，1均有映射(满射且直射)，故BOOLEAN和A同构。h-1(1)=true，h-1(0)=false成立。若有态射函子h:BOOLEANB。同样有:h(true)=yes，h(false)=no 验证(10-1)式可知BOOLEAN，B是同态的。但由于非满射(maybe无对应)，故非同构。同样，若有h:BOOLEANC。同样有:h(true)=any，h(false)=any验证(10-1)式:h(not(true)=h(flase)=any same(h(true)=same(any)=any它们依然同态，但由于非直射(非一对一),故非同构。以上仅仅是为说明概念的非常简单的例子。为了清晰表明代数间映射关系，常用交换图(commuting diagram)。h BOOLEAN A h-1 id(BOOLEAN)id(A)同构 h BOOLEAN A id(BOOLEAN)id(B)h BOOLEAN B 同态 其中id为恒等函数，其值是单位元操作。图10-1 态射的交换图 程程序序员员在在设设计计程程序序时时如如能能构构造造抽抽象象代代数数，把把它它写写成成规规格格说说明明，即即Sp代代数数，再再通通过过中中间间形形式式变变为为实实现现，可可以以看看作作是是同同态态映映射射变变成成不不同同的的代代数数。这这就就成成为为公公理理化化自自动动程程序序设设计计的的模模型型。为为此此，我我们们还还要要考考察察Sp-代代数数的的具具体体模模型型。先看先看-代数。代数。定义定义10-6(型构型构Singnature)型构是表示操作的符号(有限或无限)集。例如，我们在自然数集上指定四个函数符zero，succ，pred，plus，我们就指明了一个代数结构(N，n)。n是这四个函数符的统称叫型构。定义定义10-7(目目Arity)目是每一函数符所要求的参数个数。对一于中的每一函数符，均有一求目的函数:arity():N arity(zero)=0 /不带参数zero为常(函)数，零目算子。arity(succ)=1 arity(pred)=1 arity(plus)=2定义定义10-8(-代数代数)若一代数其承载子集合A仅由操作，则称(A，A)为_代数。我们将同一施加于三种承载子集合上，分别得到(N，N)，(Z，E)，(E，E)三个_代数。然而，我们最感兴趣的是承承载载子子元元素素均均可可由由生生成成的的项项代代数。数。定义定义10-9(_项，项，_项集，项项集，项_代数代数)若_代数(A，A)中承载子集合A中的每一元素a iA(i=1，n)均可用中的函数符及其复合表示，则每一用函数符号串表示的项称为_项。1 若，且为0目函数符，则即为_项。记为0=C。2 若，且为k0目的函数符，则形如(t1，t k)的串是_项，其中t 1，t k也是_项。记_项的集合为项的集合为T，为满足上述规则的最小项集。3 若T中没有0目，则T=。4 若T则(T，)即为项即为项_代数代数。zero，succ(zero)，succ(succ(zero)，pred(zero)，pred(pred(zero)，succ(pred(zero)，pred(succ(zero)，plus(zero，zero)，plus(succ(zero)，zero)，显然，项代数成了承载子集生成语法规则。按上述项代数定义的承载子集合T是归纳性的，即归纳出常量符号和中每个对这些符号返复操作的最小串的集合。T的归纳性质为导出项的各种特性提供了强有力的证明方法。1 证明中所有常量符号均具有性质P。2 假定项t1,t k 具有性质P，对于中所有k0目的，证明项(t1,t k)也具有性质P。这就是所谓结构归纳法。如欲在T上定义函数g，满足以下两个条件就是充分的:1 定义将g应用于常量函数符的结果。2 对于中每个k0目的，通过g(t1),g(tk)来定义g应用于(t1,t k)的结果。定义定义10-10(_同态同态_同构同构)设设(A，A)，(B，B)是是两两_代代数数，h:AB为为映映射射函函数数，仅仅当当中中每每个个k目目的的，有，有:h(A(a 1,a k)=B(h(a 1),h(a k)(10-2)则两代数则两代数_同态，同态，h为同态映射。为同态映射。若若h为为双双射射的的则则_同同态态h:AB即即为为同同构构。同同构构则则表表明明中中任任何何函函数数符符若若作作用用于于A的的承承载载子子集集上上为为真真，作作用用于于B的的承承载载子子上上亦亦为为真真。反之亦然。同样，两代数值集可以不一样。如A=true，false，(，)，B=1，0，(+*)。定理定理10-1(_同态的唯一性、存在性同态的唯一性、存在性)对于每个对于每个_代数代数(A，A)都存在唯一的都存在唯一的_同态映射同态映射 i A:TA (10-3)1 先证同态存在性。对于中某个k0目的，形如(t1，tk)的项是T的项。按结构归纳法。常量T项的 iA(t1)，iA(tk)已经定义。则iA(t1，tk)可定义为A(iA(t1)，iA(tk)。这样，T中的每一元素都作了iA定义。再检查iA是否同态的:iA(T(t1，tk)=iA(A(t1,tk)/按T定义 =A(iA(t1),iA(tk)/按i A定义其中T:TT，即将项元组映射为项(t1，tk)。此证同态。2 再证唯一性 设h是从T 到A的某个同态映射，只要证明T中的每个t都有iA(t)=h(t)，即iA，h重合。iA(t1，tk)=(iA(t1)，iA(tk)/按i定义 =A(h(t1)，h(tk)/按结构归纳 =h(T(t1，tk)/由于h是同态 =h(t1，tk)/按T定义 iA=h /此证唯一如果我们把如果我们把T看作程序设计语言的语法，看作程序设计语言的语法，_代数代数(A，A)看作是语义域或解释。看作是语义域或解释。则本定理说明语言中的每一表达式或项，在则本定理说明语言中的每一表达式或项，在(A，A)中都对应唯一的含义，即中都对应唯一的含义，即在语义域中只有一个解释。本定理的另一层意图是试图说明在语义域中只有一个解释。本定理的另一层意图是试图说明T是是“最小最小”的的_代数。代数。10.1.3 全等类全等类定义定义10-11(-代数类代数类)具有操作的代数集合称_代数类，记为C。定义定义10-12(初始代数初始代数Initial algebra)若代数类C中_代数I是初始代数，仅当对C中每一_代数J都存在着从I到J的唯一_同态。由定理10-1，项项代代数数T在在所所有有_代代数数的的类类中中是是初初始始的的。这就意味着T到到任任何何_代代数数的的值值都都存存在在着着唯唯一一的的项项映映射射。这是很强的概念。人们只要标识出某个有“意义”的_代数，即可将项映射到该代数的元素上。以此定义项的语义。定理定理10-2 若若_代数类代数类C中代数中代数A，B均为初始代数，则它们必为同构的。均为初始代数，则它们必为同构的。证:若A为初始的，B为一般_代数，按定义10-12它们必存在唯一_同态i1:AB。同样，若B为初始的，A为一般_代数，也存在唯一同态i2:BA。它们的复合 i1 o i2 =AA =idA同理，i2 o i1 =BB =idB所以，它们是同构的。初始代数只在符号形式上区别初始项，只要符号不同就是不同的值。例如，有_项代数 Bool =true，flase，not 其项集是:T =true，not(true)，not(not(true)，false，not(flase)，not(not(flase)，事实上我们知道(true，not(false)，not(not(true)，和false，not(true)，not(not(false)，是语义等价的两个类我们记为true，false。定义定义10-13(_全等全等congruence)在 _代 数(A，A)中，A上 的 关 系 R是 _全 等 关 系，若 有 R(0ik，ai，aiA)成立，仅当对中每个k目的，A(a1，ak)，A(a1，ak)R也成立。按上例，(ture，not(flase)R，则有(not(true)，not(not(false)R。全等关系若以符号直接表示两个项是全等的。以上定义是:若ture not(false)则有 not(ture)not(not(false)定义定义10-14(商代数商代数Quotient Algebra)对于_代数(A，A)中的承载子aA，按全等关系R归于a R则称商化(quotienting)。商化的结果得到全等类集合A/R=a RaA，且在A/R上对中的每个可定义以下映射:A/R(a1 R,a k R=A(a1，ak)R其中A/R A/R，表示的全等类。则称(A/R，A/R)为商代数。可以推论:1(A/R，A/R)是_代数。2 由于存在AA/R直射，h(a)=a R也是_同态。我们最感兴趣的是在项项集集T上上的的_全全等等。如果所有项对偶 R，根据T的初始性有iA:TA，则iA(t)=iA(t)即_代数A也具有等价关系R。设C(R)是所有具有R性质的_代数类。定理定理10-3 (全等的初始性全等的初始性)在具有性质在具有性质R的代数类中的代数类中_代数代数T/R是初始代数是初始代数。10.1.4 泛同构映射泛同构映射 给给定定一一操操作作集集，我我们们可可构构造造所所有有可可能能的的表表达达式式，也也就就是是对对应应于于的的所所有有可能值集的外延。在这个值集上操作的代数则称字代数可能值集的外延。在这个值集上操作的代数则称字代数。3+5按前述自然数集上代数(N，N)是_代数，但不是字代数.定义定义10-15(泛同构泛同构Universal Isomorphism)给给定定一一代代数数，从从它它的的商商代代数数出出发发可可以以找找到到许许多多同同态态映映射射，直直到到找找出出同同构构。则称为泛同构。则称为泛同构。定义定义10-16(自由字代数自由字代数Free word algebra)自由字代数是每个项均可为变量的字代数。因为按泛同构理论，从商代数寻找同构，把字代数因素化要更方便。E(Y)是有变量并以表达式形式表达的承载子集合。例10-4 _字代数的项集 设Y=x，y，z，=+，*对于_字代数(E(Y)，)可能的项集是:x,y,z,x*y，z+x，x*(y+x*z)，定义定义10-10(Sp-代数代数)我我们们称称(0，E)为为Sp-代代数数，其其中中0为为常常量量算算子子集集，为为算算子子集集，E为为公公理集。理集。公理集公理集E是由是由_项表达的全等关系。项表达的全等关系。10.2 代数规格说明代数规格说明 数据类型可以以下述等价方式描述:字代数上的某个全等关系。字代数的某个商代数。代数规格说明中以代数公理给出全等关系。代数公理是表征两个代数项全等的等式集合 x=R y(上下文清晰时略去下标R)即为一简单公理。根据公理置换型构中的操作符，即可生成全等类。置换中遵循全等性质:自反性 x=y，y=x或xy(x,y是同一项)对称性 y=R x 传递性 x=R y，y=R z 则x=R z 全等性 若xi=R yi，有某操作则 xi(x1，xm);yi(y1，ym)0in若有一最简单型构:0:N S:NN和以下公理集:R0 =R1 =0 =0 R2 =0 =S0 R3 =0 =SS0 R4 =S0 =SS0由这五个公理生成的全等类是:C/R0，R1:0，S0，SS0，如果S的语义是“后继”则C/R0，R1为自然数集。C/R2:0，S0，SS0，为所有项均全等的小代数。C/R3:0，SS0，SSSS0，S0，SSS0，SSSSS0，可以看做布尔代数值集(true，false。C/R4:0，S0，SS0，SSS0，以上(C/Ri，)都是_字代数，由于_全等的关系不同，同态映射为自然数、小代数、布尔代数、二值代数。也说明_字代数的初始性。每一代数都是一简单数据类型的模型。10.2.1 Sp代数公理代数公理10-10(Sp-代数公理代数公理)公理带有项变量的等式。形如:r(v1，vn)=s(v1，vn)当变量vi以项ti置换后 r(t1，tn)=s(t1，tn)就是全等项。当变量个数为零时即简单公理。带变量的公理 设有简单型构 0:N S:N N +:N N N R5:x+0=x;x+Sy=S(x+y)R6:SSx=x;x+0=0;x+S9=y10.3 数据类型的代数规格说明数据类型的代数规格说明 specification TURTH-VALUES sort Truth_Value operations ture:Truth_Value false:Truth_Value not_:Truth_ValueTruth_Value _:Truth_Value,Truth_ValueTruth_Value _:Truth_Value,Truth_ValueTruth_Value _=_:Truth_Value,Truth_ValueTruth_Value variablest ,u:Truth_Value equations not true=false (10.5-a)not flase=true (10.5-b)ttrue=t (10.5-c)tfalse=false (10.5-d)tu=ut (10.5-e)t true=true (10.5-f)tfalse=t (10.5-g)tu =ut (10.5-h)t=u=(not t)u (10.5-i)end specification10.3.1 简单类型的代数规格说明简单类型的代数规格说明specification NATURALS include TRUTH_VALUSE sort Natural operations 0 :Natural succ :Natural Natural pred:Natural Natural _ :Natural,Natural Truth_Value _is_ :Natural,Natural Truth_Value _+_ :Natural,Natural Natural _*_ :Natural,Natural Natural variables n,m:Natural equations pred succ n=n (10.6.-a)pred0 =0 (10.6.-b)00 =flase (10.6.-c)0succ n =true (10.6.-d)succ n 0 =false (10.6.-e)succ n succ m=nm=mn (10.6.-g)0 is 0=true (10.6.-h)0 is succ n=false (10.6.-i)succ n is succ m=n is m (10.6.-j)n is m=m is n (10.6.-k)0+n=n (10.6.-l)(succ n)+m (succ(n+m)(10.6.-m)n+m=m+n (10.6.-n)0*n=0 (10.6.-o)(succ n)*m=m+(n*m)(10.6.-p)n*m=m*n (10.6.-q)end specification 公理等式描述的是操作符的代数性质，而不是对左边表达式的定义。例如:n+m =m+n /指出+算子的可交换性。0*n =0 /指出等式两边表表达式的等价性。本规格说明并未显式给出自然数集0，1，2，3，但已给出同构的项集0，succ0，succ succ0，它与以阿拉伯数字表示的自然数集具有完全一致的代数性质。例如，pred(3)=2，我们有:pred succ succ succ0=succ succ 0 按公理(10.6-a)再如，1*n=n，我们有:(succ 0)*n n+(0*n)按公理(10.6-p)n+0 按公理(10.6-n)0+n 按公理(10.6-o)n10.3.2 参数化规格说明参数化规格说明specification NATURALS_LIST include NATURALSsort Listoperations empty_list:List conr(_,_):Natural,ListList head_of_:ListList tail_of_:ListList length_of:ListNaturalvariables c:Natural l:Listequations head_of_cons(c,l)=c tail_of_cons(c,l)=l tail_ofempty_list=empty_list length_of_empty_list=0 lenght_of_cons(c,1)=succ(length_of)end specificationspecification LISTS include NATURALS formal sort Component sort Listoperators empty_list:List cons(_,_):Component,ListList nead_of_:ListComponent tail_of :ListList length_of:ListNaturalvaribles c:Component l:Listequations head_of_cons(c,l)=c （10.7-a）tail_of_cons(cl,l)=l (10.7-b）tail_of_empty_list =empty_list （10.7-c）length_of_empty_list =0 （10.7-d）length_of_cons(c,l)=succ(length_of l)（10.7-e）end specificaionspecification TRUTH_VALUE_LISTS include instantiation of LISTS by TRUTH_VALUES using Truth_Value for Component renamed using Truth_Value_List for Listend specification(2)操作参数化specification ARRAYS include NATURALS formal sort Component formal operation maxsize:Natural sort Array operations empty_array :Array modify(_,_,_):Natural,Component,ArrayArray component_of:Natural,ArrayComponent variables c :Component j,j:Natural a :Array equations component i of modify(j,c,a)=c if i is j i maxsize (10.8-a)component i of modify(j,c,a)=component i of a if not(i is j)(10.8-b)modify(i,c,a)=a if not(imaxsize)(10.8-c)end specification 作为实例化的一个例子，请看以下的最大长度为6的真假值数组的规格说明:specification TRUTH_VALUE ARRAYS include instantiation of ARRAYS by TRUTH_VALUES using Truth_Value of Component succ succ succ succ succ succ 0 for maxsize renamed using Truth_Value_Array for Arrayend specification10.4 演算的代数规格说明演算的代数规格说明 演算的，三种归约。如果我们定义一个置换函数sub(M,a,b)表示a在表达式M中所有自由出现均以b置换，则三种归约描述为:if w is not free in M then(u.M)=(w.sub(M,u,w)(x.M)N)=sub(M,x,N)if x is not free in M then(x.(Mx)=Mspecification LAMBDA_CLACULUS include TRUTH_VALUESsorts Expr,1doperations firstid:1d nextid_ :1d 1d equals(_,_):1d,1d Truth_Value var_:1d Expr ap(_,_):Expr,ExprExpr abs(_,_):1d,Expr Expr *sub(_,_,_):Expr,1d,ExprExpr *notfree(_,_):1d,ExprTruth_Valuevariables v,w,x,y:1d M,N,E:Exprequations equals(x,x)=true equals(firstid,next(x)=false equals(nextid(x),firstid)=false equals(nextid(x),nextid(y)=equals(x,y)notfree(x,var(y)=not equals(x,y)notfree(x,app(M,N)=notfree(x,M)notfree(x,N)notfree(x,abs(y,M)=equals(x,y)not free(x,M)abs(v,M)=if notfree(w,M)then abs(w,sub(M,v,var(w)else abs(v,M)/归约 app(abs(,x,M),N)=sub(M,x,N)/归约 abs(x,(app(M,var(x)=if notfree(x,M)then M else abs(x,app(M,var(x)/归约 sub(var(y),x,E)=if equals(x,y)then E else var(y)sub(app(M,N),x,E)=app(sub(M,x,E),sub(N,x,E)sub(abs(y,M),x,E)=if equals(x,y)then abs(y,M)else if notfree(y,E)then abs(y,sub(M,x,E)else sub(abs(y,M),x,E)end specification10.5 小结小结 本章我们介绍了代数语义学，目标是以代数理论建立描述程序规格说明的代数模型，并介绍具体的定义方法。代数按不同的抽象层次有具体代数(定义值集，操作集)、抽象代数(值和操作关系)和泛代数(代数间关系)。代数间关系最重要是同态映射，同构是两代数有对等的同态映射。交换图可清晰描述范畴中代数对象的映射关系。_代数是给定型构上的代数。_同态、同构指项代数上的。给定一必然得到一类代数，初始代数即对代数类中每一_代数都有唯一同态的代数。初始代数就符号意义是不重复的，但其实际值可能相同，因此引出全等类概念。_全等工具是说代数的承载子有等价关系R，按R归类即得全等类。按全等的等价关系R归类过程称商化，商化结果得的值集构成商代数，商代数可以看作是简化了的字代数，并包含全等概念。泛同构映射指商代数寻求同构的映射。Sp_代数可以是字代数上某个全等关系，或字代数上某个商代数描述。目的是前者，以等式集合给出全等类的公理定义。