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

Slides:



Advertisements
Similar presentations
因数与倍数 2 、 5 的倍数的特征
Advertisements

第五节 函数的微分 一、微分的定义 二、微分的几何意义 三、基本初等函数的微分公式与微分运算 法则 四、微分形式不变性 五、微分在近似计算中的应用 六、小结.
2.8 函数的微分 1 微分的定义 2 微分的几何意义 3 微分公式与微分运算法则 4 微分在近似计算中的应用.
2.5 函数的微分 一、问题的提出 二、微分的定义 三、可微的条件 四、微分的几何意义 五、微分的求法 六、小结.
全微分 教学目的:全微分的有关概念和意义 教学重点:全微分的计算和应用 教学难点:全微分应用于近似计算.
說 劍 《莊子‧雜篇》─ 第 一 組 賴泊錞 謝孟儒 張維真 羅苡芸
复习: :对任意的x∈A,都有x∈B。 集合A与集合B间的关系 A(B) A B :存在x0∈A,但x0∈B。 A B A B.
第五章 二次型. 第五章 二次型 知识点1---二次型及其矩阵表示 二次型的基本概念 1. 线性变换与合同矩阵 2.
第三章 函数逼近 — 最佳平方逼近.
《高等数学》(理学) 常数项级数的概念 袁安锋
四种命题 2 垂直.
第五节 微积分基本公式 、变速直线运动中位置函数与速度 函数的联系 二、积分上限函数及其导数 三、牛顿—莱布尼茨公式.
一、原函数与不定积分 二、不定积分的几何意义 三、基本积分公式及积分法则 四、牛顿—莱布尼兹公式 五、小结
第5章 定积分及其应用 基本要求 5.1 定积分的概念与性质 5.2 微积分基本公式 5.3 定积分的换元积分法与分部积分法
第三节 函数的求导法则 一 函数的四则运算的微分法则 二 反函数的微分法则 三 复合函数的微分法则及微分 形式不变性 四 微分法小结.
第三节 格林公式及其应用(2) 一、曲线积分与路径无关的定义 二、曲线积分与路径无关的条件 三、二元函数的全微分的求积 四、小结.
第二章 导数与微分 第二节 函数的微分法 一、导数的四则运算 二、复合函数的微分法.
2-7、函数的微分 教学要求 教学要点.
第5章 §5.3 定积分的积分法 换元积分法 不定积分 分部积分法 换元积分法 定积分 分部积分法.
第二章 矩阵(matrix) 第8次课.
走进编程 程序的顺序结构(二).
第18章 代数语义学 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。 代数规格说明成为语法、语义一体化描述的形式基础。 18.1 代数基础 定义18.1 代数是形如(A,OP)的对偶,其中A是承载子(carrier)集合,OP代表了操作符的有限集。
计算机数学基础 主讲老师: 邓辉文.
§2 求导法则 2.1 求导数的四则运算法则 下面分三部分加以证明, 并同时给出相应的推论和例题 .
第一章 函数 函数 — 研究对象—第一章 分析基础 极限 — 研究方法—第二章 连续 — 研究桥梁—第二章.
计算机问题求解 – 论题 函数 2018年11月20日.
1.2子集、全集、补集(二) 楚水实验学校高一数学备课组.
第一章 函数与极限.
第八章 函数 主要内容 函数的定义与性质 函数定义 函数性质 函数运算 函数的逆 函数的合成 双射函数与集合的基数.
四、投影运算 在数据库中, 用关系来描述数据时常用投影运算进行数据操作。
C++语言程序设计 C++语言程序设计 第七章 类与对象 第十一组 C++语言程序设计.
数列.
简单介绍 用C++实现简单的模板数据结构 ArrayList(数组, 类似std::vector)
§4 谓词演算的性质 谓词逻辑Pred(Y)。 是Y上的关于类型 {F,→,x|xX}的自由代数 赋值 形式证明
代数格.
线 性 代 数 厦门大学线性代数教学组 2019年4月24日6时8分 / 45.
第十章 代数语义学 代数语义学是用代数的方法来处理满足一计算逻辑的各种模型。把模型的集合看作是代数结构。代数语义学公理规定算子的组合规则和约束。算子集和域上值集的关系正好是代数系统研究的范畴。 代数规格说明成为语法、语义一体化描述的形式基础。 10.1 代数基础 定义10.1 代数是形如(A,OP)的对偶,其中A是承载子(carrier)集合,OP代表了操作符的有限集。
第四章 一次函数 4. 一次函数的应用(第1课时).
离散数学─归纳与递归 南京大学计算机科学与技术系
复习.
第十章 双线性型 Bilinear Form 厦门大学数学科学学院 网址: gdjpkc.xmu.edu.cn
4.偏序集合中的几个特殊元素 定义:设(A,≤)是一个偏序集合, BA,若存在一个元素bB,对所有b‘B都有b’≤b, 则称b是B的最大元;若都有b≤b‘, 则称b是B的最小元。特别B=A时,称b为A的最大元或最小元。 例:A1={1,2,3,4,5,6},(A1,) 1为A1的最小元,6为A1的最大元.
测验: 2.设是群G上的等价关系,并且对于G的任意三个元素a,x,x‘,若axax’则必有x x‘。证明:与G中单位元等价的元素全体构成G的一个子群。 H={x|xG,并且xe} 对任意的xH, xe, xee=xx-1 对任意的x,yH, xe, ye, eye, x-1xyx-1x.
正切函数的图象和性质 周期函数定义: 一般地,对于函数 (x),如果存在一个非零常数T,使得当x取定义域内的每一个值时,都有
定理21.9(可满足性定理)设A是P(Y)的协调子集,则存在P(Y)的解释域U和项解释,使得赋值函数v(A){1}。
第九节 赋值运算符和赋值表达式.
第16讲 相似矩阵与方阵的对角化 主要内容: 1.相似矩阵 2. 方阵的对角化.
§6.7 子空间的直和 一、直和的定义 二、直和的判定 三、多个子空间的直和.
1.2 子集、补集、全集习题课.
1.设A和B是集合,证明:A=B当且仅当A∩B=A∪B
例:循环群的每个子群一定是循环群。 证明:设H是循环群G的子群,a是G的生成元。 1.aH
第一节 不定积分的概念与性质 一、原函数与不定积分的概念 二、不定积分的几何意义 三、基本积分表 四、不定积分的性质 五、小结 思考题.
第三章 函数的微分学 第二节 导数的四则运算法则 一、导数的四则运算 二、偏导数的求法.
4) 若A可逆,则 也可逆, 证明: 所以.
多层循环 Private Sub Command1_Click() Dim i As Integer, j As Integer
学习任务三 偏导数 结合一元函数的导数学习二元函数的偏导数是非常有用的. 要求了解二元函数的偏导数的定义, 掌握二元函数偏导数的计算.
2.2矩阵的代数运算.
上杭二中 曾庆华 上杭二中 曾庆华 上杭二中 曾庆华.
第15讲 特征值与特征向量的性质 主要内容:特征值与特征向量的性质.
2.2直接证明(一) 分析法 综合法.
第五章 函数 函数也叫映射,交换,是数学中的一个基本概念,在高数中,函数的概念是从变量的角度提出来的,这种函数一般是连续或间断连续的函数,这里将连续函数的概念推广到离散量的讨论,即将函数看作一种特殊的二元关系。
第八章 函数 主讲:李春英 办公地点:软件大楼202
第二节 函数的极限 一、函数极限的定义 二、函数极限的性质 三、小结 思考题.
《离散结构》 二元运算性质的判断 西安工程大学计算机科学学院 王爱丽.
§2 方阵的特征值与特征向量.
定义21.17:设P1=P(Y1)和P2=P(Y2),其个体变元与个体常元分别为X1,C1和 X2,C2,并且或者C1=或者C2。一个半同态映射(,):(P1,X1∪C1)→(P2,X2∪C2)是一对映射: P1→P2; : X1∪C1→X2∪C2,它们联合实现了映射p(x,c)→(p)((x),
第四节 向量的乘积 一、两向量的数量积 二、两向量的向量积.
陪集 例:三次对称群S3={e,1, 2, 3, 4, 5}的所有非平凡子群是:
§4.5 最大公因式的矩阵求法( Ⅱ ).
§2 自由代数 定义19.7:设X是集合,G是一个T-代数,为X到G的函数,若对每个T-代数A和X到A的函数,都存在唯一的G到A的同态映射,使得=,则称G(更严格的说是(G,))是生成集X上的自由T-代数。X中的元素称为生成元。 A变, 变 变, 也变 对给定的 和A,是唯一的.
Presentation transcript:

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