Matthew Hennessy

A Distributed Pi睠alculus

2007, 259pp.

Hardcover

ISBN 9780521873307

M.亨西尼著

從利用自動(dòng)柜員機(jī)在我們的銀行戶頭取出現(xiàn)金到在線購(gòu)物網(wǎng)站，交互式系統(tǒng)滲入了我們的日常生活。分布式系統(tǒng)很快已成為計(jì)算機(jī)科學(xué)中的標(biāo)準(zhǔn)，支持這些系統(tǒng)做為基礎(chǔ)的技術(shù)，包括軟件和硬件都是很先進(jìn)的。但是為確保這些系統(tǒng)正確行為的設(shè)計(jì)原理和技術(shù)卻處于更為原始的階段。為這些研究活動(dòng)準(zhǔn)備堅(jiān)實(shí)的基礎(chǔ)，系統(tǒng)行為數(shù)學(xué)模型及相關(guān)的推理工具已經(jīng)成為過去20年中理論計(jì)算機(jī)科學(xué)的中心課題。一種方法是形式演算的設(shè)計(jì)，利用它來描述和研究作為交互式系統(tǒng)基礎(chǔ)的基本概念。通訊系統(tǒng)演算可能是為了研究交互式系統(tǒng)提出的第一個(gè)演算。這種演算由兩部分組成，一部分根據(jù)它們的結(jié)構(gòu)描述系統(tǒng)的簡(jiǎn)單形式語言，它們是怎樣從單個(gè)但是互相連接的組件構(gòu)成的；第二部分語義理論，該理論尋求依據(jù)這些系統(tǒng)與用戶交互的能力對(duì)用該語言所描述的系統(tǒng)行為的理解。盡管CCS是成功的，但它只能描述非常有限范圍的系統(tǒng)，最重要的約束是對(duì)于任何一個(gè)具體的系統(tǒng)，它的連接布局必須是不變的。然而現(xiàn)代交互式系統(tǒng)是高度動(dòng)態(tài)的，其中的計(jì)算實(shí)體或代理是高度移動(dòng)的。Pi－演算是從CCS發(fā)展而來的，它試圖至少涉及這些代理的某些動(dòng)態(tài)方面，特別是它包括了通訊信道的動(dòng)態(tài)生成，這樣使得作為基礎(chǔ)的連接布局能隨著系統(tǒng)的演化而變化。

本書的目的是對(duì)Pi－演算加以拓展，提出了一種叫做ADPI的分布式Pi－演算，它被用來描述在分布世界中移動(dòng)代理的行為，是建立在現(xiàn)有的形式語言Pi－演算的基礎(chǔ)上，增加了網(wǎng)絡(luò)層和一個(gè)基本的遷移結(jié)構(gòu)。本書開發(fā)了這些分布式系統(tǒng)行為的數(shù)學(xué)理論。在該理論中類型的存在發(fā)揮了主要的作用，它還在原則上說明了該理論怎樣用于開發(fā)保證分布式代理行為的驗(yàn)證技術(shù)。

本書共有6章。1.歸納原理；2.異步Pi－演算；3.應(yīng)用程序接口類型；4.API中的類型與行為；5.分布式異步Pi－演算；6.ADPI的行為等價(jià)。

本書的大部分內(nèi)容是作者在2005至2006年任英國(guó)皇家學(xué)會(huì)/利弗休姆子爵信托高級(jí)研究員時(shí)寫的。本書對(duì)于那些具有最低限度離散數(shù)學(xué)背景的計(jì)算機(jī)科學(xué)家是容易理解的。

胡光華，高級(jí)軟件工程師

(原中國(guó)科學(xué)院物理學(xué)研究所)

Hu Guanghua, Senior Software Engineer

(Former Institute of Physics,CAS)