1、形式语义学形式语义学Formal Semantics of Programming Languages 2011.09内容回顾内容回顾n形式语义学形式语义学n什么是形式语义学？什么是形式语义学？n形式语义学的分类；形式语义学的分类；n程序设计语言的基本概念程序设计语言的基本概念n语法和语义语法和语义n不同程序设计范例及其特点不同程序设计范例及其特点n命令式语言不同结构的抽象语法定义命令式语言不同结构的抽象语法定义2022-6-82形式语义学的分类形式语义学的分类n从不同角度研究程序的含义从不同角度研究程序的含义n操作语义：操作语义：用机器模型语言来解释语言语义。即设定一个抽象用机器模型语言来解
2、释语言语义。即设定一个抽象机，用语言成分在该机器上的执行来解释语言成分的含义。（机，用语言成分在该机器上的执行来解释语言成分的含义。（实现实现 或或 执行）执行）n指称语义：指称语义：采用形式系统方法，用相应的数学对象对一个语言采用形式系统方法，用相应的数学对象对一个语言的语义进行注释。考虑每个语言成分的执行效果的语义进行注释。考虑每个语言成分的执行效果( (数学对象数学对象- -指指称称) )；（效果）；（效果）n公理语义：公理语义：把程序设计语言视为一个数学对象，建立它的公理把程序设计语言视为一个数学对象，建立它的公理系统，在此基础上对程序进行推理验证。从而使程序设计语言系统，在此基础上对
3、程序进行推理验证。从而使程序设计语言具有坚实的逻辑基础。（逻辑）具有坚实的逻辑基础。（逻辑）n代数语义：代数语义：采用代数的方法进行语义注释的方法。主要基于范采用代数的方法进行语义注释的方法。主要基于范畴论、类别代数理论、抽象数据类型；（数据和操作行为）畴论、类别代数理论、抽象数据类型；（数据和操作行为）2022-6-83程序设计语言的基本概念程序设计语言的基本概念n词法词法(lexeme)n定义语言所允许的单词的种类及其构成定义语言所允许的单词的种类及其构成(spelling)n标识符，保留字，整数，实数等标识符，保留字，整数，实数等n语法语法(syntax)n定义程序所允许的语法结构定义程
4、序所允许的语法结构(grammar)n表达式，语句，声明，函数等表达式，语句，声明，函数等n语义语义(semantics)n定义语法结构正确的程序的含义定义语法结构正确的程序的含义(meaning)n重复声明，作用域，类型检查等重复声明，作用域，类型检查等2022-6-84第二章第二章 函数式抽象描述方法函数式抽象描述方法n2.1 论域理论基础论域理论基础n2.2 Lambda演算演算n2.3 函数式抽象语言函数式抽象语言n2.4 函数式抽象语言的应用函数式抽象语言的应用 2022-6-85第二章第二章 函数式抽象描述方法函数式抽象描述方法n2.1 论域理论基础论域理论基础(Domain Th
5、eory)n2.1.0 集合的基本概念集合的基本概念n2.1.1 完全半序集完全半序集 (complete partial order set, CPO)n2.1.2 连续函数连续函数(continuous functions)n2.1.3 最小不动点最小不动点(least fixed point)2022-6-86第二章第二章 函数式抽象描述方法函数式抽象描述方法n2.2 Lambda演算演算( calculus)n2.2.1 Lambda演算介绍演算介绍n 表达式表达式n自由变量自由变量 free variables(FV)n替换替换 substitutionn变换规则变换规则 conve
6、rsion rulesn归约归约 reduction n2.2.2 Lambda演算作为计算模型演算作为计算模型n2.2.3 Lambda演算系统的扩充演算系统的扩充2022-6-87第二章第二章 函数式抽象描述方法函数式抽象描述方法n2.3 函数式抽象语言函数式抽象语言n2.3.1 函数式语言概述函数式语言概述n2.3.2 类型及其操作类型及其操作n2.3.3 无模式表达式无模式表达式n2.3.4 模式及其模式匹配模式及其模式匹配n2.3.5 基于模式的纯函数式语言基于模式的纯函数式语言2022-6-882.1.1 完全半序集完全半序集-半序集半序集n定义定义 (半序集半序集)设设D是一个集
7、合，是一个集合， 是定义在是定义在D上的上的二元关系，二元关系， 满足下面性质：满足下面性质：n自反性：自反性： x D, 有有x x;n传递性：传递性： x ,y,z D, 若有若有x y和和y z，则，则必有必有x z；n反对称性：反对称性： x ,y,z D, 若有若有x y和和y x，则必有则必有x=y；n称称 为为半序半序 关系关系(partial_order relation), n(D， )为为半序集半序集(partial_order set)2022-6-89半序集半序集n例例1nD = 1，2，pow(D)是是D的所有子集构成的集合的所有子集构成的集合， 是定义在是定义在D上
8、的上的子集关系子集关系，npow(D)=, 1,2,1,2n 是是pow(D)上的半序关系；上的半序关系；n(pow(D) ， )为半序集；为半序集；n可以用图表示：可以用图表示：2022-6-810121，2半序集半序集n例例2n数学上的数学上的 和和 构成半序关系构成半序关系n集合集合A上的恒等关系上的恒等关系 IA 是是A上的半序关系上的半序关系n正整数集合上的整除关系也是半序关系正整数集合上的整除关系也是半序关系n 和和 不能构成半序关系不能构成半序关系2022-6-811半序集的特点是：不要求对于半序集中的任意两个元素都有半序关系，即允许有些元素之间不存在半序关系！若半序集(D, )
9、中的任意两个元素之间都存在半序关系，则称(D, )为全序集。 最小上届最小上届n上/下界：设(D, )为任意半序集，而且DD, dD,则子集D的上界和下界的定义如下：n上界：若对任意dD, 都有d d, 则称d为D的上界；n下界：若对任意dD, 都有d d, 则称d为D的下界；n最小上界/最大下界：设(D, )为任意半序集，而且DD,则子集D的最小上界和最大下界的定义如下：n最小上界：设d是D的一个上界，若对D的任意一个上界d, 都有d d, 则称d为D的最小上界，并记为 D；n最大下界：设d是D的一个下界，若对D的任意一个下界d, 都有 d d, 则称d为D的最大下界，并记为 D；2022-
10、6-812特殊元素及其性质特殊元素及其性质n下界、上界、最大下界、最小上界不一定存在下界、上界、最大下界、最小上界不一定存在n下界、上界存在不一定惟一下界、上界存在不一定惟一n最大下界、最小上界如果存在，则惟一最大下界、最小上界如果存在，则惟一n最小元：设：设(D, )为任意半序集为任意半序集, d D, 如果如果对于任意对于任意D中的元素中的元素d都有都有d d ，则称，则称d为为D的的最小元。n集合的最小元就是它的最大下界，最大元就是集合的最小元就是它的最大下界，最大元就是它的最小上界；反之不对它的最小上界；反之不对. 2022-6-813半序集的特殊元素半序集的特殊元素n例例3 设设是偏
11、序集，其中是偏序集，其中nD =a, b, c, d, e, f, g, h, =, , , ,ID n设设 Ab,c,d, 求求 A 的下界、上界、最大下界的下界、上界、最大下界、最小上界、最小上界. 2022-6-814A的下界和最大下界都不存在，的下界和最大下界都不存在，A也没有最小元也没有最小元上界有上界有d 和和 f, 最小上界为最小上界为 d. 链，递增链，递减链链，递增链，递减链n定义定义 链链n设设为任意半序集为任意半序集, 是是D上的一个序列，简上的一个序列，简记为记为X Xi i, 则递增链和递减链定义如下：则递增链和递减链定义如下：n递增链：递增链：若对任意若对任意i i
12、都有都有X Xi i X Xi+1i+1 ，则称序，则称序列列XXi i 为递增链；为递增链；n递减链：递减链：若对任意若对任意i i都有都有X Xi+1i+1 X Xi i ，则称序，则称序列列XXi i 为递减链；为递减链；n链的最小上届记为：链的最小上届记为：XXi i 或或 i iX Xi i 或或 X Xi i 2022-6-8152.1.1 完全半序集完全半序集n定义定义 完全半序集完全半序集(complete partial order set, CPO)n设设为为一一个半序集个半序集, 若满足下面两个若满足下面两个条件，则称条件，则称为完全半序集：为完全半序集：nD有最小元；有
13、最小元；n对于对于D的任一递增链的任一递增链 XXi i 都有最小上届都有最小上届 XXi i 。2022-6-8162.1.1 完全半序集完全半序集n例例4 完全半序集完全半序集n如果如果D D是任意有穷整数集，是任意有穷整数集， 是定义在是定义在D D上的小上的小于等于关系，于等于关系，则则(D, (D, ) ) 为完全半序集；为完全半序集；n有最小元的有穷半序集是完全半序集；有最小元的有穷半序集是完全半序集；n如果如果D D表示开区间表示开区间( (a, b)a, b)，其中，其中a a和和b b是实数，是实数，则则(D, (D, ) ) 不是完全半序集；不是完全半序集；2022-6-8
14、172.1.1 完全半序集完全半序集n为什么引入完全半序集？为什么引入完全半序集？n在形式地描述程序设计语言的语义时在形式地描述程序设计语言的语义时(指称语指称语义方法义方法)，要求所考虑的集合都满足完全半序，要求所考虑的集合都满足完全半序集的条件；集的条件；n建立建立论域论域的数学模型：的数学模型：满足一定条件的定义了满足一定条件的定义了关系的集合关系的集合( (完全半序集完全半序集) )；n如何构造完全半序集？如何构造完全半序集？n平坦集一定是完全半序集平坦集一定是完全半序集n扩展任意集合为平坦集的方法非常简单扩展任意集合为平坦集的方法非常简单 2022-6-818平坦集平坦集n定义定义
15、平坦集平坦集n设设为一个半序集为一个半序集, 若满足下面两个若满足下面两个条件，则称条件，则称为平坦半序集为平坦半序集(平坦集平坦集)：nD有最小元；有最小元；n只有下面的关系只有下面的关系(平坦关系平坦关系)： ， d，d d, 其中其中d是是D中非中非 的元素。的元素。2022-6-819 平坦集平坦集n扩展任意一个集合为平坦集的方法扩展任意一个集合为平坦集的方法n任意一个集合任意一个集合D;n引进一个最小元引进一个最小元 D；n在集合在集合D = D D上定义平坦关系上定义平坦关系 ： D D ， D d，d d ；n为一个平坦集，简记为为一个平坦集，简记为D ；2022-6-820性质
16、：平坦集一定是完全半序集。平坦集一定是完全半序集。平坦集的例子平坦集的例子n例例5 D = 1, 1,2, 1,3,关系是关系是集合包含关系集合包含关系 ，则，则(D, )是一个平坦集是一个平坦集；其中最小元是；其中最小元是1; ;n BOOL = true, false,可以扩充为平可以扩充为平坦集：坦集：n引入引入最小元最小元 ；n定义一个平坦定义一个平坦关系关系 ： , true, false, true true, false false；n则则(BOOL , )是平坦集是平坦集2022-6-821论域问题引子论域问题引子n试编制一个程序实现下面有限自动机的试编制一个程序实现下面有限自
17、动机的功能。功能。2022-6-822XBA100011nstate = X;nreadone(ch);nwhile ch # don if ch = 1 then out(state)n else if state = X then state = A n else if state = A then state = Bn else if state = B then state = An else skip fi fi fi;fi;n readone(ch);nod 2022-6-823XBA100011可将程序看作是一个函数，函数：定义域函数：定义域 值域值域即输入到输出的映射。即输入到
18、输出的映射。程序的编者主观上认程序的编者主观上认定输入域是定输入域是0，1，#，其实还，其实还可以输入其它字符。可以输入其它字符。显然，一个正确的程显然，一个正确的程序设计必须给出序设计必须给出在输入不是在输入不是集合集合0，1，#中的一个元素时，中的一个元素时，应指出是应指出是“无定义无定义”的错误处理。的错误处理。 -论域论域做大了做大了论域论域n引入目的：引入目的：n描述描述类型类型的数学模型；的数学模型；n指称语义学和函数式语言中都要用到。指称语义学和函数式语言中都要用到。nScott论域及其构造论域及其构造2022-6-824Scott论域及其构造论域及其构造n论域论域(Domain
19、)：n定义了关系的定义了关系的,满足一定条件的集合满足一定条件的集合(CPO)；n论域分为原始域和非原始域论域分为原始域和非原始域(构造域构造域)n原始域：有限集或可枚举集都是原始域原始域：有限集或可枚举集都是原始域ntrue,false , ,-1,0,1, n非原始非原始域：可以从已知论域，应用域：可以从已知论域，应用论域构造论域构造符符进行构造进行构造。2022-6-825可以证明，如果每个成分是完全半序集，则保如果每个成分是完全半序集，则保证构造符作用后得到的仍然是完全半序集证构造符作用后得到的仍然是完全半序集. 论域构造符论域构造符n设设(Di, i )是完全半序集是完全半序集, i
20、 = 1, ,n, , 则我们定义了则我们定义了如下论域构造符：如下论域构造符： ,+, *和和，通过它们的作用，通过它们的作用可以得可以得到新的论域到新的论域；n(1)(1)元组域元组域( (乘积域或卡氏域乘积域或卡氏域) (D1 Dn , )定义如定义如下下: : nD1 Dn = (d1, , dn) | di Di , i=1, ,n；n关系关系 ：(d1, dn) (d1, , dn )当且仅当当且仅当di i di， i=1, ,n；n称为称为n n元组域，简记为元组域，简记为D1 Dn 或或D1 Dnn最小元：最小元：( D1， ， Dn )n对应没有域名的结构对应没有域名的结构
21、类型类型(struct) 2022-6-826元组域的例子元组域的例子n例例6：1，2 BOOLnD1 = 1，2，1 1，1 2，2 2 (整数上的整数上的 )nD2 = BOOL，false b false，false b true，true b true n集合：集合：D = (1,true),(1,false),(2,true),(2,false)n关系：关系： x : 自身自身: (1,true) x (1,true) ,.n (1,false) x(1,true), (2,false) x (2,true)n (1,true) x (2,true), (1,false) x(2,f
22、alse)n (1,false) x (2,true)n最小元：最小元： (1,false) 2022-6-827论域构造符论域构造符n(2)(2)联合域联合域 (D1 Dn , )定义如下定义如下: : nD1 Dn = (j,dj) | dj Dj , j=1, ,n ；n关系关系 ： n ;n (j,dj);n (i,di) (j,dj)当且仅当当且仅当i = j 而且而且 di i dj ， n i(j)=1, ,n；n简记为简记为 D1 Dn 或或D1 Dnn最小最小元元： n对应联合类型对应联合类型(union)2022-6-828联合域的例子联合域的例子n例例7：1，2 BOOL
23、nD1 = 1，2，1 1，1 2，2 2 (整数上的整数上的 )nD2 = BOOL，false b false，false b true，true b true n集合：集合：D = (1,1),(1,2),(2,true),(2,false), n关系：关系： + : 自身自身: (1,1) +(1,1) ,.n (1,1) +(1,2), (2,false) + (2,true)n +i (1,1),(1,2),(2,true), (2,false) n最小元：最小元： 2022-6-829论域构造符论域构造符n(3)(3)序列序列域域 (D* , )定义如下定义如下: : nD* =
24、 | di Di , n 0,i=1,2, ;n关系关系 ： n ;n ;n ,当且仅当当且仅当n = m 而而n 且且 di i di , i=1, ,n；n简记为简记为 D*n最小最小元元： n对应对应表表类型类型2022-6-830序列域的例子序列域的例子n例例8：1，2 *nD1 = 1，2，1 1，1 2，2 2 (整数上的整数上的 )n集合：集合：D = , ,n关系：关系： * : n自身自身: * , * .n元素个数相同的序列之间满足条件的关系有：元素个数相同的序列之间满足条件的关系有：n *, n *, *, *,n *, *,n最小元：最小元： 2022-6-831论域构
25、造符论域构造符n(4)(4)函数空间函数空间 (DD , )定义如下定义如下: : nDD = f | d D, f(d) = d D;n关系关系 ：对于任意：对于任意f,hf,h D D，n f h,当且仅当当且仅当 d D ，f(d) D h(d)n简记为简记为 DD 或或DDn最小元最小元 ： d D ， (d) = D 2022-6-832函数域的例子函数域的例子n例例9：1，2 BOOLnD1 = 1，2，1 1，1 2，2 2 (整数上的整数上的 )nD2 = BOOL，false b false，false b true，true b true n集合：函数的集合，其中每个函数的
26、定义域是集合：函数的集合，其中每个函数的定义域是D1，值域是，值域是D2；f1, f2, f3, f4nf1 = 1 false, 2 false nf2 = 1 false, 2 true nf3 = 1 true, 2 false nf4 = 1 true, 2 true n关系：关系： f : n自身自身: f1 ff1 , f2 ff2 .nf fg: 应满足应满足 f(1) f g(1) , f(2) f g(2)，即，即f1 ff2,f1 ff3,f1 ff4,f2 ff4,f3 ff4n最小元：最小元： = f1 2022-6-833论域表达式论域表达式n语法定义语法定义n原始原
27、始域是完全半序集，则论域表达式定义的集合仍然是域是完全半序集，则论域表达式定义的集合仍然是完全半序集。完全半序集。n通常表示论域时就把关系省略掉了。通常表示论域时就把关系省略掉了。2022-6-834 := := | | | | + + | | | | * * | | 论域举例论域举例n形式语义学研究的论域可以是数据域、字符域、布尔域、形式语义学研究的论域可以是数据域、字符域、布尔域、函数域、表域等，其中函数域也称函数空间最为复杂；函数域、表域等，其中函数域也称函数空间最为复杂；n原始域是完全半序集，则论域表达式定义的集合仍然是原始域是完全半序集，则论域表达式定义的集合仍然是完全半序集。完全半
28、序集。n通常表示论域时就把关系省略掉了。通常表示论域时就把关系省略掉了。2022-6-835基本域基本域(原始域原始域)：INT,BOOL,x,y集合域：集合域：a1,an 元组域：元组域：INT BOOL联合域：联合域：BOOL + REAL序列域序列域: (INT BOOL)*函数域函数域(函数空间函数空间)：INT* INT BOOL 总总 结结n知识点：知识点：n基本概念基本概念n完全半序集完全半序集n平坦集平坦集n论域及其构造符论域及其构造符n任何一个集合可以扩展成平坦集，因此任何任何一个集合可以扩展成平坦集，因此任何一个集合可以扩展成一个完全半序集；一个集合可以扩展成一个完全半序集；n论域理解为完全半序集；论域理解为完全半序集；n通过论域构造符定义的仍然是完全半序集；通过论域构造符定义的仍然是完全半序集；n论域用于定义数据类型；论域用于定义数据类型；2022-6-836
