Π演算

在理论计算机科学中，π演算（π-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