形式语义学 之论域基础课件.ppt

《形式语义学 之论域基础课件.ppt》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、形式语义学FormalSemanticsofProgrammingLanguages2011.09内容回顾形式语义学什么是形式语义学？形式语义学的分类；程序设计语言的基本概念语法和语义不同程序设计范例及其特点命令式语言不同结构的抽象语法定义2021/10/52形式语义学的分类从不同角度研究程序的含义操作语义：用机器模型语言来解释语言语义。即设定一个抽象机，用语言成分在该机器上的执行来解释语言成分的含义。（实现或执行）指称语义：采用形式系统方法，用相应的数学对象对一个语言的语义进行注释。考虑每个语言成分的执行效果(数学对象-指称)；（效果）公理语义：把程序设计语言视为一

2、个数学对象，建立它的公理系统，在此基础上对程序进行推理验证。从而使程序设计语言具有坚实的逻辑基础。（逻辑）代数语义：采用代数的方法进行语义注释的方法。主要基于范畴论、类别代数理论、抽象数据类型；（数据和操作行为）2021/10/53程序设计语言的基本概念词法(lexeme)定义语言所允许的单词的种类及其构成(spelling)标识符，保留字，整数，实数等语法(syntax)定义程序所允许的语法结构(grammar)表达式，语句，声明，函数等语义(semantics)定义语法结构正确的程序的含义(meaning)重复声明，作用域，类型检查等2021/10/54第二章函数

3、式抽象描述方法2.1论域理论基础2.2Lambda演算2.3函数式抽象语言2.4函数式抽象语言的应用2021/10/55第二章函数式抽象描述方法2.1论域理论基础(DomainTheory)2.1.0集合的基本概念2.1.1完全半序集(completepartialorderset,CPO)2.1.2连续函数(continuousfunctions)2.1.3最小不动点(leastfixedpoint)2021/10/56第二章函数式抽象描述方法2.2Lambda演算(calculus)2.2.1Lambda演算介绍表达式自由变量freevariables(FV)

4、替换substitution变换规则conversionrules归约reduction2.2.2Lambda演算作为计算模型2.2.3Lambda演算系统的扩充2021/10/57第二章函数式抽象描述方法2.3函数式抽象语言2.3.1函数式语言概述2.3.2类型及其操作2.3.3无模式表达式2.3.4模式及其模式匹配2.3.5基于模式的纯函数式语言2021/10/582.1.1完全半序集---半序集定义(半序集)设D是一个集合，≼是定义在D上的二元关系，≼满足下面性质：自反性：xD,有x≼x;传递性：x,y,zD,若有x≼y和y≼z，则必有x≼z；反对称性：

5、x,y,zD,若有x≼y和y≼x，则必有x=y；称≼为半序关系(partial_orderrelation),(D，≼)为半序集(partial_orderset)2021/10/59半序集例1D={1，2}，pow(D)是D的所有子集构成的集合，是定义在D上的子集关系，pow(D)={,{1},{2},{1,2}}是pow(D)上的半序关系；(pow(D)，)为半序集；可以用图表示：{1}{2}{1，2}2021/10/510半序集例2数学上的和构成半序关系集合A上的恒等关系IA是A上的半序关系正整数集合上的整除关系也是半序关系和不能构成半序关

6、系半序集的特点是：不要求对于半序集中的任意两个元素都有半序关系，即允许有些元素之间不存在半序关系！若半序集(D,≼)中的任意两个元素之间都存在半序关系，则称(D,≼)为全序集。2021/10/511最小上届上/下界：设(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’的任意一个上界

7、d’,都有d≼d’,则称d为D’的最小上界，并记为D’；最大下界：设d是D’的一个下界，若对D’的任意一个下界d’,都有d’≼d,则称d为D’的最大下界，并记为D’；2021/10/512特殊元素及其性质下界、上界、最大下界、最小上界不一定存在下界、上界存在不一定惟一最大下界、最小上界如果存在，则惟一最小元：设(D,≼)为任意半序集,dD,如果对于任意D中的元素d’都有d≼d’，则称d为D的最小元。集合的最小元就是它的最大下界，最大元就是它的最小上界；反之不对.2021/10/513半序集的特殊元素例3设是偏序集，其中D={a,b,c,d