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

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

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

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

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

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

6、core Erlang語(yǔ)言，給出了一個(gè)VPCΣ中結(jié)構(gòu)化的解釋?zhuān)蛔C明了形式化操作語(yǔ)義和本文解釋之間在遲符號(hào)互模擬關(guān)系下滿(mǎn)足操作一致性，這對(duì)Erlang形式化工作一個(gè)非常好的性質(zhì)。而前人的工作中因?yàn)棣醒菟阒写嬖诘膯?wèn)題大多沒(méi)有辦法給出這方面的結(jié)果，本文用一個(gè)并行通信的實(shí)例進(jìn)行了說(shuō)明。
　　總的來(lái)說(shuō)，本文主要研究了如下問(wèn)題：函數(shù)式語(yǔ)言中等價(jià)關(guān)系、表達(dá)能力關(guān)系；傳值進(jìn)程演算的表達(dá)能力；傳值進(jìn)程演算對(duì)并發(fā)函數(shù)式程序語(yǔ)言的通用解釋和正確性證明，