Π演算

在理论计算机科学中，π演算（或）是一种进程演算模型。

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

π演算语法简单，但表达能力很强（参见）。函数式程序可以被表示成π演算，这种表示强调了计算的对话本质，并与博弈语义建立了联系。π演算的扩展形式，如spi演算和应用π演算（applied π），在分析和推理方面获得了成功。除了用于描述并发系统的最初用途外，π演算也被用于推理、分子生物学（精确定义见下一节）：

• 并发（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将π演算的发展描述为试图捕捉演员模型中值和进程的一致性。

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

• (BPML)

*
*

• （基于）
• RhoLang

注释
参考文献
*
*
*
*