概率計(jì)算與可能性計(jì)算的Domain語義.pdf

1、隨著計(jì)算機(jī)技術(shù)與網(wǎng)絡(luò)技術(shù)的發(fā)展，人們將關(guān)注點(diǎn)從順序計(jì)算轉(zhuǎn)向并行計(jì)算與分布式計(jì)算.并行計(jì)算與分布式計(jì)算導(dǎo)致了程序的非確定性，而程序的非確定性計(jì)算是計(jì)算機(jī)科學(xué)的一個(gè)重要研究課題，其研究成果可用于程序規(guī)范，程序精細(xì)，軟件合成，復(fù)雜軟硬件系統(tǒng)的分析與設(shè)計(jì)等.這種非確定性有兩種不同的情況：經(jīng)典的非確定性和概率非確定性.前者是指對于同一個(gè)輸入可能出現(xiàn)不同的結(jié)果，這種非確定性被三種冪域模擬，即Plotkin冪域，Smyth冪域，Hoare冪域.后者是

2、指對于同一個(gè)輸入，給程序可能出現(xiàn)的結(jié)果各賦以一個(gè)概率值，這種非確定性被概率冪域模擬.這是最近較熱的一個(gè)研究課題，引起世界許多著名的理論計(jì)算機(jī)科學(xué)家與數(shù)學(xué)家的關(guān)注，并且取得了一系列重要的研究成果.因?yàn)楝F(xiàn)實(shí)世界中非確定現(xiàn)象除了概率現(xiàn)象外，還有大量的可能性現(xiàn)象。為此，本文提出了可能性計(jì)算的概念，即給程序可能的計(jì)算結(jié)果各賦以一個(gè)可能值，這種非確定性被可能性冪域模擬。 這篇論文的主要目的是為概率與可能性非確定計(jì)算提供語義模型，主要研究工作

3、在下面的三個(gè)方面： 第一部分：概率計(jì)算的語義模型 程序的概率計(jì)算的研究源于Kozen開創(chuàng)性的工作，現(xiàn)在主要有四種概率程序語義模型：Kozen的模型，C.Jones的模型，何積豐的模型與C.Morgan等人的模型.我們的概率計(jì)算模型是建立在C.Morgan等人的概率計(jì)算模型基礎(chǔ)上的。我們的研究分為亞概率程序與概率程序兩個(gè)方面。在亞概率程序方面，引入了亞概率程序語言，建立其公理語義與指稱語義，并且證明可靠性與完備性定理．在概

4、率程序方面，我們的研究又分為確定性概率程序與非確定概率程序．在確定型概率程序方面，我們給出一種不同于C.Morgan等人刻畫健康條件的方法，成功地建立起概率謂詞轉(zhuǎn)換器與確定性概率狀態(tài)轉(zhuǎn)換器之間的等價(jià)性。在非確定概率程序方面，我們研究了天使非確定概率程序，提出了預(yù)健康的概念，證明預(yù)健康的概率謂詞轉(zhuǎn)換器與非確定概率狀態(tài)轉(zhuǎn)換器之間等價(jià)的一個(gè)方向。 第二部分：可能性計(jì)算的語義模型 本部分我們利用可能性賦值的概念給出一種可能性計(jì)算

5、模型，目的是為了研究具有可能性的程序語義。證明可能性冪域函子是定向完備偏序集范疇Dcpo上的一個(gè)monad函子．進(jìn)一步利用可能性積分證明可能狀態(tài)轉(zhuǎn)換器語義與健康的可能謂詞轉(zhuǎn)換器語義之間的等價(jià)性．同時(shí)將可能性與天使非確定性放在一起加以討論，得到它們有關(guān)的萬有性質(zhì)。 第三部分：精細(xì)演算 精細(xì)演算是Dijkstra最弱前置演算的擴(kuò)充與進(jìn)一步發(fā)展．近來，應(yīng)明生教授研究了概率程序的精細(xì)演算．基于應(yīng)明生教授的一些想法，這部分本研究分

6、為概率精細(xì)與可能性精細(xì)兩個(gè)方面。一方面，我們討論了亞概率程序的概率精細(xì)與概率正確性．這兩個(gè)概念分別反映了一個(gè)亞概率程序被另一個(gè)亞概率程序精細(xì)的程度以及一個(gè)亞概率程序三元組的正確度．證明亞概率程序間的概率精細(xì)可以通過概率正確性來描述．另一方面，我們提出了一種基于可能性的程序精細(xì)演算模型，目的是為了進(jìn)一步形式化可能性計(jì)算．引入可能信念邏輯，得到了基本謂詞轉(zhuǎn)換器之間的對偶．給出了可能謂詞轉(zhuǎn)換器是可能天使更新與可能魔鬼更新的充分必要條件。進(jìn)一步