進程演算

在計算機科學中，進程演算（或進程代數）是用於形式化建模並發系統的多種相關方法。進程演算提供了具體描述多個獨立代理人程序或者是多個進程之間交互、通信、同步的方法，其中包含了對進程操作和分析的描述、以及證明形式化推導進程之間存在等價關係（例如：雙向模擬的運用）的代數法則。關於進程演算的典例主要包括CSP、CCS、ACP，和LOTOS。最近新增的演算包括π演算，環境演算，PEPA，融合演算和聯接演算。

基本特徵

雖然目前為止的進程演算種類繁多（包括含有隨機行為，定時信息，專門研究基礎的的交互的特例），但是所有的進程演算都有以下幾個共同特徵：

• 在獨立進程之間進行通信（消息傳遞）時比修改共享變量更能體現交互性；
• 使用基本元和能合併這些基本元的操作符的集合來描述進程和系統；
• 定義了能通過方程式推理方法推導出進程表達式的操作符的代數法則。

數學表示

定義進程演算，起步於定義一組「名字」（或通道），它們的用途是提供通信手段。在許多實現中，通道有優秀的內部結構以提高效率，不過這是從理論模型中抽象出來的。除命名之外，需要從之前的進程中運用一個方法來構建新的進程，其中的基礎運算符，總是以某些形式或其他方式呈現，包括：

• 進程的並行組合；
• 詳述用於傳送和接受數據的通道；
• 交互操作的順序化；
• 隱藏交互點；
• 遞歸或進程複製。

並行組合

兩個進程P和Q的並行組合，通常寫做P|Q，它是將進程演算從運算序列模型中識別出來的關鍵基本式。並行組合允許P和Q相互獨立並且同時進行運算。但它也允許進行交互，那就是同步及P通過兩者共享的通道將信息流傳遞至Q（或反之亦然）。至關重要的是，代理或進程可以一次連接到多個通道。通道可以是同步或異步的。在同步通道的情況下，發送信息的代理需要等待至另一個代理接收到信息。異步通道不要求任何的同步。在一些進程演算（特別是π演算）中，它們的通道本身可以作為信息通過（其他的）通道發送，允許進程相互連接的拓撲結構發生改變。一些進程演算也允許通道在執行運算的過程中被創建。

通信

交互可以作為（但不總是）有向的信息流。也就是說，輸入和輸出能作為雙重交互基本元被區分。進行這種區分的進程演算通常定義一個輸入操作符（e.g X(v)）和一個輸出操作符（e.g X<y>）,這兩者作為一個以雙重交互基本元進行同步的交互點（這裏是X）。 信息應該被交換，它將從輸出流向輸入進程。輸出基本元將指定要發送的數據。在X<y>中，這個數據是y。類似的，如果一個輸入想要接受數據，當數據到達時，一個或多個綁定變量將作為佔位符來替換數據。在X(v)中，v扮演那個角色。在交互中可以交換的數據類型的選擇是區分不同進程演算的關鍵特徵之一。

順序組合

有時交互必須在時間上有序。例如，它可能要求指定算法：首先在X上接收數據，然後在y上傳送數據。順序組合可用於這些目的。在其他運算模型中它非常有名。在進程演算中，序列化運算符通常與輸入或輸出或兩者結合。例如，進程X（v）.P將等待（數據）輸入到X上，只有當這個輸入完成時進程P才會被激活，通過X接受的數據代替標識符v。

歸約語義

歸約法則運用的關鍵，包含了進程演算的計算實質，單獨的依據並行組合、順序化、輸入和輸出。演算間的歸約細節不同，但是實質保持大致相同。通用的歸約法則是：$x\langle y\rangle \cdot P\;\vert \;x(v)\cdot Q\longrightarrow P\;\vert \;Q[^{y}\!/\!_{v}]$。

該歸約規則的解釋是：

1. 進程$x\langle y\rangle \cdot P$發送信息，即此處的y，沿着雙向的通道X，進程$x(v)\cdot Q$接受通道X上的信息。
2. 一旦信息被發送，$x\langle y\rangle \cdot P$就成為了進程P，而$x(v)\cdot Q$就變成了進程$Q[^{y}\!/\!_{v}]$，即Q與佔位符v取代y，接受到了X上的數據。

P這類進程涉及的輸出運算符的連續性本質上影響了演算的性質。

隱藏

進程不限制能給出交互點的連接數量，但是交互點允許相互干擾（即交互作用）。對於一個簡潔，微小和組合式的綜合系統，抗干擾的能力是至關重要的。當組合代理並行時，隱藏操作允許控制交互點之間形成的連接。隱藏能用多種多樣的方式表示。例如，在π演算中，隱藏一個P中的命名X可以被描述為（v X）P,然而在CSP中它可能被寫做P\{X}.

遞歸與複製

迄今提出的操作僅描述有限的交互,也因此不滿足包含非終止行為的完全可計算性。遞歸和複製允許以有限步描述無限的行為。遞歸具有的連續性領域是眾所周知的，複製！P可以被理解為縮寫可數集無限數的P進程的並行組合：

$!P=P\mid !P$

空進程

進程演算通常還包含沒有交互點的空進程（多樣的表示為nil，0，STOP，δ或一些其他的適當符號），它是完全無活動的，並且它唯一的用途表現在作為歸納錨點置於可以被生成的活躍進程之上。 離散和連續進程代數 已經針對離散時間和連續時間研究過進程代數（真實時間和稠密時間）。

歷史發展

在20世紀上半葉，提出了各種形式論來獲得可計算函數的非正式概念，μ遞歸函數，圖靈機和lambda演算可能是如今最著名的例子，令人驚訝的事實是，在它們可以相互編碼的意義上，它們彼此之間基本上是等同的，支撐着Church-Turing論題。另一個難得的對它們共同特徵的評論是：它們幾乎都是作為最容易理解的連續計算模型，隨後的計算機科學的整合需要更細微的計算概念的表達，特別是並行和通信的明確表達。作為並發模型的進程演算，1962年提出的Petri網，以及1973年提出的演員模型，就是在這條探究路線上湧現的。進程演算的研究開始於1973年至1980年期間，與Robin Milner對通信系統演算(CCS)的開創性工作有關。C.A.R. Hoare的通信順序進程（CSP）首次出現於1978年，隨後直到20世紀80年代初期才被開發為一個完整的進程演算。CCS和CSP在發展的過程中，發生了許多思想上的交叉。在1982年Jan Bergstra和Jan Willem Klop開始致力於研究後來被熟知的通信處理代數（ACP），並且提出了術語「進程代數」來描述他們的工作。CCS、CSP和ACP構成了進程演算的三個重要的分支：其餘大多數的進程演算的根源都可以追溯到這三個演算的其中之一。

現今研究

研究的進程演算多種多樣但不是全部都符合這裏描述的範例。最突出的例子可能是灰箱演算。作為進程演算研究預期的熱門領域，目前對進程演算的研究集中在以下問題上：

• 發展新的進程演算以更好的對運算情況進行建模。
• 為給定的進程演算找到良好性質的演算進行運算。這是有價值的，因為
  • 大多數演算相當的混亂，這樣的情況是相當普遍的，對於任意進程來說都描述不了太多；
  • 計算程式很少耗盡整個演算。相反，它們只使用在形式上受限制的進程。約束進程的模型主要是通過表徵系統的方式來研究。
• 遵循Hoare邏輯的思想，進程邏輯允許人們推理有關進程的（實質上的）任意屬性；
• 行為理論：兩個進程相同意味着什麼意思？我們如何確定兩個進程是否不同？我們可以找到進程的等價類的典型嗎？通常，如果沒有上下文（即並行運行的其他進程）可以檢測到差異，則認為進程是相同的。不幸的是，使得這樣的直覺知識變得準確是很難的，大多產生難處理的相同特徵（在大多數情況下也必須是不可判定的，作為停機問題的結果）。互模擬是有助於對進程等價的推理的技術工具。
• 進程的表達性。編程經驗表明，某些問題在某些語言中比在其他語言中更容易解決。這種現象要求演算建模運算具有比Church-Turing論文提供的表達性更精確的特徵。這樣做的一種方法是考慮兩種形式論之間的編碼，並看看編碼可以潛在地保存什麼屬性。可以保存的屬性越多，編碼的表達能力就越強。對於進程演算，著名的結果是同步的π演算比其異步變體更具表達性，具有與高階π演算相同的表達能力，但小於灰箱演算。
• 使用進程演算來對生物系統建模（隨機π演算，BioAmbients，Beta Binder，BioPEPA，Brane calculus）。它認為提供一些組合性的進程理論工具能幫助生物學家更加正規的組織他們的知識。

軟件實現

進程代數的想法提出後已經產生了許多工具，包括：

• CADP
• 並行工具台
• mCRL2工具集

與其他並發模型的關係

歷史獨異點是能夠一般的表示獨立通信進程歷史的自由對象。進程演算是形式語言以一致的方式應用於歷史獨異點之後得到的。即是說，一個歷史獨異點只能夠記錄事件的順序，帶有同步性，但是這不表明允許狀態的轉變。因此，進程演算之於歷史獨異點相當於形式語言之於自由獨異點（形式語言是Kleene star產生的字符所組成的所有可能的有限長度字符串的子集）。

使用通道進行通信是將進程演算與其它並發模型區分開的特徵之一，例如Petri網和演員模型（參見演員模型和進程演算條目）在進程演算中包含通道的基本動機之一是實現某些代數方法，從而讓用代數方法來推導進程變得簡單。