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

抽象代数 只给出一抽象的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: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 态射是表达两代数的结构相似性的有力工具。

定义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)。

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

若有态射函子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)。

h BOOLEAN A h-1 id(BOOLEAN) id(A) 同构 BOOLEAN A id(BOOLEAN) id(B) 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 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Σ，∑)即为项_代数。

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。 这就是所谓结构归纳法。

如欲在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，(+*)}。

定理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 //此证唯一

如果我们把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: 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]}。

定义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性质的∑_代数类。

定理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或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) 0≤i≤n

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

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

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

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

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

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

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