- A+
概述
在本系列文章的第一篇中我们介绍了λ演算的语法和操作语义。
本篇将会介绍另一种可计算性理论中的计算模型—π演算。之所以介绍π演算，是因为它是并发计算的基础模型，并且是ρ演算的理论先驱。具体来说，π演算是一种基于命名概念的进程演算。在进程演算中，我们将独立的代理或进程间的交互表示为消息传递，而非共享变量的修改（如在λ演算中）。
π演算与λ演算的区别源于其包含的名称与进程，及一些与λ演算所不同的构造项，也包含了负责实现并发的并行进程组合。因此，π演算中存在两个不同的实体，进程与名称，并且包含进程与名称间不同的交互内容。与λ相同的是，π演算中进程也是由名字构造的。
并行组合方式允许进程中的计算并行或独立进行，也可以在共享通道上进行通信。这对智能合约类应用和虚机存储状态转换非常有意义。
在下文中，我们会讨论π演算的语法，结构同余及语义操作。
π演算
这里我们会介绍Robin Milner所提出的π演算的简化版本。
语法
π演算的BNF表示：
P,Q ::=0 | x(y).P | x̅⟨y⟩.P | (𝜈x)P | P|Q |!P (1.1)
如λ演算一样，x可以看做集合X中的参数，就算我们不了解上述表达式的含义，仅依据上一篇文章中的介绍，我们即可知该表达式也可以写作：
P[X]::= 0 | X(X).P[X] | X̅⟨X⟩.P[X]| (𝜈X)P[X]| P[X]|P[X] | !P[X]
以明确表示该表达式对集合X的依赖。
回到表达式（1.1），该语法中的合规项，即等号右侧的一系列表达式，也可被称为项构造函数。接下来我们讨论下这些项构造函数。
停止进程：0
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P |(νx)P | P|Q | !P
这个进程代表“什么都不做”，即执行已经完成，进程已经停止。
输入前缀进程：x(y).P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P |(νx)P | P|Q | !P
此进程表示:等待一个名称被发送到通道x，并用该新名称替换进程P中的名称y。这个过程与λ演算中λy.P项—进程P中绑定名称y—是类似的作用。
输出前缀进程：x̅⟨y⟩.P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q |!P
在通道x上将名称y作为替代名称发送到等待通道x的输入前缀进程中，然后运行进程P。
（译者：在π演算中，上述该三种进程被统一描述为π.P，其中π被称为前缀，π.P被称为前缀进程，其中π可以为空即停止进程，x(y).P即输入前缀进程，x̅⟨y⟩.P即输出前缀进程，详见参考资料[1]）
限制或创建新名称：(νx)P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P | (νx)P | P|Q |!P
（νx）P-读作“new x in P” (在P进程中的创建新名称x)- 将x定义为新名称并在过程P中将其绑定。
平行组合：P|Q
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P |(νx)P | P|Q | !P
P|Q - 读作“P par Q” - 表示进程P和Q同时有效; 他们可以独立行动，也可以互相沟通。
复制：!P
P,Q ::= 0 | x(y).P | x̅⟨y⟩.P |(νx)P | P|Q | !P
!P - 读做“bangP” - 表示P | P |...，可以按需复制大量副本。此进程始终可以创建P的新副本。规约规则会限制其不会出现无限并发活动的风险。
π演算中的每个进程都是从停止进程0构建的。让我们从0开始构建一些简单的进程。
一些简单的进程
- 0
这是最简单的进程，所有其他进程都由它创建。
- x(y).0
此进程等待通道x上的消息y然后停止。
- x̅⟨y⟩.0
此进程在通道x上发送消息y，然后停止。
- (νx)0
此进程在已停止的进程中声明一个新名称x。
你是否觉得这个进程有与我们上面已有的进程有重复？
- 0|0
已停止的进程与已停止的进程同时运行。
你是否觉得这个进程有与我们上面已有的进程有重复？
- x̅⟨y⟩.0 | x(z).0
此进程同时在通道x上发送和接收消息。进程间的通信就是这么发生的。
同时在同一通道上发送和接收消息即允许在该通道上进行通信。一般来说，过程x̅⟨y⟩.P| x(z).Q对应于通道x上的通信。所以说x和x̅是名称/协同名称的关系。
结构同余
译者注：同余关系即代数系统的集合中的等价关系，此处结构同余即结构一致的意思。
直觉上我们会觉得上述例子中某些进程之间存在等价关系。例如，P|0，0|P和P都应该是等价的。我们来看下是否真的如此。
过程P|0意味着我们正在同时运行已停止的进程0和进程P，这与进程P独自运行不应该有任何不同。一般来说，我们用P≡Q表示过程P和Q的结构一致性。我们的“直觉”可以由如下结构同余的公理来描述
- α等价
如果可以通过重命名P中绑定的一个或多个名称从而获得Q，则可以称P≡Q（我们将在后面的系列文章中更深入地讨论自由/绑定名称）。这类似于λ演算中的α转换。如果两个程序仅仅其中使用的变量名称不同而其他结构相同，则可以称两个程序是相同的。它们执行相同的代码，但可能以相同的方式通过不同的名称调用执行。
- 并行组合公理
- P | Q ≡ Q | P并发进程的顺序无关紧要，因为它们同时执行。因此，进程P| Q和Q | P是等价的。
- (P | Q)| R ≡ P | (Q | R)par运算符（可以理解为或运算）应该是关联的。上面我们讨论了将两个进程并行运行，如果我们想把三个进程放在一起，有两种不同的方法可以做到这一点。这种等价表示这两种方式是相同的，因为我们会同时运行这三个进程。
- P | 0 ≡ P运行已停止的进程0与进程P，和单独运行P不应该有任何不同。这个等价就是这个意思，使用已停止进程0与其他进程并行组合就相当于任意数字与0求和。
- 限制公理
- (𝜈x)(𝜈y)P ≡ (𝜈y)(𝜈x)P在进程中声明新名称时，顺序无关紧要。上面的公理即描述这一概念。
- (𝜈x)0 ≡ 0在已停止的进程中声明新名称不应执行任何操作。因此，它应该等同于停止的进程。
- 复制公理
- !P ≡ P | !P通过复制进程，我们始终可以创建进程的新副本。因此，进程!P和P|!P是等价的。
- 与限制和并行有关的公理
如果名称x在Q中绑定，则 (νx)(P | Q) ≡ (νx)P | Q
以上便是π演算中结构同余的性质。结构同余与计算不可分割，也就是说，从计算的角度来看，两个结构同余进程的运算结果是相同的。
结构同余是数学中所谓的等价关系的一个例子。这里我们将其视为进程的运算也是等价的。
下面我们将精确地描述π演算中的通信概念并介绍操作语义。
操作语义（即规约规则）
回想一下表达式(1.1)，前缀x̅⟨y⟩表示在通道x上发送消息y，前缀x(z)表示在通道x上接收消息z。当同一通道上的发送和接收同时发生时，发生通信，接收消息进程收到信息并使用。表达式如下：
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
→是“规约”符号，我们称之为通信规约或通信规则。这意味着如果我们发现两个进程x̅⟨y⟩.P和x(z).Q并发运行，则y在通道x上发送，y代替进程Q中的z，进程P和Q {y/z}并发运行。这类似于λ演算中的β规约。这个规则很重要，这里再强调一遍：
- 通信规则
x̅⟨y⟩.P | x(z).Q → P | Q{y/z}
当通信规则与并行组合、限制和结构同余组合时有：
- 并行组合
如果P → Q, 则有P | R → Q | R.
- 限制
如果P → Q, 则有(𝜈x)P → (𝜈x)Q.
- 结构同余
如果P ≡ P’, Q ≡ Q’, 且P’ → Q’, 则有P → Q.
下面我们来介绍更多的例子来帮助大家理解上述内容。
(1) x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
证明：前两个过程x̅⟨y⟩.0和x(z).P将发生通信，可得：
x̅⟨y⟩.0 | x(z).P → 0 | P{y/z}
并且由并行公理已知0 | P {y / z}≡P{y / z}，因此在通信规则与并行公理共同作用下，可得：
x̅⟨y⟩.0 | x(z).P | Q → P{y/z} | Q
(2) x̅⟨y⟩.0 | x(u).P | x(v).Q 不唯一规约
表达式中有两种可能发生的通信（x̅⟨y⟩.0 | x(u).P与x̅⟨y⟩.0 | x(v).Q），我们有两个有效的规约。 其中一种规约是由第一和第二项之间的通信引起的，即规约为：
P{y/u}| x(v).Q
另一种规约来自第一和第三项之间的通信，即规约为：
x(u).P| Q{y/v}
(3) (νx)(x̅⟨y⟩.0 | x(z).P) | x(u).Q → P{y/z} | x(u).Q
证明：与前一个示例相反，在并行组合中将名称x限制为前两个项即不会发生不一致规约。这里，由（νx）限制的名称x与出现在项x(u).Q中的名称x不同。因此，只有前两个项通讯导致规约，可得：
P{y/z} | x(u).Q
(4) !x̅⟨y⟩.0 | x(u).P→ !x̅⟨y⟩.0 | P{y/u}
证明：我们知道!x̅⟨y⟩.0≡!x̅⟨y⟩.0| x̅⟨y⟩.0因复制操作总是允许创建另一个副本。现在我们在x̅⟨y⟩.0和x(u).P之间有一个通信发生，并可以规约为P {y/u}。因此，我们可得：
!x̅⟨y⟩.0 | P{y/u}
综上所述，π演算是基于命名概念的并发计算模型，其中我们将代理之间的交互表示为消息传递。当同一个通道上同时存在发送和接收进程时便会发生消息传递。在π演算中区分名称和进程，并可以让两个进程并行计算。这也是π演算与λ演算最主要的差异。
如果您需要学习π演算的完整版本，请参阅参考文献[1]。这里我们并没有讨论选择运算符和进程运算，因为我们引入π演算的意图是了解其并发性以及如何在语法中处理它。
以上两篇可计算理论模型初识系列文章的目的是引出ρ演算并为DoCC课程学习奠定基础，我们将在下一篇文章中实现我们的目标。
参考资料
[1]Computational calculi primer Part 2: π-calculus (https://blog.rchain.coop/calculus-primer-%CF%80-calculus/)
[2]The Polyadic π-Calculus: A Tutorial (http://www.lfcs.inf.ed.ac.uk/reports/91/ECS-LFCS-91-180/)
本文由微信公众号:Rchain中文社区 翻译
