（计算数学专业论文）概率计算与可能性计算的domain语义.pdf

上海师范大学博士论文 同时将可能性与天使非确定性放在一起加以讨论， 得到它们有关的万有性质. 第三部分:精细演算 精 细 演 算是d ijk s t r a 最弱前置 演算的 扩充与 进一步发 展， 近 来， 应明生 教授 研究了 概率程 序的 精细 演算 . 基于 应明 生 教授的一 些想法， 这部分我 们的 研究分为 概率精 细与可能 性精细 两个方面. 一方面， 我们讨论了亚概率程序的概率精细与概率正确性. 这两个概念分别反映 了 一个亚概率程序被另一个亚概率程序精细的程度以及一个亚概率程序三元组的正确度. 证 明亚 概率程序间的概率精细可以通过概率正确性来描述. 另一方面， 我们提出了一种基于可 能性的程序精细演算模型， 目的是为了进一步形式化可能性计算. 引入可能信念逻辑， 得到 了基本谓词转换器之间的对偶. 给出了可能谓词转换器是可能天使更新与可能魔鬼更新的 充 分 必 要条 件. 进 一步证明 形式定理 ， 是说 任意一个强 单调的 可能谓词 转换器都 是某个可能 天 使 更 新与某 个可能 魔鬼更新的 合成. 讨 论了 可能 谓词转换器的同 态特征. 最后， 我们研究 了 一 些 重要的 可能谓词 转换器: 单 调的 可能谓 词转换器， 合 取与析取的 可能谓词转 换器， 并 证明所有的程序状态都是强单调的. 关键词: 概率计算; 可能性计算; 精细演算; 谓词转换器; 状态转换器; 语义模型. 棍率计葬与可能径计葬的do ma i n语义 abs t r a c t wi t h c o m p u t e r t e c h n o l o g y a n d n e t w o r k t e c h n o l o g y d e v e l o p m e n t , p e o p l e t u r n a t t e n t i o n t o p a r a ll e l c o m p u t a t i o n a n d d i s t r i b u t e d c o m p u t a t i o n fr o m s e q u e n t i a l c o m p u t a t i o n . p a r a ll e l c o m p u t a t i o n a n d d i s t ri b u t e d c o m p u t a t i o n r e s u l t i n t h e n o n - d e t e r m i n i s m o f p r o g r a m s , t h e n o n - d e t e r m i n i s t i c c o m p u t a t i o n o f p r o g r a m s i s a n i mp o r t a n t t o p i c o f i n v e s t i g a t i o n i n c o m p u t e r s c i e n c e , w h o s e r e s e a r c h r e s u l t s c a n b e a p p li e d t o p r o g r a m s p e c i fi c a t i o n , p r o g r a m r e fi n e m e n t , s o f t w a r e c o mb i n a t i o n , t h e a n a l y s i s a n d d e s i gn o f c o m p l e x s o ft w a r e a n d h a r d w a r e s y s t e m s a n d s o o n . th i s k i n d o f n o n d e t e r mi nis m ha s t wo di ff e r e n t c a s e s : c l a s s i c a l n o n - d e t e r -in i a m a n d p r o b a b il is t i c n o n - d e t e r m i n i s m. t h e f o r m e r r e f e r s t o p r o d u c e t h e d i ff e r e n t p o s s i b l e o u t c o m e s o f t h e p r o g r a m f o r t h e s a m e i n p u t v a l u e , t h i s k i n d o f n o n - d e t e r m in i s m is mo d e l l e d 勿 t h r e e k i n d s o f p o w e r d o m a i n s , i . e . , p lo t k i n p o w e r d o m a i n , s m y t h p o w e r d o ma i n a n d h o a r e p o w e r d o ma i n . t h e l a t t e r r e f e r s t o g i v e a p r o b a b i l is t i c v a l u e o f p o s s i b le o u t c o m e s o f p r o g r a m f o r t h e s a m e i n p u t , t h i s k in d o f n o n - d e t e r m i n i s m i s m o d e ll e d 勿 p r o b a b i l i s t i c p o w e r d o ma i n , r e c e n t l y w h i c h i s a p o p u l a r t o p i c , m o r e t h e o r e t i c c o mp u t e r s c i e n t i s t s a n d m a t h e m a t i c i a n d e v o t e d t h e m s e l v e s t o t h is fi e l d a n d g o t m a n y i m p o r t a n t r e s u l t s . s i n c e t h e n o n - d e t e r m i n is t i c p h e n o m e n o n s i n t h e r e al w o r l d i n c l u d e m a n y p o s s i b i li s t i c p h e n o m e n o n s b e s i d e s p r o b a b i l i s t i c p h e n o m e n o n s , f o r t h i s r e a s o n , w e p r o p o s e t h e n o t i o n o f p o s s i b i l is t ic c o m p u t a t i o n , w h i c h r e f e r s t o g i v e a p o s s i- b il is t i c v al u e o f t h e p o s s i b l e c o m p u t a t i o n o u t c o m e o f p r o g r a m, t h i s k i n d o f n o n - d e t e r m i n i s m i s m o d e l l e d 勿 p o s s i b il i s t i c p o w e r d o m a i n . t h e m a i n a i m o f t h i s t h e s is i s t o p r o v i d e s e m a n t i c m o d e l s f o r t h e p r o b a b i l is t i c a n d p o s s i - b i l i s t ic n o n - d e t e r m i n i s t i c c o m p u t a t io n , ma i n r e s e a r c h e s c o n s is t i n t h e f o l l o w i n g t h r e e a s p e c t s : p a rt 1 : s e m a n t i c mo d e l o f p r o b a b i l i s t i c c o mp u t a t i o n t h e r e s e a r c h o f p r o b a b il i s t i c p r o g r a m s c a m e fr o m k o z e n s o ri g i n al w o r k , n o w t h e r e a r e m a in f o u r k i n d s o f t h e s e m a n t i c m o d e l s o f p r o b a b i l i s t i c p r o g r a m s : k o z e n s m o d e l , c . j o n e s m o d e l , h e s m o d e l a n d c .mo r g a n s e t al m o d e l s . o u r p r o b a b i l i s t i c c o m p u t a t i o n m o d e l i s b a s e d o n c . m o r g a n s e t al p r o b a b i l i s t i c c o m p u t a t i o n m o d e l . o u r r e s e a r c h e s c a n b e d i v i d e d i n t o t w o p a r t s : s u b - p r o b a b i li s t ic p r o g r a m s a n d p r o b a b i l is t i c p r o g r a m s . o n s u b - p r o b a b i l i s t i c p r o g r a m s , i n t r o d u c e s u b - p r o b a b il i s t i c p r o g r a m l a n g u a g e , g i v e i t s a x i o m a t i c s e m a n t i c s a n d 上海师范大学博士论之 d e n o t a t i o n a l s e ma n t i c s a n d p r o v e i t s s o u n d n e s s a n d c o m p l e t e n e s s t h e o r e m . o n p r o b a b i l i s - t i c p r o g r a m s , o u r r e s e a r c h e s c a n a l s o b e d i v i d e d i n t o t w o p a r t s : d e t e r m i n i s t ic p r o b a b il is t i c p r o g r a m s a n d n o n - d e t e r m i n i s t i c p r o b a b i l i s t ic p r o g r a m s . a b o u t d e t e r m i n i s t i c p r o b a b il is t i c p r o g r a m s , w e g i v e a n a p p r o a c h d i ff e r e n t fr o m c . mo r g r a n s t o c h a r a c t e r i z e h e a l t h i n e s s c o n - d i t i o n s , s u c c e e d i n s e t t i n g u p e q u i v a l e n c e b e t w e e n p r o b a b i l i s t i c p r e d i c a t e t r a n s f o r me r s a n d d e t e r m i n i s t i c p r o b a b i l is t i c s t a t e t r a n s f o r m e r s . o n t h e o t h e r h a n d , w e s t u d y n o n - d e t e r m i n is t i c p r o b a b i li s t i c p r o g r a m s . p r o p o s e t h e n o t i o n o f p r e - h e a l t h i n e s s a n d p r o v e o n e s i d e o f e q u i v a - l e n c e b e t w e e n p r e - h e al t h y p r o b a b i l i s t i c p r e d i c a t e t r a n s f o r m e r s a n d n o n - d e t e r m i n i s t i c p r o b a - b i l i s t i c s t a t e t r a n s f o r me r s . p a rt 2 : s e m a n t i c mo d e l o f p o s s i b i l i s t i c c o m p u t a t i o n i n t h i s p a rt , w e g iv e a k i n d o f p o s s i b i li s t i c c o m p u t a t i o n mo d e l 勿 t h e n o t i o n o f p oss i b i l i t y v a l u a t i o n , a i m i n g a t s t u d y i n g p r o g r a m s e m a n t i c s w i t h p o s s i b i li t y . p r o v e t h a t t h e p o s s i b il i s t i c p o w e r d o m a i n f u n c t o r i s a mo n a d i c f u n c t o r o n t h e d i r e c t e d c o m p l e t e p a r t i a l s e t c a t e g o ry dc p o . t h e n p o i n t o u t t h e e q u iv a l e n c e b e t w e e n p o s s i b i li s t i c s t a t e t r a n s f o r m e r s e ma n t i c s a n d p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s e m a n t ic s . a t t h e s a m e t i m e , p u t t h e p o s s i b i li t y a n d t h e a n g e li c n o n - d e t e r m i n i s m t o g e t h e r t o d i s c u s s a n d g i v e t h e i r u n i v e r s a l p r o p e rt i e s . pa rt 3 : re fi n e me n t ca l c ul u s r e f i n e m e n t c a l c u l u s i s a n e x t e n s i o n a n d f u r t h e r d e v e l o p m e n t o f d ij k s t r a s w e a k e s t p r e - c o n d it i o n c a l c u l u s , r e c e n t l y , mi n g s h e n g y i n g s t u d i e d r e fi n e m e n t c a l c u l u s o f p r o b a b i l i s t i c p r o- g r a m s . b a s e d o n mi n g s h e n g y i n g s s o m e i d e a s , i n t h i s p a r t , o u r r e s e a r c h e s c o n s i s t o f t w o p a r t s : p r o b a b i l i s t ic r e fi n e m e n t c al c u l u s a n d p o s s i b i b s t i c r e fi n e m e n t c a l c u l u s . o n o n e h a n d , w e d i s c u s s p r o b a b i l i s t i c r e fi n e m e n t a n d p r o b a b i l i s t i c c o r r e c t n e s s b e t w e e n s u b - p r o b a b i l i s t i c p r o g r a m s . t h e t w o n o t i o n s r e fl e c t t h e d e g r e e t h a t a s u b - p r o b a b i l i s t i c p r o g r a m i s r e fi n e d 妙 a n o t h e r s u b - p r o b a b i l i s t i c p r o g r a m a n d t h e d e g r e e o f c o r r e c t n e s s o f a s u b - p r o b a b i l i s t i c t r i p l e r e s p e c t i v e l y . p r o v e t h a t p r o b a b i l i s t i c r e f in e me n t b e t w e e n s u b - p r o b a b i li s t i c p r o g r a m s c a n b e d e s c r i b e d b y p r o b a b i l i s t i c c o r r e c t n e s s . o n t h e o t h e r h a n d , w e i n t r o d u ce a k i n d o f r e f i n e m e n t c a l c u l u s m o d e l b a s e d o n p o s s i b il i t y , t h e a i m is t o f u r t h e r f o r m al i z e p o s s i b i l i s t i c c o mp u t a t i o n . we i n t r o d u ce p o s s i b i l i s t i c b e li e f l o g i c , p r o v e t h e d u a l it i e s t h e o r e m s b e t w e e n b a s i c p r e d i c a t e t r a n s f o r me r s . g i v e a s u ffi c i e n t a n d n e c e s s a ry c o n d i t i o n f o r a p o s s i b i li s t i c 棍率计算与可能性计茸的d o ma in语义 p r e d i c a t e t r a n s f o r m e r t o b e a p o s s i b i l i s t i c a n g e li c u p d a t e o r p o s s i b i l is t i c d e m o n i c u p d a t e . f a r t h e r , p r o v e t h e n o r m a l f o r m t h e o r e m w h i c h s a y s t h a t a n y s t r o n g l y m o n o t o n i c p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s c a n b e w r i t t e n a s a s t a t e m e n t t e r m c o n s i s t i n g o f a p o s s i b i l i s t i c a n g e l i c u p d a t e f o ll o w e d勿 a p o s s i b i l i s t i c d e m o n i c u p d a t e . mo r e o v e r , h o m o m o r p h i s m p r o p e rt i e s o f p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s a r e d i s c u s s e d . a t l a s t , w e s t u d y s o m e i m p o rt a n t p o s - s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s : m o n o t o n e p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s , c o n j u n c t i v e p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s a n d d is j u n c t i v e p o s s i b i l i s t i c p r e d i c a t e t r a n s f o r m e r s a n d p r o v e t h a t a l l p r o g r a m s t a t e m e n t s a r e a ll s t r o n g l y m o n o t o n i c ke y w o r d s : p r o b a b i l i s t i c c o m p u t a t i o n ; p o s s i b i l i s t i c c o m p u t a t i o n ;c a l c u lu s ; p r e d i c a t e t r a n s f o r me r ; s t a t e t r a n s f o r me r ; s e ma n t i c mo d e l . v 论文独创性声明 本论文是我个人在导师指导下进行的研究工作及取得的研究成果。论文中除了特别加 以标注和致谢的地方外，不包含其他人或机构已 经发表或撰写过的研究成果。其他同志对 本研究的启发和所做的贡献均已在论文中做了明确的声明并表示了谢意。 作 者 签 名 :引 亘 日 a : y v . ) . s ， “ 论文使用授权声明 本人完全了解上海师范大学有关保留、使用学位论文的规定，即;学校有权保留送交 论文的 复印 件， 允许论文 被查阅 和借阅 ; 学 校可以公 布论 文的 全部 或部 分内 ig - , 可以采 用影 印、缩印或其它手段保存论文。 保密的论文在解密后遵守此规定。 作者 签 :. 师签 :1/0 - 日 :叫 “ 呀 棍率计葬与可能性计葬的do ma i n语又 第一章引言 1 . 1计算与程序语言之间的关系 计算是一个非常广义的概念， 有精确计算， 近似计算， 数值计算， 符号计算等. 随着科学的 发展， 人 们对计算的 精 度要求 越来越高 ， 而且计 算的复杂 度也越 来越高 ， 这 一切的实 现离 不 开计 算机软 件与硬 件的发 展. 程序语 言作为 计算机的 软件， 它是 数据结 构加 算法， 而算 法是 实现计算的方法， 技巧与思路， 它依靠编程来实现. 对计算过程的不同看法产生了不同的计 算模型 ( 因 此产生了 不同的 编程 语言) ， 主 要模型 有: 命令 式模型与 函 数式模 型. 命 令式 模型 把计 算看 成一系 列操 作的 执行， 基本的 计 算元 素是一 组基本 操作 ， 计 算过 程在 一个环 境里 进 行， 操作的 效果就 是改 变环境的 状态 . 而函数 式模型 把计算看 成对 数据的 函数 变换， 基本 计 算元素是一组基本函数， 一个计算就是一系列的函数变换. 因此， 可以说程序语言是实现计 算的手 段或 工具. 本论文 关注的 不是 具体的 计算 方法， 而是 针对程 序语言 ， 计算的形 式化问 题， 进一步说就是研究计算的语义问 题. 从上面的论述中可以看出程序语言可以依据计算的直觉概念来解释， 然而， 一个非形式 化且不 准确的 解 释可能 会 产生不 一致性 与 歧义， 因此， 程序 语言语 义的 形 式化 是一项 重要的 工 作. 关于 这 方面的 工 作可以 参 考文 献【 1 2 , 1 4 , 6 6 , 7 6 . 现在 有一些 形式 化 方法 定义 程序 语言的 语义. 下面 我们主 要介绍 两种定 义语 义的 方法 ， 即指 称的 方 法与公 理化 方法 . 其它重 要的 方 法有 操作 语义6 9 与 代数 语义 【 2 8 , 3 6 , 5 2 . 用指称 的方 法定 义程 序语言的 语义 来自 s c o t t 与 s t r a c h e y 8 2 . 指 称语义 是从 一个 抽象的 观点 看 待计 算: 存在 着两 个域 ， 一 个是 语法 域， 在语 法域中 定义了 一 个形 式语 言系 统; 另外 一 个是 数学 域( 语 义域 ) . 用一 个语义解 释函 数， 以 语义域中的 对象( 值 ) 来注 释语法域中 定义的 对 象. 因 此 ， 可以 说 指称 语义 关注的 是计 算的 效 果. 语义 域通常 要通 过递 归的 方式 定义 . 由 于 基数的原 因， 要在 一般的 集 合结构 上定 义 通常 是办不到 的 因 此， 语义 域经常带 有拓 扑结 构， 在此结构上定性或定量的分析计算的信息. 指称语义常用的拓扑结构是完备偏序集， 公 理语 义方法是 把程序 设计语言 视为 一个数 学对象 ， 建立它 的公 理系 统， 从而 使程 序设 计语 言 有坚实的 逻辑 基础 . 因此 ， 可以 说公 理 语义关注的 是 计算的 可靠 性问 题. 公 理语 义中 常 用的 是证明 系 统: 计算 被表 示为 程序 行为 的断 言. 众所 周知的 是 h o a r e 的全 正确 逻辑 ， 断 言 是 p s q 这种形 式， 意思是 ， 如果 程 序s 在某个初 始状态 满足谓 词 p , 则 程序 执行并 且终 上海师范大学博士论之 止 ， 且 终止 状态满 足谓词 q . 另 外 ， 公 理语义也 可以 不通 过形式 证明 系统 给出: 程序的 行为 可 以 被看 成转换谓 词的函 数 . 如 d ij k s t r a 的最弱 前置 语义 2 3 1 , 就是把 程序 s看作 一个函 数， 此 函 数把 输出 空间 上的谓 词 q映成 使 h o a r e 断言 p s q 有效的 所有 尸中最 弱的 一 个. 在这 种 谓词 转换器 语义 下， 每 个指 令被 指派 给它的 最弱 谓词 转换器 . 关 于这 一课 题有许多 研究 成 果3 , 4 , 1 3 , 1 5 , 1 8 , 1 9 ,3 0 , 3 5 ,5 6 , 6 0 , 6 1 ,6 2 , 6 4 , 6 7 , 6 8 , 7 0 , 8 1 , 8 3 1 . 指称语义与公理语义间的关系是本论文研究的重点之一 程序的指称可以看成从输入空 间到输出空间的函数， 我们称之为状态转换器. 而程序的公理语义可以看成谓词转换器. 通 常 这两 种转换器是 同态 而非同 构 ， 然 而， 在某些健 康条 件下 p l o t k i n 在 文献 7 0 中指出 它 们是 同 构的 . 另 外， m . m . b o n s a n g u e 在 文 献 5 中 研究了 指 称语义 与公 理语 义的 拓扑 对偶 . 1 . 2 概率计算 尸 内 概率 计算是 指程 序做非 确定性 选择 受某个 概率分 布控 制， 即 指派 一 个概率分布 给程 序可 能的计算结果. 关于程序的概率计算这一课题， 现在有许多研究成果， 下面我们介绍一些主 要的工作. k o z e n 的概 率程序 语义模型 ! 4 9 , 5 0 ， 其概率分布 是定义 在状态空 间子 集的a 一代数 上的 . 他认为 可计算函 数是模 连续而非 s c o t t - s t r a c h y 类型的序 连续. k o z e n 的贡献 之一是 使用算 数算子 +而非 通常的 逻辑 算子合成两 个程序， 即 尸p +q ， 意思是以 概率 p 执行程序 尸 ， 而 以 1 一 p 的概率 执行 程序q ; c .j o n e s 的 概率程 序模型!4 4 , 4 司 ， 其概率 分 布是定义 在状态 空间 的 s c o t t 的拓扑上的 ， 这是 s m y t h 的观点 : 开集作为可计算的 特征或可能 的测试. 她在任意 的 d c p 。 上构 造了 概 率幂 域， 以 此 来 模拟概 率程 序的非 确 定性. 而 且她 给出了 h o a r e 类型的 命 令式 概率 语言并 且给出了 它的 指 称语 义与公理 语义 ， 进一步 证明了 可 靠性与 完备性 定理; 何 积丰的 概 率程序 语义 模型 ! 3 4 ， 其 概率 分布是定 义 在状 态空间 的 幕集 上的 . k o z e n 与j o n e s 主 要研 究了 确定型 概率 程序， 而何 积丰 主要 研究了 非确 定型 概率 程序 在文 献3 4 1 ， 他 给出了 卫 式语 言的 两种 模型: 关 系模 型与 提 升模型 ， 并 且指出 关 系模 型 优于提 升 模型. 后 来， 关系 模型 成为 人 们研究非 确定 概率 程 序的 一 个主 要模型 ; 牛 津大 学概 率程 序调 查组 m o r g a n , m c i v e r 等 人概率程 序语义 模型 ! 4 2 , 6 0 ,6 1 , 6 2 , 6 3 ,8 5 1 ， 其概率分布 是直接定义在 状态空间上的. 他们做 了 许多 漂亮的工作 ， 如: 他们 成功地建 立了 概率 谓词转 换器与概率 状态 转换器间的 等价性 ， 分层刻画了 系统的健康条件 ， 在此系统中， 确定 性、 魔鬼、 概率及天使选择并存; r . t i x , k . k e i m e l 与 p lo t k i n 的工 作! 8 7 , 8 8 ， 他们 提出 了 幂锥的 概念， 基于 j o n e s 的 概率 程序模型 ， 在 棍单计茸与可能径计葬的do ma i n语4 三 种幂 锥下 ， 即 h o a r e , s m y t h 与 p l o t k i n 幂 锥， 合 成了 概 率与 非确 定. 1 . 3 可能性计算 我们己经介绍了 程序的概率计算， 本节我们介绍另一种计算模型一可能性计算. 现实世 界， 非确定 现象中 除了 概率现象还 有许多 可能性 现象. 概率现象与可能 性现象的 根本区 别 在于 : 概率事 件的结 果是“ 非 此即比 ” ， 即 结果是 确定的 ， 而 可能 性事件 的结果 是“ 亦 此亦比 ” ， 即结果 是不确 定的. 如: “ 投硬币 ” ， 结果 要么是正 面要么是反 面， 不可能出 现一半是 正面 一 半是反面的 情况. 然而 ， 如果一个三十岁的 人站在你 面前 ， 问“ 此人是青年 还是 中年 ?， 答 案可能 是此 人青 年的 程 度有多大 ， 中 年的 程 度又有多 大. 关于可能 性理论 ， 己 有许多 研究 成 果 2 0 , 2 4 , 8 0 , 8 6 , 1 0 0 . 程序 世界 也有可 能性 现象 ， m e e h 二在文 献! 5 3 中 指出 可能 性逻 辑可以 用 于多 种 语言一 扩充 的 标准 语言 如p r o l o g , f o rt r a n , a p l , j a v a 及 一些 设计 语言如 f i l , f l i n t . 他的工作合成了可能性与函数式设计语言. 我们主要工作之一是研究了可能性计算的语义 模型. 1 . 4 精细演算 精细演算是推理程序精细与正确性的逻辑框架. 它的主要作用在于命令式语言的获取， 即 程 序通过 逐步 精细 构造 ， 精 细的每 一步都 保持 原有程 序的正 确性 . 精细 演算 是d i j k a t r a 最 弱前置演算的扩充， 即程序状态由谓词转换器模拟. r - j . b a c k 在冈中 详细 地介绍了 经典的 精细 演算语 言， 此语言是由 基本的 谓词 转换 器， 函 数复合 ， 以 及无限 交与 无限 并的格 算子合成 得到的 . 这种语言 表达能 力很强 ， 足够模 拟可 执 行的序 列程 序与 抽象 规范 . 程 序语言的 语义 域由 单调的 谓词 转换 器构成 ， 这种语义 建 立在 格 理论的 解 释上 : 魔 鬼 选择 被程 序的交 模 拟， 而天使 选 择被并 模 拟. 应明 生 教授 在文 献! 9 5 中 介绍了概 率程 序的精 细演 算. 为了 同 经典的 精细 演算 相协 调， 他 引入强单调的概率谓词转换器的概念， 在此基础上建立了形式定理. 形式定理表明任意单调 的 谓词 转换器 可以 通过 天 使更新与魔鬼 更新构 造， 它对于 序列程序 语言的理 论分 析非 常重 要. 应教授 还定义了 测 度的 概念， 以此 表示概 率程 序间 的 精细度与 概率 程序的正 确 度， 这一 概念推广了经典的精细与正确性的概念， 使之从二值逻辑成为概率逻辑. 上海师范大学博士论之 l s 本文工作 我们的 工 作是 建立 在以 上工 作基 础上的 ， 主要 贡献 有下 面三 个方面 . 第一个贡献是第三章与第四章， 主要研究了亚概率计算与概率计算. 在亚概率计算方面， 我们引入了亚概率程序语言， 建立了它的公理语义与指称语义并且证明可靠性与完备性定 理 . 在 概率 计算方 面 ， 我们 利用 c . m o r g a n 等 人的 概率 计算 模型研究 概率 程序 . 给出 一 种不同 于 c . m o r g a n 等人 刻画 健康条件的 方 法， 成 功地建 立 起概率谓词转 换器与 确定 性概率 状态转 换器之间的等价性. 另一方面， 我们研究了天使非确定概率程序. 提出了预健康的 概念， 并且 证明预健康的概率谓词转换器与非确定概率状态转换器之间等价的一个方向. 第二 个 贡献 是第 五章， 主要 研究了 可能 性计 算. 我们 提出了 可能 性计 算语 义模 型， 得到了 可能状态转化器语义与可能谓词转换器语义的等价性. 证明可能性幂域函子是定向完备偏 序 集 范 畴 d e p 。 上 的 m o n a d 函 子 . 进 一 步 利 用 m o d u le lo ,i 的 概 念 ， 将 可 能 性 与 天 使 非 确 定 性 放在一起加以讨论， 得到它们有关的 万有性质. 第三 个贡献 是第 六章， 主要研究了 概率 精细 演算与 可能性精 细演算 . 在概 率精细 演算方 面， 讨论了 亚 概率 程序的 概率精 细与 概率正 确性. 在可 能性精 细演算 方面， 引入了 可 能信念 逻辑， 得到了基本谓词转换器的对偶并且证明强单调的可能谓词转换器的形式定理. 进一步 我们研究了一些重要的可能谓词转换器， 并且证明所有的 程序状态都是强单调的. 棍率计茸与可能径计算的do ma i n语义 第二章预备知识 本 章我 们介绍 一些 本论文 所需 的预 备知 识， 主要 有三个 部分 : 论 域理 论， 范 畴理 论与 蕴涵 算子. 论域理论主要应用于计算与可计算理论以及程序语义， 目的是为其上定义可计算函数 的空 间 建立 语义模型 . 在论 域理 论中 计算 被看 成信息 域间的 映 射， 即 s c o t t 连续映 射. s c o t t 连 续映 射与 可计算 性有着 非常 重要的 联 系; 范 畴理 论在 计算机 科学中 有 着重要的 应 用， 主要作 用在 于解 释与阐 述抽象 概念， 建立不 同分 支的关 联. 程序在范 畴中 被解释 为结构 ， 结 构的初 始 含义 是集合 与函 数， 后来 指合 适的 拓扑 空间 与连 续映 射. 范畴 理论 也是 代数 语义 学的 基 础; 蕴涵算子的作用在于推理， 可以说任何一个旨 在推理形式化的系统都离不开它. 而公理语义 的一 个 重要作用 是推理 程 序的正 确 性， 即 计算的 可 靠性 . 介绍 蕴涵 算子的目 的 之 一在于 程序 推理 . 在本 论文中 ， 我 们 有时使 用 x : a与 f . x 表示 x e a与了 ( 习 . 2 . 1论域理论 本节 我 们介绍 论域 理论中 的 一些 定义 和命 题， 主要 参考 文献 1 2 ,2 9 , 1 0 2 令( d , 自 是一 偏序 集. d的 子集 x是定向 的 ， 如 果它 非空 并且 对于 任 意两 个元 素a , 6 : x , 有一 个 a ， 好的 上界 x : x . 定向 完备 偏序 集( d c p o ) 是 一偏序 集( d , 自 并且它的 每个 定向 子 集 x有 最 小 上 界 u x . 完 备 偏 序 集 成 (c p o ) 是 指 有 最 小 元 的 d c p o . 一个函 数从d c p o d到d c p o e是 s c o t t 连续当 且仅当它保持偏序与定向子集的并 ， 即 了 是 s c o t t 连续， 如果 二 cy ， 有f ( x ) c f ( y ) ， 并且 对 于任意 的定向 子 集x i f ( u x ) = u z e x f ( x ) 我 们 用! d*司表示 所有 从d到 e的 s c o t t 连续函 数. o是 s c o t t 开集当 且仅当对于 任意的 x : 0与 ， 如果 x二y ， 有 ， : 0 ， 并 且对于所有的定 向 子集 x , ux: 0蕴涵 存在 x : x满足 x : 0 . d 的所有 s c o t t 开 集构成 d上的一 个拓扑称 为 s c o t 七 拓 扑， 表示为 以 d ) . 双小于 关系， 记作 ， 二 ， 当 且 仅当 对于所 有的 定向 子 集 x, y c _ x蕴涵 x 中 存在一 个元素 d 满足 x cd 一 个d c p o 尸是连 续的， 如果 对于任 意的 x : p , y : y x 是定向 的并 且 x =v v : ， x 一 个c p o p是 连续 格如 果p是 连续的 并 且p是 完备 格. 定 理2 . 1 如果 c p o p是 连续的 并 且 q 是 连续 格， 那么 p*q 1 是 连续 格 命题2 . 2 下面的结论成立. ( 1 ) 如 果 二 ， ， 那 么 x v . 上海布范大学博士论丈 ( 2 ) 如 果 : 。 ， z ， 并 且 x v 。 存 在 ， 那 么 : v y 二 ( 3 ) 如 果 二 y , y z ， 那 么 x z . 命题 2 . 3 如果 d是 d c p o ， 那么 0 m = y l y : d , ， x 是s c o t t 开 集. 2 . 2范畴理论 这一 部分 范畴 术语 来自 2 , 8 , 3 3 , 1 0 2 ) . 范畴c由以下几部分构成: ( 1 ) 范 畴的 对象 类 c i , ( 2 ) 对于 所有 的 a , b: ic i ， 从 a到 b态 射集 c ( a , b ) . ( 3 ) 对于 所有 a , b , c: i c i ， 合 成 操作。 : c ( b , c ) x c ( a , b ) *c ( a , c ) , () 对于 所有 a: i c i ， 恒