可计算性理论模型初识(二):π演算

  • A+
所属分类:RChain知识库

可计算性理论模型初识(二):π演算

概述

在本系列文章的第一篇中我们介绍了λ演算的语法和操作语义。

本篇将会介绍另一种可计算性理论中的计算模型—π演算。之所以介绍π演算,是因为它是并发计算的基础模型,并且是ρ演算的理论先驱。具体来说,π演算是一种基于命名概念的进程演算。在进程演算中,我们将独立的代理或进程间的交互表示为消息传递,而非共享变量的修改(如在λ演算中)。

π演算与λ演算的区别源于其包含的名称与进程,及一些与λ演算所不同的构造项,也包含了负责实现并发的并行进程组合。因此,π演算中存在两个不同的实体,进程与名称,并且包含进程与名称间不同的交互内容。与λ相同的是,π演算中进程也是由名字构造的。

并行组合方式允许进程中的计算并行或独立进行,也可以在共享通道上进行通信。这对智能合约类应用和虚机存储状态转换非常有意义。

在下文中,我们会讨论π演算的语法,结构同余及语义操作。

π演算

这里我们会介绍Robin Milner所提出的π演算的简化版本。

语法

π演算的BNF表示:

P,Q ::=0 | x(y).P x̅y.| (𝜈x)P||!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

这个进程代表“什么都不做”,即执行已经完成,进程已经停止。

输入前缀进程:x(y).P

P,Q ::= 0 | x(y).P | x̅y.P |(νx)P|| !P

此进程表示:等待一个名称被发送到通道x,并用该新名称替换进程P中的名称y。这个过程与λ演算中λy.P项—进程P中绑定名称y—是类似的作用。

输出前缀进程:x̅⟨y⟩.P

P,Q ::= 0 | x(y).P x̅y.P | (νx)P||!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||!P

(νx)P-读作“new x in P” (在P进程中的创建新名称x)- 将x定义为新名称并在过程P中将其绑定。

平行组合:P|Q

P,Q ::= 0 | x(y).P x̅y.P |(νx)| P|Q | !P

P|Q - 读作“P par Q” - 表示进程P和Q同时有效; 他们可以独立行动,也可以互相沟通。

复制:!P

P,Q ::= 0 | x(y).P x̅y.P |(νx)P|!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并发进程的顺序无关紧要,因为它们同时执行。因此,进程P| Q和Q | P是等价的。
    •  (Q)| ≡ | (R)par运算符(可以理解为或运算)应该是关联的。上面我们讨论了将两个进程并行运行,如果我们想把三个进程放在一起,有两种不同的方法可以做到这一点。这种等价表示这两种方式是相同的,因为我们会同时运行这三个进程。
    • P | 0 ≡ P运行已停止的进程0与进程P,和单独运行P不应该有任何不同。这个等价就是这个意思,使用已停止进程0与其他进程并行组合就相当于任意数字与0求和。
  • 限制公理
    • (𝜈x)(𝜈y)≡ (𝜈y)(𝜈x)P在进程中声明新名称时,顺序无关紧要。上面的公理即描述这一概念。
    • (𝜈x)0 ≡ 0在已停止的进程中声明新名称不应执行任何操作。因此,它应该等同于停止的进程。
  • 复制公理
    • !≡ | !P通过复制进程,我们始终可以创建进程的新副本。因此,进程!P和P|!P是等价的。
  • 与限制和并行有关的公理

如果名称x在Q中绑定,则 (νx)(Q) ≡ (νx)Q

以上便是π演算中结构同余的性质。结构同余与计算不可分割,也就是说,从计算的角度来看,两个结构同余进程的运算结果是相同的。

结构同余是数学中所谓的等价关系的一个例子。这里我们将其视为进程的运算也是等价的。

下面我们将精确地描述π演算中的通信概念并介绍操作语义。

操作语义(即规约规则)

回想一下表达式(1.1),前缀x̅⟨y⟩表示在通道x上发送消息y,前缀x(z)表示在通道x上接收消息z。当同一通道上的发送和接收同时发生时,发生通信,接收消息进程收到信息并使用。表达式如下:

x̅y.x(z).→ Q{y/z}

→是“规约”符号,我们称之为通信规约或通信规则。这意味着如果我们发现两个进程x̅⟨y⟩.P和x(z).Q并发运行,则y在通道x上发送,y代替进程Q中的z,进程P和Q {y/z}并发运行。这类似于λ演算中的β规约。这个规则很重要,这里再强调一遍:

  • 通信规则

x̅y.x(z).→ Q{y/z}

当通信规则与并行组合、限制和结构同余组合时有:

  • 并行组合

如果→ Q, 则有→ R.

  • 限制

如果→ Q, 则有(𝜈x)→ (𝜈x)Q.

  • 结构同余

如果≡ P’≡ Q’, 且P’ → Q’, 则有→ 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中文社区 翻译

查看原文

  • 作者微信
  • weinxin
  • 微信公众号
  • weinxin
avatar

发表评论

:?: :razz: :sad: :evil: :!: :smile: :oops: :grin: :eek: :shock: :???: :cool: :lol: :mad: :twisted: :roll: :wink: :idea: :arrow: :neutral: :cry: :mrgreen: