Π-演算

在理论计算机科学中，**π-演算**（**-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，并将接收到的名称绑定到名称 。通常，这模拟了一个等待网络通信的进程，或者是只能通过 `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 内部分配新常量  的进程。π-演算中的常量仅由其名称定义，且始终是通信通道。创建新名也被称为“限制”（restriction）。
* **零进程**（Nil process），记作 0，是一个执行已完成并停止的进程。

尽管 π-演算 的极简性阻止了我们以通常意义上的方式编写程序，但扩展该演算非常容易。例如，定义控制结构（如递归、循环和顺序组合）以及数据类型（如一阶函数、真值、列表和整数）都很容易。此外，已经有人提出了考虑到分布式或公钥密码学的 π-演算 的扩展形式。由 Abadi 和 Fournet 提出的“应用 π-演算” https://www.soe.ucsc.edu/~abadi/Papers/isss02.pdf ，通过用任意数据类型扩展 π-演算，为上述各种扩展奠定了形式化的理论基础。

### 一个小例子

下面是一个由三个并行组件组成的进程小例子。通道名称  仅为前两个组件所知。

:
\begin{align}
  (\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
\end{align}


前两个组件能够在通道  上进行通信，名称  被绑定到 。因此，进程的下一步是：

:
\begin{align}
  (\nu x) & \; ( \; 0 \\
          & \; | \; \overline{z} \langle x \rangle . \; x(y). \; 0 \; )  \\
          & \; | \; z(v). \; \overline{v}\langle v \rangle . \; 0
\end{align}


注意，剩余的  不受影响，因为它是在内部作用域中定义的。

第二个和第三个并行组件现在可以在通道名称  上通信，名称  被绑定到 。进程的再下一步是：

:
\begin{align}
  (\nu x) & \; ( \; 0 \\
          & \; | \; x(y). \; 0  \\
          & \; | \; \overline{x}\langle x \rangle . \; 0 \; )
\end{align}


注意，由于局部名称  已经被输出， 的作用域被扩展以覆盖第三个组件。最后，通道  可用于发送名称 。之后，所有并发执行的进程都将停止：

:
\begin{align}
  (\nu x) & \; ( \; 0  \\
          & \; | \; 0  \\
          & \; | \; 0 \; )

\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}

在下面的具体语法中，前缀的绑定优先级高于并行组合 (|)，并使用括号来消除歧义。

名称通过**限制**和**输入前缀构造**进行绑定。形式上，π-演算中进程的自由名集合通过下表归纳定义。进程的约束名集合定义为进程中不在自由名集合中的名称。

### 结构同余

对于归约语义和带标号迁移语义来说，**结构[[同餘關係|同余]]**（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  is not a free name of Q.

最后这条公理被称为“辖域扩张”（scope extension）公理。该公理至关重要，因为它描述了约束名  如何通过输出动作被挤出（extruded），从而导致  的作用域被**扩张**。在  是 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)  

注意，由于局部名称  已被输出， 的作用域扩展覆盖了第三个组件。这是使用辖域扩展公理捕捉到的。

接下来，使用归约替换公理，我们得到：

: (\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）仅当  和 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 的复制输入进程可以理解为服务器，在通道  上等待客户端调用。调用服务器会生成进程 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）中观察到， 其中他在 π-演算中提出了两种λ演算的编码。一种编码模拟了及早（按值调用）求值策略，另一种编码模拟了正规序（按名调用）策略。在这两种编码中，关键的洞察是将环境绑定（例如，“ 绑定到项 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'
   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'
   implies that there exists some q' such that 
q \xrightarrow{\overset{}{\alpha}} q'
  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'
   且 (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 开发的工具  http://www.proverif.ens.fr/，它基于将应用 π-演算翻译成 Blanchet 的逻辑编程框架。另一个例子是由 Andrew Gordon 和 Alan Jeffrey 开发的 Cryptyc http://www.cryptyc.org，它使用 Woo 和 Lam 的对应断言（correspondence assertions）方法作为类型系统的基础，以检查加密协议的认证属性。

大约在 2002 年，Howard Smith 和 Peter Fingar 开始对将 π-演算作为业务流程的描述工具感兴趣。到 2006 年 7 月，社区中出现了关于这种方法有多大用处的讨论。最近，π-演算构成了 (BPML) 和微软 XLANG 的理论基础。

π-演算也引起了分子生物学领域的兴趣。 1999 年， 和  表明，人们可以用 π-演算的扩展描述细胞信号通路（即所谓的 RTK/MAPK 级联），特别是描述实现这些通信任务的分子“乐高积木”。 在这篇开创性论文之后，其他作者描述了最小细胞的整个代谢网络。 2009 年，Anthony Nash 和  提出了一个 π-演算框架来模拟指导*盘基网柄菌*（Dictyostelium discoideum）聚集的信号转导。

## 历史
π-演算最初由 Robin Milner、Joachim Parrow 和 David Walker 于 1992 年，基于 Uffe Engberg 和 Mogens Nielsen 的思想 开发而成。 它可以看作是 Milner 关于进程演算 CCS（）工作的延续。在他的图灵奖演讲中，Milner 将 π-演算的发展描述为试图捕捉Actor 模型中值和进程的一致性。

## 实现

以下编程语言实现了 π-演算或其变体之一：

* (BPML)
* 
* 
*  (基于 )
* RhoLang

## 注释

## 参考文献
* 
* 
* 
*