《代数语义学》ppt课件

《《代数语义学》ppt课件》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第十章代数语义学代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。代数规格说明成为语法、语义一体化描述的形式基础。10.1代数基础定义10.1代数是形如(A，OP)的对偶，其中A是承载子(carrier)集合，OP代表了操作符的有限集。OPi(a1，a2，…an)=as:A→A(ai，as∈A，i=1‥n)具体代数({true，false}，{∧，∨，})//布尔代数(N，{+，*})//整数代数(S，{gcd，lcm})//S-代数抽象代

2、数只给出一抽象的A集合和(组合)算子{o}，以及在构造中某些必需满足的公理、定理。抽象代数从更高的层次上研究构造子和承载子之间的关系，它不规定具体的值集和操作集，只给出一抽象的A集合和(组合)算子{o}，以及在构造中某些必需满足的公理、定理。《抽象代数》中对构造子不同的约定(即应满足的性质)得到不同的抽象代数:群:(A，{o})//o不满足任何定理半群:(A，{o})//o必需满足结合律:xo(yoz)=(xoy)oz独导半群满足恒等定律:xo(i(a))=x=(i(a))ox//其中(A，{o})是一个半群,i是恒等操作(函数)i(a)为A的单位元。若o是+，

3、A是整数集，i((a)=0。同样若o是*，i(a)=1。单位元是相对o而言的。每一群(A，{o,i})中都有一逆操作i-1的独异(A，{o，i-1})满足逆定律:xoi-1=i(a)=i-1ox更为抽象的是泛代数(universalalgebra)它把具体代数看作是具有某种操作性质的“对象”去研究各“对象”的“关系”。这些“关系”被抽象为态射(morphism)。定义10-2(子代数)设(A，OP)是一个代数，(B，OP)也是一代数且(A，OP)，则称(B，OP)是(A，OP)的子代数，写为(B，OP)≤(A，OP)。定义10-3(范畴category)范畴C

4、是(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:X→Y，f∈C(X,Y)。X为态射函子f（function）的域(domain)，Y为f的协域(codomain)。公理保证这种映射总是有效。对于每个态射函数的对偶(f，g)，若一态射函数的域是另一态射函数的协域，即f:X→Y;g:Y→Z，则可利用组合算子o形成新的态射fog:X→Z。组合算子服从结合律。若f:X→Y，g:Y→Z，

5、h:Z→W，则有:(hog)of=ho(gof):X→W对于范畴每一对象X均存在着恒等(identity)态射idx:X→X。因此，对任何态射有:idxof:(X→X)o(X→Y)=X→Y:fgoidyf:(Y→Z)o(Y→Y)=Y→Z:g态射是表达两代数的结构相似性的有力工具。定义10-4(单射，满射，双射)若有态射函子f:A→B，对于任意两对象a1，a2∈A，且a1≠a2，都有f(a1)≠f(a2)，(f(a1)，f(a2)∈B)，则f称为单射(injective)函子。对于任意b∈B都可以找到一个a∈A，使得b

6、

7、=

8、

9、f(a)，则f称为满射(surjec

10、tive)函子。若f:A→B的f既是单射又是满射，则f是可逆的，即存在f-1:B→A。f称为双射(bijective)函子。定义10-5(同态映射homomorphism)若态射函子f:A→B是从代数(A，OP)到(B，OP，)的映射。如果对任意op∈OP，a1，a2，…an∈A有:f(op(a1，a2，…an))=op'(f(a1)，f(a2)，…f(an))(10-1)其中op'∈OP'，f(a1)，f(a2)，…f(an)∈B，n=0，1…k。意即代数A中某k目操作op，若将其k个变元先映射到代数B中，总可以找到同目的操作op'，以映射后的变元作变元，其结

11、果和op运算后再映射的结果一致。(A，OP)，(B，OP，)是同态的。同理。若f:A→B中f是单射的且满足(10-1)，则称单同态(monomorphism)。若f是满射的且满足式(10-1)，则称满同态(epimorphism)。若f是双射的且满足式(10-1)，则称同构(isomorphism)。同态保持两代数结构的相似性，同构即两代数结构相等，仅管其中值集不相同。BOOLEAN=({true，false}，not)not(true)=falsenot(false)=trueA=({0,1}，flip)flip(0)=1flip(1)=0B({yes,no,

12、maybe}，chang