基于π演算的編程與表達(dá)能力研究.pdf

1、π演算是由Milner、Parrow和Walker基于CCS演算提出的能夠描述并發(fā)計(jì)算的模型。它是目前最重要的進(jìn)程演算,因此其它模型與它之間的表達(dá)能力比較有著重要意義:對(duì)于一些順序計(jì)算模型,如果能找到它們?cè)讦醒菟阒械木幋a,那么我們可以從并發(fā)的角度來(lái)研究順序計(jì)算；對(duì)于一些看似比π演算能描述更多現(xiàn)象的計(jì)算模型,比如能夠描述移動(dòng)設(shè)備上的移動(dòng)計(jì)算的Ambient演算,如果能夠找到它們?cè)讦醒菟阒械木幋a,那么就進(jìn)一步證明了π演算的表達(dá)能力。這樣的問(wèn)

2、題一些已有了答案,而一些仍然懸而未決,其中比較著名的就是λ演算在π演算中是否存在編碼的問(wèn)題。
　　 本文運(yùn)用基于π的編程提出一個(gè)解決上述問(wèn)題的統(tǒng)一方法:即將其它模型的語(yǔ)法語(yǔ)義用程序解釋,然后再用π演算進(jìn)行編程,從而得到由其它模型到π演算的編碼。這樣的方法簡(jiǎn)單直接,我們用這種方法找到了λ演算在π演算中的編碼,并研究了MA演算在π中的編碼。我們相信此方法可以用來(lái)解決更多模型與π演算之間的表達(dá)能力比較問(wèn)題。
　　 本文的主要貢

3、獻(xiàn)可概括為以下三個(gè)方面:
　　 1.基于π演算的編程與表達(dá)能力.π演算一直被人們當(dāng)成進(jìn)程代數(shù)的范例來(lái)研究,而從程序語(yǔ)言角度對(duì)π演算進(jìn)行的研究不多。事實(shí)上,π演算有著天生的編程能力,可以方便地對(duì)各種數(shù)據(jù)結(jié)構(gòu)進(jìn)行編程。本文使用π演算對(duì)鏈表、樹(shù)等常見(jiàn)數(shù)據(jù)結(jié)構(gòu)及其操作進(jìn)行了刻畫(huà)和研究。模型之間表達(dá)能力比較的重要方法之一就是設(shè)計(jì)從一個(gè)模型到另一個(gè)模型的編碼,可是往往由于模型之間的差別太大,這樣的編碼很難找到。大多數(shù)模型的對(duì)象都可以用程序來(lái)

4、解釋,歸約的發(fā)生就像程序運(yùn)行之后數(shù)據(jù)發(fā)生變化,本文以Spi演算、λ演算和Mobile Ambient演算為例,用程序直觀地解釋了它們的語(yǔ)法語(yǔ)義。從而提出一種基于π的編程方法來(lái)輔助設(shè)計(jì)其它模型在π演算中的編碼,使得原本很難聯(lián)系的模型之間的編碼變得簡(jiǎn)單直接。
　　 2.λ演算與π演算.上述方法的一個(gè)成功應(yīng)用就是回答了一個(gè)長(zhǎng)久以來(lái)未解決的問(wèn)題:λ演算到π演算上有沒(méi)有一個(gè)好的編碼?Milner早在1990年就給出了Lazyλ演算到π演算

5、的編碼,Lazyλ是一個(gè)受限制的λ版本,Milner提出疑問(wèn),他認(rèn)為完全λ演算的歸約規(guī)則要從π的角度去解釋是相當(dāng)難的,甚至可能不存在這樣的解釋。
　　 本文提出將λ演算中的項(xiàng)表示為二叉樹(shù),β歸約理解為對(duì)樹(shù)結(jié)構(gòu)的調(diào)整,我們可以發(fā)現(xiàn)λ演算的歸約規(guī)則比Lazyλ演算的歸約規(guī)則在樹(shù)結(jié)構(gòu)上更加對(duì)稱(chēng),更加優(yōu)美。在將二叉樹(shù)和對(duì)樹(shù)結(jié)構(gòu)的操作用π編程之后,我們就得到了從λ演算到π演算的編碼。為了證明編碼保持(preserves)并反映(refle