Π演算

在理論電腦科學中，π演算（π-calculus或pi-calculus）是一種進程演算模型。

π演算允許通過通道本身傳遞通道名稱。得益於此，它可以描述計算過程中網路拓撲可能發生變化的並發計算系統。

π演算語法簡單，但表達能力很強（參見）。函數式程序可以被表示成π演算，這種表示強調了計算的對話本質，並與博弈語義建立了聯繫。π演算的擴展形式，如spi演算和應用π演算（applied π），在分析和推理密碼學協議方面獲得了成功。除了用於描述並發系統的最初用途外，π演算也被用於推理業務流程建模語言、分子生物學以及人工智慧中的智能體。

## 非形式化定義

π演算屬於進程演算家族——用於描述和分析並發計算屬性的數學形式體系。事實上，與λ演算類似，π演算極其精簡：它不包含諸如數字、布爾值、數據結構、變量、函數甚至通常的控制流語句（如`if-then-else`、`while`）等原語。

### 構造進程

π演算的核心概念是名稱（name）。該演算的簡潔性在於名稱兼具通信通道與變量的雙重角色。

演算中可用的進程構造原語如下（精確定義見下一節）：

- 並發（Concurrency），記作$P \mid Q$，表示進程/線程$P$和$Q$同時執行。
- 通信（Communication），包括：
- 輸入前綴（Input prefixing）$c\left(x\right).P$：表示一個進程，它先等待一個通過名為$c$的通信通道發出的消息，收到該消息後繼續執行$P$，並將接收到的名稱綁定到名稱x。通常，這模擬了一個等待網路通信的進程，或者是只能通過`goto c`操作使用一次的標籤`c`。
- 輸出前綴（Output prefixing）$\overline{c} \langle y \rangle.P$：描述了名稱$y$通過通道$c$被發射出去，隨後繼續執行$P$。通常，這模擬了在網路上發送消息或執行`goto c`操作。
- 複製（Replication），記作$!\,P$，可以看作是一個總是能創建$P$的新副本的進程。通常，這模擬了一個網路服務，或者是一個等待任意數量`goto c`操作的標籤`c`。
- 創建新名（Creation of a new name），記作$\left(\nu x\right)P$，可以看作是一個在$P$內部分配新常量x的進程。π演算中的常量僅由其名稱定義，且始終是通信通道。創建新名也被稱為「限制」（restriction）。
- 零進程（Nil process），記作$0$，是一個執行已完成並停止的進程。

儘管π演算的極簡性阻止了我們以通常意義上的方式編寫程序，但擴展該演算非常容易。例如，定義控制結構（如遞歸、循環和順序組合）以及數據類型（如一階函數、真值、列表和整數）都很容易。此外，已經有人提出了考慮到分布式或公鑰密碼學的π演算的擴展形式。由Abadi和Fournet提出的「應用π演算」，通過用任意數據類型擴展π演算，為上述各種擴展奠定了形式化的理論基礎。

### 一個小例子

下面是一個由三個並行組件組成的進程小例子。通道名稱x僅為前兩個組件所知。

$$\begin{align} <pre> (\nu x) & \; ( \; \overline{x} \langle z \rangle . \; 0 \\ & \; | \; x(y) . \; \overline{y}\langle x \rangle . \; x(y) . \; 0 \; ) \\ & \; | \; z(v) . \; \overline{v}\langle v \rangle . 0 </pre> \end{align}$$

前兩個組件能夠在通道x上進行通信，名稱y被綁定到z。因此，進程的下一步是：

$$\begin{align} <pre> (\nu x) & \; ( \; 0 \\ & \; | \; \overline{z} \langle x \rangle . \; x(y). \; 0 \; ) \\ & \; | \; z(v). \; \overline{v}\langle v \rangle . \; 0 </pre> \end{align}$$

注意，剩餘的y不受影響，因為它是在內部作用域中定義的。

第二個和第三個並行組件現在可以在通道名稱z上通信，名稱v被綁定到x。進程的再下一步是：

$$\begin{align} <pre> (\nu x) & \; ( \; 0 \\ & \; | \; x(y). \; 0 \\ & \; | \; \overline{x}\langle x \rangle . \; 0 \; ) </pre> \end{align}$$

注意，由於局部名稱x已經被輸出，x的作用域被擴展以覆蓋第三個組件。最後，通道x可用於發送名稱x。之後，所有並發執行的進程都將停止：

$$\begin{align} <pre> (\nu x) & \; ( \; 0 \\ & \; | \; 0 \\ & \; | \; 0 \; ) </pre> \end{align}$$

## 形式化定義

### 語法

令Χ為一組稱為「名稱」的對象集合。π演算的抽象語法由以下BNF文法構建（其中x和y是Χ中的任意名稱）：

$$\begin{align} P, Q ::= & \; x(y).P \,\,\, \, \, & \text{Receive on channel }x\text{, bind the result to }y\text{, then run }P \\ & \; | \; \overline{x} \langle y \rangle.P \,\,\, \, \, &\text{Send the value }y\text{ over channel }x\text{, then run }P \\ & \; | \; P|Q \,\,\, \, \, \, \, \, \, &\text{Run }P\text{ and }Q\text{ simultaneously} \\ & \; | \; (\nu x)P \,\,\, &\text{Create a new channel }x\text{ and run }P \\ & \; | \; !P \,\,\, &\text{Repeatedly spawn copies of }P \\ & \; | \; 0 & \text{Terminate the process} \end{align}$$

在下面的具體語法中，前綴的綁定優先級高於並行組合（|），並使用括號來消除歧義。

名稱通過限制和輸入前綴構造進行綁定。形式上，π演算中進程的自由名集合通過下表歸納定義。進程的約束名集合定義為進程中不在自由名集合中的名稱。

構造｜自由名(Free names)

$x(y).P$｜x; P的自由名，除去y

$\overline{x} \langle y \rangle.P$｜x; y; P的所有自由名

$P|Q$｜P和Q的所有自由名

$(\nu x)P$｜P的自由名，除去x

$!P$｜P的所有自由名

$0$｜無

### 結構同餘

對於歸約語義和帶標號遷移語義來說，結構同餘（Structural congruence）的概念都是核心。如果兩個過程在結構上完全相同，則稱它們在結構上是同餘的。特別地，並行組合滿足交換律和結合律。

更準確地說，結構同餘被定義為過程構造所保留的最小等價關係，並滿足以下條件：

α轉換（Alpha-conversion）:

- $P \equiv Q$ if $Q$ can be obtained from $P$ by renaming one or more bound names in $P$.

並行組合公理:

- $$P|Q \equiv Q|P$$
- $$(P|Q)|R \equiv P|(Q|R)$$
- $$P | 0 \equiv P$$

限制公理:

- $$(\nu x)(\nu y)P \equiv (\nu y)(\nu x)P$$
- $$(\nu x)0 \equiv 0$$

複製公理:

- $$!P \equiv P|!P$$

限制與並行關聯公理:

- $(\nu x)(P | Q) \equiv (\nu x)P | Q$ if x is not a free name of $Q$.

最後這條公理被稱為「轄域擴張」（scope extension）公理。該公理至關重要，因為它描述了約束名x如何通過輸出動作被擠出（extruded），從而導致x的作用域被擴張。在x是$Q$的自由名的情況下，可以使用α轉換來使擴展得以繼續進行。

### 歸約語義

我們記作$P \rightarrow P'$，如果$P$可以執行一個計算步，之後它變為$P'$。這個歸約關係$\rightarrow$定義為在一組歸約規則下封閉的最小關係。

捕捉進程通過通道進行通信能力的主要歸約規則如下：

- $$\overline{x}\langle z \rangle.P | x(y).Q \rightarrow P | Q[z/y]$$

其中$Q[z/y]$表示將進程$Q$中自由出現的$y$替換為自由名$z$。如果$y$的自由出現位置處於$z$不自由的位置，則可能需要進行α轉換。

還有三條附加規則：

- If $P \rightarrow Q$ then also $P|R \rightarrow Q|R$.

這條規則表明並行組合不會抑制計算。

- If $P \rightarrow Q$, then also $(\nu x)P \rightarrow (\nu x)Q$.

這條規則確保計算可以在限制內部進行。

- If $P \equiv P'$ and $P' \rightarrow Q'$ and $Q' \equiv Q$, then also $P \rightarrow Q$.

最後一條規則指出，結構同餘的進程具有相同的歸約。

### 回顧示例

再次考慮該進程

$$(\nu x)(\overline{x} \langle z \rangle.0 | x(y). \overline{y}\langle x \rangle . x(y).0 ) | z(v) . \overline{v}\langle v \rangle. 0$$

應用歸約語義的定義，我們得到歸約：

$$(\nu x)(\overline{x} \langle z \rangle.0 | x(y). \overline{y}\langle x \rangle . x(y).0 ) | z(v) . \overline{v}\langle v \rangle. 0 \rightarrow (\nu x)(0| \overline{z}\langle x \rangle . x(y). 0 ) | z(v). \overline{v}\langle v \rangle .0$$

注意，應用歸約替換公理後，自由出現的$y$現在被標記為$z$。

接下來，我們得到歸約：

$$(\nu x)(0| \overline{z}\langle x \rangle . x(y). 0 ) | z(v). \overline{v}\langle v \rangle .0 \rightarrow (\nu x)(0| x(y). 0 | \overline{x}\langle x \rangle .0)$$

注意，由於局部名稱x已被輸出，x的作用域擴展覆蓋了第三個組件。這是使用轄域擴展公理捕捉到的。

接下來，使用歸約替換公理，我們得到：

$$(\nu x)(0 | 0 | 0)$$

最後，使用並行組合和限制的公理，我們得到：

$$0$$

### 帶標號語義

另外，也可以為π演算賦予帶標號遷移語義（labelled transition semantics），就像通信系統演算中所做的那樣。

在這種語義中，狀態$P$經過動作$\alpha$遷移到另一狀態$P'$記為：

- $$P\,\xrightarrow{\overset{}\alpha} P'$$

其中狀態$P$和$P'$代表進程，而$\alpha$是「輸入動作」$a(x)$、「輸出動作」$\overline{a}\langle x \rangle$或「沉默動作」τ。

關於帶標號語義的一個標準結論是，它在結構同餘的意義上與歸約語義（reduction semantics）一致，即$P \rightarrow P'$ if and only if $P\,\xrightarrow{\overset{}\tau}\equiv P'$

## 擴展與變體

上述語法是最小化的。然而，可以通過多種方式對語法進行修改。

語法中可以加入「非確定性選擇算子」$P + Q$。

語法中還可以加入對「名稱相等」的測試$[x=y]P$。這個「匹配算子」（match operator）僅當x和$y$是同一個名稱時才能作為$P$繼續執行。

類似地，也可以加入用於「名稱不等」的「不匹配算子」。能夠傳遞名稱（URL或指針）的實際程序經常使用此類功能：為了在演算內部直接對這些功能建模，這個擴展及相關擴展通常很有用。

異步π演算（Asynchronous π-calculus）只允許沒有後續進程（continuation）的輸出，即形式為$\overline{x}\langle y \rangle$的輸出原子，從而產生了一個更小的演算。然而，原演算中的任何進程都可以用更小的異步π演算來表示，方法是使用額外的通道來模擬接收進程的顯式確認。由於無後續進程的輸出可以對傳輸中的消息進行建模，該片段表明，直觀上基於同步通信的原始π演算，在其語法內部包含了一個表達力強的異步通信模型。但是，上述定義的非確定性選擇算子無法用這種方式表達，因為無衛選擇會被轉換為有衛選擇；這一事實已被用於證明異步演算的表達力嚴格弱於同步演算（帶有選擇算子的情況）。

多元π演算（Polyadic π-calculus）允許在單個動作中通信多個名稱：$\overline{x}\langle z_1,...,z_n\rangle.P$（多元輸出）和$x(z_1,...,z_n).P$（多元輸入）。這種多元擴展（在研究名稱傳遞進程的類型時特別有用）可以通過傳遞一個私有通道的名稱編碼到一元演算（monadic calculus）中，然後通過該私有通道按順序傳遞多個參數。該編碼通過以下子句遞歸定義：

$\overline{x}\langle y_1,\cdots,y_n\rangle.P$ is encoded as $(\nu w) \overline{x}\langle w \rangle.\overline{w}\langle y_1\rangle.\cdots.\overline{w}\langle y_n\rangle.[P]$

$x(y_1,\cdots,y_n).P$ is encoded as $x(w).w(y_1).\cdots.w(y_n).[P]$

所有其他進程構造在編碼中保持不變。

在上式中，$[P]$表示以相同方式對後續進程$P$中的所有前綴進行編碼。

並不需要複製算子$!P$的全部能力。通常，人們只考慮「複製輸入」$! x(y).P$，其結構同餘公理為$! x(y).P \equiv x(y).P | !x(y).P$。

諸如$!x(y).P$的複製輸入進程可以理解為伺服器，在通道x上等待客戶端調用。調用伺服器會生成進程$P[a/y]$的一個新副本，其中a是客戶端在調用過程中傳遞給伺服器的名稱。

可以定義高階π演算（Higher order π-calculus），其中不僅可以傳遞名稱，還可以通過通道傳遞進程。高階情況的關鍵歸約規則是：

$$\overline{x}\langle R \rangle.P | x(Y).Q \rightarrow P | Q[R/Y]$$

這裡，$Y$表示一個「進程變量」，可以被實例化為一個進程項。Sangiorgi證明了傳遞進程的能力並不會增加π演算的表達力：傳遞進程P可以通過僅傳遞一個指向P的名稱來模擬。

## 特點

### 圖靈完備性

π演算是一個通用的計算模型。這一點最早由Milner在他的論文《函數即進程》（Functions as Processes）中觀察到，其中他在π演算中提出了兩種λ演算的編碼。一種編碼模擬了及早（按值調用）求值策略，另一種編碼模擬了正規序（按名調用）策略。在這兩種編碼中，關鍵的洞察是將環境綁定（例如，「x綁定到項$M$」）建模為複製代理，這些代理通過回傳指向項$M$的連接來響應對其綁定的請求。

使這些編碼成為可能的π演算特性是名稱傳遞和複製（或者等價地，遞歸定義的代理）。在缺乏複製/遞歸的情況下，π演算不再是圖靈完備的。這一點可以從以下事實看出：對於無遞歸的π演算，甚至對於有限控制π演算——其中任何進程中的並行組件數量都受某個常數上限的限制——互模擬等價性變得可判定。

## π演算中的互模擬

與進程演算一樣，π演算允許定義互模擬等價（bisimulation equivalence）。在π演算中，互模擬等價（也稱為互模擬性，bisimilarity）的定義既可以基於歸約語義，也可以基於帶標號遷移語義。

在π演算中，（至少）有三種定義帶標號互模擬等價的不同方法：早（Early）、晚（Late）和開放（Open）互模擬性。這源於π演算是一種傳值進程演算這一事實。

在本節的剩餘部分，我們令$p$和$q$表示進程，$R$表示進程上的二元關係（binary relation）。

### 早互模擬與晚互模擬

早互模擬性和晚互模擬性都是由Milner、Parrow和Walker在他們關於π演算的原始論文中制定的。

進程上的二元關係$R$是一個早互模擬（early bisimulation），如果對於每一對進程$(p, q) \in R$：

- whenever $p \,\xrightarrow{a(x)}\,p'$ then for every name $y$ there exists some $q'$ such that $q \,\xrightarrow{a(x)}\,q'$ and $(p'[y/x],q'[y/x]) \in R$;
- for any non-input action $\alpha$, if ${ p \xrightarrow{\overset{}{\alpha}} p' }$ then there exists some $q'$ such that $q \xrightarrow{\overset{}{\alpha}} q' <pre>$ and $(p',q') \in R$;
- 以及$p$和$q$互換後的對稱要求。

如果存在某個早互模擬$R$使得$(p,q) \in R$，則稱進程$p$和$q$是早互模擬的，記作$p \sim_e q$。

在晚互模擬性中，遷移匹配必須獨立於被傳輸的名稱。進程上的二元關係$R$是一個晚互模擬（late bisimulation），如果對於每一對進程$(p, q) \in R$：

- whenever $p \xrightarrow{a(x)} p'$ then for some $q'$ it holds that $q \xrightarrow{a(x)} q'$ and $(p'[y/x],q'[y/x]) \in R$ for every name y;
- for any non-input action $\alpha$, if $p \xrightarrow{\overset{}{\alpha}} p' <pre>$ implies that there exists some $q'$ such that $</pre> q \xrightarrow{\overset{}{\alpha}} q' <pre>$and $(p',q') \in R$;
- 以及$p$和$q$互換後的對稱要求。

如果存在某個晚互模擬$R$使得$(p,q) \in R$，則稱進程$p$和$q$是晚互模擬的，記作$p \sim_l q$。

$\sim_e$和$\sim_l$都有一個問題，即它們不是同餘關係，這意味著它們不能被所有的進程構造所保持。更確切地說，存在進程$p$和$q$使得$p \sim_e q$但$a(x).p \not \sim_e a(x).q$。可以通過考慮包含在$\sim_e$和$\sim_l$中的最大同餘關係來解決這個問題，分別稱為早同餘和晚同餘。

### 開放互模擬

幸運的是，第三種定義是可能的，它避免了這個問題，即Sangiorgi提出的開放互模擬性（open bisimilarity）。

進程上的二元關係$R$是一個開放互模擬，如果對於每一對元素$(p, q) \in R$以及對於每一個名稱替換$\sigma$和每一個動作$\alpha$，每當$p\sigma \xrightarrow{\overset{}{\alpha}} p'$時，都存在某個$q'$使得$q\sigma \xrightarrow{\overset{}{\alpha}} q' <pre>$且$(p',q') \in R$。

如果存在某個開放互模擬$R$使得$(p,q) \in R$，則稱進程$p$和$q$是開放互模擬的，記作$p \sim_o q$。

#### 早、晚和開放互模擬性是不同的

早、晚和開放互模擬性是不同的。它們具有真包含關係，因此$\sim_o \subsetneq \sim_l \subsetneq \sim_e$。

在某些子演算（如異步π演算）中，已知晚、早和開放互模擬性是重合的。然而，在這種背景下，更合適的概念是異步互模擬性。

在文獻中，術語開放互模擬通常指的是一個更複雜的概念，其中進程和關係由區分關係（distinction relations）索引；詳情參見上述Sangiorgi的論文。

### 倒刺等價

或者，可以直接從歸約語義定義互模擬等價。如果進程$p$立即允許在名稱$a$上進行輸入或輸出，我們記作$p \Downarrow a$。

進程上的二元關係$R$是一個倒刺互模擬（barbed bisimulation），如果它是一個對稱關係，並且滿足對於每一對元素$(p, q) \in R$，我們要麼：

(1) $p \Downarrow a$ if and only if $q \Downarrow a$ for every name $a$

並且

(2) for every reduction $p \rightarrow p'$ there exists a reduction $q \rightarrow q'$

使得$(p',q') \in R$。

如果存在一個倒刺互模擬$R$使得$(p,q) \in R$，我們稱$p$和$q$是倒刺互模擬的。

定義上下文為帶有一個空洞的π項，如果不論對於什麼上下文$C[]$，我們都有$C[P]$和$C[Q]$是倒刺互模擬的，則稱兩個進程P和Q是倒刺同餘的（barbed congruent），記作$P \sim_b Q\,\!$。事實證明，倒刺同餘與由早互模擬性誘導的同餘相重合。

## 應用

π演算已被用於描述許多不同類型的並發系統。事實上，一些最新的應用已經超出了傳統電腦科學的範疇。

1997年，馬丁·阿巴迪和Andrew Gordon提出了π演算的一個擴展——Spi-演算，作為描述和推理密碼學協議的形式化符號。Spi演算用加密和解密原語擴展了π演算。2001年，馬丁·阿巴迪和Cedric Fournet推廣了密碼學協議的處理，提出了應用π演算（applied π calculus）。現在有大量工作致力於應用π演算的變體，包括許多實驗性驗證工具。其中一個例子是由Bruno Blanchet開發的工具ProVerif，它基於將應用π演算翻譯成Blanchet的邏輯編程框架。另一個例子是由Andrew Gordon和Alan Jeffrey開發的Cryptyc，它使用Woo和Lam的對應斷言（correspondence assertions）方法作為類型系統的基礎，以檢查加密協議的認證屬性。

大約在2002年，Howard Smith和Peter Fingar開始對將π演算作為業務流程的描述工具感興趣。到2006年7月，社區中出現了關於這種方法有多大用處的討論。最近，π演算構成了業務流程建模語言（BPML）和微軟XLANG的理論基礎。

π演算也引起了分子生物學領域的興趣。1999年，Aviv Regev和Ehud Shapiro表明，人們可以用π演算的擴展描述細胞信號通路（即所謂的RTK/MAPK級聯），特別是描述實現這些通信任務的分子「樂高積木」。在這篇開創性論文之後，其他作者描述了最小細胞的整個代謝網絡。2009年，Anthony Nash和Sara Kalvala提出了一個π演算框架來模擬指導盤基網柄菌（Dictyostelium discoideum）聚集的信號轉導。

## 歷史

π演算最初由Robin Milner、Joachim Parrow和David Walker於1992年，基於Uffe Engberg和Mogens Nielsen的思想開發而成。它可以看作是Milner關於進程演算CCS（通信系統演算）工作的延續。在他的圖靈獎演講中，Milner將π演算的發展描述為試圖捕捉演員模型中值和進程的一致性。

## 實現

以下程式語言實現了π演算或其變體之一：

- 業務流程建模語言(BPML)
- occam-π
- Pict程式語言
- JoCaml（基於Join演算）
- RhoLang