《第十章代数语义学课件培训资料》由会员分享，可在线阅读，更多相关《第十章代数语义学课件培训资料（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集合和
2、(组合)算子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) =
3、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)，m
4、orp(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 (
5、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既
6、是单射又是满射，则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，)是同
7、态的。 同理。若f: AB中f是单射的且满足(10-1)，则称单同态(monomorphism)。 若f是满射的且满足式(10-1)，则称满同态(epimorphism)。 若f是双射的且满足式(10-1)，则称同构(isomorphism)。,若有态射函子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(f
8、lase) = 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代数，再通过中间形式变为实现，可以看作是同态映射变成不同
9、的代数。这就成为公理化自动程序设计的模型。为此，我们还要考察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(
10、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 ，为满足上述规则
11、的最小项集。 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
12、 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的承载子集上为真
13、，作用于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 (
14、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)中都对应唯一的含义，即在语义
15、域中只有一个解释。本定理的另一层意图是试图说明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 = tru
