π演算

在理论计算机科学中，π演算（英語：π-calculus或pi-calculus）是一种进程演算模型。

π演算允许通过通道本身传递通道名称。得益于此，它可以描述计算过程中网络拓扑可能发生变化的并发计算系统。

π演算语法简单，但表达能力很强（参见§ 语法）。函数式程序可以被表示成π演算，这种表示强调了计算的对话本质，并与博弈语义建立了联系。π演算的扩展形式，如spi演算和应用π演算（applied π），在分析和推理密码学协议方面获得了成功。除了用于描述并发系统的最初用途外，π演算也被用于推理业务流程建模语言^[1]、分子生物学^[2]以及人工智能中的智能体。

π演算属于进程演算家族——用于描述和分析并发计算属性的数学形式体系。事实上，与λ演算类似，π演算极其精简：它不包含诸如数字、布尔值、数据结构、变量、函数甚至通常的控制流语句（如if-then-else、while）等原语。

π演算的核心概念是名称（name）。该演算的简洁性在于名称兼具通信通道与变量的双重角色。

演算中可用的进程构造原语如下^[3]（精确定义见下一节）：

• 并发（Concurrency），记作${\displaystyle P\mid Q}$，表示进程/线程${\displaystyle P}$和${\displaystyle Q}$同时执行。
• 通信（Communication），包括：
  • 输入前缀（Input prefixing）${\displaystyle c\left(x\right).P}$：表示一个进程，它先等待一个通过名为${\displaystyle c}$的通信通道发出的消息，收到该消息后继续执行${\displaystyle P}$，并将接收到的名称绑定到名称x。通常，这模拟了一个等待网络通信的进程，或者是只能通过goto c操作使用一次的标签c。
  • 输出前缀（Output prefixing）${\displaystyle {\overline {c}}\langle y\rangle .P}$：描述了名称${\displaystyle y}$通过通道${\displaystyle c}$被发射出去，随后继续执行${\displaystyle P}$。通常，这模拟了在网络上发送消息或执行goto c操作。
• 复制（Replication），记作${\displaystyle !\,P}$，可以看作是一个总是能创建${\displaystyle P}$的新副本的进程。通常，这模拟了一个网络服务，或者是一个等待任意数量goto c操作的标签c。
• 创建新名（Creation of a new name），记作${\displaystyle \left(\nu x\right)P}$，可以看作是一个在${\displaystyle P}$内部分配新常量x的进程。π演算中的常量仅由其名称定义，且始终是通信通道。创建新名也被称为“限制”（restriction）。
• 零进程（Nil process），记作${\displaystyle 0}$，是一个执行已完成并停止的进程。

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

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

${\displaystyle {\begin{aligned}(\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{aligned}}}$

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

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

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

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

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;x(y).\;0\\&\;|\;{\overline {x}}\langle x\rangle .\;0\;)\end{aligned}}}$

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

${\displaystyle {\begin{aligned}(\nu x)&\;(\;0\\&\;|\;0\\&\;|\;0\;)\end{aligned}}}$

令Χ为一组称为“名称”的对象集合。π演算的抽象语法由以下BNF文法构建（其中x和y是Χ中的任意名称）：^[4]

${\textstyle {\begin{aligned}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{aligned}}}$

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

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

构造	自由名(Free names)
${\displaystyle x(y).P}$	x; P的自由名，除去y
${\displaystyle {\overline {x}}\langle y\rangle .P}$	x; y; P的所有自由名
${\displaystyle P|Q}$	P和Q的所有自由名
${\displaystyle (\nu x)P}$	P的自由名，除去x
${\displaystyle !P}$	P的所有自由名
${\displaystyle 0}$	无

对于归约语义和带标号迁移语义来说，结构同余（Structural congruence）的概念都是核心。如果两个过程在结构上完全相同，则称它们在结构上是同余的。特别地，并行组合满足交换律和结合律。

更准确地说，结构同余被定义为过程构造所保留的最小等价关系，并满足以下条件：

α转换（Alpha-conversion）:

• ${\displaystyle P\equiv Q}$ if ${\displaystyle Q}$ can be obtained from ${\displaystyle P}$ by renaming one or more bound names in ${\displaystyle P}$.

并行组合公理:

• ${\displaystyle P|Q\equiv Q|P}$
• ${\displaystyle (P|Q)|R\equiv P|(Q|R)}$
• ${\displaystyle P|0\equiv P}$

限制公理:

• ${\displaystyle (\nu x)(\nu y)P\equiv (\nu y)(\nu x)P}$
• ${\displaystyle (\nu x)0\equiv 0}$

复制公理:

• ${\displaystyle !P\equiv P|!P}$

限制与并行关联公理:

• ${\displaystyle (\nu x)(P|Q)\equiv (\nu x)P|Q}$ if x is not a free name of ${\displaystyle Q}$.

最后这条公理被称为“辖域扩张”（scope extension）公理。该公理至关重要，因为它描述了约束名x如何通过输出动作被挤出（extruded），从而导致x的作用域被扩张。在x是${\displaystyle Q}$的自由名的情况下，可以使用α转换来使扩展得以继续进行。

我们记作${\displaystyle P\rightarrow P'}$，如果${\displaystyle P}$可以执行一个计算步，之后它变为${\displaystyle P'}$。这个归约关系${\displaystyle \rightarrow }$定义为在一组归约规则下封闭的最小关系。

捕捉进程通过通道进行通信能力的主要归约规则如下：

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

其中${\displaystyle Q[z/y]}$表示将进程${\displaystyle Q}$中自由出现的${\displaystyle y}$替换为自由名${\displaystyle z}$。如果${\displaystyle y}$的自由出现位置处于${\displaystyle z}$不自由的位置，则可能需要进行α转换。

还有三条附加规则：

• If ${\displaystyle P\rightarrow Q}$ then also ${\displaystyle P|R\rightarrow Q|R}$.

这条规则表明并行组合不会抑制计算。

• If ${\displaystyle P\rightarrow Q}$, then also ${\displaystyle (\nu x)P\rightarrow (\nu x)Q}$.

这条规则确保计算可以在限制内部进行。

• If ${\displaystyle P\equiv P'}$ and ${\displaystyle P'\rightarrow Q'}$ and ${\displaystyle Q'\equiv Q}$, then also ${\displaystyle P\rightarrow Q}$.

最后一条规则指出，结构同余的进程具有相同的归约。

再次考虑该进程

${\displaystyle (\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}$

应用归约语义的定义，我们得到归约：

${\displaystyle (\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}$

注意，应用归约替换公理后，自由出现的${\displaystyle y}$现在被标记为${\displaystyle z}$。

接下来，我们得到归约：

${\displaystyle (\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的作用域扩展覆盖了第三个组件。这是使用辖域扩展公理捕捉到的。

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

${\displaystyle (\nu x)(0|0|0)}$

最后，使用并行组合和限制的公理，我们得到：

${\displaystyle 0}$

另外，也可以为π演算赋予带标号迁移语义（labelled transition semantics），就像通信系统演算中所做的那样。

在这种语义中，状态${\displaystyle P}$经过动作${\displaystyle \alpha }$迁移到另一状态${\displaystyle P'}$记为：

• ${\displaystyle P\,{\xrightarrow {\overset {}{\alpha }}}P'}$

其中状态${\displaystyle P}$和${\displaystyle P'}$代表进程，而${\displaystyle \alpha }$是“输入动作”${\displaystyle a(x)}$、“输出动作”${\displaystyle {\overline {a}}\langle x\rangle }$或“沉默动作”τ。^[5]

关于带标号语义的一个标准结论是，它在结构同余的意义上与归约语义（reduction semantics）一致，即${\displaystyle P\rightarrow P'}$ if and only if ${\displaystyle P\,\xrightarrow {\overset {}{\tau }} \equiv P'}$^[6]

上述语法是最小化的。然而，可以通过多种方式对语法进行修改。

语法中可以加入“非确定性选择算子”${\displaystyle P+Q}$。

语法中还可以加入对“名称相等”的测试${\displaystyle [x=y]P}$。这个“匹配算子”（match operator）仅当x和${\displaystyle y}$是同一个名称时才能作为${\displaystyle P}$继续执行。

类似地，也可以加入用于“名称不等”的“不匹配算子”。能够传递名称（URL或指针）的实际程序经常使用此类功能：为了在演算内部直接对这些功能建模，这个扩展及相关扩展通常很有用。

异步π演算（Asynchronous π-calculus）^[7][8]只允许没有后续进程（continuation）的输出，即形式为${\displaystyle {\overline {x}}\langle y\rangle }$的输出原子，从而产生了一个更小的演算。然而，原演算中的任何进程都可以用更小的异步π演算来表示，方法是使用额外的通道来模拟接收进程的显式确认。由于无后续进程的输出可以对传输中的消息进行建模，该片段表明，直观上基于同步通信的原始π演算，在其语法内部包含了一个表达力强的异步通信模型。但是，上述定义的非确定性选择算子无法用这种方式表达，因为无卫选择会被转换为有卫选择；这一事实已被用于证明异步演算的表达力严格弱于同步演算（带有选择算子的情况）。^[9]

多元π演算（Polyadic π-calculus）允许在单个动作中通信多个名称：${\displaystyle {\overline {x}}\langle z_{1},...,z_{n}\rangle .P}$（多元输出）和${\displaystyle x(z_{1},...,z_{n}).P}$（多元输入）。这种多元扩展（在研究名称传递进程的类型时特别有用）可以通过传递一个私有通道的名称编码到一元演算（monadic calculus）中，然后通过该私有通道按顺序传递多个参数。该编码通过以下子句递归定义：

${\displaystyle {\overline {x}}\langle y_{1},\cdots ,y_{n}\rangle .P}$ is encoded as ${\displaystyle (\nu w){\overline {x}}\langle w\rangle .{\overline {w}}\langle y_{1}\rangle .\cdots .{\overline {w}}\langle y_{n}\rangle .[P]}$

${\displaystyle x(y_{1},\cdots ,y_{n}).P}$ is encoded as ${\displaystyle x(w).w(y_{1}).\cdots .w(y_{n}).[P]}$

所有其他进程构造在编码中保持不变。

在上式中，${\displaystyle [P]}$表示以相同方式对后续进程${\displaystyle P}$中的所有前缀进行编码。

并不需要复制算子${\displaystyle !P}$的全部能力。通常，人们只考虑“复制输入”${\displaystyle !x(y).P}$，其结构同余公理为${\displaystyle !x(y).P\equiv x(y).P|!x(y).P}$。

诸如${\displaystyle !x(y).P}$的复制输入进程可以理解为服务器，在通道x上等待客户端调用。调用服务器会生成进程${\displaystyle P[a/y]}$的一个新副本，其中a是客户端在调用过程中传递给服务器的名称。

可以定义高阶π演算（Higher order π-calculus），其中不仅可以传递名称，还可以通过通道传递进程。高阶情况的关键归约规则是：

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

这里，${\displaystyle Y}$表示一个“进程变量”，可以被实例化为一个进程项。Sangiorgi证明了传递进程的能力并不会增加π演算的表达力：传递进程P可以通过仅传递一个指向P的名称来模拟。

π演算是一个通用的计算模型。这一点最早由Milner在他的论文《函数即进程》（Functions as Processes）中观察到，^[10]其中他在π演算中提出了两种λ演算的编码。一种编码模拟了及早（按值调用）求值策略，另一种编码模拟了正规序（按名调用）策略。在这两种编码中，关键的洞察是将环境绑定（例如，“x绑定到项${\textstyle M}$”）建模为复制代理，这些代理通过回传指向项${\displaystyle M}$的连接来响应对其绑定的请求。

使这些编码成为可能的π演算特性是名称传递和复制（或者等价地，递归定义的代理）。在缺乏复制/递归的情况下，π演算不再是图灵完备的。这一点可以从以下事实看出：对于无递归的π演算，甚至对于有限控制π演算——其中任何进程中的并行组件数量都受某个常数上限的限制——互模拟等价性变得可判定。^[11]

与进程演算一样，π演算允许定义互模拟等价（bisimulation equivalence）。在π演算中，互模拟等价（也称为互模拟性，bisimilarity）的定义既可以基于归约语义，也可以基于带标号迁移语义。

在π演算中，（至少）有三种定义带标号互模拟等价的不同方法：早（Early）、晚（Late）和开放（Open）互模拟性。这源于π演算是一种传值进程演算这一事实。

在本节的剩余部分，我们令${\displaystyle p}$和${\displaystyle q}$表示进程，${\displaystyle R}$表示进程上的二元关系（binary relation）。

早互模拟性和晚互模拟性都是由Milner、Parrow和Walker在他们关于π演算的原始论文中制定的。^[12]

进程上的二元关系${\displaystyle R}$是一个早互模拟（early bisimulation），如果对于每一对进程${\displaystyle (p,q)\in R}$：

• whenever ${\displaystyle p\,{\xrightarrow {a(x)}}\,p'}$ then for every name ${\displaystyle y}$ there exists some ${\displaystyle q'}$ such that ${\displaystyle q\,{\xrightarrow {a(x)}}\,q'}$ and ${\displaystyle (p'[y/x],q'[y/x])\in R}$;
• for any non-input action ${\displaystyle \alpha }$, if ${\displaystyle {p{\xrightarrow {\overset {}{\alpha }}}p'}}$ then there exists some ${\displaystyle q'}$ such that ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$ and ${\displaystyle (p',q')\in R}$;
• 以及${\displaystyle p}$和${\displaystyle q}$互换后的对称要求。

如果存在某个早互模拟${\displaystyle R}$使得${\displaystyle (p,q)\in R}$，则称进程${\displaystyle p}$和${\displaystyle q}$是早互模拟的，记作${\displaystyle p\sim _{e}q}$。

在晚互模拟性中，迁移匹配必须独立于被传输的名称。进程上的二元关系${\displaystyle R}$是一个晚互模拟（late bisimulation），如果对于每一对进程${\displaystyle (p,q)\in R}$：

• whenever ${\displaystyle p{\xrightarrow {a(x)}}p'}$ then for some ${\displaystyle q'}$ it holds that ${\displaystyle q{\xrightarrow {a(x)}}q'}$ and ${\displaystyle (p'[y/x],q'[y/x])\in R}$ for every name y;
• for any non-input action ${\displaystyle \alpha }$, if ${\displaystyle p{\xrightarrow {\overset {}{\alpha }}}p'}$ implies that there exists some ${\displaystyle q'}$ such that ${\displaystyle q{\xrightarrow {\overset {}{\alpha }}}q'}$and ${\displaystyle (p',q')\in R}$;

• 以及${\displaystyle p}$和${\displaystyle q}$互换后的对称要求。

如果存在某个晚互模拟${\displaystyle R}$使得${\displaystyle (p,q)\in R}$，则称进程${\displaystyle p}$和${\displaystyle q}$是晚互模拟的，记作${\displaystyle p\sim _{l}q}$。

${\displaystyle \sim _{e}}$和${\displaystyle \sim _{l}}$都有一个问题，即它们不是同余关系，这意味着它们不能被所有的进程构造所保持。更确切地说，存在进程${\displaystyle p}$和${\displaystyle q}$使得${\displaystyle p\sim _{e}q}$但${\displaystyle a(x).p\not \sim _{e}a(x).q}$。可以通过考虑包含在${\displaystyle \sim _{e}}$和${\displaystyle \sim _{l}}$中的最大同余关系来解决这个问题，分别称为早同余和晚同余。

幸运的是，第三种定义是可能的，它避免了这个问题，即Sangiorgi提出的开放互模拟性（open bisimilarity）。^[13]

进程上的二元关系${\displaystyle R}$是一个开放互模拟，如果对于每一对元素${\displaystyle (p,q)\in R}$以及对于每一个名称替换${\displaystyle \sigma }$和每一个动作${\displaystyle \alpha }$，每当${\displaystyle p\sigma {\xrightarrow {\overset {}{\alpha }}}p'}$时，都存在某个${\displaystyle q'}$使得${\displaystyle q\sigma {\xrightarrow {\overset {}{\alpha }}}q'}$且${\displaystyle (p',q')\in R}$。

如果存在某个开放互模拟${\displaystyle R}$使得${\displaystyle (p,q)\in R}$，则称进程${\displaystyle p}$和${\displaystyle q}$是开放互模拟的，记作${\displaystyle p\sim _{o}q}$。

早、晚和开放互模拟性是不同的。它们具有真包含关系，因此${\displaystyle \sim _{o}\subsetneq \sim _{l}\subsetneq \sim _{e}}$。

在某些子演算（如异步π演算）中，已知晚、早和开放互模拟性是重合的。然而，在这种背景下，更合适的概念是异步互模拟性。

在文献中，术语开放互模拟通常指的是一个更复杂的概念，其中进程和关系由区分关系（distinction relations）索引；详情参见上述Sangiorgi的论文。

或者，可以直接从归约语义定义互模拟等价。如果进程${\displaystyle p}$立即允许在名称${\displaystyle a}$上进行输入或输出，我们记作${\displaystyle p\Downarrow a}$。

进程上的二元关系${\displaystyle R}$是一个倒刺互模拟（barbed bisimulation），如果它是一个对称关系，并且满足对于每一对元素${\displaystyle (p,q)\in R}$，我们要么：

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

并且

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

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

如果存在一个倒刺互模拟${\displaystyle R}$使得${\displaystyle (p,q)\in R}$，我们称${\displaystyle p}$和${\displaystyle q}$是倒刺互模拟的。

定义上下文为带有一个空洞[]的π项，如果不论对于什么上下文${\displaystyle C[]}$，我们都有${\displaystyle C[P]}$和${\displaystyle C[Q]}$是倒刺互模拟的，则称两个进程P和Q是倒刺同余的（barbed congruent），记作${\displaystyle P\sim _{b}Q\,\!}$。事实证明，倒刺同余与由早互模拟性诱导的同余相重合。

π演算已被用于描述许多不同类型的并发系统。事实上，一些最新的应用已经超出了传统计算机科学的范畴。

1997年，马丁·阿巴迪和Andrew Gordon提出了π演算的一个扩展——Spi-演算，作为描述和推理密码学协议的形式化符号。Spi演算用加密和解密原语扩展了π演算。2001年，马丁·阿巴迪和Cedric Fournet推广了密码学协议的处理，提出了应用π演算（applied π calculus）。现在有大量工作致力于应用π演算的变体，包括许多实验性验证工具。其中一个例子是由Bruno Blanchet开发的工具ProVerif[2]，它基于将应用π演算翻译成Blanchet的逻辑编程框架。另一个例子是由Andrew Gordon和Alan Jeffrey开发的Cryptyc[3]，它使用Woo和Lam的对应断言（correspondence assertions）方法作为类型系统的基础，以检查加密协议的认证属性。

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

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

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

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

• 业务流程建模语言(BPML)
• occam-π
• Pict
• JoCaml（基于Join演算）
• RhoLang

• Milner, Robin. Communicating and Mobile Systems: The π-calculus. Cambridge, UK: Cambridge University Press. 1999. ISBN 0-521-65869-1.  含有內容需登入查看的頁面 (link)
• Milner, Robin. The Polyadic π-Calculus: A Tutorial. F. L. Hamer; W. Brauer; H. Schwichtenberg (编). Logic and Algebra of Specification. Springer-Verlag. 1993. 
• Sangiorgi, Davide; Walker, David. The π-calculus: A Theory of Mobile Processes. Cambridge, UK: Cambridge University Press. 2001. ISBN 0-521-78177-9. 
• Mironov, Andrew. A simple proof of the coincidence of observational and labeled equivalence of processes in applied pi-calculus. 2025.