[数学]形式语义学 之论域基础.ppt

形式语义学,Formal Semantics of Programming Languages 2011.09,内容回顾,形式语义学 什么是形式语义学？ 形式语义学的分类； 程序设计语言的基本概念 语法和语义 不同程序设计范例及其特点 命令式语言不同结构的抽象语法定义,2019/1/15,2,形式语义学的分类,从不同角度研究程序的含义 操作语义：用机器模型语言来解释语言语义即设定一个抽象机，用语言成分在该机器上的执行来解释语言成分的含义实现 或 执行） 指称语义：采用形式系统方法，用相应的数学对象对一个语言的语义进行注释考虑每个语言成分的执行效果(数学对象-指称)；（效果） 公理语义：把程序设计语言视为一个数学对象，建立它的公理系统，在此基础上对程序进行推理验证从而使程序设计语言具有坚实的逻辑基础逻辑） 代数语义：采用代数的方法进行语义注释的方法主要基于范畴论、类别代数理论、抽象数据类型；（数据和操作行为）,2019/1/15,3,程序设计语言的基本概念,词法(lexeme) 定义语言所允许的单词的种类及其构成(spelling) 标识符，保留字，整数，实数等 语法(syntax) 定义程序所允许的语法结构(grammar) 表达式，语句，声明，函数等 语义(semantics) 定义语法结构正确的程序的含义(meaning) 重复声明，作用域，类型检查等,2019/1/15,4,第二章 函数式抽象描述方法,2.1 论域理论基础 2.2 Lambda演算 2.3 函数式抽象语言 2.4 函数式抽象语言的应用,2019/1/15,5,第二章 函数式抽象描述方法,2.1 论域理论基础(Domain Theory) 2.1.0 集合的基本概念 2.1.1 完全半序集 (complete partial order set, CPO) 2.1.2 连续函数(continuous functions) 2.1.3 最小不动点(least fixed point),2019/1/15,6,第二章 函数式抽象描述方法,2.2 Lambda演算( calculus) 2.2.1 Lambda演算介绍 表达式 自由变量 free variables(FV) 替换 substitution 变换规则 conversion rules 归约 reduction 2.2.2 Lambda演算作为计算模型 2.2.3 Lambda演算系统的扩充,2019/1/15,7,第二章 函数式抽象描述方法,2.3 函数式抽象语言 2.3.1 函数式语言概述 2.3.2 类型及其操作 2.3.3 无模式表达式 2.3.4 模式及其模式匹配 2.3.5 基于模式的纯函数式语言,2019/1/15,8,2.1.1 完全半序集---半序集,定义 (半序集) 设D是一个集合，≼是定义在D上的二元关系，≼满足下面性质： 自反性：x  D, 有x≼x; 传递性：x ,y,z D, 若有x≼y和y ≼z，则必有x≼z； 反对称性：x ,y,z D, 若有x≼y和y ≼x，则必有x=y； 称≼为半序 关系(partial_order relation), (D，≼)为半序集(partial_order set),2019/1/15,9,半序集,例1 D = {1，2}，pow(D)是D的所有子集构成的集合，是定义在D上的子集关系， pow(D)={, {1},{2},{1,2}} 是pow(D)上的半序关系； (pow(D) ， )为半序集； 可以用图表示：,2019/1/15,10,,,,,半序集,例2 数学上的和构成半序关系 集合A上的恒等关系 IA 是A上的半序关系 正整数集合上的整除关系也是半序关系 和不能构成半序关系,2019/1/15,11,半序集的特点是：不要求对于半序集中的任意两个元素都有半序关系，即允许有些元素之间不存在半序关系！ 若半序集(D, ≼)中的任意两个元素之间都存在半序关系，则称(D, ≼)为全序集。

最小上届,上/下界：设(D, ≼)为任意半序集，而且D’D, dD,则子集D’的上界和下界的定义如下： 上界：若对任意d’D’, 都有d’ ≼ d, 则称d为D’的上界； 下界：若对任意d’D’, 都有d ≼ d’, 则称d为D’的下界； 最小上界/最大下界：设(D, ≼)为任意半序集，而且D’D,则子集D’的最小上界和最大下界的定义如下： 最小上界：设d是D’的一个上界，若对D’的任意一个上界d’, 都有d ≼ d’, 则称d为D’的最小上界，并记为 D’； 最大下界：设d是D’的一个下界，若对D’的任意一个下界d’, 都有 d’ ≼ d, 则称d为D’的最大下界，并记为 D’；,2019/1/15,12,,特殊元素及其性质,下界、上界、最大下界、最小上界不一定存在 下界、上界存在不一定惟一 最大下界、最小上界如果存在，则惟一 最小元：设(D, ≼)为任意半序集, dD, 如果对于任意D中的元素d’都有d ≼ d’ ，则称d为D的最小元 集合的最小元就是它的最大下界，最大元就是它的最小上界；反之不对.,2019/1/15,13,,半序集的特殊元素,例3 设是偏序集，其中 D ={a, b, c, d, e, f, g, h}, ≼={,, , , ,,,,}∪ID 设 A＝{b,c,d}, 求 A 的下界、上界、最大下界、最小上界.,2019/1/15,14,A的下界和最大下界都不存在， A也没有最小元 上界有d 和 f, 最小上界为 d.,链，递增链，递减链,定义 链 设为任意半序集, 是D上的一个序列，简记为{Xi}, 则递增链和递减链定义如下： 递增链：若对任意i都有Xi ≼ Xi+1 ，则称序列{Xi}为递增链； 递减链：若对任意i都有Xi+1 ≼ Xi ，则称序列{Xi}为递减链； 链的最小上届记为：{Xi}或 iXi 或 Xi,2019/1/15,15,2.1.1 完全半序集,定义 完全半序集(complete partial order set, CPO) 设为一个半序集, 若满足下面两个条件，则称为完全半序集： D有最小元； 对于D的任一递增链 {Xi}都有最小上届 {Xi}。

2019/1/15,16,2.1.1 完全半序集,例4 完全半序集 如果D是任意有穷整数集，是定义在D上的小于等于关系，则(D, ) 为完全半序集； 有最小元的有穷半序集是完全半序集； 如果D表示开区间(a, b)，其中a和b是实数，则(D, ) 不是完全半序集；,2019/1/15,17,2.1.1 完全半序集,为什么引入完全半序集？ 在形式地描述程序设计语言的语义时(指称语义方法)，要求所考虑的集合都满足完全半序集的条件； 建立论域的数学模型：满足一定条件的定义了关系的集合(完全半序集)； 如何构造完全半序集？ 平坦集一定是完全半序集 扩展任意集合为平坦集的方法非常简单,2019/1/15,18,平坦集,定义 平坦集 设为一个半序集, 若满足下面两个条件，则称为平坦半序集(平坦集)： D有最小元； 只有下面的关系(平坦关系)：  ≼ ， ≼ d，d ≼d, 其中d是D中非的元素2019/1/15,19,,,,平坦集,扩展任意一个集合为平坦集的方法 任意一个集合D; 引进一个最小元D； 在集合D’ = D  {D}上定义平坦关系≼ ： D ≼ D ， D ≼ d，d ≼d ； 为一个平坦集，简记为D ；,2019/1/15,20,性质：平坦集一定是完全半序集。

平坦集的例子,例5 D = {{1}, {1,2}, {1,3}},关系是集合包含关系，则(D, )是一个平坦集；其中最小元是{1}; BOOL = {true, false},可以扩充为平坦集： 引入最小元； 定义一个平坦关系≼ ：  ≼  ,  ≼ true,  ≼ false, true ≼ true, false ≼ false； 则(BOOL , ≼)是平坦集,2019/1/15,21,论域问题引子,试编制一个程序实现下面有限自动机的功能2019/1/15,22,,,,,,,,,,,X,B,A,1,0,0,0,1,1,state = ‘X’; readone(ch); while ch’#’ do if ch = ‘1’ then out(state) else if state = ‘X’ then state = ‘A’ else if state = ‘A’ then state = ‘B’ else if state = ‘B’ then state = ‘A’ else skip fi fi fi;fi; readone(ch); od,2019/1/15,23,,,,,,,,,X,B,A,1,0,0,0,1,1,,,可将程序看作是一个函数， 函数：定义域 值域 即输入到输出的映射。

程序的编者主观上认定输入域是 {0，1，#}，其实还可以输入其它字符显然，一个正确的程序设计必须给出 在输入不是集合{0，1，#}中的一个元素时，应指出是“无定义” 的错误处理 ----论域做大了,论域,引入目的： 描述类型的数学模型； 指称语义学和函数式语言中都要用到 Scott论域及其构造,2019/1/15,24,Scott论域及其构造,论域(Domain)： 定义了关系的,满足一定条件的集合(CPO)； 论域分为原始域和非原始域(构造域) 原始域：有限集或可枚举集都是原始域 {true,false}, {…,-1,0,1,…}  非原始域：可以从已知论域，应用论域构造符进行构造2019/1/15,25,可以证明，如果每个成分是完全半序集，则保证构造符作用后得到的仍然是完全半序集.,论域构造符,设(Di, ≼ i )是完全半序集, i = 1, …,n, 则我们定义了如下论域构造符：,+, *和，通过它们的作用可以得到新的论域； (1)元组域(乘积域或卡氏域) (D1… Dn , ≼)定义如下: D1… Dn = {(d1, … , dn) | diDi , i=1, …,n}； 关系≼ ：(d1,…, dn) ≼ (d1’, … , dn ’)当且仅当di ≼ i di’， i=1, …,n； 称为n元组域，简记为[D1… Dn ]或D1… Dn 最小元：(D1，… ， Dn ) 对应没有域名的结构类型(struct),2019/1/15,26,元组域的例子,例6：{1，2}  BOOL D1 = {1，2}，1 ≼ 1，1 ≼2，2 ≼2 (整数上的) D2 = BOOL，false ≼b false，false ≼b true，true ≼b true 集合：D = {(1,true),(1,false),(2,true),(2,false)} 关系： ≼x : 自身: (1,true) ≼x (1,true) ,…. (1,false) ≼x(1,true), (2,false) ≼x (2,true) (1,true) ≼x (2,true), (1,false) ≼x(2,false) (1,false) ≼x (2,true) 最小元： (1,false),2019/1/15,27,论域构造符,(2)联合域 (D1… Dn , ≼)定义如下: D1  …  Dn = {(j,dj) | djDj , j=1, …,n}  {}； 关系≼ ：  ≼ ;  ≼(j,dj); (i,di) ≼(j,dj)当且仅当i = j 而且 di ≼ i dj ， i(j)=1, …,n； 简记为 [D1  …  Dn ］或D1  …  Dn 最小元： 对应联合类型(union),2019/1/15,28,联合域的例子,例7：{1，2}  BOOL D1 = {1，。