稳定模糊谓词与谓词转换器

作     者：马艳芳 

作者单位：上海师范大学 

学位级别：硕士

导师姓名：陈仪香

授予年度：2007年

学科分类：07[理学] 070104[理学-应用数学] 0701[理学-数学] 

主      题：拓扑理论 domain理论 模糊谓词 谓词转换器 

摘      要：本文在格上拓扑学的基础上讨论程序设计语言的语义，而格上拓扑学最近的研究方向主要是论域（Domain）理论。Scott开创了论域理论，其目的是给程序语义建立数学模型。论域是一个定向完备偏序集，即dcpo。在dcpo上的所有Scott开集可构造一个拓扑就是Scott拓扑。在程序设计语言语义中，由于形式化侧重面和使用数学工具不同，形式语义学可分为四大类：操作语义学、指称语义学、代数语义学和公理语义学。指称语义学是公认的标准形式语义学，论域是其基础和核心。从而拓扑学的基本概念在研究程序设计语言的指称语义中有极好的应用。 在程序的公理语义学中，一个重要内容就是谓词转换器语义。Hoare的程序逻辑是由三元组{P}S{Q}组成，其中P是前置条件，S是程序，Q是后置条件。Dijkstra在Hoare逻辑基础上首先提出最弱前置条件的概念，并且建立最弱谓词转换器，这个谓词转换器给程序语言提供了一个语义模型。后来，研究学者为了给带有概率选择的程序提供语义模型，提出概率谓词转换器。而为了解决现实世界中的不确定和不精确现象，陈仪香和Jung引入模糊谓词概念，提出并讨论了模糊谓词转换器理论。同时为了讨论模糊谓词转换器与概率谓词转换器之间的关系，陈仪香和Plotkin提出并讨论了健康模糊谓词转换器。 在文章中主要提出一种新的模糊谓词-稳定模糊谓词，它是一个从相容交的dcpoD到[0，1]闭区间的稳定映射，其目的是讨论模糊谓词的稳定性。作者主要证明dcpoD上的所有稳定模糊谓词构成的集合在点式序下构成一个模糊的ξ—半拓扑。举例说明稳定模糊谓词在线性和运算下未必封闭，但一些特殊的稳定模糊谓词具有这个性质。给出稳定模糊谓词的数乘运算仍是稳定模糊谓词的证明。同时证明D上所有相容开集构成的ξ—半拓扑与D上所有稳定模糊谓词构成的模糊ξ—半拓扑是同态的。为了描述程序的语义，建立完全相容稳定模糊谓词转换器，给出她与状态转换器之间的一个保序关系，说明完全相容稳定模糊谓词转换器一定是状态转换器。同时，给出健康模糊谓词转换器的完备性，并且证明健康模糊谓词转换器在线性运算下封闭。