在計算機科學中，進程演算（或進程代數）是用於正規建模並發系統的多種相關方法。進程演算提供了具體描述多個獨立代理人程式或者是多個進程之間互動、通信、 同步的方法。
其中包含了對進程操作和分析的描述、以及證明形式化推導進程之間存在等價關係（例如：雙向模擬的運用）的代數法則。關於進程演算的典例主要包括 CSP, CCS, ACP, 和LOTOS.最近新增的演算包括π演算，環境演算，PEPA，融合演算和聯接演算。
基本介紹
- 中文名：進程演算
- 外文名：Process calculus
基本特徵,數學表示,並行組合,通信,順序組合,歸約語義,隱藏,遞歸與複製,,空進程,離散和連續進程代數,歷史發展,現今研究,軟體實現,與其他並行模型的關係,
基本特徵
雖然目前為止的進程演算種類繁多（包括含有隨機行為，定時信息，專門研究基礎的的互動的特例），但是所有的進程演算都有以下幾個共同特徵：
1.在獨立進程之間進行通信（訊息傳遞）時比修改共享變數更能體現互動性；
2.使用基本元和能合併這些基本元的操作符的集合來描述進程和系統；
3.定義了能通過方程式推理方法推導出進程表達式的操作符的代數法則。
數學表示
定義進程演算，一開始目的是為了提供通信手段的命名（如信道），在許多實現中，信道有優秀的內部結構以提高效率，不過這是從理論模型中抽象出來的。除命名之外，需要從之前的進程中運用一個方法來構建新的進程，其中的基礎運算符，總是以某些形式或其他方式呈現，包括：
1.進程的並行組合；
2.詳述用於傳送和接受數據的信道；
3.互動操作的順序化；
4.隱藏互動點；
5.遞歸或進程複製；
並行組合
兩個進程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<y>.P|X(v).Q → P|Q[y/v]
該歸約規則的解釋是：
- 進程X<y>.P傳送信息，即此處的y，沿著雙向的信道X.，進程X(v).Q接受信道X上的信息。
- 一旦信息被傳送，X<y>.P就成為了進程P，而|X(v).Q就變成了進程Q[y/v]，即Q與占位符v取代y，接受到了X上的數據。
P這類進程涉及的輸出運算符的連續性本質上影響了演算的性質。
隱藏
進程不限制能給出互動點的連線數量，但是互動點允許相互干擾（即互動作用）。對於一個簡潔，微小和組合式的綜合系統，抗干擾的能力是至關重要的。當組合代理並行時，隱藏操作允許控制互動點之間形成的連線。隱藏能用多種多樣的方式表示。例如，在π演算中，隱藏一個P中的命名X可以被描述為（v X）P,然而在CSP中它可能被寫做P\{X}.
遞歸與複製,
迄今提出的操作僅描述有限的互動,也因此不滿足包含非終止行為的完全可計算性。遞歸和複製允許以有限步描述無限的行為。遞歸具有的連續性領域是眾所周知的，複製！P可以被理解為縮寫可數集無限數的P進程的並行組合：
!P=P|!P
空進程
進程演算通常還包含沒有互動點的空進程（多樣的表示為nil，0，STOP，δ或一些其他的適當符號），它是完全無活動的，並且它唯一的用途表現在作為歸納錨點置於可以被生成的活躍進程之上。
離散和連續進程代數
已經針對離散時間和連續時間研究過進程代數（真實時間和稠密時間)。[4]
歷史發展
在20世紀上半葉，提出了各種形式論來獲得可計算函式的非正式概念，μ遞歸函式，圖靈機和lambda演算可能是如今最著名的例子，令人驚訝的事實是，在它們可以相互編碼的意義上，它們彼此之間基本上是等同的，支撐著Church-Turing論題。另一個難得的對它們共同特徵的評論是：它們幾乎都是作為最容易理解的連續計算模型，隨後的計算機科學的整合需要更細微的計算概念的表達，特別是並行和通信的明確表達。作為進程演算的並行模型，1962年的Petri網，以及1973年出現於線路查詢的Actor模型。進程演算的研究開始於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構成了進程演算的三個重要的分支：其餘大多數的進程演算的根源都可以追溯到這三個演算的其中之一。
現今研究
研究的進程演算多種多樣但不是全部都符合這裡描述的範例。最突出的例子可能是灰箱演算。作為進程演算研究預期的熱門領域，目前對進程演算的研究集中在以下問題上：
- 發展新的進程演算以更好的對運算情況進行建模。
- 為給定的進程演算找到良好性質的微積分進行運算。這是有價值的因為（1）大多數演算相當的混亂，這樣的情況是相當普遍的，對於任意進程來說都描述不了太多；（2）計算程式很少耗盡整個演算。相反，它們只使用在形式上受限制的進程。約束進程的模型主要是通過表征系統的方式來研究。
- 遵循Hoare邏輯的思想，進程邏輯允許人們推理有關進程的（實質上的）任意屬性；
- 行為理論：兩個進程相同意味著什麼意思？我們如何確定兩個進程是否不同？我們可以找到進程的等價類的典型嗎？通常，如果沒有上下文（即並行運行的其他進程）可以檢測到差異，則認為進程是相同的。不幸的是，使得這樣的直覺知識變得準確是很難的，大多產生難處理的相同特徵（在大多數情況下也必須是不可判定的，作為停機問題的結果）。互模擬是有助於對進程等價的推理的技術工具。
- 進程的表達性。編程經驗表明，某些問題在某些語言中比在其他語言中更容易解決。這種現象要求演算建模運算具有比Church-Turing論文提供的表達性更精確的特徵。這樣做的一種方法是考慮兩種形式論之間的編碼，並看看什麼屬性通過編碼可以潛在地保存。可以保留的屬性越多，表示編碼目標的表達能力越強。對於進程演算，著名的結果是同步的π演算比其異步變體更具表達性，具有與高階π演算相同的表達能力，但小於灰箱演算。[需要引證]
- 使用進程演算來對生物系統建模（隨機π演算，BioAmbients，Beta Binder，BioPEPA，Brane calculus）。它認為提供一些組合性的進程理論工具能幫助生物學家更加正規的組織他們的知識。
軟體實現
進程代數的想法提出後已經產生了許多工具包括：
.CADP[1]
.並行工具台
.mCRL2工具集
與其他並行模型的關係
歷史獨異點是能夠一般的表示獨立通信進程歷史的自由對象。進程演算是形式語言以一致的方式套用於歷史獨異點之後得到的。[5]即是說，一個歷史獨異點只能夠記錄事件的順序，帶有同步性，但是這不表明允許狀態的轉變。因此，進程演算之於歷史獨異點相當於形式語言之於自由獨異點（形式語言是Kleene star產生的字元所組成的所有可能的有限長度字元串的子集）。
使用信道進行通信是將進程演算與其它並行模型區分開的特徵之一，例如Petri網和Actor模型（見Actor模型和進程演算）在進程演算中包含信道的基本動機之一是實現某些代數方法，從而讓用代數方法來推導進程變得簡單。
