概率计算与可能性计算的Domain语义

摘要

随着计算机技术与网络技术的发展，人们将关注点从顺序计算转向并行计算与分布式计算.并行计算与分布式计算导致了程序的非确定性，而程序的非确定性计算是计算机科学的一个重要研究课题，其研究成果可用于程序规范，程序精细，软件合成，复杂软硬件系统的分析与设计等.这种非确定性有两种不同的情况：经典的非确定性和概率非确定性.前者是指对于同一个输入可能出现不同的结果，这种非确定性被三种幂域模拟，即Plotkin幂域，Smyth幂域，Hoare幂域.后者是指对于同一个输入，给程序可能出现的结果各赋以一个概率值，这种非确定性被概率幂域模拟.这是最近较热的一个研究课题，引起世界许多著名的理论计算机科学家与数学家的关注，并且取得了一系列重要的研究成果.因为现实世界中非确定现象除了概率现象外，还有大量的可能性现象。为此，本文提出了可能性计算的概念，即给程序可能的计算结果各赋以一个可能值，这种非确定性被可能性幂域模拟。 这篇论文的主要目的是为概率与可能性非确定计算提供语义模型，主要研究工作在下面的三个方面： 第一部分：概率计算的语义模型 程序的概率计算的研究源于Kozen开创性的工作，现在主要有四种概率程序语义模型：Kozen的模型，C.Jones的模型，何积丰的模型与C.Morgan等人的模型.我们的概率计算模型是建立在C.Morgan等人的概率计算模型基础上的。我们的研究分为亚概率程序与概率程序两个方面。在亚概率程序方面，引入了亚概率程序语言，建立其公理语义与指称语义，并且证明可靠性与完备性定理．在概率程序方面，我们的研究又分为确定性概率程序与非确定概率程序．在确定型概率程序方面，我们给出一种不同于C.Morgan等人刻画健康条件的方法，成功地建立起概率谓词转换器与确定性概率状态转换器之间的等价性。在非确定概率程序方面，我们研究了天使非确定概率程序，提出了预健康的概念，证明预健康的概率谓词转换器与非确定概率状态转换器之间等价的一个方向。 第二部分：可能性计算的语义模型 本部分我们利用可能性赋值的概念给出一种可能性计算模型，目的是为了研究具有可能性的程序语义。证明可能性幂域函子是定向完备偏序集范畴Dcpo上的一个monad函子．进一步利用可能性积分证明可能状态转换器语义与健康的可能谓词转换器语义之间的等价性．同时将可能性与天使非确定性放在一起加以讨论，得到它们有关的万有性质。 第三部分：精细演算 精细演算是Dijkstra最弱前置演算的扩充与进一步发展．近来，应明生教授研究了概率程序的精细演算．基于应明生教授的一些想法，这部分本研究分为概率精细与可能性精细两个方面。一方面，我们讨论了亚概率程序的概率精细与概率正确性．这两个概念分别反映了一个亚概率程序被另一个亚概率程序精细的程度以及一个亚概率程序三元组的正确度．证明亚概率程序间的概率精细可以通过概率正确性来描述．另一方面，我们提出了一种基于可能性的程序精细演算模型，目的是为了进一步形式化可能性计算．引入可能信念逻辑，得到了基本谓词转换器之间的对偶．给出了可能谓词转换器是可能天使更新与可能魔鬼更新的充分必要条件。进一步证明形式定理，是说任意一个强单调的可能谓词转换器都是某个可能天使更新与某个可能魔鬼更新的合成。讨论了可能谓词转换器的同态特征。 最后，本文研究了一些重要的可能谓词转换器；单调的可能谓词转换器，合取与析取的可能谓词转换器，并证明所有的程序状态都是强单调的。

目录

文摘

英文文摘

声明

第一章引言

1.1计算与程序语言之间的关系

1.2概率计算

1.3可能性计算

1.4精细演算

1.5本文工作

第二章预备知识

2.1论域理论

2.2范畴理论

2.3蕴涵算子

第三章亚概率计算

3.1预备知识

3.2亚概率程序语言

3.3亚概率程序的逻辑系统

3.4可靠性与完备性

第四章概率计算

4.1概率幂域

4.2确定性概率状态转换器

4.3概率谓词转换器

4.4概率转换器间的等价

4.5非确定概率程序

第五章可能性计算

5.1赋值与状态转换器语义

5.2可能谓词

5.3谓词转换器语义

5.4可能性积分与语义等价

5.5可能性幂域的Monad

5.6合成可能性与非确定

第六章精细演算

6.1概率精细与概率正确性

6.2可能信念逻辑

6.3关系与关系更新

6.4基本的谓词转换器与对偶

6.5特殊的谓词转换器

6.5.1单调的可能谓词转换器

6.5.2合取与析取的可能谓词转换器

参考文献

致谢

博士期间的科研成果及参加的科研项目