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

《【教学课件】第十章代数语义学.ppt》由会员分享，可在线阅读，更多相关《【教学课件】第十章代数语义学.ppt（31页珍藏版）》请在三一办公上搜索。

1、第十章 代数语义学,代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。代数规格说明成为语法、语义一体化描述的形式基础。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，以及在构造中某些必

2、需满足的公理、定理。抽象代数从更高的层次上研究构造子和承载子之间的关系，它不规定具体的值集和操作集，只给出一抽象的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)中都有一

3、逆操作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(

4、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)

5、=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，)的映

6、射。如果对任意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)，则称同构(isomorphi

7、sm)。,同态保持两代数结构的相似性，同构即两代数结构相等，仅管其中值集不相同。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(

8、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)

9、=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、数的具体模型。先看-代数。定义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)为_代数。我们

11、将同一施加于三种承载子集合上，分别得到(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

12、(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，满足以下两个条件就是充分的

13、: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

14、，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)=(i

15、A(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的唯一_同态。

16、由定理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

17、=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，则有(

18、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直射，

19、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)给定一代数，从它的商代数出发可以找到许多同态映射，直到找出同

20、构。则称为泛同构。,定义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 代数规格说明 数据类型可以以下述等价方式描述:字代数上的某个全等关系。字代数的某个商代

21、数。代数规格说明中以代数公理给出全等关系。代数公理是表征两个代数项全等的等式集合 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的语义是“后继”则

22、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)就是全等项。当变量个数为零时即简单公理。

23、带变量的公理 设有简单型构 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=y,10.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,Tr

24、uth_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 specification,10.3.1 简单类型的代数规格说明specification NATURALS include TRUTH_VALUSE sort

25、 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)0m=mn(10.6.-g)0 is 0=true(10.6.-h)0 is

26、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

27、，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)n,10.3.2 参数化规格说明specification NATURALS_LIST include NATURALSsort Listoperations empty_list:List conr(_,_):N

28、atural,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 specification,specification LISTS include NATURALS formal so

29、rt 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）len

30、gth_of_cons(c,l)=succ(length_of l)（10.7-e）end specificaion,specification 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

31、 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

32、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_Ar

33、ray for Arrayend specification,10.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

34、 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:Expr,equations equals(x,x)=true equals(firstid,next(x)=false equals(nextid(x),firstid)=false equals(nextid(x),nextid(y)=equ

35、als(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(

36、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 specification,10.5 小结 本章我们介绍了代数语义学，目标是以代数理论建立描述程序规格说明的代数模型，并介绍具体的定义方法。代数按不同的抽象层次有具体代数(定义值集，操作集)、抽象代数(值和操作

37、关系)和泛代数(代数间关系)。代数间关系最重要是同态映射，同构是两代数有对等的同态映射。交换图可清晰描述范畴中代数对象的映射关系。_代数是给定型构上的代数。_同态、同构指项代数上的。给定一必然得到一类代数，初始代数即对代数类中每一_代数都有唯一同态的代数。初始代数就符号意义是不重复的，但其实际值可能相同，因此引出全等类概念。_全等工具是说代数的承载子有等价关系R，按R归类即得全等类。按全等的等价关系R归类过程称商化，商化结果得的值集构成商代数，商代数可以看作是简化了的字代数，并包含全等概念。泛同构映射指商代数寻求同构的映射。Sp_代数可以是字代数上某个全等关系，或字代数上某个商代数描述。目的是前者，以等式集合给出全等类的公理定义。,