1991年ACM圖靈演講:互動的要素

我非常榮幸獲得這個以 Pdan Turing 為名的獎項。也許 Turing 會很高興它頒給了一位在他母校劍橋大學 King's College 接受教育的人。1956年我在那裡寫下了我的第一個電腦程式；它是在 EDSAC 上完成的。當然 EDSAC 創造了歷史。但我慚愧地說，它並沒有吸引我進入計算領域，而且我忽略了電腦四年之久。1960年，我認為處理電腦可能比處理學童更為平和——那時我是一名教師——於是我向倫敦的 Ferranti 應徵了一份工作，當時正值 Pegasus 問世。面試時我被問到是否願意將一生奉獻給電腦。這個令人畏懼的想法從未在我腦海中出現過。嗯，我現在還在這裡，而且我有幸與電腦科學一同成長。

這個獎項提供了一個不尋常的機會，我希望也是一種許可，讓我能夠從個人的角度反思一條研究路線。我認為我應該抓住這個機會，因為在我的興趣中，有一條主線已經讓我全神貫注了20年。描述這種經歷肯定能產生洞見，前提是要記住它是一條個人的主線；科學是由許多這樣的主線編織而成，當每一條主線在成品織物中都難以追蹤時，科學就更加強大。

研究的主軸

我想要談論的主線是併發計算的語義基礎。我將首先解釋我如何開始認識到併發需要一種全新的方法，而不僅僅是擴展解釋循序計算的實體和結構的庫。然後我將討論我為尋找併發的基本結構所做的努力，這些努力受到循序語義經驗的指導。這項工作催生了 Calculus for Communicating Systems (CCS)。接著我將簡要討論這些結構在多大程度上可以用數學方式理解，就像循序計算可以用函數來理解一樣。最後，我將概述一種新的併發基本演算；它突顯了命名或引用的舊概念，這個概念迄今為止在計算理論中一直被視為次等公民。

多層次解釋與通用框架

我必須聲明。我反對這樣一種觀點，即對於像併發計算這樣龐大的事物的所有方面，可能存在一種唯一的概念模型，或者一種首選的形式系統。從某種意義上說，併發計算就是我們整個學科——它包含循序計算作為一個行為良好的特殊領域。我們需要許多解釋層次：為不同的專業領域需要許多不同的語言、演算和理論。應用是多種多樣的：保險公司中的資訊流、網路通訊、飛行控制電腦之間的即時通訊、資料庫中的併發控制、平行物件導向程式的行為、併發邏輯程式設計中變數的語義分析。我們當然不期望所有這些的討論和分析術語都相同。

但還有一個補充的觀點要提出，那就是：電腦科學家，以及所有科學家，都在尋求一個通用框架來連結和組織多個解釋層次；此外，這個通用框架必須是語義性的，因為我們的解釋（包括程式）通常使用形式語言——而且常常是混合形式系統，以處理我們業務中的大型異質系統。對於規模小得多的循序計算世界，一個通用的語義框架建立在數學函數這個核心概念之上，並以函數演算的形式正式表達——Alonzo Church 的 λ 演算就是著名的原型。可以說，函數是我們討論循序程式設計語義時呼吸空氣中的一個基本成分。但對於併發程式設計和一般的互動系統，我們還沒有可與之媲美的東西。

那麼，我們從哪裡找到併發的語義成分，或者如何提煉它們呢？這是一個宏大的目標，因為，正如我之前所說，併發是無處不在的。我相信，解釋併發計算的正確想法只會來自邏輯和數學模型與實際經驗的恰當提煉之間的辯證法。我進行一部分辯證。我試圖調和兩者之間的對立——因為它確實似乎是一種對立——一方面是函數演算所體現的純粹和簡單，另一方面是程式設計和通訊的現實所啟發的關於併發和互動的一些非常具體的想法。

互動的要素

在整個七十年代，我開始相信，併發和互動的理論需要一個新的概念框架，而不僅僅是對我們認為循序計算中自然的東西的細化。通常，給人信念的經驗並非事先規劃且不深刻。但我想回憶我的一個經歷，因為它在這裡以多種方式服務於這個主題。它發生在我試圖擴展 Scott-Strachey 方法來處理程式語言語義時，這種方法完美地處理了最複雜的循序語言，但也要處理併發語言。嘗試必須進行，而且我對成功持樂觀態度。

在那種方法中，一個沒有中間輸入/輸出的循序程式，完美地由一個從記憶體到記憶體的函數來表示。(我使用「記憶體」一詞指代一個記憶體狀態，包含所有程式變數的值。) 但 Dana Scott 發展了領域理論——一種特殊性質的偏序集——它為 λ 演算提供了意義，λ 演算是最主要的函數演算。因此，在 Scott-Strachey 方法中，命令式程式的意義在由方程式給出的領域中：

Program Meanings = Memories --> Memories.

一切都與這個領域運作良好，原因在於：對於任何循序語言中的每個語法結構，都有一個抽象操作，該操作從其組成程式的意義來構建複合程式的意義。也就是說，語義是組合性的——一個基本屬性。

現在，併發引入的事物之一是非確定性。(當然，沒有併發也可以有非確定性，但在我看來，是併發將非確定性強加給你。) Plotkin 透過他的冪域構造來處理非確定性，這是一種領域理論的絕技。對於任何合適的領域 D，它提供了一個冪域 P(D)，其元素是 D 的子集。因此，考慮到非確定性，我們可以將程式的意義重新定義為：

Program Meanings = Memories --> P(Memories)

——本質上是記憶體上的關係。這種語義對於那種透過向循序語言添加「不管」分支而獲得的非確定性語言來說是完全組合性的。

但併發帶來了一個衝擊；如果你可以將子程式結合起來並行運行，組合性就會喪失，因為它們會相互干擾。準確地說，存在具有相同關係意義的程式 P1 和 P2，但當它們各自與第三個程式 Q 並行運行時，它們的行為不同。一個簡單的例子是：

Program P1 : x := 1 ; x := x + 1 Program P2 : x := 2

在沒有干擾的情況下，P1 和 P2 都透過將 x 的值替換為 2 來轉換初始記憶體，因此它們具有相同的意義。但如果你採用程式

Program Q : x := 3

並依次與 P1 和 P2 並行運行：

Program R1 : P1 par Q Program R2 : P2 par Q

那麼程式 R1 和 R2 具有不同的意義。(即使賦值語句是不可分割執行的，R1 可能最終 x 等於 2、3 或 4，而 R2 只能最終 x 等於 2 或 3。) 因此，一個組合性的語義必須更精細；它必須考慮到程式與記憶體互動的方式。

事後看來，這種現象 hardly 令人驚訝。但是，如果我們不能使用記憶體上的函數或關係來解釋併發程式，那麼我們可以使用什麼呢？嗯，自然可以給關係意義一個更細的粒度，這樣它就能記錄程式從一次記憶體訪問到下一次訪問所做的每一步——這可以在不離開領域理論的情況下完成。但這個現象教了我一個更激進的教訓：一旦記憶體不再受單個主控，那麼程式與記憶體關係的「主控對從屬」(或者：函數對值) 的觀點就變成了一種虛構。一句古老的諺語說：伺候兩個主控的人，一個也伺候不好。最好發展一個互動系統的通用模型，其中程式與記憶體的互動只是對等體之間互動的一個特例。

視覺化有所幫助。圖 1 非正式地展示了共享記憶體模型。它僅透過使用不同形狀的節點來表示元件之間的主動/被動區別。(我在圖中將始終使用方塊表示主動程序，圓圈表示被動事物。) 當然，一般來說，程式使用多個變數，所有這些變數都儲存在 M 中。

Figure 1. The shared memory model 圖 1：共享記憶體模型

為了消除主動/被動區別，我們將 M 提升到程序的地位；然後我們將程式變數 x, y, ... 視為程式與記憶體之間互動通道的名稱，如圖 2 所示。

Figure 2. Memory as an interactive process 圖 2：記憶體作為互動程序

現在，更一般地思考，讓我們使用記憶體來說明程序——任何種類的——都可以組合起來形成更大的程序。在循序世界中，可以維持記憶體是單塊的便利虛構；但在併發程式設計中這很不現實，因為記憶體的不同部分可以同時被訪問。因此，我們更進一步，如圖 3 所示，將每個記憶體單元視為一個程序，比如 X，透過一個適當命名的通道連結到一個或多個程式（它們本身就是程序）。

Figure 3. Memory as a distributed process 圖 3：記憶體作為分散式程序

軟體工程師很可能抵制這種同質處理，並堅守共享記憶體模型；這對他們很重要，因為它允許一種有助於編寫正確程式的方法論。理論家可能會反駁說，在一個基本模型中容忍兩種實體，而只需要一種就足夠了，這是科學上的詛咒；他們也可能會指出，共享記憶體模型的主動/被動區別不容易容納混合體，例如你在不使用時會自行重組的資料庫。而這兩種態度都是正確的。

所以讓我們回憶起對許多層次解釋的需求。William of Occam 反對實體的過度增殖，但僅限於超出所需的部分——procter necessitatem！電腦系統工程師迫切需要豐富的本體論；他們歡迎能夠為不同目的使用不同的概念和模型。例如，共享記憶體模型是他們工具庫的自然組成部分。但電腦科學家也必須尋找隱藏在各種模型之下的基本事物；他們不僅對個別設計和系統感興趣，還對其組成部分的統一理論感興趣。為了在併發的基本模型中實現統一，所有互動——以及因此所有互動者——必須被同等對待；這就是我為什麼稱這項工作為「互動的要素」。

為了避免給人留下我只考慮程式、記憶體或電腦系統的印象，我在圖 4 中展示了一個行動電話網絡，其中通道是無線電通道。通訊協定允許汽車切換通道到最近的基地台，整個系統由中央監控和控制。現在，我們希望我們的結構能夠在離散層次完美地描述這些系統；互動的要素不應該僅限於電腦系統。

Figure 4. A mobile telephone network 圖 4：行動電話網絡

我一直在說的很多東西，在六十年代 Carl-Adam Petri 就已經很清楚了，他是離散併發系統科學建模的先驅。Petri 的工作在併發理論的根基處佔有穩固的地位。他宣稱他的網理論的目標——在最低層次——是公正地作為物理世界的模型和計算的模型。對他來說，記憶體暫存器和程式已經由同一種類型的對象——即網——來建模，這打破了主動/被動的二分法。網理論的概念框架盡可能簡潔。這確實為個別系統的分析和系統的分類帶來了清晰和深度。

靜態結構

除了質疑構成系統的實體的主動/被動二分法之外，併發在原始結構方面要求一種新的方法。我一直想推進的，作為 Petri 網理論的補充，是系統的合成或組合觀點，這在程式設計中很熟悉。這本質上是一種代數觀點，因為代數是關於結構及其意義的。對於循序計算，這種觀點體現在 λ 演算中，與——例如——經典的自動機理論形成對比。

為了處理併發，我們不應該僅僅向循序計算的語言和理論添加額外的內容——特別是構建從較小系統構建較大系統的額外結構。如果我們這樣做，那麼我們當然會擁有比以前更多的原始結構。這是一種實現「併發比循序更複雜」預言的絕佳方式。而且這也常常被做到。嗯，併發可能更複雜，但我們不應如此輕易地放棄。我們應該將自己限制在對併發本身而言必不可少的結構上；這樣我們確實可以將循序計算視為更高層次、更具體的解釋。

考慮循序組合 P; Q——這個熟悉的冒號，是循序命令式程式設計的基本膠水。為了實現併發，我們應該保留循序組合並僅添加並行組合嗎？嗯，對於程式語言來說，我們可能想這樣做，因為我們必須給程式設計師他們熟悉的工具以及新的東西。但是我們應該在一個基本演算中這樣做嗎？我相信不應該；因為循序組合實際上是並行組合 P|Q 的特例，當這個結構被恰當地理解時。我將它理解為 P 和 Q 彼此並行運行，並以我們設計好的方式互動。因此，循序組合是唯一在 P 結束而 Q 開始時才發生互動的特殊情況。在這裡允許一種特殊的互動會違反我們的原則，即在基本模型中，所有互動都是同一種類型的。

正是這種世俗的觀察阻止了我試圖從循序性進行外推，並促使我嘗試在一個新演算中捕捉一組對併發基本結構。這就是我理解 Church 對循序計算所做的事情，透過 λ 演算。我們希望與函數演算匹配，不是透過複製其結構，而是透過模仿其兩個屬性：它是合成性的——我們在其中構建系統，因為術語的結構表示程序的結構；它是計算性的——其基本語義概念是計算步驟。它的另一個屬性，即它具有一個公認的數學解釋，我們目前還無法匹配（儘管正在取得良好進展）。但 Church 自己理解他的 λ 演算術語是該詞計算意義上的函數；他當時還沒有 Scott 的指稱。總結一下：對我來說，函數演算是一個範例——但不是一個平台——用來構建通訊系統的演算。

我剛才指出，程序的循序組合是並行組合的特例。事實上，在設計 CCS 時，我堅持只用一個組合子來組合互動或共存的程序。這看似要求很高，因為我也堅持將記憶體暫存器建模為程序，所以這個相同的組合子必須能夠將它們組合成一個記憶體，組合使用它們的程序，並組合程序與記憶體。但一個組合子確實足夠了，這是因為所有互動確實可以用相同的方式處理。例如，我們可以將圖 3 的系統寫成

P|M|Q 其中 M = X|Y|Z

或寫成

νx(X) | νy(Y) | νz(Z) | P | Q

即使程式 P 和 Q 除了透過記憶體互動之外還以其他方式互動，或者 X、Y 和 Z 不僅僅是儲存暫存器，而是程序和遠程記憶體之間的媒介，也會使用完全相同的表達式。表達式的形式與這五個程序的性質無關。隨著這個單一組合子成為核心，演算的代數性質開始顯現。並行組合背後的直覺是我們只是將系統的元件組裝在一起——因此我們期望組合子是結合的和可交換的。這就是為什麼我們的表達式中沒有括號。成員的每種不同排序和括號表示系統到子系統的不同劃分。

我們的代數如何更明確地反映元件之間連結引起的結構？我們首先注意到，圖 3 中的元件 P、Q、x 等本身將是程序表達式；此外，通道 y 僅連結 P 和 Y，因為這些將是通道名稱 y 僅出現的表達式。我們這裡不給出像 Y 這樣的暫存器的程序表達式；足以說每個這樣的表達式將確定其位置作為通道名稱。因此我們可以說，從 P 的觀點來看，名稱 y 定位了單元 Y。現在圖 3 非常清楚地展示了這種位置概念；我們也希望我們的代數能夠捕捉這個概念。為此，我們引入一個額外的組合子來確保暫存器 Y 僅對 P 可訪問——即，通道 y 對它們是局部的。我們稱這個新組合子為限制；例如，在表達式

νy(Y|P)

中，通道 y 被限制用於 Y 和 P 之間。希臘字母 ν 的使用部分是因為與 "new" (新) 的雙關語；實際上，限制只是程式設計中局部變數宣告概念的提煉。因此對於圖 3 的整個系統，我們可以更準確地寫成

νx(νy(Y|P) | νz(Z|Q) | X)

這類表達式很好地代表了一般互動系統的空間或靜態結構，儘管我們只為程式和記憶體進行了說明。像圖 3 這樣的圖，我們可以稱為流圖，是相當形式化的對象。事實上，限制和組合遵循某些方程式，這些方程式定義了流圖的代數理論。

動態結構

現在讓我們來看看這些系統的動態方面：它們的行為。事實上，正是在動態中，我們可以將 λ 演算的循序、層次控制與 CCS 的併發、非層次控制進行對比。在 λ 演算中，所有計算都歸結為一件事，稱為歸約——將參數傳遞給函數的行為；我們可以稱之為 λ 演算行為的原子。同樣地，一個互動——單個資料在程序之間的傳遞——是 CCS 中行為的原子。我們現在將看到這如何允許夥伴之間的對稱性，以及它如何反映社區中每個程序都具有持久身份的概念。

我們將透過每個演算的基本計算規則來考察這種對比。在每個演算中，系統都使用一個二元組合子來構建。在 λ 演算中，組合子稱為應用，既不具有交換性也不具有結合性。當一個術語 M 應用於另一個術語 N 時，

M(N)

第一個術語 M——運算元——掌握控制權。運算元致力於接收 N，即被運算元；如果並且當運算元呈現為抽象 λx.M[x] 的形式（其中方括號表示 M 可能包含約束變數 x）時，則符號 λ 表示運算元的控制區域，並將發生以下歸約：

(λx.M[x])(N) ~> M[N]

(其中右邊的括號表示 N 已替換了 M 中的 x)。這是 λ 演算的基本計算規則，即函數應用的動態；對許多人來說，它更熟悉的形式是 Algol 60 的複製規則，該規則是從它派生的。圖 5 以圖形方式表示了這個操作；請注意，被運算元 N 由一個圓圈表示，在歸約中是一個被動資料——它只有在 M 允許時才會稍後作為運算元取得控制權。

Figure 5. The λ-calculus reduction (λx.M[x])N -> M[N] 圖 5：λ 演算的歸約 (λx.M[x])N -> M[N]

另一方面，在 CCS 中，當兩個術語 P 和 Q 並行組合時，

P|Q

兩者都掌握控制權。P 可能從 Q 接收消息，就像 Q 可能從 P 接收一樣。一個術語可以採取兩種所謂的行動，使其能與另一個術語互動。當一個夥伴採取輸入形式 λx.P[x] 而另一個採取輸出形式 $\bar{a}V$.Q 時，我們就有了組合

λx.P[x] | $\bar{a}V$.Q

其中夥伴具有所謂的互補控制區域 $a$ 和 $\bar{a}$——即通道名稱 $a$ 的正極和負極。然後可能發生以下互動：

λx.P[x] | $\bar{a}V$.Q ---> P[V] | Q

這是一種夥伴行動的同步。

但關鍵是，在併發中存在許多通道，而不僅僅一個；因此，表示 λ 演算中單一控制區域的符號 λ，現在只成為許多通道中的一個，這些通道可能是同時活躍的。CCS 使用簡單的名稱 a, b, c, ... 來表示這些通道。因此，我們得到了 CCS 的基本計算規則，如圖 6 所示。計算僅包括這個單一規則的迭代，重複轉換表達式；在任何階段，表達式的結構代表系統的空間配置。圖 6 中的圖顯示了動態行為——被動資料的傳遞——疊加在表示空間配置的流圖上。

Figure 6. The CCS interaction ax.P[x] | aV.Q -> P[V]|Q 圖 6：CCS 的互動 ax.P[x] | $\bar{a}V$.Q -> P[V]|Q

讓我們更仔細地看看這裡的區別。首先，在 λ 演算的情況下，第二個夥伴僅僅是一個被動資料，但在 CCS 的情況下，它交出它的資料 V 並繼續獨立存在。這正是允許併發程序之間持續互動，每個程序都保持其身份的原因。其次，並行組合具有交換性；P|Q 與 Q|P 意義相同。在 CCS 中，與 λ 演算不同，任一夥伴都可以充當接收者——而且該夥伴稍後可能成為發送者。第三，並行組合也具有結合性；結合交換性，這使得互動紀律擺脫了術語結構的束縛，術語結構在 λ 演算中代表層次控制。正如我們在程式與記憶體互動的例子中看到的，控制紀律現在由哪些通道 a, b, ... 連結哪些程序來決定。

這些細節有些技術性。但焦點在於：併發與循序計算之間的區別可以集中在各自演算的單一基本計算規則中。透過修改 λ 演算中的歸約概念，我們為併發程序獲得了一種互動規則，這是我們在函數模型的純粹性與真實併發系統的動態性之間進行綜合的第一階段。

將同步互動作為程式設計原語的想法在我以代數形式表達它之前就已經被 Tony Hoare 所知。這些步驟是獨立完成的，動機不同，這證明這個想法是自然的。Hoare 將這個想法納入他的程式語言 CSP 中，後來與同事一起圍繞它發展了一個理論。它為 Ada 的 rendezvous 機制提供了基礎，並成為程式語言 Occam 中的互動原子。我的貢獻是將互動作為代數演算的基石。八十年代發展起來的程序代數，如 CCS、CSP 和 Bergstra 和 Klop 的 ACP，一直是許多語義研究的主題。它們也已成為，或演變成，積極使用的設計工具；特別是，規範語言 Lotos 已被廣泛應用於通訊協定。

語義

我想消除這樣一種擔憂：併發，至少在我處理它的方式下，是極端具體和機械的。難道沒有一些抽象的數學事物隱藏在其背後嗎，我們應該將「程序」一詞保留給這些事物——而不是將我們的代數表達式冠以那個名字嗎？畢竟，我們已經習慣於在抽象意義上使用「函數」這個詞，因此當我們指向 λ 演算中的一個表達式並說「那個函數」時，人們通常理解我們指的是「那個表達式所指稱的數學函數」。如果一個表達式沒有公認的指稱，我們可能會感到不舒服。

程序語義有大量且不斷增長的文獻。它並不簡單；但已經取得了一些令人興奮的進展。我之前談到 Scott 領域在併發程式中的可能應用，事實上，對程序代數研究了各種有趣的領域。還有許多研究關注程序的意義如何由其可觀察行為決定。這個想法是：觀察一個程序 precisely 是與它互動，並且只有當我們無法透過觀察區分兩個系統——比如 CCS 中的兩個程序術語——時，它們才應該具有相同的指稱。這項研究主要致力於分類可以進行的更強和更弱的可觀察區別，以及在每種情況下的數學表徵。已經取得了很大的成就；還有很多工作要做。

這些關於觀察的評論到目前為止同樣適用於循序程序；但是——正如所料——併發引出了其自身的問題。一個重要的主題是因果獨立性的概念，這在 Petri 網理論中是核心。現在，兩個程序——每個都包含併發元件——對於外部觀察者來說可能是 indistinguishable 的，但它們在觀察到的行動之間的因果關係上卻不同。我可能會觀察你從樹上摔下來，然後觀察到救護車到達，但我仍然不知道前者是否導致了後者。因此，觀察語義忽略了因果關係。但是也有很好的理由建立尊重因果聯繫的語義模型——例如 Nielsen 等人的事件結構。這個主題太複雜，無法在此處理；我提及它僅僅是為了表明併發確實引出了新的語義問題。

無論研究何種數學模型，我認為程序演算為這項研究提供了一個重要的視角。只有當併發系統的語義理論——最終——變得既抽象又形式化時，許多人才會滿意。但要達到這個目標，我們首先必須提煉互動動態的本質；這就是像 CCS 這樣的形式程序演算試圖做的事情。

值

我們現在開始在函數範例和互動現實之間進行綜合的第二階段。這一次我關注的是在它自己的概念框架內使併發演算 fully expressive。首先，我需要解釋 λ 演算在這方面如何成功，而 CCS 和類似的併發演算卻有所不足。稍後我們將找到補救方法。

人們經常非正式地使用 λ 演算，僅僅是為了在熟悉的資料上導出新的運算元。在討論算術時，他們會寫

f = λx (x^2 + 1)

或者

F = λfλx (f(x) + 1)

——也就是說，他們混合了 λ 演算和算術的結構，不願意將一個編碼到另一個中。這樣處理，λ 演算就像一些計算腳手架，真正的工人（如數字、運算元如平方、相加或微分）在上面爬上爬下。

這種 λ 演算的輔助使用非常自然，但很難在函數框架內構成一個自包含的計算模型。每次我們添加新的資料結構類型——如陣列、列表、樹——實際上我們都在擴展演算。但對於理解程式語言來說，重要的是我們用來解釋它們的基本模型應該盡可能同質和完整，不需要特殊的擴展。

非常了不起的是，λ 演算確實實現了這種同質性和完整性。在其純粹形式中，它確實具有完整的能力來表示資料結構並用它們進行計算；我們可以用單獨的腳手架做一切事情。Church 為算術證明了這一點；Böhm 等人已將其擴展到其他形式的資料結構。此外，還存在類型紀律——特別是 Girard-Reynolds 二階 λ 演算——這允許以一種受控的方式完成這項工作，為分析循序程式語言及其各自的類型紀律構建一個統一的框架。

那麼，併發呢？大多數併發形式系統也提供了一種不同種類的腳手架，值和運算元可以在上面移動；這些值和運算元與腳手架本身完全不同。再次看看 CCS (圖 6)；在那個互動中，資料 V 實際上是一個代表數字之類東西的表達式——與程序表達式 P 截然不同的一種類型。為了強調這一點，圖 7 顯示了 CCS 中 Double 這個程序的定義，它重複地透過通道 a 輸入一個數字，並透過通道 b 輸出該數字的兩倍。這個簡短的定義中，竟然包含不少於五種不同的東西：程序 (例如 Double)、通道 (a, b)、變數 (x)、運算元 ($\times$) 和值表達式 (2 $\times$ x)。而且其中四種（除了運算元）已經出現在 CCS 的基本計算規則中——見圖 6。這種混雜程度難道不過分嗎？

Figure 7. A doubling process in CCS 圖 7：CCS 中的一個倍增程序

嗯，在高級程式語言或規範語言如 Lotos 中，這是完全允許的，用戶期望一個豐富且冗餘的工具包。但對於真正基本的演算，情況就不那麼舒適了。一個基本演算應該施加盡可能少的分類，因為不同的更高級別的解釋會施加不同的分類。現在，純粹的 λ 演算只由兩種東西構成：術語和變數。我們能否為程序演算實現同樣的經濟性？Carl Hewitt 和他的 Actors 模型很久以前就回應了這個挑戰；他宣稱一個值、一個值上的運算元和一個程序都應該是同一種類型的東西：一個 actor。這個目標給我留下了深刻的印象，因為它意味著我們已經討論過的表達式的同質性和完整性。但直到很久之後，我才看到如何在代數演算方面實現這個目標。我知道 CCS 有所不足；但我希望它能產生洞見，找到剩下的路。

命名 (Names)

最近，在 Engberg 和 Nielsen 的重要洞見基礎上，我的同事 Joachim Parrow 和 David Walker 與我一起找到了一種具有與純粹 λ 演算相同的內部完整性的演算。它也很簡潔；在代數程序演算的傳統中，很難看出它如何能夠進一步簡化。我們稱之為 π 演算 (pi-calculus)，而關鍵思想是命名或引用。(或許我們不應該驚訝於透過更加重視命名來獲得更強的表達完整性；因為系統中的併發活動蘊含著其組成部分的獨立身份，而利用這種身份需要一種識別手段。)

命名，儘管在某些模型中（例如函數模型）被很好地隱藏起來，但在實際計算中卻是普遍存在的。想想它有多少變體。本質上，它只是提供對…好吧，任何事物的訪問；但我們傾向於在不同上下文中以不同方式看待變數、地址、位置、指標、通道——真正原因在於它們提供了對不同事物的訪問。在古老和現代的程式語言中，這種多樣性令人驚訝：Algol 60 的變數、Pascal 的指標、Ada 或 Occam 的通道、邏輯程式設計的邏輯變數、物件導向程式設計的物件引用等等。因此，本著 Hewitt 的精神，我們的第一步是要求所有由術語指示或由名稱訪問的事物——值、暫存器、運算元、程序、物件——都是同一種類型的東西：它們都應該是程序。從那以後，我們將透過名稱訪問視為計算的原始材料；然後我們要做的就是定義程序——本身可訪問——如何操縱訪問的方法。

要感受這個激進的變化，再看看 CCS 的計算規則，圖 6。在那張圖中，a、x 和 V 是不同種類的：通道、變數、值。在 π 演算中，通道和變數都將僅僅是名稱，而像 V 這樣的值將是一個由名稱定位的程序。關鍵的直覺是：一個值只是一種特殊類型的程序，一種可以重複成為相同觀察對象的程序。因此，表達式 V 現在確實與任何其他程序表達式屬於同一類別——並且要觀察它，必須有一個互動的通道。因此，值 V 將由一個名稱（例如 v）定位，就像記憶體單元 X（參見圖 3）由名稱 x 定位一樣。因此，在 π 演算中，計算步驟採取的形式是

aX.P[x] | V | $\bar{a}v$.Q -> P[v] | V | Q

計算步驟以圖形方式顯示在圖 8 中。在那張圖中，每個大寫字母代表一個程序，而每個小寫字母是一個名稱。還要注意的是，一個名稱可以作為通道被主動使用（例如 a），或者作為資料被被動提及（例如 x 和 v）。但在這個互動中，值 V 不再是參與者，甚至不是被動的。因此，呈現互動的最簡單方法如下：

aX.P[x] | $\bar{a}v$.Q ---> P[v] | Q

這最終是 π 演算的基本計算規則；它清楚地顯示了與 CCS 的關鍵區別——傳遞的資料現在「僅僅」是一個名稱，一種訪問方式。由於名稱沒有結構，計算步驟是真正的原子性——與 λ 演算不同，λ 演算中歸約的被運算元可能是一個複雜的資料。

$Figure 8. The π-calculus interaction ax.P[x] | V | $\bar{a}v$.Q -> P[v] | V | Q$ 圖 8：π 演算的互動 ax.P[x] | V | $\bar{a}v$.Q -> P[v] | V | Q

您對此很可能會產生兩種反應。首先，您可能覺得沒有什麼新鮮事；您一直都知道在實際、接地氣的計算中，傳遞的是指標而不是實際值。我回答說，如果互動的要素已經在程式設計中很熟悉，那就再好不過了——而且，我們也會在程式設計之外的領域使用它們。

其次，您可能會反對說，當我們開始以一種恰當抽象的方式思考計算時，所有這些機械的事情——指標之類的東西——都被掃到地毯下，並且應該好好隱藏起來。我同意，就此而言：儘管我們以一種很好的抽象方式思考循序計算，但在併發方面我們並沒有走得很遠。但這裡的關鍵是：一方面，當我們真正面對現實時，引用的概念拒絕保持隱藏；另一方面，它似乎難以進行理論處理——至少，它很少受到理論處理。我相信 π 演算開始解決這個僵局；它開始為引用提供一種易於處理的理論，從而也為併發和互動提供理論。

我不會詳細討論 π 演算。但為了顯示它在經濟性上與 λ 演算接近，讓我並列展示這兩個演算的語法（參見圖 9 和圖 10）。π 演算的 alternative action 結構意味著——如同在 CSP、CCS 或 Occam 中一樣——恰好會發生一個選擇。replication 結構 !P 大致意味著 P|P|...，你想要多少個 P 的拷貝並行運行都可以。我們已經說明了其他結構。

λ-calculus 語法	π-calculus 語法
變數 x, y, z...	名稱 x, y, z...
術語 M ::= x (變數)	行動術語 A ::= $\bar{x}z.P$ (透過 x 發送 z), $xy.P$ (透過 x 接收任何 y)
	術語 P ::= A$_1$ + ... + A$_n$ (選擇行動 n $\ge$ 0)
M$_1$(M$_2$) (應用)	P$_1$
$\lambda y.M$ (抽象)	$\nu y P$ (限制)
(y 的出現是綁定)	!P (複製)
基本計算規則 (λy.M$_1$[y])(M$_2$) ~> M$_1$[M$_2$]	(y 的出現是綁定)
	基本計算規則 $xy.P_1[y]

圖 9：λ 演算 圖 10：π 演算的簡化形式

為了看看這個演算如何運作，回憶一下圖 4 的行動電話網絡。我們將汽車和基地台之間的通道建模為兩個 π 演算名稱——一個用於通話，一個用於切換；參見圖 11。該圖顯示了 CAR 程序（關於這兩個通道是參數化的）的定義。CAR 有兩種選擇行動；它可以通話，或者如果基地台請求，它可以切換其通道。（這裡 CAR 是遞歸定義的，但遞歸可以從 π 演算的複製中導出。）該圖還顯示了定義整個網絡的表達式。其他元件的定義與 CAR 一樣容易。

Figure 11. The mobile telephone network in the π-calculus 圖 11：π 演算中的行動電話網絡

CAR(talk, switch) $\stackrel{def}{=}$ talk(word). CAR(talk, switch)
                + switch$\langle$t,s$\rangle$. CAR(t, s)

NETWORK $\stackrel{def}{=}$ $\nu talk_1 \nu switch_1 \nu talk_2 \nu switch_2 \dots$ (CAR(talk$_1$, switch$_1$) | STATION$_1$ | ... | CONTROL)

在這個例子中，汽車從一個基地台到另一個基地台的「移動」，與圖 10 中建模的值 V 的「移動」沒有什麼不同。因此，移動不限於值；各種程序之間的移動都可以用這種方式建模。π 演算的本質在於其對限制（建模空間配置，例如圖 3 的表達式 (1)）與配置的動態變化之間的相互作用的技術管理。

總結一下：即使在這種簡單形式下，也有幾個理由聲稱 π 演算的通用性：

它直接描述了改變配置的系統，例如行動電話網絡，或資源流動和分配的分散式作業系統。
它允許以統一的方式定義資料結構。因此，它支援像 CCS 這樣的程序代數作為更高層次的解釋。
存在將 λ 演算本身簡單翻譯成 π 演算的方法，該翻譯 faithful 計算行為。因此，它支援函數式程式設計作為更高層次的解釋。
它為物件導向程式設計以及其他程式設計範例提供了一個方便的語義基礎。
它像 λ 演算一樣，易於應用類型紀律；這將允許我們添加在易於處理的語義框架中如此重要的分類。

實際上，這五個屬性中最具體的第一個是我們首先努力實現的：描述移動性或變化配置的能力。這是塑造 π 演算的目標。令人意外的喜悅是發現移動性實際上是關鍵；一旦在技術上掌握了這一點，就發現其他屬性也存在，無需任何額外添加。

結論

我追溯了一條在尋求併發基本模型的研究主線，這條主線以循序範例為指導。我敢於談論語義是因為我一直希望正確的語義基元對我們所有人都很熟悉——不是因為我們思考它們，而是因為我們自然而然地以它們來構思我們的想法。無論我討論的基元是否正確，它們肯定具有那種熟悉的性質。

您可能因我 persistent 的還原論而感到冒犯；我一次又一次地用一個事物解釋另一個事物（一個值「僅僅」是一個程序，等等）。我看不出有其他方法可以達到既通用又易於處理的東西。但請允許我重複一遍：多層次的解釋是不可或缺的。事實上，更高層次的實體肯定比低層次的實體種類更多。

我聲稱 π 演算具有一定的通用性，儘管肯定有一些它不能直接處理的事情。它需要更多的研究。一項重要的任務是將它與 Hewitt 的 Actors 進行比較；我們遵循 Actors 直覺的地方肯定有一些一致之處，也有一些微妙的差異，例如對名稱的處理。更一般地說，π 演算是一個形式演算，而 Actors 模型在精神上更接近物理學的方法，旨在識別支配互動原始概念的定律。

最後，我們如何評估或測試一個計算模型，例如程序演算？從一個重要的意義上說，電腦科學確實是一門實驗科學，儘管——正如 Alan Newell 和 Herbert Simon 在他們 1975年的圖靈獎演講中指出的那樣——它可能不符合實驗方法的狹窄刻板印象，因為我們確實會在實際應用中測試我們的機器、語言和系統。但這樣，實驗測試也以間接的方式印證了我們的基本模型；因為我們最終是根據這些模型來設計、定義和分析我們的成果的。

除了外在的實驗測試之外，還有內在的數學測試。分離出對計算實踐真正基本的思想已經夠難了；找到那些同時允許易處理理論的思想就更難了。正是這兩種測試之間的衝突構成了我所闡述的辯證方法的基礎。我試圖展示如何從實踐中提煉，並由既定的邏輯範例指導，產生一個清晰定義的候選理論，該理論現在必須提交給更深入的數學測試和更深入的實驗測試。

我相信電腦科學在這種通用的科學方法上與物理學差異不大，即使在實驗標準上有所不同。像許多電腦科學家一樣，我希望有一門廣泛的資訊科學來研究現象——無論是人造的還是自然的——以與現有的豐富物理科學相匹配。如果我所描述的基本想法能夠朝這個方向邁出一小步，我將感到欣慰。

致謝

在這項努力中，我欠許多人的情，並感謝他們所有；特別是我的長期同事 Rod Burstall 和 Gordon Plotkin，我從他們那裡學到了很多東西並獲得了很大的支持；David Park，他在一個重要時刻對我產生了強烈的影響，並一直鼓勵我；以及 Tony Hoare、Carl-Adam Petri 和 Dana Scott，他們的工作一直是我的靈感來源。

來源與相關文獻

這裡引用了一些重要來源和相關論文，按章節列出。

Entitles. Tennent [36] 是 Scott-Strachey 語義方法的經典著作。Gunter 和 Scott [13] 是 Scott 領域理論的最新著作。它包含有關冪域的章節，冪域最初發表在 [32] 中。Petri 的博士論文 [31] 是關於 Petri 網理論的第一本出版物，Reisig [33] 是一本入門教科書。
Static constructions. Church [9] 是關於 λ 演算的第一本出版物；Barendregt [5] 提供了 λ 演算的最新完整著作。Milner [21] 首次論述了 CCS，並在後來的教科書 [22] 中更新了它。Milner 在 [20] 中介紹了流圖代數，這是一種程序的靜態代數。
Dynamic constructions. Hoare [16] 介紹了程式語言 CSP，並在教科書 [17] 中介紹了它的代數理論。Baeten 和 Weijland [4] 闡述了最初由 Bergstra 和 Klop 提出的程序代數 ACP。規範語言 Lotos 由 Brinksma [7] 設計。
Meaning. 一些重要的併發領域理論模型是 Brookes 等人的失敗模型 [8]、Hennessy 的接受樹 [14] 以及 Abramsky 的 bislmulation 領域 [1]。程序的 observation equivalence 由 Milner [21] 引入；Park [30] 透過 bislmulation 的概念將其置於更穩固的數學基礎上。Nielsen 等人的事件結構 [28] 將領域理論與 Petri 網的因果結構結合在一起。
Values. Böhm 和 Berarducci [6] 展示瞭如何將資料結構編碼到 λ-calculus 中。二階 (多態) λ-calculus 是在七十年代初由 Girard [11] 和 Reynolds [34] 獨立發現的。Hewitt Actors 模型的早期介紹見於 Hewitt 等人 [15]；關於 Actors 的最新書籍是 Agha [2]。Smalltalk [12] 可能是第一種將值——即使是最簡單的，如數字——視為接收訊息的物件的程式語言。
Names. Astesiano 和 Zucca [3] 研究了 CCS 的一個版本，其中通道（即，本文中的名稱）可以參數化值，從而允許一些移動性。Kennaway 和 Sleep [19] 將傳輸名稱作為訊息的思想構建到一種分散式作業系統語言中。1980 年，在 Arhus，Mogens Nielsen 和我曾試圖在 CCS 中代數地處理移動性，但失敗了。Engberg 和 Nielsen [10] 後來成功了，提供了一個具有動態重配置的程序演算的第一個代數處理（他們的報告未發表）。這些思想得到了 Milner 等人的改進和加強，形成了 π-calculus [25]。Milner [23] 提供了一個更通用形式的最新教程，也處理了類型結構。作為如何應用 π-calculus 的易懂示例，Orava 和 Parrow [29] 對簡化行動電話網絡進行了嚴格研究，我在此處使用了這個示例。λ-calculus 翻譯成 π-calculus 由 Milner [24] 給出。Walker [38] 首次探索了使用 π-calculus 為併發物件導向程式設計提供語義。Honda 和 Tokoro [18] 提供了一個適合非同步通訊的 π-calculus 的有趣變體，使其更接近於 Actors 和物件導向程式設計。實現移動性的另一種方法是允許程序本身在互動中傳輸。Nielson [27] 和 Thomsen [37] 研究了這些所謂的二階程序。Thomsen 還提供了一個將二階程序翻譯成 π-calculus 的方法，並證明它保留了操作行為。Sangiorgi 將這種翻譯推廣到 oo-order 程序，並證明適合的行為等價性在翻譯的兩個方向上都保留。他的結果由 Milner [23] 總結，並將出現在 Sangiorgi 的博士論文 [35] 中。這項關於更高階的研究加強了對 π-calculus 表達完整性的主張。
Conclusion. Newell 和 Simon 的圖靈獎演講 [26] 探討了電腦科學中實證研究的性質。

CR Categories and Subject Descriptors

D.3.1 [Programming languages]: Formal Definitions and Theory--semantics; D.3.2 [Programming languages]: Language Classifications--concurrent, distributed and parallel languages; object-oriented languages; F.1.2 [Computation by Abstract Devices]: Modes of Computation--parallelism and concurrency; F.3.2 [Logic and Meanings of Programs]: Semantics of Programming Languages--algebraic approaches to semantics; operational semantics; F.3.3 [Logics and Meanings of Programs]: Studies of Program Constructs--control primitives; functional constructs; F.4.1 [Mathematical Logic and Formal Languages]: Mathematical Logic--lambda calculus and related systems

General Terms

Languages, Theory

Additional Keywords and Phrases

CCS, interaction, naming and reference, pi calculus, process algebra, process calculus, reduction rule

About the Author

ROBIN MILNER 是愛丁堡大學電腦科學系的計算理論教授，他在那裡工作了 20 年。在此之前，他在 Stanford University 的人工智能實驗室研究了兩年。1986年，他成為愛丁堡電腦科學基礎實驗室的創始主任。目前，他持有 UK Science and Engineering Research Council 的五年期高級研究員職位。