Presentation is loading. Please wait.

Presentation is loading. Please wait.

第十章 代数语义学 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。 代数规格说明成为语法、语义一体化描述的形式基础。 10.1 代数基础 定义10.1 代数是形如(A,OP)的对偶,其中A是承载子(carrier)集合,OP代表了操作符的有限集。

Similar presentations


Presentation on theme: "第十章 代数语义学 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。 代数规格说明成为语法、语义一体化描述的形式基础。 10.1 代数基础 定义10.1 代数是形如(A,OP)的对偶,其中A是承载子(carrier)集合,OP代表了操作符的有限集。"— Presentation transcript:

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必需满足结合律: 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

3 更为抽象的是泛代数(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:X→Y,f∈C(X,Y)。X为态射函子f(function)的域(domain),Y为f的协域(codomain)。公理保证这种映射总是有效。 对于每个态射函数的对偶(f,g),若一态射函数的域是另一态射函数的协域,即f:X→Y; g: Y→Z,则可利用组合算子o形成新的态射f o g: X→Z。组合算子服从结合律。若f: X→Y,g:Y→Z,h:Z→W,则有: (h o g) o f = h o (g o f): X→W 对于范畴每一对象X均存在着恒等(identity)态射idx: X→X。因此,对任何态射有: idx o f : (X→X) o (X→Y) = X→Y: f g o idy f : (Y→Z) o (Y→Y) = Y→Z: g 态射是表达两代数的结构相似性的有力工具。

4 定义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|| =|| f (a),则f称为满射(surjective) 函子。 若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',以映射后的变元作变元,其结果和op运算后再映射的结果一致。(A,OP),(B,OP,)是同态的。 同理。若f: A→B中f是单射的且满足(10-1),则称单同态(monomorphism)。 若f是满射的且满足式(10-1),则称满同态(epimorphism)。 若f是双射的且满足式(10-1),则称同构(isomorphism)。

5 同态保持两代数结构的相似性,同构即两代数结构相等,仅管其中值集不相同。
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: BOOLEAN→A。具体定义是: 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成立。

6 若有态射函子h:BOOLEAN→B。同样有:
h(true) = yes,h(false) = no 验证(10-1)式可知BOOLEAN,B是同态的。但由于非满射(maybe无对应),故非同构。 同样,若有h: BOOLEAN→C。同样有: h(true) = any,h(false) = any 验证(10-1)式: h(not(true)) = h(flase) = any same(h(true)) = same(any) = any 它们依然同态,但由于非直射(非一对一),故非同构。以上仅仅是为说明概念的非常简单的例子。为了清晰表明代数间映射关系,常用交换图(commuting diagram)。

7 h BOOLEAN A h-1 id(BOOLEAN) id(A) 同构 BOOLEAN A id(BOOLEAN) id(B) BOOLEAN B 同态 其中id为恒等函数,其值是单位元操作。 图10-1 态射的交换图

8 程序员在设计程序时如能构造抽象代数,把它写成规格说明,即Sp代数,再通过中间形式变为实现,可以看作是同态映射变成不同的代数。这就成为公理化自动程序设计的模型。为此,我们还要考察Sp-代数的具体模型。先看∑-代数。 定义10-6(型构Singnature) 型构是表示操作的符号(有限或无限)集。例如,我们在自然数集上指定四个函数符{zero,succ,pred,plus},我们就指明了一个代数结构(N,∑n)。∑n是这四个函数符的统称叫型构。 定义10-7(目Arity) 目是每一函数符所要求的参数个数。对一于∑中的每一函数符σ,均有一求目的函数: arity(σ): ∑→N arity(zero) = // 不带参数zero为常(函)数,零目算子。 arity(succ) = 1 arity(pred) = 1 arity(plus) = 2

9 定义10-8(∑-代数) 若一代数其承载子集合A仅由∑操作,则称(A,∑A)为∑_代数。 我们将同一∑施加于三种承载子集合上,分别得到(N,∑N),(Z,∑E),(E,∑E)三个∑_代数。然而,我们最感兴趣的是承载子元素均可由∑生成的项代数。 定义10-9 (∑_项,∑_项集,项_代数) 若∑_代数(A,∑A)中承载子集合A中的每一元素a i∈A(i=1,…n)均可用∑中的函数符及其复合表示,则每一用函数符号串表示的项称为∑_项。 [1] 若σ∈∑,且为0目函数符,则σ即为∑_项。记为σ0 = C。 [2] 若σ∈∑,且为k>0目的函数符,则形如σ(t1,…t k)的串是∑_项,其中t 1,…t k也是∑_项。 记∑_项的集合为TΣ ,为满足上述规则的最小项集。 [3] 若TΣ中没有0目σ,则TΣ = Φ。 [4] 若TΣ≠则(TΣ,∑)即为项_代数。

10 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,对于∑中所有k>0目的σ,证明项 σ(t1,…,t k)也具有性质P。 这就是所谓结构归纳法。

11 如欲在TΣ上定义函数g,满足以下两个条件就是充分的:
[1] 定义将g应用于常量函数符的结果。[2] 对于∑中每个k>0目的σ,通过g(t1),…,g(tk)来定义g应用于σ(t1,…,t k)的结果。 定义10-10 (∑_同态∑_同构) 设(A,∑A ),(B,∑B)是两∑_代数,h: A→B为映射函数,仅当∑中每个k目的σ,有: h(σA (a 1 ,…,a k)) = σB (h(a 1),…,h(a k)) (10-2) 则两代数∑_同态,h为同态映射。 若h为双射的则∑_同态h: A→B即为同构。同构则表明∑中任何函数符若作用于A的承载子集上为真,作用于B的承载子上亦为真。反之亦然。同样,两代数值集可以不一样。如A = {true,false,(∧,∨)},B = {1,0,(+*)}。

12 定理10-1(∑_同态的唯一性、存在性) 对于每个∑_代数(A,∑A)都存在唯一的∑_同态映射 i A: TΣ→A (10-3) [1] 先证同态存在性。 对于∑中某个k>0目的σ,形如σ(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Σ: TΣ→TΣ,即将项元组< t1,…tk >映射为项σ(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 //此证唯一

13 如果我们把TΣ看作程序设计语言的语法,∑_代数(A,∑A)看作是语义域或解释。则本定理说明语言中的每一表达式或项,在(A,∑A)中都对应唯一的含义,即在语义域中只有一个解释。本定理的另一层意图是试图说明TΣ是“最小”的∑_代数。 全等类 定义10-11(∑-代数类) 具有∑操作的代数集合称∑_代数类,记为C。 定义10-12(初始代数Initial algebra) 若代数类C中∑_代数I是初始代数,仅当对C中每一∑_代数J都存在着从I到J的唯一∑_同态。 由定理10-1,项代数TΣ在所有∑_代数的类中是初始的。这就意味着TΣ到任何∑_代数的值都存在着唯一的项映射。这是很强的概念。人们只要标识出某个有“意义”的∑_代数,即可将项映射到该代数的元素上。以此定义项的语义。

14 定理10-2 若∑_代数类C中代数A,B均为初始代数,则它们必为同构的。 证: 若A为初始的,B为一般∑_代数,按定义10-12它们必存在唯一∑_同态i1: A→B。同样,若B为初始的,A为一般∑_代数,也存在唯一∑同态i2: B→A。它们的复合 i1 o i2 = A→A = idA 同理,i2 o i1 = B→B = 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]}。

15 定义10-13 (∑_全等congruence) 在∑_代数(A,∑A)中,A上的关系R是∑_全等关系,若有<ai,ai'>∈R(0≤i≤k,ai,ai'∈A)成立,仅当对∑中每个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)中的承载子a∈A,按全等关系R归于[a] R则称商化(quotienting)。商化的结果得到全等类集合A/R = {[a] R|a∈A},且在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] 由于存在A→A/R直射,h(a) = [a] R也是∑_同态。 我们最感兴趣的是在项集TΣ上的∑_全等。如果所有项对偶<t,t'> R ,根据TΣ的初始性有iA: TΣ→A,则iA(t) = iA(t')即∑_代数A也具有等价关系R。设C(R)是所有具有R性质的∑_代数类。

16 定理10-3 (全等的初始性) 在具有性质R的代数类中∑_代数TΣ/R是初始代数。 泛同构映射 给定一操作集,我们可构造所有可能的表达式,也就是对应于∑的所有可能值集的外延。在这个值集上操作的代数则称字代数。 3+5按前述自然数集上代数(N,∑N)是∑_代数,但不是字代数. 定义10-15(泛同构Universal Isomorphism) 给定一代数,从它的商代数出发可以找到许多同态映射,直到找出同构。则称为泛同构。

17 定义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是由∑_项表达的全等关系。

18 即为一简单公理。根据公理置换型构中的操作符,即可生成全等类。置换中遵循全等性质:
10.2 代数规格说明 数据类型可以以下述等价方式描述: ·字代数上的某个全等关系。 ·字代数的某个商代数。 代数规格说明中以代数公理给出全等关系。 代数公理是表征两个代数项全等的等式集合 x = R y(上下文清晰时略去下标R) 即为一简单公理。根据公理置换型构中的操作符,即可生成全等类。置换中遵循全等性质: 自反性 x = y,y = x或x≡y(x,y是同一项) 对称性 y = R x 传递性 x = R y,y = R z 则x = R z 全等性 若xi = R yi,有某操作σ则 xi≡σ(x1,…,xm); yi≡σ(y1,…,ym) ≤i≤n

19 若有一最简单型构: 0: →N S: N→N 和以下公理集: 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,∑)都是∑_字代数,由于∑_全等的关系不同,同态映射为自然数、小代数、布尔代数、二值代数。也说明∑_字代数的初始性。每一代数都是一简单数据类型的模型。

20 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 = y}

21 10.3 数据类型的代数规格说明 specification TURTH-VALUES sort Truth_Value operations ture: Truth_Value false: Truth_Value not_: Truth_Value→Truth_Value _∧_: Truth_Value , Truth_Value→Truth_Value _∨_: Truth_Value , Truth_Value→Truth_Value _ = >_: Truth_Value , Truth_Value→Truth_Value variablest , u: Truth_Value equations not true = false (10.5-a) not flase = true (10.5-b) t∧true = t (10.5-c) t∧false = false (10.5-d) t∧u = u∧t (10.5-e) t ∨ true = true (10.5-f) t∨false = t (10.5-g) t∨u = u∨t (10.5-h) t=>u = (not t )∨u (10.5-i) end specification

22 简单类型的代数规格说明 specification NATURALS include TRUTH_VALUSE sort Natural operations 0 : Natural succ : Natural → Natural pred : Natural → Natural _<_ : Natural , Natural → Truth_Value _>_ : Natural , Natural → Truth_Value _is_ : Natural , Natural → Truth_Value _+_ : Natural , Natural → Natural _*_ : Natural , Natural → Natural variables n , m: Natural

23 equations pred succ n = n (10.6.-a)
pred0 = (10.6.-b) 0< = flase (10.6.-c) 0<succ n = true (10.6.-d) succ n <0 = false (10.6.-e) succ n <succ m = n<m (10.6.-f) n>m = m<n (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 = (10.6.-o) (succ n)* m = m+(n*m) (10.6.-p) n*m = m*n (10.6.-q) end specification

24 公理等式描述的是操作符的代数性质,而不是对左边表达式的定义。
例如: n+m = m+n //指出'+'算子的可交换性。 0*n = //指出等式两边表表达式的等价性。 本规格说明并未显式给出自然数集{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 按公理(10.6-n) ≡ 0+n 按公理(10.6-o) ≡ n

25 参数化规格说明 specification NATURALS_LIST include NATURALS sort List operations empty_list: List conr(_,_): Natural , List→List head_of_: List→List tail_of_: List→List length_of: List→Natural variables c: Natural l: List equations 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 sort Component sort List operators empty_list: List cons(_,_) : Component , List→List nead_of_ : List→Component tail_of : List→List length_of : List→Natural varibles c: Component l: List equations 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 = (10.7-d ) length_of_cons(c , l) = succ(length_of l )(10.7-e ) end specificaion

26 specification TRUTH_VALUE_LISTS
include instantiation of LISTS by TRUTH_VALUES using Truth_Value for Component renamed using Truth_Value_List for List end specification (2) 操作参数化 specification ARRAYS include NATURALS formal sort Component formal operation maxsize: Natural sort Array operations empty_array : Array modify(_,_,_): Natural , Component , Array→Array component_of: Natural , Array→Component variables c : Component j , j : Natural a : Array

27 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 (i<maxsize) (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 Array

28 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)) = M specification LAMBDA_CLACULUS include TRUTH_VALUES sorts Expr , 1d operations firstid: 1d nextid_ : 1d → 1d equals(_,_): 1d , 1d → Truth_Value var_ : 1d → Expr ap(_,_): Expr , Expr→Expr abs(_,_): 1d , Expr → Expr * sub (_,_,_): Expr , 1d , Expr→Expr * notfree(_,_): 1d , Expr→Truth_Value variables v , w , x , y: 1d M , N , E: Expr

29 equations 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))) // η归约

30 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 specification

31 10.5 小结 本章我们介绍了代数语义学,目标是以代数理论建立描述程序规格说明的代数模型,并介绍具体的定义方法。 代数按不同的抽象层次有具体代数(定义值集,操作集)、抽象代数(值和操作关系)和泛代数(代数间关系)。 代数间关系最重要是同态映射,同构是两代数有对等的同态映射。 交换图可清晰描述范畴中代数对象的映射关系。 ·∑_代数是给定型构∑上的代数。∑_同态、同构指项代数上的。 给定一∑必然得到一类代数,初始代数即对代数类中每一∑_代数都有唯一∑同态的代数。 初始代数就符号意义是不重复的,但其实际值可能相同,因此引出全等类概念。∑_全等工具是说∑代数的承载子有等价关系R,按R归类即得全等类。 按全等的等价关系R归类过程称商化,商化结果得的值集构成商代数,商代数可以看作是简化了的字代数,并包含全等概念。 泛同构映射指商代数寻求同构的映射。 Sp_代数可以是字代数上某个全等关系,或字代数上某个商代数描述。目的是前者,以等式集合给出全等类的公理定义。


Download ppt "第十章 代数语义学 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。 代数规格说明成为语法、语义一体化描述的形式基础。 10.1 代数基础 定义10.1 代数是形如(A,OP)的对偶,其中A是承载子(carrier)集合,OP代表了操作符的有限集。"

Similar presentations


Ads by Google