代数语义学

《代数语义学》由会员分享，可在线阅读，更多相关《代数语义学（37页珍藏版）》请在金锄头文库上搜索。

1、第 1 页 共 39 页代数代数语义语义学学代数代数语义语义学用数学函数的指称或描述程序的行学用数学函数的指称或描述程序的行为为和状和状态态。它是面向。它是面向值值(域域)的。的。以最以最终值终值刻划程序的效刻划程序的效应应。用。用语义语义函数得到各种域上函数得到各种域上值值来刻划程序的行来刻划程序的行为为。当然，。当然，这这些效些效应应和行和行为为都是在既定模型上的都是在既定模型上的值值。 。代数代数语义语义学是用代数的方法来学是用代数的方法来处处理理满满足一足一计计算算逻辑逻辑的各种模型。把模型的的各种模型。把模型的集合看作是代数集合看作是代数结结构。代数构。代数语义语义学的公理学的公理规

2、规定了算子的定了算子的组组合合规则规则和和约约束。算子集束。算子集和域上和域上值值集的关系正好是代数系集的关系正好是代数系统统研究的范畴。正是由于域上研究的范畴。正是由于域上值值都可以用算子都可以用算子生成，算子集及其生成，算子集及其约约束就成了束就成了论论域的域的语语法。同法。同样样，域上，域上值值反映了反映了语义语义。因此，代数。因此，代数规规格格说说明成明成为语为语法、法、语义语义一体化描述的形式基一体化描述的形式基础础。在程序。在程序语语言的言的类类型型检查检查、 、类类型型多多态态、抽象数据、抽象数据类类型、正确性型、正确性证证明、面向明、面向对对象中得到广泛象中得到广泛应应用。用。

3、本章讨论语义学的代数途径：17.1 节 先复习担象代数中的基本理论继而介绍代数和字代数、商代数；17.2 节 介绍以代数模型与代数规格说明中的问题；17.3 节 是类型的代数规格说明的写法；17.4 节 给出 演算的代数规格说明实例。17.1 代数基础代数基础代数学是研究数的运算规则，和数学符号在满足这些规则中的结构。计算机中的数据天然具有代数性质; 离散数据对应的符号运算。所以，代数是精确描述离散数据和类型的数学工具。17.1.1 抽象代数中的基本概念和定义: 定义定义 17.1(代数代数)代数是形如(A，OP)的对偶，其中 A 是承载子(carrier)集合，OP 代表了操第 2 页 共

4、39 页作符的有限集。其中每个 OPi是以 A 的元素操作数并返回某个 A 的元素的算子(操作符)，即OPi(a1，a2，an) = as: AA(ai，as A，i = 1n)其中 OPi的变元 a1an和 as都是承载子集合 A 中的离散数据。可以在不同的抽象层次上研究代数，我们给出:(true，false， ) /布尔代数(N，+，*) /整数代数(S，gcd，lcm) /S-代数都是具体代数，即指定具体的值集和操作集，第一行是布尔数据类型的完整模型。第二行，N 是整数集，所指定的操作是说明只研究整数的加、乘运算的代数。第三行 S 是整数或实数集，gcd 是求最大公约数，lcm 求最小公

5、倍数。我们就叫它 S-代数，在 S 集上研究这两种运算的代数。我们不能随意指定操作如:(N，+，0 目的函数符，则形如 (t1，t k)的串是_项，其中 t 1，t k也是_项。记_项的集合为 T ，为满足上述规则的最小项集。3 若 T中没有 0 目 ，则 T = 。4 若 T 则(T，)即为项_代数。例 17-3 设定义如前例，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

6、)，显然，项代数成了承载子集生成语法规则。程序设计语言中的数据和操作可按某给定的型构以项代数构造。项_代数是特殊的_代数。按上述项代数定义的承载子集合 T是归纳性的，即归纳出常量符号和中每个 对这些符号返复操作的最小串的集合。T的归纳性质为导出项的各第 10 页 共 39 页种特性提供了强有力的证明方法。例如，为了证明 T中所有项均具有 P 性质，只要证明以下两点就是充分的。1 证明中所有常量符号均具有性质 P。2 假定项 t1,t k 具有性质 P，对于中所有 k0 目的 ，证明项(t1,t k)也具有性质 P。这就是所谓结构归纳法。它在项的结构上归纳。我们也可以用结构归纳法定义 T上的关系

7、和函数。例如，如欲在 T上定义函数 g，满足以下两个条件就是充分的:1 定义将 g 应用于常量函数符的结果。2 对于中每个 k0 目的 ，通过 g(t1), g(tk) 来定义 g 应用于 (t1, t k) 的结果。这两个条件可归并为:假定将 g 应用于项 t1, t k的结果成立，则对中每个 k0 目的 ,可定义 g 应用于 (t1,t k)的结果。有了结构归纳法我们继续考察项代数的性质。定义定义 17-10 (_同态，同态，_同构同构)设(A，A )，(B，B) 是两_代数，h: AB 为映射函数，仅当中每个 k 目的 ，有:h(A (a 1 , a k) = B (h(a 1), h(

8、a k) (17-2)则两代数_同态，h 为同态映射。通俗地说_同态为你有的承载子集及其服从的操作性质我也有，反过来则未必。当然具体值集可以不一样。读者可按此定义验证例 17-2 中 (N, N) 和 (Z，Z) 非同态，而 (N，N) 和 (E，E) 是同态的。若 h 为双射的则_同态 h: AB 即为同构。同构则表明中任何函数符若第 11 页 共 39 页作用于 A 的承载子集上为真，作用于 B 的承载子上亦为真。反之亦然。同样，两代数值集可以不一样。如 A = true，false，(,)，B = 1，0，( + , * )。请注意 同态和一般代数同态是一个意思，只是它仅限于集，更容易满

9、足。定理定理 17-1(_同态的唯一性、存在性同态的唯一性、存在性)对于每个_代数(A，A)都存在唯一的_同态映射i A: TA (17-3)证明1 先证同态存在性。对于中某个 k0 目的 ，形如 (t1，tk)的项是 T的项。按结构归纳法。常量 T项的 iA (t1) ，iA(tk)已经定义。则 iA(A (t1, , tk)可定义为A (iA (t1) , , iA(tk)。这样，T中的每一元素都作了 iA定义。再检查 iA是否同态的:设中的 是 k 目的，则有:iA(T ( t1 , tk ) = iA (A( t1, tk ) /按 T定义= A (iA (t1), , iA(tk)

10、/按 i A定义其中 T: TT，即将项元组映射为项 (t1, tk)。此证同态。 2 再证唯一性设 h 是从 T 到 A 的某个同态映射，只要证明 T中的每个 t 都有 iA(t) = h(t)，即 iA，h 重合。不失一般性，设 是 k 目的，有:iA (t1, tk) = (iA(t1), iA(tk) /按 i 定义= A(h(t1), h(tk) /按结构归纳第 12 页 共 39 页= h (T(t1, tk) /由于 h 是同态= h (t1, tk) /按 T定义 iA = h 此证唯一。 如果我们把 T看作程序设计语言的语法，_代数(A，A)看作是语义域或解释。则本定理说明语

11、言中的每一表达式或项，在(A，A)中都对应唯一的含义，即在语义域中只有一个解释。本定理的另一层意图是试图说明 T是“最小”的_代数。一般说来，_代数(A，A)有许多项是相等的。如(N，N)的 pred(succ(zero)和 zero; (E,E)的 succ(pred(zero)和 zero。既然存在唯一的同态 iA; TA，若(A，A)中有 iA(t1) = iA(t2)，则 T中 t1和 t2必然相等。这样，T就应该是“最小”的_代数了。事实上是做不到的。为了证明这一点，设 A 等于 T，那么存在的唯一同态就是 T上的恒等函数 idT。只有在 t1和 t2在语法上也完全一致时，idT(t

12、1) = idT(t2)才是正确的。17.1.3 全等类全等类在讨论全等类之前我们先作几个定义。定义定义 17-11(-代数类代数类)具有操作的代数集合称_代数类，记为 C。定义定义 17-12(初始代数初始代数 Initial algebra)若代数类 C 中_代数 I 是初始代数，仅当对 C 中每一_代数 J 都存在着从 I 到 J 的唯一_同态。由定理 17-1，项代数 T在所有_代数的类中是初始的。这就意味着 T到任何_代数的值都存在着唯一的项映射。这是很强的概念。人们只要标识出某个有“意义”的_代数，即可将项映射到该代数的元素上。以此定义项的语义。第 13 页 共 39 页定理定理

13、17-2 若_代数类 C 中代数 A，B 均为初始代数，则它们必为同构的。证: 若 A 为初始的，B 为一般_代数，按定义 17-12 它们必存在唯一_同态 i1: AB。同样，若 B 为初始的，A 为一般_代数，也存在唯一同态i2: BA。它们的复合i1 o i2 = AA = idA同理，i2 o i1 = BB = idB所以，它们是同构的。初始代数只在符号形式上区别初始项，只要符号不同就是不同的值。例如，有_项代数Bool = true，flase，not其项集是:T = true，not(true)，not(not(true), , false，not(flase)，not(not(

14、flase),事实上我们知道(true，not(false)，not(not(true),，和false，not(true)，not(not(false), 是语义等价的两个类我们记为true, false。定义定义 17-13 (_全等全等 congruence)在_代数(A, A)中，A 上的关系 R 是_全等关系，若R (0ik，ai，aiA)成立，仅当对中每个 k 目的 R 也成立。按上例，(ture，not(false)R，则有( not( true )，not(not(false)R。全等关系若以符号直接表示两个项是全等的。以上定义是:第 14 页 共 39 页若 ture not(false) 则有not(ture) not(not(false)定义定义 17-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)为商代