對稱π演算和Lambda-π演算的綜合-對稱λ-π演算.pdf

1、摘要計(jì)算機(jī)軟件理論發(fā)展至今，研究焦點(diǎn)己從順序計(jì)算轉(zhuǎn)移到了并行計(jì)no(of序計(jì)算可以很容易地理解成函數(shù)式計(jì)算，而入演算模型則是函數(shù)式計(jì)算的最佳形式化工具。利用它，人們很容易就解決了函數(shù)式順序計(jì)算中的許多理論問題，并在實(shí)踐中得到了印證。并行計(jì)算則因其本身的復(fù)雜性和不確定性，從一開始就對理論工作者提出了很高的要求。從Milner提出CCs以來，各種從不同側(cè)面反映并發(fā)本質(zhì)的模型被相繼提出。在這些模型中，進(jìn)程代數(shù)(如GCS)因概念簡潔，可用的數(shù)學(xué)

2、工具豐富，得到了廣泛的研究。二一演算是對CCs的繼承和發(fā)展。從進(jìn)程代數(shù)的觀點(diǎn)來看，盡管用二演算來描述并行模型還有很多工作需要去研究，但是人們也同時(shí)著手探討用新的通信機(jī)制來描述并行計(jì)算，而且在試圖尋找一種將并行計(jì)算和順序計(jì)算直接統(tǒng)一起來的模型，這樣做可“息可以對進(jìn)程代數(shù)的研究帶來一些有益的”示，)本文提出了對稱“一演算，然后針對它進(jìn)行了系統(tǒng)、深入的研究，給出了A演算與二演算均是它的子語言的證據(jù)，我的主要的工作包括以下幾個(gè)方面:1.將兩類二

3、演算變體的特點(diǎn)綜合，給出了對稱不二演算的模型2.將二演算翻譯成對稱A，演算及給出了完全刻劃定理3.將八演算翻譯成對稱Arr演算以上所作的研究工作很有價(jià)值。對稱7演算無輸人輸出之分，Lambdaw演算中進(jìn)程與通道沒有區(qū)分。解這兩類二演算的特點(diǎn)綜合1可以得到一種新的二演算模型1稱之為對稱年二演算。本論文定義了這種新演算，并且給出它的操作語義，文中還將探討如何用它來翻譯二演算，針對二是對稱Ar的子語言，我們試圖給出能用對稱Aa演算來完全刻劃，

4、演算的證據(jù)在各種互模擬中我們考慮接口(Barbed)互模擬，這是因?yàn)榻涌诨ツM最能比較兩種語言的表達(dá)能力和區(qū)分能力。文中最后給出了A演算在對稱Ar演算中的翻譯，可以看到這種翻譯很方便直接，這主要得益于對稱Ar演算的簡潔性。關(guān)被詞:二一演算，進(jìn)程，通道，完全刻劃，互模擬Ti#言第一章引言1.1研究背景在計(jì)算機(jī)理論科學(xué)的領(lǐng)域中，用形式化的方法來研究計(jì)算是十分必要和有效的手段，形式化的方法可以為研究工作引人大量的數(shù)學(xué)和邏輯的方法，這是理論研究

5、中最為精確的研究手段。通常，用入演算來描述順序計(jì)算模型，這種方法已經(jīng)非常成熟并且在幾乎所有順序計(jì)算的實(shí)踐中得到了驗(yàn)證，反過來它又通過形式化的數(shù)學(xué)和邏輯方法為順序計(jì)算問題提供了驗(yàn)證手段。然而，并行計(jì)算以其獨(dú)有的復(fù)雜性和并發(fā)行為的不確定性給計(jì)算機(jī)理論工作者提出了巨大的挑戰(zhàn)。9()年代初，Milner提出了二演算，它是目前被研究得最為廣泛最為深人的一種并發(fā)演算模型。全世界許多學(xué)者和專家針對二演算紛紛以自己獨(dú)到的眼光提出了各種改進(jìn)的形式。其中引

6、人注目的還有一個(gè)問題就是:如何為順序與并發(fā)的計(jì)算模型提供一個(gè)一致性的形式化描述模型。傅育熙教授提出了一種對稱的二演算模型。無輸入輸出之分的對稱二演算[1)的特點(diǎn)是:從通信角度講，它沒有輸入與輸出之分，是在共有的通信通道上交換名字，是對稱的，其中關(guān)鍵點(diǎn)是它沒有抽象名.它的改進(jìn)之處在于將，演算中的輸入輸出兩種行為用一種來表達(dá)，大大簡化了二演算，為對它的更深入的研究作了很好的鋪墊。傅育熙教授還就順序與并發(fā)計(jì)算的一致性描述模型提出了一個(gè)Lanl

7、bd。二演算的模型。通道(Channel)與進(jìn)程(Process)統(tǒng)一的Lambda二演算[2][3]的特點(diǎn)是:通道與進(jìn)程是不區(qū)分的，都被看成是同一種名，都可以通過通信進(jìn)行交換或轉(zhuǎn)移。這樣的處理大大增強(qiáng)了二演算的描述能力，通過將，中的通道與進(jìn)程看成同一種名，很容易證明A演算是Lambda一二演算的子語言。本文就是在這樣的背景下，提出了將對稱二演算與Lambda一二演算兩者綜合起來，得到一種新的演算模型，對稱aa演算。它充分利用了這兩種演