《代数语义学.docVIP

代数语义学 代数语义学用数学函数的指称或描述程序的行为和状态。它是面向值(域)的。以最终值刻划程序的效应。用语义函数得到各种域上值来刻划程序的行为。当然，这些效应和行为都是在既定模型上的值。 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学的公理规定了算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。正是由于域上值都可以用算子生成，算子集及其约束就成了论域的语法。同样，域上值反映了语义。因此，代数规格说明成为语法、语义一体化描述的形式基础。在程序语言的类型检查、类型多态、抽象数据类型、正确性证明、面向对象中得到广泛应用。 本章讨论语义学的代数途径： 17.1节 先复习担象代数中的基本理论继而介绍代数和字代数、商代数； 17.2节 介绍以代数模型与代数规格说明中的问题； 17.3节 是类型的代数规格说明的写法； 17.4节 给出λ演算的代数规格说明实例。 17.1 代数基础 代数学是研究数的运算规则，和数学符号在满足这些规则中的结构。计算机中的数据天然具有代数性质; 离散数据对应的符号运算。所以，代数是精确描述离散数据和类型的数学工具。 17.1.1 《抽象代数》中的基本概念和定义: 定义17.1(代数) 代数是形如(A，OP)的对偶，其中A是承载子(carrier)集合，OP代表了操作符的有限集。 其中每个OPi是以A的元素操作数并返回某个A的元素的算子(操作符)，即 OPi(a1，a2，…an) = as: A→A(ai，as ∈A，i = 1‥n) 其中OPi的变元a1…an和as都是承载子集合A中的离散数据。可以在不同的抽象层次上研究代数，我们给出: ({true，false}，{∧，∨， ? }) //布尔代数 (N，{+，*}) //整数代数 (S，{gcd，lcm}) //S-代数 都是具体代数，即指定具体的值集和操作集，第一行是布尔数据类型的完整模型。第二行，N是整数集，所指定的操作是说明只研究整数的加、乘运算的代数。第三行S是整数或实数集，gcd是求最大公约数，lcm求最小公倍数。我们就叫它S-代数，在S集上研究这两种运算的代数。 我们不能随意指定操作如: (N，{+，}) 就不是一个代数，因为操作，当有两个N的元素比较时结果值是真假值，超出了N的范围。反过来，我们倒可以把操作集看作承载子集的构造子，它按照算子OPi规定的规则生成。 抽象代数从更高的层次上研究构造子和承载子之间的关系，它不规定具体的值集和操作集，只给出一抽象的A集合和(组合)算子{o}，以及在构造中某些必需满足的公理、定理。《抽象代数》中对构造子不同的约定(即应满足的性质)得到不同的抽象代数: 群: (A，{o}) //o不满足任何定理 半群: (A，{o}) // o必需满足结合律: x o (y o z) = (x o y) o z 独异半群: (A，{o，i}) //其中(A，{o})是一个半群, i是恒等操作(函数) 独导半群满足恒等定律: x o (i(a)) = x = (i(a)) o x 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)。通过态射可以知道两代数是否同态、同构、和等价。程序是数据（对象）集和该数据集上的操作集构成，从代数的意义上写一个程序就是构造一具体代数。抽象的语法就是抽象的字代数，将它态射到等价的有“值”的代数上就得到它的语义解释。 定义17-2(子代数) 设(A，OP)是一个代数 ，(B，OP)也是一代数且?(A，OP)，则称(B，OP)是(A，O