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

形式语义学 FormalSemanticsofProgrammingLanguages2011 09 内容回顾 形式语义学什么是形式语义学 形式语义学的分类 程序设计语言的基本概念语法和语义不同程序设计范例及其特点命令式语言不同结构的抽象语法定义 2020 3 26 2 形式语义学的分类 从不同角度研究程序的含义操作语义 用机器模型语言来解释语言语义 即设定一个抽象机 用语言成分在该机器上的执行来解释语言成分的含义 实现或执行 指称语义 采用形式系统方法 用相应的数学对象对一个语言的语义进行注释 考虑每个语言成分的执行效果 数学对象 指称 效果 公理语义 把程序设计语言视为一个数学对象 建立它的公理系统 在此基础上对程序进行推理验证 从而使程序设计语言具有坚实的逻辑基础 逻辑 代数语义 采用代数的方法进行语义注释的方法 主要基于范畴论 类别代数理论 抽象数据类型 数据和操作行为 2020 3 26 3 程序设计语言的基本概念 词法 lexeme 定义语言所允许的单词的种类及其构成 spelling 标识符 保留字 整数 实数等语法 syntax 定义程序所允许的语法结构 grammar 表达式 语句 声明 函数等语义 semantics 定义语法结构正确的程序的含义 meaning 重复声明 作用域 类型检查等 2020 3 26 4 第二章函数式抽象描述方法 2 1论域理论基础2 2Lambda演算2 3函数式抽象语言2 4函数式抽象语言的应用 2020 3 26 5 第二章函数式抽象描述方法 2 1论域理论基础 DomainTheory 2 1 0集合的基本概念2 1 1完全半序集 completepartialorderset CPO 2 1 2连续函数 continuousfunctions 2 1 3最小不动点 leastfixedpoint 2020 3 26 6 第二章函数式抽象描述方法 2 2Lambda演算 calculus 2 2 1Lambda演算介绍 表达式自由变量freevariables FV 替换substitution变换规则conversionrules归约reduction2 2 2Lambda演算作为计算模型2 2 3Lambda演算系统的扩充 2020 3 26 7 第二章函数式抽象描述方法 2 3函数式抽象语言2 3 1函数式语言概述2 3 2类型及其操作2 3 3无模式表达式2 3 4模式及其模式匹配2 3 5基于模式的纯函数式语言 2020 3 26 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 orderrelation D 为半序集 partial orderset 2020 3 26 9 半序集 例1D 1 2 pow D 是D的所有子集构成的集合 是定义在D上的子集关系 pow D 1 2 1 2 是pow D 上的半序关系 pow D 为半序集 可以用图表示 2020 3 26 10 半序集 例2数学上的 和 构成半序关系集合A上的恒等关系IA是A上的半序关系正整数集合上的整除关系也是半序关系 和 不能构成半序关系 2020 3 26 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 2020 3 26 12 特殊元素及其性质 下界 上界 最大下界 最小上界不一定存在下界 上界存在不一定惟一最大下界 最小上界如果存在 则惟一最小元 设 D 为任意半序集 d D 如果对于任意D中的元素d 都有d d 则称d为D的最小元 集合的最小元就是它的最大下界 最大元就是它的最小上界 反之不对 2020 3 26 13 半序集的特殊元素 例3设是偏序集 其中D a b c d e f g h ID设A b c d 求A的下界 上界 最大下界 最小上界 2020 3 26 14 A的下界和最大下界都不存在 A也没有最小元上界有d和f 最小上界为d 链 递增链 递减链 定义链设为任意半序集 是D上的一个序列 简记为 Xi 则递增链和递减链定义如下 递增链 若对任意i都有Xi Xi 1 则称序列 Xi 为递增链 递减链 若对任意i都有Xi 1 Xi 则称序列 Xi 为递减链 链的最小上届记为 Xi 或iXi或Xi 2020 3 26 15 2 1 1完全半序集 定义完全半序集 completepartialorderset CPO 设为一个半序集 若满足下面两个条件 则称为完全半序集 D有最小元 对于D的任一递增链 Xi 都有最小上届 Xi 2020 3 26 16 2 1 1完全半序集 例4完全半序集如果D是任意有穷整数集 是定义在D上的小于等于关系 则 D 为完全半序集 有最小元的有穷半序集是完全半序集 如果D表示开区间 a b 其中a和b是实数 则 D 不是完全半序集 2020 3 26 17 2 1 1完全半序集 为什么引入完全半序集 在形式地描述程序设计语言的语义时 指称语义方法 要求所考虑的集合都满足完全半序集的条件 建立论域的数学模型 满足一定条件的定义了关系的集合 完全半序集 如何构造完全半序集 平坦集一定是完全半序集扩展任意集合为平坦集的方法非常简单 2020 3 26 18 平坦集 定义平坦集设为一个半序集 若满足下面两个条件 则称为平坦半序集 平坦集 D有最小元 只有下面的关系 平坦关系 d d d 其中d是D中非 的元素 2020 3 26 19 平坦集 扩展任意一个集合为平坦集的方法任意一个集合D 引进一个最小元 D 在集合D D D 上定义平坦关系 D D D d d d 为一个平坦集 简记为D 2020 3 26 20 性质 平坦集一定是完全半序集 平坦集的例子 例5D 1 1 2 1 3 关系是集合包含关系 则 D 是一个平坦集 其中最小元是 1 BOOL true false 可以扩充为平坦集 引入最小元 定义一个平坦关系 true false true true false false 则 BOOL 是平坦集 2020 3 26 21 论域问题引子 试编制一个程序实现下面有限自动机的功能 2020 3 26 22 X B A 1 0 0 0 1 1 state X readone ch whilech doifch 1 thenout state elseifstate X thenstate A elseifstate A thenstate B elseifstate B thenstate A elseskipfififi fi readone ch od 2020 3 26 23 X B A 1 0 0 0 1 1 可将程序看作是一个函数 函数 定义域 值域即输入到输出的映射 程序的编者主观上认定输入域是 0 1 其实还可以输入其它字符 显然 一个正确的程序设计必须给出在输入不是集合 0 1 中的一个元素时 应指出是 无定义 的错误处理 论域做大了 论域 引入目的 描述类型的数学模型 指称语义学和函数式语言中都要用到 Scott论域及其构造 2020 3 26 24 Scott论域及其构造 论域 Domain 定义了关系的 满足一定条件的集合 CPO 论域分为原始域和非原始域 构造域 原始域 有限集或可枚举集都是原始域 true false 1 0 1 非原始域 可以从已知论域 应用论域构造符进行构造 2020 3 26 25 可以证明 如果每个成分是完全半序集 则保证构造符作用后得到的仍然是完全半序集 论域构造符 设 Di i 是完全半序集 i 1 n 则我们定义了如下论域构造符 和 通过它们的作用可以得到新的论域 1 元组域 乘积域或卡氏域 D1 Dn 定义如下 D1 Dn d1 dn di Di i 1 n 关系 d1 dn d1 dn 当且仅当di idi i 1 n 称为n元组域 简记为 D1 Dn 或D1 Dn最小元 D1 Dn 对应没有域名的结构类型 struct 2020 3 26 26 元组域的例子 例6 1 2 BOOLD1 1 2 1 1 1 2 2 2 整数上的 D2 BOOL false bfalse false btrue true btrue集合 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 2020 3 26 27 论域构造符 2 联合域 D1 Dn 定义如下 D1 Dn j dj dj Dj j 1 n 关系 j dj i di j dj 当且仅当i j而且di idj i j 1 n 简记为 D1 Dn 或D1 Dn最小元 对应联合类型 union 2020 3 26 28 联合域的例子 例7 1 2 BOOLD1 1 2 1 1 1 2 2 2 整数上的 D2 BOOL false bfalse false btrue true btrue集合 D 1 1 1 2 2 true 2 false 关系 自身 1 1 1 1 1 1 1 2 2 false 2 true i 1 1 1 2 2 true 2 false 最小元 2020 3 26 29 论域构造符 3 序列域 D 定义如下 D di Di n 0 i 1 2 关系 当且仅当n m而且di idi i 1 n 简记为D 最小元 对应表类型 2020 3 26 30 序列域的例子 例8 1 2 D1 1 2 1 1 1 2 2 2 整数上的 集合 D 关系 自身 元素个数相同的序列之间满足条件的关系有 最小元 2020 3 26 31 论域构造符 4 函数空间 D D 定义如下 D D f d D f d d D 关系 对于任意f h D D f h 当且仅当 d D f d D h d 简记为 D D 或D D 最小元 d D d D 2020 3 26 32 函数域的例子 例9 1 2 BOOLD1 1 2 1 1 1 2 2 2 整数上的 D2 BOOL false bfalse false btrue true btrue集合 函数的集合 其中每个函数的定义域是D1 值域是D2 f1 f2 f3 f4 f1 1 false 2 false f2 1 false 2 true f3 1 true 2 false f4 1 true 2 true 关系 f 自身 f1 ff1 f2 ff2 f fg 应满足f 1 fg 1 f 2 fg 2 即f1 ff2 f1 ff3 f1 ff4 f2 ff4 f3 ff4最小元 f1 2020 3 26 33 论域表达式 语法定义原始域是完全半序集 则论域表达式定义的集合仍然是完全半序集 通常表示论域时就把关系省略掉了 2020 3 26 34 论域举例 形式语义学研究的论域可以是数据域 字符域 布尔域 函数域 表域等 其中函数域也称函数空间最为复杂 原