可计算性理论模型初识(三):ρ-演算

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

概述

上一篇文章中我们介绍了π-演算—一个基于名称理论的进程演算,因此他并非一个封闭的理论(译者注:封闭理论即一个理论没有对其他环境的依赖,π-演算可看做基于名称理论提供了一套名称间相互通信进程的理论,因此该理论不是封闭的)。本文将介绍的ρ-演算是一个基于引用概念的异步消息传递演算。且ρ-演算中的名称完全依赖于进程理论(译者注:简单可理解为名称由进程创建,该理论中名称也被视为一种特殊的进程—引用进程,quoted process),因此它是一个封闭的理论。ρ-演算或称为RHO-演算是为Refective,High-Order Calculus(反射高阶演算)的缩写。这里“反射”的意思是名称和进程之间的转换(通过引用和解除引用);“高阶”的意思是结果语言表达力很强。(译者注:高阶这里意思可能与高阶函数一致,比如上一篇π-演算中介绍的函数嵌套A(B(x)),只不过ρ-演算中的高阶函数通过反射而不是进程变量来表示)

本文是可计算性理论模型初识系列的最后一篇,后面的文章中我们会依照DoCC的课程继续讲解。

ρ-演算

ρ-演算由π-演算进化而来。在π-演算中,名称和进程是两个截然不同的对立存在。然而在ρ-演算中,我们有用于将名称和进程互相转换的构造函数。核心思想是进程即为程序,名称即为进程的引用,代表了进程中的代码。因此我们可以运行一个进程,即执行一个程序,引用进程捆绑其代码并发送这段代码到另一个通道中,并取消代码的引用以获取一段程序的运行实例。

与π-演算中一致的是,ρ-演算中我们通过消息传递来表示不同代理间的交互。

语法

ρ-演算的BNF表达式,以Rholang规范表示如下:

P,Q ::= 0 | for(← x)x!(P)| P|| *x

x,y ::= @P

该表达式有很多与π-演算相似的地方。如π-演算中的停止进程,发送,接受及并行组合也同样包含于ρ-演算中。主要差异即在于ρ-演算中可以将进程引用为一个名称并可以将名称解除引用为一个进程,这个特性增强了ρ-演算的表达能力。

  • 停止进程:0

P,Q ::= | for(y ← x)P | x!(P) | P|Q | *x

x,y ::= @P

停止进程是一个原子进程,表示“什么都不做”。所有ρ-演算都可以从这个特殊的进程构造出来。这里与λ-演算和π-演算的所有项都是由名称构造出来的方式类似。主要区别在于我们不需要一组名称来构造项。使用停止进程即可以完成名称类似的工作。

  • for输入:for(← x)P

P,Q ::= 0 | for(← x)P x!(P) | P||*x

x,y ::= @P

该进程类似于π-演算中的输入前缀x(y).P。此进程在通道x上等待接收消息,当收 到消息时置换进程P中的名称y并执行P。

  • 在通道x上发送:x!(P)

P,Q ::= 0 | for(← x)x!(P) | P||*x

x,y ::= @P

引用进程@P被发送到通道x。该进程类似于π-演算中的输出进程x̅y.P。但在ρ-演算中我们可以使用解除引用将消息转换为进程。

  • 进程并行组合:Q

P,Q ::= 0 | for(← x)x!(P)| P|| *x

x,y ::= @P

进程P和Q并行运行,与π-演算一致。

  • 解除引用:*x

P,Q ::= 0 | for(← x)x!(P)| P|*x

x,y ::= @P

*x—读作”drop x”—可以将一个名称转换为其所代表的进程(因为所有名称都是引用的进程)要将名称@P转换为进程,解除引用即可。

  • 名称都是引用的进程:@P

P,Q ::= 0 | for(← x)x!(P)| P|| *x

x,y ::= @P

每个名称都是一个引用的进程。这个可理解为:名称是计算机代码,进程即是计算机的程序;代码是静态的,进程是动态的。给定一个程序(进程)我们可以写出它的代码(引用);而我们有了代码(名称),我们就可以执行一段程序(解除引用)。因此我们认为进程*@P与P是一致的,即语义置换的结果。

我们从停止进程0开始,来构造ρ-演算中的所有名称和进程。我们先简单构造几个ρ-演算进程,之后再进入结构同余、其他等价概念、句法语义置换及操作语义等内容的介绍。

  • 0

这是最简单的进程,什么都没有发生。

  • *0

这是错误的语法—ρ演算规定只能解除引用一个名称,0是一个进程,因此这不是一个有效的ρ-演算进程。

  • 0 | 0

这可以说是第二简单的进程—并行运行两个停止进程,该进程可以简化吗?

  • *@0

因为0是最简单的进程,@0即为最简单的名称,*@0即解除@0的引用。该进程可以简化吗?

  • @(0 | 0)!(0)

0 | 0是一个进程,因此@(0 |0)是一个供发送消息的通道的名称。此进程在通道@(0 | 0)上发送@0。

  • for(@(0 | 0) ← @0)0

该进程在通道@0上等待接收消息,收到后会在进程0中用接受到的消息替换@(0 | 0)并运行进程0。

  • @0!(0) | for(@0 ← @0)0

该进程在通道@0上同时发送和接收消息@0。如在π-演算中一致,该进程会导致进程间的通信。

  • @(@0!(0))!(0)

由于@0!(0)是一个进程,可以用它来形成名称@(@0!(0)),因此该进程即在通道@(@0!(0))上发送名称@0。

  • for(@0 ← @(0 | 0))@0!(0)

此进程在通道@(0 | 0)等待接收消息替换进程@0!(0)中的名称@0。

后面我们来讨论ρ-演算中的多种等价概念。

等价概念

结构同余

像π-演算中一样,我们期望从计算的角度来看某些进程是等价的。同样,由符号“≡“表示的等价被称为结构同余。这是最基础的等价,包含α等价在内的等价均满足如下内容:

  • P | 0 ≡ P
  • P | Q ≡ Q | P
  • (P | Q) | R ≡ P | (Q | R)

结构同余只与进程有关,与名称无关。

名称等价

名称等价(由≡N来表示)包含两种情况:(1)单个名称的引用与解除引用;(2)结构同余进程的引用。

(1)@(*x) ≡N  x

这个等式表示引用一个解除引用的名称,与原名称是等价的。这里的思路等于如果我们将代码转换为程序并再将程序转换回代码,则只是简单的重现了最开始的代码而已。

(2)如果 P ≡ Q, 则有@P ≡N @Q

该等价表明如果两个进程P和Q是结构同余的,则引用两个进程的名称@P和@Q也是等价的。即具有相同效果的两个程序应该也拥有相同的两段代码。

译者注:这里无需纠结说两个效果相同的程序可能拥有不那么一致的高级语言代码,如果这里的代码都视为给同平台编写的同版本汇编语言的话,应该还是比较一致的。

α-等价

回想λ-演算中α-转换的概念,两个结构相同只有名字不同的两个项是等价的。在ρ-演算(以及π-演算)中有个类似的概念被称为α-等价,用≡α来表示。两个ρ-演算如果仅是他们所使用的名称不同,则可称为α等价。即 P ≡α Q,则P和Q仅仅是构造它们的名称不同。两个有效的α等价的进程举例:

x!(0) ≡α y!(0)

P | for(y ← x)0 ≡α P | for(w ← u)0

两个α等价的进程拥有相同的代码,因为他们代表相同的程序。

置换及操作语义

正如其他演算,ρ演算也同样拥有置换规则以及这些置换在计算方面的含义,即通信规则(comm rule)。 我们将用(P){y/ x}表示在进程P中用名称y置换名称x。

句法置换

句法置换的规则决定了名称的置换如何转换为进程的置换(因为进程也是从进程0和名称构建的)。在名称层面上,置换是直截了当的,但我们必须在一个进程中建立名称置换的概念。因此,我们对每个项的构造函数都有一个规则,进程中名称置换的基本规则如下:

  • (0){@Q/@P} = 0

在停止进程中对名称做任何置换都不会改变停止进程。

  • (!R){@Q/@P} = !(R){@Q/@P}

(译者注:这里”!”前面没有名称,不是通道发送,是复制,与π-演算中一致,参考上一篇π-演算中的介绍。该等式即先复制R再置换名称与先置换R中的名称再复制是效果一致的)

如果只有一个被复制的进程内的名称被置换,则我们可以先做置换名称后复制置换后的进程。

  • (R | S){@Q/@P} = (R){@Q/@P} | (S){@Q/@P}

在两个并行运行的进程中做名称置换,等于将两个进程分别置换后再并行运行。

  • (x!(R)){@Q/@P} = (x){@Q/@P}!((R){@Q/@P})

发送进程的名称置换。首先,我们先把通道名称x进行适当的置换,即(x){@ Q / @ P},这是一个可以发送消息的新通道。然后,我们将进程R进行适当的置换即(R){@ Q / @P},这是准备在通道上发送的新消息。

  • (for(y ← x)R){@Q/@P} = for(z ←(x){@Q/@P})((R){z/y}){@Q/@P}

接收进程的名称置换。这个规则看起来有点复杂,我们拆开来看。第一步,我们为接收通道x进行名称置换,即(x){@Q/@P}。之后,我们将名称y改变为名称z。因为我们改变了这个名称标签,所以需要在进程R中将z置换为y,即(R){z/y}。最后,我们需要为(R){z/y})进行名称置换,即(R){z/y}){@Q/@P}。

  • 若 x ≡N @P,则(*x){@Q/@P} = *@Q;否则有(*x){@Q/@P} = *x

置换解除引用的名称是直截了当的。如果名称x即为名称@P,则我们进行预期的置换即将x置换为@Q。如果x不等于@P,则该置换对*x没有任何改变。

通用的名称置换有如下规则:

x ≡N @P,则(x){@Q/@P} = @Q;否则有(x){@Q/@P} = x

而在ρ-演算中,我们也要考虑等价名称的置换。

这些句法置换规则告诉我们如何进行进程的置换,但并没有告诉我们这些置换在计算方面意味着什么。这就是语义置换将要说明的地方。

语义置换

语义置换概念可以给我们一些具体的理解。上文中讨论了引用进程和解除引用名称,引用进程是如何成为名称,以及如何解除引用名称获取进程,但我们没有明确地将这两个概念联系起来。

上文中我们介绍了如下规则:

x ≡N @P,则(*x){@Q/@P} = *@Q;否则有(*x){@Q/@P} = *x

即我们在取消引用的进程中用@Q置换@P,如果x等同于@P,则得到进程Q;否则即可以完全忽略该置换进程。

而这正是我们需要的,以确保我们可以将进程视为程序而将名称作为代码。我们希望能够获取程序(进程),记下其代码(引用进程),然后将代码作为程序运行(解除引用的进程)并返回原始程序(进程)。语义置换即是将上述内容结合在一起。

操作语义

ρ-演算中也有通信的概念。当在同一个通道中同时发送和接收消息时即发生通信。通信的形式即进程的规约:

x!(Q) | for(z ← x)P → (P){@Q/z}

可以使用名称来扩展这种通信的概念,相当于将通信推广到具有等价名称的通道上发送和接收消息:

  • 通信规则:如果x ≡N y,则有如下规约

x!(Q) | for (z ← y)P → (P){@Q/z}

该规则表明并行运行的发送进程x!(Q)与接收进程for (z ← y),具有相同名称xy的通道,可以进行名称的置换后进行规约为(P){@Q/z}。该规则使我们可以使用代理代替已经引用为名称的进程进行同步及通信。

与π-演算相同,通信规则也可以与并行组合和结构同余共同使用:

  • 并行组合:如果P→P',那么P | Q→P'| Q

该规则表明如果P可以规约为P',则P | Q可以规约为P'| Q。

  • 结构同余:如果有P≡P'Q≡Q',且P'→Q',则P→Q

该规则表明,如果我们有进程P与P'结构同余,进程Q与Q'结构同余,且P'可以规约为Q',则P也可以规约为Q。

下面我们举一些例子来帮助我们理解。

1.@0!(0) | for(@(@0!(0)) ← @0)0 → 0

发送进程@0!(0)与接收进程for(@(@0!(0)) ← @0)0使用同一个通道@0,因此由通信规则可规约为

(0){@0/@(@0!(0))}

又因为句法置换中我们介绍到(0){z/y} = 0,所以该进程最终被规约为0

2.for(@0 ← x)@0!(0)| x!(@0!(0)) → @(@0!(0))!(0)

首先可以注意到发送和接收都在通道x上,因此发生了通信。为了简化上述公式,我们使P = @0!(0)Q = @0!(0),则上述公式可简化为:

for(@0← x)P | x!(Q)

使用通信规约可得:

(P){@Q/@0}

展开P和Q得到:

(@0!(0)){@(@0!(0))/@0}

使用发送进程的句法置换规则有:

(@0){@(@0!(0))/@0}!((0){@(@0!(0))/@0})

接着使用置换规则可将上式简化为:

@(@0!(0))!(0)

因此原表达式可以简化为在通道@(@0!(0))发送@0

3.for(@0 ← @(@0!(0)))*(@0) | @(@0!(0))!(!(@0!(0))) →!(@0!(0))

首先我们看下这里发生了什么。有两个进程在并行运行,接收进程为for(@0 ← @(@0!(0)))*(@0),发送进程为@(@0!(0))!(!(@0!(0))) →!(@0!(0))。为了简化公式,我们这里设y = @0, P = *y, Q = y!(0), x = @Q, R =!Q。我们将原始公式简化为:

for(y← x)P | x!(R)

这里我们可以清楚的看到接收和发送通道相同触发了通信规约,有:

(P){@R/y}

将展开后得:

(*y){@R/y}

依据解除引用的语义置换,该表达式可简化为R,即:

!(@0!(0))

上述表达式的意思为复制在通道@0上发送消息@0

 

综上,本文简单介绍了ρ-演算,也是可计算性理论模型初识系列的最后一篇。后面的文章中我们将开始DoCC课程的跟进讲解。

 

参考资料

[1]COMPUTATIONALCALCULUS PRIMER PART 3: Ρ-CALCULUS (https://blog.rchain.coop/calculus-primer-%CF%81-calculus/

[2]Meredith, Radestock (2005). A Reflective Higher-Order Calculus. Retrieved June16, 2018. (https://www.sciencedirect.com/science/article/pii/S1571066105051893)

转载地址:https://mp.weixin.qq.com/s?__biz=MzU0MzY4NDQ4MQ==&mid=2247483919&idx=1&sn=1ef5d041c165a02a7074b743f2ceb3cd&chksm=fb06e0e1cc7169f72d44b53ae4cbb6da74695c44526a4207abe1cc3ebb7caea8bbf67b2f4917&mpshare=1&scene=23&srcid=0903iQVr5w7dJpgsZz3seCCE#rd

发表评论

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