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

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

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

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

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

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