（基础数学专业论文）稳定模糊谓词与谓词转换器.pdf

摘要 本文在格上拓扑学的基础上讨论程序设计语言的语义，而格上拓扑学最近的研究 方向主要是论域( d o m a i n ) 理论s c o t t 开创了论域理论，其目的是给程序语义建 立数学模型论域是一个定向完备偏序集，即d c p o 在d c p o 上的所有s c o t t 开集可 构造一个拓扑就是s c o t t 拓扑在程序设计语言语义中，由于形式化侧重面和使用数 学工具不同，形式语义学可分为四大类；操作语义学，指称语义学、代数语义学和公 理语义学指称语义学是公认的标准形式语义学，论域是其基础和核心从而拓扑学 的基本概念在研究程序设计语言的指称语义中有极好的应用 在程序的公理语义学中，一个重要内容就是谓词转换器语义h o a r e 的程序逻辑 是由三元组 p 剐q ) 组成，其中p 是前置条件，s 是程序，q 是后置条件d i j k s t r a 在h o a r e 逻辑基础上首先提出最弱前置条件的概念，并且建立最弱谓词转换器，这 个谓词转换器给程序语言提供了一个语义模型后来，研究学者为了给带有概率选择 的程序提供语义模型，提出概率谓词转换器而为了解决现实世界中的不确定和不精 确现象，陈仪香和j u n g 引入模糊谓词概念，提出并i - t 论了模糊谓词转换器理论同 时为了讨论模糊谓词转换器与概率谓词转换器之间的关系，陈仪香和p l o t k i n 提出并 讨论了健康模糊谓词转换器 在文章中主要提出一种新的模糊谓词一稳定模糊谓词，它是个从相容交的d c p o d 到【o ，1 】闭区间的稳定映射，其目的是讨论模糊谓词的稳定性作者主要证明d c p o d 上的所有稳定模糊谓词构成的集合在点式序下构成一个模糊的一半拓扑举例 说明稳定模糊谓词在线性和运算下未必封闭，但一些特殊的稳定模糊谓词具有这个性 质给出稳定模糊谓词的数乘运算仍是稳定模糊谓词的证明同时证明d 上所有相容 开集构成的f 一半拓扑与d 上所有稳定模糊谓词构成的模糊f 一半拓扑是同态的为 了描述程序的语义，建立完全相容稳定模糊谓词转换器，给出她与状态转换器之间的 个保序关系，说明完全相容稳定模糊谓词转换器一定是状态转换器同时，给出健 康模糊谓词转换器的完备性，并且证明健康模糊谓词转换器在线性运算下封闭 关键词：拓扑理论，d o m a i n 理论，模糊谓词，谓词转换器 a b s t r a c t t h i sp a p e ri st od i s c u s st h ep r o g r a md e s i g n i n gs e m a n t i co nt h eb a s eo ft h el a t t i c e t o p o l o g y a n dt h em a i nr e s e a r c hc o n t e n ti st h ed o m a i nt h e o r y s c o t tf i r s ti n i t i a t e st h e d o m a i nt h e o r y , t h ea i mi st op r o v i d eam a t h e m a t i c a lm o d e lf o rt h ep r o g r a ms e m a n - t i c d o m a i ni sad i r e c t e dc o m p l e t ep a r t i a lo r d e rs e t ，c a l l e da sd c p o a l lt h es e to fs c o t t o p e ns e t si s as c o t tt o p o l o g y b e c a u s eo ft h ed i f f e r e n te m p h a s i t i o n sa n dt h em a t h e - m a t i c a lt o o l sw h e nw er e s e a r c ht h ep r o g r a md e s i g n i n gl a n g u a g e s ，t h ef o r m a ls e m a n t i c s c a nb ed i v i d e di n t of o u rc l a s s e s ：o p e r a t i o n a ls e m a n t i c s ；d e n o t a t i o n a ls e m a n t i c s ；a l g e - b f a ls e m a n t i c sa n da x i o m a ls e m a n t i c s t h ed e n o t a t i o n a ls e m a n t i c si st h i n k e do fa s t h ec r i t e r i as e m a n t i c d o m a i ni st h eb a s ea n dc o r eo fd e n o t a t i o n a ls e m a n t i c s a n d ，t h e t o p o l o g yk n o w l e g c sh a v eb e e nu s e di nt h ep r o g r a ms e m a n t i c s p r e d i c a t et r a n s f o r m e rs e m a n t i ci sa ni m p o r t a n tc o n t e n ti nt h ea x i o m a ls e m a n t i c s t h eh o a r ek s i ci st h et r i p l e p ) s q ) ，pi st h ep r e c o n d i t i o n ，si st h ep r o g r a m ，q i st h ep o s t - c o n d i t i o n o nt h eb a s eo fh o a r el o g i c ，d i j k s t r af i r s ti n t r u d u e e st h ed e f t - n a t i o no ft h ew e a k e s tp r e c o n d i t i o na n dp r e s e n t e st h ep r e d i c a t et r a n s f o r m e r s ，c a l l e da s t h ew e a k e s tp r e d i c a t et r a n s f o r m e r s ，d e f i n e da sw p ，w h i c hm a p sap o s t c o n d i t i o nt ot h e w e a k e s tp r e c o n d i t i o n s o ，t h i sp r e d i c a t et r a n s f o r m e rp r o v i d eas e m a n t i c a lm o d e lf o r p r o g r a ml a n g u a g e l a t e r ，i no r d e rt op r o v i d eas e m a n t i c a lm o d e lf o rt h ep r o g r a mw i t h p r o b a b i l i t yc h o i c e ，m a n yr e s e a r c h e r sr e s e a r c ht h ep r o b a b i l i s t i cp r e d i c a t et r a n s f o r m e r s t h e ni no r d e rt oa c c o u n tf o rm a n yn o n - d e t e r m i n a t o na n dd i s p r e m i s ep h e n o m e n o n si n r e a lw o r l d ，p r o f e s s e rc h e ny i x i a n ga n dp r o f e s s e rj u n gc o m b i n e st h ez a d e h 8f u z z ys e t t h e o r yw i t ht h es c o t td o m a i n ，i n t r u d u c i n gt h ef u z z yp r e d i c a t ew h i c hi sa s c o t tc o n t i n u e f u n c t i o nf r o mad o m a i n ( d c p o ) t ot h eu n i ti n t e r v a l 【0 ，1 】a n dt h ef u z z yp r e d i c a t et r a n s - f o r m e r s a tt h es a m et i m e ，p r o f e s s e rc h e ny i ) c i a n ga n dp r o f c s s e rp l o t k i np r e s e n t st h e h e a l t h yf u z z yp r e d i c a t et r a n s f o r m e r si no r d e rt os h o wt h er e l a t i o nb e t w e e nt h ef u z z y p r d e c a t et r a n s f o r m e r sa n d t h ep r o b a b i l i t yp r e d i c a t et r a n s f o r m e r s i nr e n c e n t l yr e s e a r c h ，f u z z yp r e d i c a t et r a n s f o r m e rc a np r o v i d et h ef u z z yl o g i cs e n m a n t i cf o rt h ep r o b a b i l i s t e c o m p u t a t i o n i nt h i sp a p e r ，t h ea u t h o rw i l lp r e s e n tan e wf u z z yp r e d i c a t e ，c a l l e da st h es t a b l e f u z z yp r e d i c a t eo nt h eb a s eo ft h ef u z z yp r e d i c a t e ，w h i c hi sas t a b l ef u n c t i o nf r o md c p o i i i i v 2 0 0 7 上海师范大学硕士学位论文 dw i t ht h ec o n s i s t e n tm e e t si n t ot h eu n i ti n t e r v a l 【0 ，l 】t h ea i mi st od i s c u s st h e s t a b l ep r o p e r t yo ff u z z yp r e d i c a t e i nt h i sp a p e r ，t h ea u t h o rm a l n l yw i l lp r o v et h es e t o fa l ls t a b l ef u z z yp r e d i c a t e so nd c p odi saf u z z y 一s e m i t o p o l o g yo nt h ep o i n t w i s e o r d e r t h ea u t h o rw i l lg i v ea ne x a m p l et os h o wt h el i n e a ra d do f s t a b l ef u z z yp r e d i c a t e s u n n e c e s s a r i l yi st h es t a b l e ，b u ts o m es p e c i a ls t a b l ef u z z yp r e d i c a t e so w nt h i sp r o p e r t y a tt h es a m et i m e ，t h ea u t h o rp r o v et h ep r o d u c to fan u m b e ri nt h eu n i ti n t e r v a l 【o ，1 】 a n das t a b l ef u z z yp r e d i c a t ei ss t a b l e a l s o ，t h ea u t h o rs h o wt h es e to fa l lt h ec o n s i s t e n t o p e ns e t so nda n dt h es e to fa l lt h es t a b lf u z z yp r e d i c a t e si sh o m o m o r p h i c t h e n i no r d e rt od e p i c tt h es e m a n t i c ，t h ea u t h o rw i l ls e tu pt h ec o m p l e t ec o n s i s t e n ts t a b l e f u z z yp r e d i c a t et r a n s f o r m e r s ，s h o w i n gt h er e l a t i o nw i t ht h es t a t et r a n s f o r m e r s a tt h e s a i n et i m e t h ea u t h o ri sg o i n gt op r o v et h eh e a l t h yf u z z yp r e d i c a t et r a n s f o r m e r si sa c p oo nt h ep o i n t w i s eo r d e ra n dt h el i n e a rp r o p e r t i e s k e y w o r d s ：t o p o l o g yt h e o r y , d o m a i nt h e o r y ，f u z z yp r e d i c a t e ，p r e d i c a t et r a n s - 论文独创性声明 本论文是我个人在导师指导下进行的研究工作及取得的研究 成果。论文中除了特别加以标注和致谢的地方外，不包含其他人 或机构已经发表或撰写过的研究成果。其他同志对本研究的启发 和所做的贡献均已在论文中做了明确的声明并表示了谢意。 作者签名：马端日期：伽7 论文使用授权声明 本人完全了解上海师范大学有关保留、使用学位论文的规定， 即：学校有权保留送交论文的复印件，允许论文被查阅和借阅； 学校可以公布论文的全部或部分内容，可以采用影印、缩印或其 它手段保存论文。保密的论文在解密后遵守此规定。 作者签名：马描劳导师签名： 期：加五s 2 斗 第一章引言 1 第一章引言 格上拓扑学从序的角度来说是格，而从拓扑的方面来讲则是拓扑空间格上拓扑 学最近的研究方向主要是论域理论( d o m a i n ) d a n as c o t t 1 ，2 ，3 】为了给程序语言 提供语义数学模型提出了论域的概念，并且已经广泛地被数学家和计算机科学家研究 4 ，5 】论域是个定向完备偏序集，即d c p o 而d c p o 上的所有s c o t t 开集构成个拓 扑，称为s c o t t 拓扑程序设计语言是人类用来和计算机系统进行通信，并控制其工作 的人工语言作为语言，人工语言和自然语言一样，有其语法，语义和语用的范畴程 序设计语言的语法是指程序的组成规则；语义是指程序的含义；语用的所指，说法不 一，大致包括程序的使用效果形式语义学是研究程序设计语言语义的学问她以数 学为工具，运用符号和公式，严格地解释程序设计语言的语义，使语义形式化由于形 式化中侧重面和使用的数学工具不同，形式语义学可分为四大类：操作语义学、指称 语义学、代数语义学和公理语义学指称语义学是公认的标准形式语义学，论域理论 是指称语义学的基础和核心从而拓扑学的基本概念在研究程序设计语言的指称语义 中有极好的应用人们可以把拓扑空间认为数据类型，空间中的点认为计算过程( 程 序) ，开集认为规范( 性质) ，z o 认为程序z 具有规范o ，谓词认为空间x 到布尔 代数 o ，1 ) 保结构的算子若在 o ，1 上引入适当的拓扑结构，则他是某种连续型映 射，并且s x 是开集当且仅当有连续映射( 谓词) p ：x 一 o ，1 ) 使得s = p - 1 ( 1 ) 因此我们可以认为谓词与开集是等同的这种观点在理解程序设计语言指称语义和程 序逻辑的关系时特别有用 抽象地看，程序可看作是一个状态转换器一将一个状态映射成另一个状态，而状 态域上的条件反映了程序变元应具有的性质这个条件从内涵角度来看则为谓词，从 外延角度则是状态域上的子集因此状态域上具有什么特点的子集才是谓词的外延集 合一直是人们所关注的，同时状态域具有什么结构也是人们关注的p l o t k i n 6 ，7 】选 用的状态域是平坦集合，而谓词是状态域的任意子集，使用s m y t h 8 ，9 1 域，得到了不 确定状态转换器与健康谓词转换器的相互确定关系s m y t h 将p l o t k i n 的状态域推广 到了一般的论域，谓词是论域上的s c o t t 1 0 开集，程序是论域间的s c o t t 连续映射 陈仪香【1 l 】选用了稳定论域为状态域，谓词是其上的相容开集，程序是稳定映射及其 扩展从而在一定意义上来讲一个状态转换器是个谓词转换器 2 稳定模糊谓词与谓词转换器 谓词转换器语义是程序设计语言语义中公理语义学的一个重要的内容把程序看 作成一台机器，谓词看成这台机器在工作前后应满足的条件工作前满足的条件称为 前置条件，在纯h o a r e 1 2 】逻辑中，这种条件的基本公式为 p ) s r ，p 是前置条件， s 是机器，r 是后继条件，其中p 是充分条件，他保证了当s 执行完毕后，有后继条 件兄成立d i j k s t r a 1 3 推进了一步，要求p 是充要的，提出了最弱前置条件的概念， 并且建立了谓词转换器，称为最弱谓词转换器，记为w p 它把个后置条件映射为最 弱前置条件，这个最弱前置条件是由程序和后置条件共同决定的，由此，这个谓词转 换器给程序语言提供了一个语义模型后来，有很多研究学者研究最弱谓词转换器， 如h o a r e ，m o r r i s ，p l o t l 【i n ，s m y t h 等在他们的研究中谓词是从状态空间s 到 o ，1 的映射，称为布尔谓诃在1 9 8 1 年的时候，k o z e n 1 4 ，1 5 1 提出了概率谓词的概念， 而后人们开始研究概率谓词转换器，如h e e t a l 1 6 ，j o n e s 1 7 ，m c l v e r 1 8 ，m o r g a n 1 9 ， 仫 2 0 】，y i n g 2 1 】等在他们的工作中谓词是从状态空间s 到【0 ，1 】( 或j 矿) 的映 射研究概率谓词转换器的目的是为了给带有概率选择的程序提供语义模型然而， 在现实世界中有很多不确定和不精确现象并不能完全用概率来刻画，如。年轻”和“年 老”正是基于这样的考虑，z a d e h 【2 2 】提出了模糊集合的概念，其目的在于将这些不 确定和不精确现象进行数学精确的表达近来，陈仪香和j u n g 【2 3 1 将z a d e h 的模糊集 理论和s c o t t 2 4 的论域理论有机结合起来，引入模糊谓词概念，它是论域( d c p o ) 到 o ，1 的s c o t t 连续映射，在此基础上提出并讨论了模糊谓词转换器理论最近研究表 明，模糊谓词转换器可用来建立概率计算的模糊逻辑语义【2 5 】 本文在格上拓扑学和模糊谓词理论的基础上来进一步讨论了程序设计语言语义中 谓词转换器语义，提出一种新的模糊谓词一稳定模糊谓词它是一个从相容交的d c p o d 到f 0 ，1 1 的稳定映射，其目的是讨论模糊谓词的稳定性在文章中，主要证明相容交 的d c p o 上的所有稳定模糊谓词构成的集合在点式序下构成一个模糊的一半拓扑 举例说明稳定模糊谓词在线性和运算下未必是封闭的，但一些特殊的稳定模糊谓词具 有这个性质同时还将证明稳定模糊谓词的数乘运算仍是稳定模糊谓诃证明d 上所 有相容开集构成的f 一半拓扑与d 上的所有稳定模糊谓词构成的模糊f 一半拓扑是同 态的为了描述程序的语义，建立完全相容稳定模糊谓词转换器，并且给出她与状态 转换器之间的一个保序关系说明一个完全相容稳定模糊谓词转换器一定是状态转换 器同时，还进一步给出健康模糊谓词转换器的完备性，即所有健康模糊谓词转换器 构成的集合在点式序下构成一个完备偏序集并且证明健康模糊谓词转换器在线性运 第一章引言 3 算下是封闭的 第一章中主要介绍本文的背景和重要性第二章介绍本文所需要的一些基本的论 域和谓词转换器的基本知识，如d c p o ，s c o t t 开集，s c o t t 拓扑，s c o t t 连续，稳定映 射，模糊谓词，模糊谓词转换器，模糊谓词转换器的健康标准等第三章主要给出稳 定模糊谓词的定义，她是一个从相容交的d c p od 到【0 ，1 】的稳定映射，证明d 上 的所有稳定模糊谓词构成的集合在点式序下构成一个模糊的f 一半拓扑；还举例说明 两个稳定模糊谓词的线性和未必是稳定的；给出特殊的稳定模糊谓词满足线性和的运 算；证明稳定模糊谓词的数乘仍然是稳定；证明d 上所有相容开集构成的f 一半拓扑 与d 上的所有稳定模糊谓词构成的模糊f 半拓扑是同态的在第四章中讨论健康模 糊谓词转换器在点式序下构成了一个c p o ，并证明两个健康模糊谓词转换器的线性组 合仍然是健康的第五章建立完全相容稳定模糊谓词转换器，给出她与状态转换器之 间的个保序关系说明一个完全相容稳定模糊谓词转换器是个状态转换器 4 稳定模糊谓词与谓词转换器 第二章预备知识 在这一章中主要回顾本文所需要的一些论域的基本知识，包括；d c p o ，s c o t t 连 续s c o t t 拓扑、稳定映射等，其详细内容可参见文献f 3 2 1 同时还给出谓词理论的一 些基本定义，如，模糊谓词、谓词转换器等 定义2 1 【3 2 】设x 是一集合，若x 上的二元关系满足下面条件，则称二元关 系为偏序关系，简称序关系或偏序，而( x ，) 称为偏序集 自反性；v x ，z z ； 传递性；比，y ，z 咒若z y ，y z ，则z sz 反对称性：妇，y x ，若z y ，y s z ，则z = y 定义2 2 3 2 设a 是偏序集p 的子集，z p ， 若v a a ，a z ，则z 称为a 的上界；对偶地， 若v a a ，z a ，则z 称为a 的下界 符号u b ( a ) ，l b ( a ) 将分别表示a 的所有上界之集和下界之集 定义2 3 【3 2 】设p 是一偏序集， 若口p ，忱p 都有a z 扛o ) ，则称口是最小元( 最大元) 定义2 4 3 2 1 设p 是一偏序集， p 的子集a 称为上集，若z a 且卫sy 则有y a ；对偶地， p 的子集a 称为下集，若z a 且y 则有y a 定义2 5 【3 2 】设p 是偏序集，a 是其子集，则 集合t a = d p iz y ，弘舢是包含a 的最小上集，而符号tz 直接表 示t o ； 集合l a = p iy sz ，弘a 是包办a 的最小下集，而符号iz 直接表 示l 。) 定义2 6 3 2 1 设a 是x 的子集， 若u b ( a ) 有最小元z ，则称是a 的最小上界或并，以后用v a 表示a 的并； 若l b ( a ) 有最大元q 则称z 是a 的最大下界或交，以后用a a 表示a 的并交 定义2 7 【3 2 】带有最小元的偏序集称为p 偏序集 定义2 8 【2 6 设p 是一偏序集，p 的非空子集x 称为定向的( 渗透的) ，若x 的每一对元素在x 中有上界( 下界) 第二章预备知识 5 定义2 9 【3 2 设p 是个偏序集，p 的非空上有界子集称为相容集 定义2 1 0 【2 6 】设x 是一偏序集，若x 的每个定向集都有最小上界( 即并) ，则 称偏序集x 是定向完备偏序集( 简称d c p o ) 定义2 1 1 【3 2 】定向完备的p 偏序集称为完备偏序集，简称c p o 由于拓扑学的基本概念在计算机科学程序设计语言的指称语义中起到重要作用， 下面介绍论域理论中的重要的一类拓扑- s c o t t 拓扑s c o t t 拓扑与s c o t t 连续映射保 持和谐性 定义2 1 2 【2 6 】设d 是完备集，a d ，若a 满足条件： ( 1 ) a 是一上集；且 ( 2 ) 设是d 的任一定向集，若v a ，则有z 使得z a 则称a 是d 的 s c o t t 开集，d 的所有s c o t t 开集构成个拓扑，称为s c o t t 拓扑，记作盯( d ) ( d ，口( d ) ) 称为s c o t t 空间 偏序关系刻画了信息的渐进关系，而计算是一个渐进的具体过程，计算的每一步 使得渐进更趋向目标因此，直观上讲，计算是信息加工过程，而数学上看，计算是 信息域间的映射这个映射从数学意义上来讲应该是连续的，称为s c o t t 连续下面 介绍s c o t t 连续的定义 定义2 1 3 【2 6 设d ，e 是完备偏序集，是d 到e 的映射，若，满足 ( 1 ) 单调的：若z y ，有，( z ) ，( p ) ； ( 2 ) 连续的t 对于d 中的任意定向集都有 f ( v a ) = v ，( ) 则称，是s c o t t 连续函数 一般地，把含有最小元的d c p o 称为论域，在本文中所指的论域均为代数论域，下 面给出代数论域的定义 定义2 1 4f 3 2 设d 是完备偏序集，则 1 d 上的双小于关系定义为；对于任意的x ，y d ，z 暑，当且仅当对于d 的任 意定向集，只要y v a 就有6 使得z sj ； 2 d 的元素z 称为有限元或紧元，若z z 用符号尼( d ) 表示d 的所有有限 元之集符号l l o = 瓦( d ) ：耖sz ) 3 d 称为代数的，若妇d ，舢是定向的，且= v l 【z ； 6 稳定模糊谓词与谓词转换器 4 代数的完备偏序集称为论域 定义2 1 5 【3 2 】设d 是定向完备偏序集，如果比，y 上有界，且z v y 存在，则称 此d c p o 是相容完备的d c p o 定义2 1 6 2 3 1 设d 是一个d c p o ，从d 到【0 ，1 1 闭区间的s c o t t 连续映射称为模 糊谓词在d 上的所有模糊谓词构成的集合记作巧( d ) 由于模糊谓词本身是一个映射，所以自然地存在模糊谓词的序关系如下 p q 当且仅当p ( x ) q ( z ) ，v z d 在这个序关系的基础上可以考虑模糊谓词的交和并 定理2 1 【2 5 】巧( d ) 构成个模糊拓扑，即1 和0 是属于巧( d ) ，且模糊谓词关 于有限交和任意并是封闭的 b e v y 2 7 为了研究p c f 语言的语义模型，引入了稳定映射概念，或者说关注s c o t t 连续映射的稳定性 b e r r y 表明p c f 语言的全抽象论域语义模型中的映射只能是稳 定映射，因此稳定映射是论域理论中一类重要的映射 定义2 1 7 【2 7 】设d ，e 是完备偏序集，：d e 是s c o t t 连续映射，若，满 足忱d ，( z ) ，3 2 ：0 d 使得2 ：0 ，y s ，( 勋) ，并且比z ，只要y s ，( 。) ， 就有蜘，则称，是稳定映射 直观上讲，是稳定映射当且仅当对于任一已知结果y ，( o ) 都有来自的最 小信息如，即局部最小信息，使得它在，作用下达到原已知结果y ，这个最小信息记为 m ( ，。，) ，即m ( f ，z ，y ) 是集合 z d ：一z ，ys ，( z ) ) 的最小元 虽然稳定映射是在完备偏序集上定义的，但在不同的论域上有不同的表现如在 文献【3 2 】中，设d ，e 是相容交的完备偏序集，是d e 是s c o t t 连续映射，则 ，是稳定映射当且仅当，保相容集之交 在文献 3 2 】中把每个相容集都有交的论域称为稳定论域，而在稳定论域上s c o t t 开集的一种特殊的情形是相容开集，下面给出相容开集的定义 定义2 1 8 【3 2 】设d 是相容交的完备偏序集， d 的s c o t t 开集u 称为相容的， 若对于矿的任一非空子集x ，只要x 相容就有 x 矿符号( d ) 表示d 上的所有 相容开集构成的集合 稳定论域上的所有相容开集族关于集合运算不再构成一拓扑，而是一种半拓扑 这种拓扑与稳定映射保持了象s c o t t 拓扑与s c o t t 连续映射一样的和谐性 第二章预备知识 7 程序的公理语义是在程序正确性验证的基础上发展起来的，研究把程序执行的 效果也考虑进去的逻辑系统，程序逻辑是其核心，它是关于程序性质推理的形式系 统，推理过程由一组规则组成，h o a r e 1 2 】逻辑是一个著名的程序逻辑，它是由形如 尸) 科q 的式子组成，其中s 是程序，而p 以及q 是性质，条件，谓词，且表明若 程序s 在输入具有性质p 的状态后终止，则s 输出的状态具有性质q 条件p 称为 前置条件，而条件q 称为后置条件前置条件p 是使程序s 终止且输出的结果满足 后置条件q 的充分条件d i j k s t r a 1 3 在研究带有卫式命令的非确定语言的语义时提 出了最弱前置条件的概念条件尸是最弱前置条件是说，若有另一个谓词一作为前 置条件时也能使程序s 终止，结果满足后置条件q ，则定有p ，强于p 明显地，最弱 前置条件是充要的，且由程序s 以及后置条件q 惟一确定，记作w p ( s ，q ) d i j k s t r a 的基本想法是将程序s 看作谓词转换器，它将每个谓词( 条件) q 转换成最弱前置条 件w p ( sq ) 即有，w p ( 8 一) 是个谓词到谓词的映射另一个方面，抽象地看，程 序又可看作个状态转移映射一将状态映射成状态也即状态转换器是个谓词转 换器，但是一个谓词转换器未必是状态转换器，从而d i j k s t r a 在引入谓词转换器时要 求它具有下列三个条件成立，称为健康条件这样所得到的谓词转换器是可以由计算 机计算的，其健康条件如下 ( w p l ) ( 反常排除律) w p ( s ，f a l s e ) = f a l s e ； ( w p 2 ) ( 单调律) 若q p j 则w p ( s q ) 一w p ( 只p ) ； ( w p 3 ) ( 与分布律) w p ( s ，qar ) = w p ( s ，q ) aw p ( s ，p ) d i j k s t r a 1 3 关于谓词转换器的健康条件中( w p 2 ) 是关于谓词的蕴涵算子，而 ( w p 3 ) 是关于谓词的合取算子，但对于谓词的析取情况变得很复杂 定理2 2 3 2 】对于确定程序s ，有下面的或分布律 ( w p ( s ，q ) v w p ( s ，r ) ) 一w p ( s ，q v r ) 定义2 1 9f 3 2 若谓词p 与兄满足p a r = f a l s e ，则称谓词p 与谓词r 是不 可兼或的，而它们的或称为不可兼或，记作p v 兄 现引入了谓词转换器的相容条件 ( w p 4 ) ( 相容条件) w p ( s ，pvr ) = w p ( sp ) vw p ( 只兄) 定义2 2 0 3 2 】满足相容条件的健康谓词转换器称为相容谓词转换器 陈仪香在文献 3 2 中的稳定论域基础上引入了完全相容谓词转换器的定义 8 稳定模糊谓词与谓词转换器 定义2 2 1 3 2 】设d ，e 是稳定论域，健康谓词转换器f ：f ( e ) 一f ( d ) 称为完全 相容的，若对于f ( e ) 的任意不相交集簇 以) 叫都有 f ( u 阢) = i i f ( u i ) 在接下来的几章中，详细地讨论稳定模糊谓词和相应的谓词转换器的相关定理与 性质 3 1 稳定模糊谓词的定义和拓扑性质 9 第三章稳定模糊谓词 由于模糊谓词是s c o t t 连续映射，所以自然地考虑模糊谓词的稳定性，即稳定模 糊谓词本章主要在模糊谓词的基础上提出一种新的模糊谓词一稳定模糊谓词，证明 所有稳定模糊谓词组成的集合在点式序下构成模糊一半拓扑，表明岛( d ) ，( 功是一 个d 一超滤子同时还表明稳定模糊谓词在数乘运算下是封闭的，但有例子表明她在 和运算下未必封闭 3 1 稳定模糊谓词的定义和拓扑性质 由于模糊谓词是一个从d c p o 到【0 ，1 】闭区间的s c o t t 连续映射，下面在这个基础 上给出稳定模糊谓词的定义同时根据格上拓扑学的一些知识来讨论稳定模糊谓词的 一些拓扑性质首先给出本节用到的几个定义 虽然论域本身不构成格，但格在论域理论中有重要的应用 定义3 1 1 3 0 】设二是一偏序集， 若l 的每个有限子集都有交，则称工为交半格 若工的每个有限子集都有并，则称l 为并半格 注一般地半格指的是交半格 定义3 1 2 【3 0 】设a 是p 半格，即带有最小元的半格，0 与1 为它的最小元和 最大元， 1 设a ，b a 若o ab = 0 ，则称a 与b 是分离的 2 a 的子集x 称为分离，若x 中任意两个不同元素都分离； 3 若a 的任意的分离子集都有并( 即最小上界) ，则称a 是分离完备半格，简称 d 一半格 定义3 1 3 3 2 】设x ，y 是半格，若，：x y 是保有限交映射，则称，是半格 同态 定义3 1 4 【3 0 】设a 是d 一半格，f 是a 的子集，若f 满足； ( 1 ) f 是上集； ( 2 ) 1 f ，0 隹f ； 1 0 第三章稳定模糊谓词 ( 3 ) 若o ，b f 则a a6 f ；则称f 是a 上的一滤子； 进步地，f 还满足 ( 4 ) 若对于a 的任一分离子集x ，u x f 定有f n x 是单点集，则称f 为a 上的d 一超滤子 用符号d f i l t ( a ) 表示a 的所有d 一超滤子之族 下面介绍半拓扑空间的定义 定义3 1 5 3 1 设x 是一集合，a ( x ) 是x 的一些子集组成的集簇，二元组 ( x ，n ( x ) ) 称为d 一型半拓扑空间，简称为d 一半空间，而q ( x ) 中的元素称为d 一 半空间x 的开集 定义3 1 6 【3 1 】设( x ，q ( x ) ) 是p 空间，若q ) 满足 ( 1 ) 0 ，x q ( x ) ； ( 2 ) 若以v q ( x ) ，贝q u n v q ( x ) ； ( 3 ) 若 矾) 叫是n ( x ) 的任一不相交集族( 即v ，j 1 只要i j 就有阢n = 口) ， 则这集族的集合并u 阢q ) ，则称a ( x ) 为x 上的一半拓扑，而( x ，q ) ) 称 为一半拓扑空间，简称为f 一半空间，以下符号u 表示不相交集族的并 定义3 1 7 设d 是相容交的d c p o ，p 乃( d ) 是模糊谓词，如果p 是稳定映 射，则称p 为稳定模糊谓词在d 上的所有稳定模糊谓词构成的集合记为s ，( d ) 其 上的序关系也是点式序关系，即p q 毋( d ) ， p q ，当且仅当p ( x ) q ( z ) ，0 d 性质3 1 1 常量谓词1 和0 是稳定的 下面介绍在证明过程中用到的一个重要引理，先给出几个相关的定义 定义3 1 8 【2 6 设l 是个偏序集，则l 是完备半格当且仅当每个非空子集都有 交，每个定向子集都有并 定义3 1 9 2 6 一个偏序集l 称为连续的，如果它满足渐进公理 ( 忱l ) x = v t l 【z 其中u z = u a l u z ) 是定向的 由论域理论知道当a 是一个完备半格并且是并半格时， lz = u a i z 是定向的，从而可以把连续偏续集的定义协a ，z = v t 舢z 定义为z = s u p u z 即 3 1 稳定模糊谓词的定义和拓扑性质 1 1 无论什么时候z 菇y ，则j u z 使得u 菇y 也就是说若v u z 都有l , y ，则z y 事实上，若= v t u z ，且$ 盛y ，则有v 扎菇y ，从而j u 非z 使得菇y 否则若 讹u z 有y ，则v j iz y 矛盾因为 0 ，1 】是一个完备格，且是连续的从而有 下面的引理 引理3 1 1 在 0 ，1 】闭区间中有下面的事实；如果y t o ，t 0 都有t b ，则 a b 性质3 1 ，2 如果p q 毋( d ) ，则p a q 西( d ) 证明定义( p a q ) ( z ) = e ( x ) a q ( z ) ，忱d 因为p i q 是稳定的，所以p ，q 是s c o t t 连续的由定理2 1 ，可知p a q 是s c o t t 连续的 设a 是d 上的相容集合，我们需要证明 ( p a q ) ( a a ) = ( p a q ) c a ) 由p a q 的单调性得( p a q ) ( a ) ( p a q ) ( a ) 下面我们证明相反的不等式，即 ( p a q ) ( a ) ( p a q ) ( a ) ， 因为v x a ，( p a q ) ( 。) p ( z ) ，( p a q ) ( z ) sq 扣) ，因此 ( p aq ) ( a ) a p ( a ) = p ( a a ) ， ( p aq ) ( a ) sa q ( a ) = q c a a ) ， 所以 ( p a q ) ( a ) p ( a a ) a q ( a ) = ( p a q ) ( a ) 因此 ( p a q ) ( a a ) = ( p a q ) ( a ) 至此表明了p a q 西( d ) 下面证明paq 是p 与q 的交事实上，由于v x d ，由paq 的定义可 知，( p a q ) ( z ) = e ( x ) a q ( z ) sp ( z ) ，( p a q ) ( z ) = e ( z ) a q ( z ) q ( z ) ，从而有 p a q p ，p a q q 第三章稳定模糊谓词 若有r p i rsq ，则有忱d ，r ( z ) p ( 。) ，r ( z ) q ( z ) ，从而有r ( z ) p ( x ) q ( z ) = ( p a q ) ( z ) 因此r p a q ，说明p a q 是p 与q 的交 o 我们已经知道乃( d ) 是个模糊拓扑，但是毋( d ) 未必是模糊拓扑，因为稳定 模糊谓诃的点式并未必属于西( d ) ( 见下例) 例如设d = 上，o ，b ，t ) ，序关系如图所示 a b 糍0攀 ，( 6 ) =9 ( 6 ) = j ，( t ) = ；g ( t ) = ； ( ，v g ) ( 。) ( ，v 9 ) ( 6 ) = j 1 五1 = 互1 ， 3 1 稳定模糊谓词的定义和拓扑性质 1 3 证明因为 五， ，) 是稳定映射，所以 五，i ， 是s c o t t 连续的由定理2 1 可知任意并v ， 是s c o t t 连续的，从而分离并u 也是s c o t t 连续的 i e l i e l 下面只需要证明u 五保相容交 i e i 设e 是d 上的相容集合，d 是e 的上界，则我们需要证明下面式子成立， ( 1 l ) ( e ) = ( ) ( e ) 因为a e v x e ，故( u f 4 ) ( n e ) ( u 五) ( z ) ，从而 4 e i4 e i ( 1 lf i ) (