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

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

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

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

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

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

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

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