函數(shù)式程序語言與傳值進程演算的關(guān)系研究.pdf

1、基于進程演算的程序語言設(shè)計與實現(xiàn)能夠?qū)⒉l(fā)理論的語法和語義理論研究真正應(yīng)用于實踐，并從根本上用高效的并發(fā)計算去替代傳統(tǒng)的順序計算，這是研究進程演算的一個關(guān)鍵問題。本文從經(jīng)典的順序函數(shù)式類型程序語言出發(fā)，層層深入地考慮現(xiàn)有成熟的程序語言與傳值進程演算之間的關(guān)系。首先，本文把PCF（編程可計算函數(shù)式語言）作為最初的切入點，去討論程序語言之間的表達能力關(guān)系，如果有了一個語法類型系統(tǒng)更簡單而且表達能力足夠強的語言，那么就便于去研究與進程演算之間

2、的關(guān)系；進一步的，在PCF的基礎(chǔ)上，本文討論并發(fā)高性能的函數(shù)式語言，研究其與進程演算之間的表達能力關(guān)系，這對于進程演算的應(yīng)用價值將會有更深的體現(xiàn)，對進程演算中的理論研究結(jié)果也將有更直觀的認識。
　　進程演算中現(xiàn)有應(yīng)用于程序語言的工作，主要是集中在π演算上，該傳名進程演算對于通信相對抽象。在程序語言的實現(xiàn)中也存在語法和等價關(guān)系的問題，現(xiàn)在基于π演算的程序語言性能上還有很大的不足，都需要更多的工作來找合適的進程演算模型和等價關(guān)系，以促

3、進進程演算在程序語言中的應(yīng)用。
　　本文工作的主要貢獻主要分為三個方面：
　　1.通過在按值歸約PCF引入完備和可判定的一階理論Presburger算術(shù)，本文提出了一個類型系統(tǒng)更簡單的語言PCFLC。從遞歸函數(shù)定義和程序語言表達能力兩方面來研究了PCFLC和按值歸約PCF的關(guān)系：遞歸函數(shù)定義方面，本文提出一個了PCF的極小化模型，給出了函數(shù)階的概念，并且證明了任意函數(shù)階的項都可以在PCFLC中定義出來；程序語言表達能力方面，

4、定義了類型程序語言中的值應(yīng)用互模擬等價關(guān)系，給出了一個從按值歸約PCF到PCFLC的編碼，這個編碼對于值應(yīng)用互模擬是完全抽象的，這部分工作表明了PCFLC和按值歸約PCF在操作語義上有相同的表達能力，而其語法簡單可以做為一個中間模型來比較程序語言的表達能力。
　　2.進程演算中實際應(yīng)用最多的模型是π演算，但現(xiàn)有π演算中的等價關(guān)系大多不適用于類型函數(shù)式語言的驗證，并且對于無限值的編碼也缺乏效率。傳值進程演算雖然抽象性低于π演算，但有

5、很好的方法來解決這些問題。因此本文提出了一個傳值進程演算的變種VPCΣ，并且引入了很多內(nèi)置的函數(shù)來使其對于實際程序的驗證和分析更加有效，然后給出了其的符號操作語義，并研究了VPCΣ的表達能力。
　　3.提出了一個VPCΣ中的通用解釋程序語言解釋框架。在此框架下，對并發(fā)函數(shù)式語言Erlang的核心語義進行了解釋，并給出正確性的證明，主要包括：參照Erlang及其核心部分core Erlang的手冊歸規(guī)范形式化了該語言的操作語義；對于

6、core Erlang語言，給出了一個VPCΣ中結(jié)構(gòu)化的解釋；證明了形式化操作語義和本文解釋之間在遲符號互模擬關(guān)系下滿足操作一致性，這對Erlang形式化工作一個非常好的性質(zhì)。而前人的工作中因為π演算中存在的問題大多沒有辦法給出這方面的結(jié)果，本文用一個并行通信的實例進行了說明。
　　總的來說，本文主要研究了如下問題：函數(shù)式語言中等價關(guān)系、表達能力關(guān)系；傳值進程演算的表達能力；傳值進程演算對并發(fā)函數(shù)式程序語言的通用解釋和正確性證明，