高阶移动嵌入式资源中名字传递的CPS编码

理论计算机科学电子笔记128（2005）131-150www.elsevier.com/locate/entcs高阶移动嵌入式资源中名字传递的CPS编码Mikkel Bundgaard1 Thomas Hildebrandt2Jens Chr.Godskesen3哥本哈根大学计算机科学系Rued Langgaards Vej 7，DK-2300 Copenhagen S，Denmark摘要我们在高阶移动嵌入资源（Homer）的演算中提出了同步π演算的编码，这是一种在嵌套位置中具有移动进程的纯高阶演算，定义为Bucksen的Plain CHOCS的核心进程传递子集的简单，保守的扩展。我们证明了我们的编码是完全抽象的倒钩互模拟和倒钩一致的声音。我们的编码表明，高阶进程传递与（本地）命名位置中的移动资源一起足以表达π演算名称传递。该编码采用了一种新颖的连续传递方式，以方便同步通信的编码。关键词：π演算，名称传递编码，过程传递，嵌套位置，连续传递，显式替换1介绍π演算[8，7]被大多数人认为是模拟移动系统的经典过程演算。与其前身CCS相比，其最突出的特点是通过归约规则n（m）.P|no.Q→π{o/m}P|Q1电子邮件：mikkelbu@itu.dk2 电子邮件地址：hilde@itu.dk3 电子邮件地址：jcg@itu.dk1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.033132M. Bundgaard等人理论计算机科学电子笔记128（2005）131以及创建具有静态作用域的本地名称。结合这些概念提供了π演算的大部分表达能力。值得注意的是，通过用进程的链接表示进程的位置，动态改变进程之间的通信链接的能力使得对移动计算进程进行建模成为可能十年来，这种对流动性的解释非常成功，但它也有其局限性。最近，已经提出了许多演算，例如Ambient演算[1]和Seal演算[2]，它们在嵌套位置中显式表示移动计算资源，这在π演算中不容易建模。许多提出的演算也包括π演算的名称传递能力，这增加了演算的复杂性。一个自然的问题是，名称传递是否可以单独使用嵌套位置中的移动计算资源来表示。在本文中，我们提出了同步π演算的组合编码，从而在具有嵌套位置的纯高阶演算中进行名称传递，作为对Plain CHOCS [ 11 ]的核心进程传递子集的简单保守扩展而获得Albersen证明了π演算可以在Plain CHOCS中进行编码，通过使用显式名称替换来编码动态链接。该演算是[5]中提出的高阶移动嵌入式资源的荷马演算的简化变体。荷马演算没有显式的名称替换。[11]在《古兰经》中，没有一个人是被禁止的。Homer在（本地）命名位置中引入了移动计算资源，我们的编码表明，这与高阶进程传递一起足以表达π演算名称传递，而不依赖于名称替换。该编码采用了一种新颖的连续传递方式，以方便同步通信的编码。为了便于记忆，在PlainCHOCS中引入了进程的移动性，用进程传递代替了π演算中的名字我们将分别用前缀nq（发送）和n（x）（接收）来表示这种交互。这里x是一个过程变量，接收的过程用它来代替，如归约规则所正式表示的那样nqp1n（x）.p2\p1<$p2[q/x].（ 一）像往常一样，在p2中可能有任意次数的x，这意味着过程可以被丢弃和复制，使Plain CHOCS成为非线性高阶微积分。然而，正如Albersen所指出的，进程q在被移动之前不能开始计算，一旦它开始计算，它就不能再被移动这被称为代码移动性或弱移动性，与流程移动性或强移动性相反，M. Bundgaard等人理论计算机科学电子笔记128（2005）131133可以在计算过程中移动。在Homer中，嵌套位置中的强移动计算资源通过允许额外的交互类型来引入，由两个新的互补前缀nq（资源）和n（x）（取）给出。该过程不需要。p1表示驻留在位置（或地址）n处的资源q，其可以由补充动作prefix，n（x）移动或采取。p2。正如前面的相互作用，同步是由减少nq p1n（x）. p2\p1<$p2[q/x].（二）这两种类型的交互之间的重要区别是，nq中的资源q能够通过允许向q发送资源和从q获取资源来与其位置之外的进程交互。换句话说，q的状态可以被位置n之外的进程修改。我们引入了这种交互，就像在移动资源（MR）演算[4]中一样，通过允许序列作为下行前缀中的地址来获取和发送。例如，在take前缀的地址中使用序列n1n2，q可以从在地址n1处运行的资源中的地址n2获取，如n1n2q。 qJqjj. p1<$n1n2（x）. p2\n1qJQj。 p1<$p2[q/x]。我们也允许接收地址和资源前缀中的名称序列这允许地址空间的物理嵌套结构不同于抽象结构n1n2q。 p1<$n1n2（x）. p2\p1<$p2[q/x].总而言之，两种双重类型的进程移动允许我们在嵌套位置结构中表达移动资源，该嵌套位置结构可以在本地或向上移动（和复制），并且发送可以由本地进程或子资源接收（和复制）的被动资源。上述相互作用是本文结果所需的唯一一种相互作用唯一的另一个特征是在π-演算和普通CHOCS中发现的局部名称。 设（n）p表示一个过程p，其中n是本地的。完整的荷马演算[5]也允许移动资源可以做出内部反应。然而，这需要在语义中更仔细地处理自由名称相关工作Alfressen证明了π演算的递归和名称传递可以在Plain CHOCS [11]中通过传递线而不是134M. Bundgaard等人理论计算机科学电子笔记128（2005）1311名字 表示π演算名称a的a-wire定义为：我？ . 是吗？X. c！X. nil + o？ . c？X. 一个！X.没有，其中，I和O用于指示线路是用于输入还是输出，而C用作辅助转发器。Alfresen使用了两个层次的编码方案，类似于本文中提出的编码：结构定义的编码将自由名称和由输入前缀绑定的名称转换为过程变量，并将由限制绑定的名称转换为线，在顶层，用线表示自由名称的过程变量的实例化。编码中最复杂的部分是对定义为作为分x（y）.P）1=.x [c <$→ cJ][i <$→ iJ][o <$→ oJ] |iJ！.cJ？y. （P）J\iJ\oJ.Σ我的天P）= x [c <$→cJ][i <$→iJ][o <$→oJ]|oJ！.cJ！y. （P）cJ\iJ\oJ，1 1\其中（x [c <$→cJ][i <$→iJ][ o <$→oJ]|......你好。. ）\cJ\iJ\oJ使用显式替换[c<$→cJ][i<$→iJ][o<$→oJ]来定位x的线输入。这种本地化对于编码是必不可少的，因为编码一阶演算，像π演算一样，是动态链接（名称替换）。本文提出的编码方式在一个关键的方式不同的编码由Albersen，因为荷马没有包括显式的名称替换Plain CHOCS的相反，我们获得动态链接的可能性，在（本地）位置与强移动资源进行通信。Zimmer在[12]中提出了将同步π演算编码为仅包含移动原语和环境的层次结构的受限环境演算，因此既没有通信也没有名称替换。就像本文中的演示一样，Zimmer设计了一个中间演算πesc（具有显式替换和通道的π演算），但是πesc具有显式变量和通道作为语法的一部分，我们遵循π esc演算[3]的路径，也是一个具有显式替换的π演算，并考虑我们在一个全局环境中的过程。齐默和我们的方法之间的另一个明显的区别是，移动环境的移动性是主观的，而荷马的移动性是客观的。Seal演算[2]是一个具有名称传递、非线性过程传递和命名嵌套位置的演算。 但是，在Seal中是否可以将名称传递简化为进程传递还不清楚，因为Seal语义中移动进程的作用域扩展依赖于名称传递。M. Bundgaard等人理论计算机科学电子笔记128（2005）131135一阶和高阶演算之间的联系已经在几个上下文中进行了研究，最值得注意的是在[9]中，Sangiorgi展示了包含一阶和高阶通信原语的高阶π演算如何可以在一阶π演算中表示。我们按照与[10]相同的方法，通过证明π演算过程和它们在Homer中的编码之间的运算对应，证明了π演算和它在Homer中的编码之间的对应，由此我们可以推断关于倒钩互模拟的完全抽象性和关于倒钩同余的可靠性。纲要在第二节中，我们介绍了荷马的语法和约简语义。在第三节中，我们对一元同步π-演算做了同样的工作，并引入了一个具有显式替换的π-演算。我们在第4节中介绍了编码并给出了编码的示例。在第5节中，我们证明了π演算过程之间的操作对应关系，并在荷马，完全抽象的倒钩互模拟，和健全的倒钩同余编码。2荷马我们假设e是由m和n组成的名称N的有限集合，并且n是由名称的有限集合组成的。我们让δ在非空的名称序列上取值，称为地址。我们假设一组无限的过程变量V，其范围为x和y。过程表达式的集合P然后由语法定义：p，q，r=0..普什克..（n）p... λ.X其中前缀集合Λ由语法定义.λ：：=.δ（x）在δ处接收一个资源并将其绑定到x..δ（x）从δ获取资源并将其绑定到x..δr发送资源r给δ..δrδ处的资源r流程构造函数是来自并发流程演算的标准构造函数，扩展了λ演算和Plain CHOCS中的流程变量。对于荷马的介绍，它的语义和例子，见[5]。136M. Bundgaard等人理论计算机科学电子笔记128（2005）131γ前缀δr和δ（x）对应于发送和接收前缀，CHOCS，除了路径，而不仅仅是名称被允许作为地址。允许强移动性的新前缀是前缀δr和δ（x）。我们定义δ=δ，并让限制运算符（n）绑定名称n，前缀δ（x）和δ（x）绑定变量x。 自由名和自由变量的集合fn（λ），fn（p）和fv（λ），fv（p）也像通常一样相应地定义。我们说一个没有自由变量的过程是封闭的，设Pc表示封闭过程的集合。 对于P的任意子集PJ，设PJ/α表示过程的α-等价类（关于名称和变量）表情 我们将过程p[q/x]定义为p，其中x的所有自由出现都被q替换，如果必要的话，对p进行α转换，使得q中没有自由名和变量是绑定的。为了方便起见，我们省略了尾随的0，因此将λ写成λ。0的情况。 我们让prefixing和restriction是正确的结合和绑定强于并 行 计 算 。 或 者 namesnn={n1 ， ..， nk} ， 其 中 t （ n） p 表 示（n1）· · ·（nk）p。 我们将mn写成mn，也就是简单地将mn=。最后，我们将在不会发生混淆的情况下为单例集{n}写n。2.1减少我们提供荷马通过使用上下文，结构一致性和减少规则定义的减少语义。结构同余是P/α上满足以下规则的最小同余。E1. p0 pE2. （n）0万0E3. pqq pE4. （n）（m）pE5。 （ppJ）pjjp（pjpJJ）E6. （n）p<$q<$（n）（p<$q），如果n/∈ fn（q）通常，上下文C是有洞（-）的项，我们写C（p）表示p插入上下文C的洞中。请注意，p的自由名（和变量）可以通过将p插入到上下文的hole中来绑定。我们将fn（C）定义为fn（C（0）），将fv（C）定义为fv（C（0））。求值上下文E是没有自由变量的上下文，它的洞没有前缀保护，也没有作为发送或资源前缀的对象出现，即。E：：=（−）..埃普..pE..（n）E ，对p∈Pc.由于我们的演算允许涉及任意远距离深度的项的作用，因此我们定义了一个由pathaddressγ∈N索引的p a thcontextsCnindexed的函数M. Bundgaard等人理论计算机科学电子笔记128（2005）131137єδγγδγγδγγ和一个叫“我的护士”的护士。 路径地址γ表示在其中找到了该文本的 空洞的路径，并且集合n表示该空洞的名字。我们通过C：：=（−）和d来归纳地定义文本中的路径当p，q∈Pc时，Cnm：：=δ（n）（Cmp）。 q，其中，rennnγ=n。δγ γ副条件确保路径地址中没有任何名称是绑定的。当资源从子位置占用时，我们需要处理范围扩展。为此，我们在路径上下文上定义一个开Cn\minductivivelyy：Cn\m=Cn，γ єCn1n2\mє=δ（n1\m）（Cn2\m p）如果Cn<$1n<$2 =δ（n1）（Cn2p）q和mf n（Cn<$1n<$2） = 附带条件确保打开的名称不等于作用域之外的任何名称。当应用于归约规则时，这个条件总是可以通过α-转换来满足，并确保我们可以通过使用开运算符来扩展范围，并将限制放在顶层。我们最终将\定义为Pc/α上满足以下规则的最小二元关系，并且在所有求值上下文E和结构同余下是封闭的。（send）γδγ q<$Cm<$（δ（x）. p）\q<$Cm<$（p[r/x]），如果m<$$>（fn（r）<$δ）=γ γ（take）Cm（δr. q）<$γδ（x）. p\（n<$$>m<$）（Cm<$\n<$（q）<$p[r/x]），γ γ如果n=fn（r）andndm（δfn（p））=（发送）规则表示如何将被动资源r向下发送到子位置γ，其中在地址δ处接收被动资源r，并且可能以若干副本将被动资源r替换到接收进程p中。边条件保证了r的自由名不能被路径上下文绑定。这总是可以通过α转换来保证，因此永远不会阻塞移动性。（take）规则捕获从子位置γ获取资源r，其中资源r在地址δ处运行并被替换到进程p中，可能是几个副本。open运算符用于扩展局部namesdefinedinCm在静止状态下自由发生。注意，对于γ=π，两个规则简化为引言中给出的两个简化规则（1）和（2）我们可以使用资源的可这是一个类似于[11]中的编码，除了138M. Bundgaard等人理论计算机科学电子笔记128（2005）131递归变量可能出现在子位置，这使得定义稍微复杂一些。德费恩rec x . p = def（a）（rec a x. p），其中rec a x . p=arr且r=a（x）。p [（ax）/x]，其中a/∈fv（p）.直观地，r在p中x的所有出现处放置reca x.p的副本，即rec a x.p\p[rec a x .p/x]。3π演算本文给出了一元同步π-演算，它不需要求和和重复.给出了它的句法结构、结构同余关系和反应规则。对于更全面的介绍和描述π演算，见例。[8，7]。在本文中，我们将只考虑没有复制的π演算，以便使编码的呈现，特别是编码的证明简洁。但是，既然我们可以在荷马中编码一般递归，从而编码复制，我们也可以编码复制算子。尽管荷马的一些过程构造器与π演算的构造器冲突，但我们仍然使用相同的符号，因为任何歧义都可以从上下文中轻松解决。我们让N表示一个无穷大的名字集，让m，n在N上的范围。然后，过程表达式的集合Pπ由语法P，Q：：=0..P|Q..（νn）P..nm.P..n（m）.P我们考虑π-演算项直到α-转换，并定义了与Homer相同的π-演算中的结构同余式π我们定义反应关系→π在评估上下文Eπ：：=（−）..E π|P..P|Eπ..（νn）Eπ，其中P∈ Pπ.→π则是Pπ上满足以下规则的最小二元关系，并且在所有求值上下文Eπ和结构同余下都是闭的。（React）n（m）.P|n<$mJ<$.Q→π {mJ/m}P|Q像往常一样，我们让{n/m}P表示m的所有自由出现的过程P用n代替，使用α-转换以避免n在P中被束缚。M. Bundgaard等人理论计算机科学电子笔记128（2005）131139πσ3.1具有显式替换的我们引入了一个中间演算：π演算与显式替换，以简化我们的编码证明，并使我们的编码更清晰的直觉。这种π演算与传统π演算的唯一区别是我们记录了在全局环境中发生的反应中的取代。一个环境σ与一个过程P相关联，从而产生判断：σP。 置换是从名字到名字的部分函数，我们用domσ（codomσ）表 示函数σ的定义域 （codomain ）。 此外，对 于一个判断σ<$P，我们要求domσ<$ fn（P）。 我们写idA来代替A上的恒等式。我们用Pσ表示过程，其中P中的所有自由名都按σ被同时替换。设σ[m<$→n]表示扩张的子空间σ，使得m映射到n.最后，我们用Pπσ表示过程判断集。我们像以前一样定义反应关系→πσ，除了关于下面的规则，其中第一个副条件总是可以由α满足。转换.它保证了本地名称与替换中已经存在的名称不同，特别是进程的自由名称（React σ）σn（m）.P|nJ<$mJ<$.Q →σ[m <$→σmJ]<$P|Q，若m/∈domσ∈ codomσ且σn=σNJ我们注意到，传统π-演算项和相应的显式替换项。引理3.1若P=Qσ则P→πPJ= QJσJ。4编码PJi <$σ <$Q→σJ<$QJ使得我们采用下面的简写来获取地址n处的计算资源的副本，并将副本放置在变量x中作为前缀和x，定义为ndx。p= defn（x）。（nxp）我们将N \ {v，c，s，r}中的π -演算过程编码为N中的Homer过程NJ{v，c，s，r}，其中NJ的范围为NJ，MJ，并且我们假设n∈ N到NJ∈NJ的映射是双射.的πσ140M. Bundgaard等人理论计算机科学电子笔记128（2005）131名称{v，c，s，r}用作编码4中的辅助名称。然后，我们将π演算名称n编码为移动资源（n），它可以执行两项任务：沿着名称n发送和接收。发送n= v（x）。c（y）。nx. yn= v（x）。c（y）。n（z）。（a）（a）（a）（a）段所指的人;a（zJ）。（yzJ））<$n）=s发送n接收n发送n过程可以看作是分别在位置v和c上取两个参数。在位置v上，它接受要发送的名称<$m）的编码，在位置c上接受延续<$P）的编码，从而产生以下形式的过程n<$m）<$。（P）。接收n也有两个参数：在位置v上，它有一个进程Bind b= v（x）。bjx负责绑定接收到的名称，在位置c上是延续的编码（Q），导致以下形式的过程n（z）。（a）（b）（a）（b）（a）（b）（c）（a）（b）（c）（a）（b）（c）（a）（b）（c）（a）（b）（c）（a）（b）（c）（a（zJ）。（<$Q）（？zJ））。并行地，这两个过程可以在位置n上执行同步，对应于真正的π演算同步在同步之后，接收到的名称<$m）被发送到绑定b进程，并最终与延续并行放置，从而产生<$P）<$Q）bJ<$<$m）。一个π-演算过程的编码 P 在两个层面上进行：在顶层，我们翻译所有σ中的名称。其次，我们给出了P的合成编码。令<$σP）表示以下内容.j（m）<$P）n∈domσn<$$> σn）<$，Wherem={nJ|n∈ dom σ和nσn}。 请注意，名称n（或者更准确地说，它在替换下的图像）作为资源保存在这是一个dddressnJ。限制机制限制替代名称的位置，它们直观地绑定到本地名称。那么π演算的编码过程P被定义为b_idf n（P）P）。下面归纳地给出了localnames的编码（<$−）、平行合成和非活性过程。<$（v n）P）=（n）（nJ）（<$P）<$nJ<$n）P|Q）=<$P）<$Q）（0）=04集合N′{v，c，s，r}用于可读性，可以对v和c使用相同的名称，并利用嵌套名称来区分发送和接收方法。M. Bundgaard等人理论计算机科学电子笔记128（2005）131141J我们将π演算的输出和输入前缀编码如下我知道。 P）=（a）（nJd x. （ajuvenxjuvenmJd y. 作为vy。 ascP） as（xJJ）. a（z）。xJJ））P）=（a）（nJdx . （mJ）（axarvBind m. arc（P）ar（xJJ）. a（z）。xJJ））其中Bind m= v（x）。我的天啊。如上所述，进程Bind m负责将接收到的 名称绑定到本地名称m。直觉，我知道。 P）首先在本地地址nJ处复制加密名称，并将其保存在本地地址a处。然后，获取位置mJ处的编码名称的副本，该副本与延续（P）一起被发送到在a处的编码名称。然后检索发送部分，最后丢弃位置a处的编码名称n（m）.P）使用相同的模板进行编码，但由于绑定的原因，它有点复杂。首先，我们限制了输入前缀的形式参数的位置，以确保它只对延拓可用，并且它可以被α转换。其次，我们使用Bindm进程来创建一个新位置，以包含接收到的编码名称。有几个相关的意见，从编码。首先，我们对名称替换的编码在很大程度上依赖于与本地资源通信的能力，Homer中的命名位置以及我们复制资源的能力。我们使用与本地命名位置中的资源进行通信的能力来本地化通信，而不是像CHOCS编码中那样使用名称子项我们利用Homer的非线性特性，每次使用一个名字时，都会复制一个名字的编码。其次，在编码中的几个地方使用了强移动资源：在接收n的编码中，以及在两个前缀中，我们将资源发送到本地地址，让它们进行计算，然后再次使用资源还要注意的是，π演算过程的反应和我们的π演算中的显式替换反应（以及编码）之间存在微妙的差异。π演算中的反应（P→πP）可以减少自由名的集合，而这个集合在替换中被保留，因此保持固定我们的编码。实际上，同样的情况也发生在Milner和Jensen的异步π演算（没有复制和求和）的编码中，最后，请注意编码的连续传递样式如何促进同步通信的编码。142M. Bundgaard等人理论计算机科学电子笔记128（2005）131F一πσ.4.1例作为一个例子，我们的编码如何正确地模拟π演算中的显式替换反应，我们看看这个过程，我是A nm。 m（d）。 P|n（f）。 好的 Q→πσidA[f <$→m]<$m（d）. P|你好。 Q→πσidA[f <$→m][d<$→e]<$P|Q，WhhereAisthestofreenamesinnnm. m（d）。 P|n（f）。 好的 Q. 勒廷r=<$n∈AnJ <$$>n）<$，我们得到如下约简我 知 道 。 m （ d ） 。 P ） n （ f ） . 好的 Q ） r\nm）。 分（d）。 P）n（fJ）（n（z）. （a）（f）（i）（ Q）z （j））r\n（f，J）. 分（d）。 P）fe.Q）fjm）r\n（fJ）（dJ）。<$P）<$Q）<$dJ<$<$e）<$d fJ<$m）<$dr<$=<$id[f<$→m][d <$→e]<$P|Q），whe e e efee. Q）z/f=aBindfavz。 a（zJ）。（）Q）zJ）is的部分在Bindf的帮助下将接收到的名称绑定到本地名称f，而n运行坐标系f′。 Q）。5通信证明在本节中，我们证明了编码的可靠性。遵循[10]中的方法，我们首先证明了在Homer中π演算过程σP和它的编码<$σP）我们在π-演算项P中定义强倒钩为通常的σ<$P↓σn，如果联系我们 可以对主语n执行输入动作，我们定义弱倒钩，联系我们 如果σP→σn↓; 相应地，在荷马史诗中，如果p可以执行接收动作n（m）和pn，如果p\n↓n。然后，我们定义了一个匹配的倒钩双相似性之间的π演算和荷马条款。.定义5.1匹配倒钩双相似性是最大的关系式<$Pπσ/α×Pc/α，如果当（σ<$P，q） ∈，• 如果σ<$P→πσM. Bundgaard等人理论计算机科学电子笔记128（2005）131143JJJ.则存在qJ使得q\<$qJ和σJ<$P<$q• 如果q\qJ，则存在PJ和σJ，使得σ<$P→<$σJ<$PJ，.πσσjPq• 若σ<$P↓n则q<$nJ144M. Bundgaard等人理论计算机科学电子笔记128（2005）131J• 若q↓n则σ <$P<$n本文的主要结果是，在编码和编码过程之间存在匹配的倒钩互模拟。Theore. m5.2对于所有π-c演算P和替换sσ，我们有σP<$σ P）。D. 定义5.3B将被简化。在荷马史诗中，在Pc/α上的H，使得当p≠Hq时，• 若p↓n则q↓n• 如果p\pJ，则存在qJ，使得q\≠qJ，.pHqJ从Thm。5.2因此，编码相对于倒钩互模拟是完全抽象的。.推论5.4设ππ表示π演算中的标准倒钩双相似性，..则我们有σ<$ P<$π σ <$Q i<$P）<$H<$ σ<$ Q）。从编码的组合性，我们可以证明关于倒刺同余的可靠性。Theorem5.5LettingCHden. o eaHomercon tex t， Cπaπ-calculuscon tex t， w.我们有了那个C.H. CH（<$σ <$P））<$HCH（<$σ<$Q））蕴涵<$Cπ<$σJ。σσJ<$Cπ （ P ） <$πσJ<$Cπ （ Q ） ， 使 得 dom σJ<$fn （ Cπ ） \dom σ 和 domσJ<$dom σ =<$。6结论和今后的工作在本文中，我们提出了一种新的编码的名称传递，因此名称替换，在荷马的π演算使用进程传递，强移动资源，命名嵌套的位置，和本地名称。我们已经使用了一种延续传递风格来提供同步通信的优雅编码。我们引入了一个带有显式替换的π-演算，以保持反应下的自由名集合，并使对应关系变得直观。在本文中，我们只描述了有限π演算的编码，而没有匹配，我们将在即将发表的论文中描述如何编码完整的π从本文所做的工作中产生了几个有趣的问题。首先，合乎逻辑的下一步是看看是否有可能编码荷马的一个版本，在荷马中扩展了名字传递。 目前还不清楚如何进行这样的编码，或者是否有可能。其次，寻找关于倒钩同余的编码的完整性结果将是有趣的。如[10]所述，这是一个M. Bundgaard等人理论计算机科学电子笔记128（2005）131145同步演算的困难问题一个可能的解决方案是在π演算和荷马中都使用倒刺同余的标记互模拟特征我们在[5]中探索了Homer中的标记互模拟同余。引用[1] 卡尔代利湖和A. D. Gordon，Mobile ambients，in：M. Nivat，编辑，第一届软件科学和计算结构基础国际会议论文集（FOSSACS140-155[2] 卡斯塔尼亚湾和F. Z. Nardelli，The Seal calculus revisited：Contextual equivalence andbissimilarity，in：M. Agrawal和A. Seth，编辑，第22届软件技术和理论计算机科学基础会议论文集（FSTTCS85比96[3] 法拉利，G.，联合Montanari和P. Quaglia，具有显式替换的π-演算，理论计算机科学168（1996），pp. 53比103[4] Godskesen，J.C.的方法，T. Hildebrandt和V.Sassone，移动资源的演算，在：L。布里姆，P. Jancar，M. Kr et'etunsky'aA. 库切拉，编辑，出版13本书并发理论会议（CONCUR（2002），pp.272-287。[5] 希尔德布兰特，T.，J. C. Godskesen和M. Bundgaard，Homer的互模拟同余- 高阶移动嵌入式资源的演算，技术报告，哥本哈根IT大学理论计算机科学系（2004年），即将出版。[6] Jensen，O.H. 和R.Milner，Bigraphs and mobile processes（revised），Technical ReportUCAM-CL-TR-580，University of Cambridge，Computer Laboratory（2004）.[7] 米尔纳河，[8] 米尔纳河，J. Parrow和D.Walker，A calculus of mobile processes，Part I and II，Journal of Information and Computation100（1992），pp.1[9] Sangiorgi，D.，“Expressing Mobility in Process Algebras: First-Order and Higher-OrderParadigms,”毕业论文，计算机科学系，爱丁堡大学（1992年）。[10] Sangiorgi，D.和D.沃克，[11] 汤姆森，B.，Plain CHOCS：A second generation calculus for higher order processes，ActaInformatica30（1993），pp. 1-59号。[12] Zimmer，P.，关于纯移动环境的表现力，在：L。Aceto和B. Victor，editors，Proceedings ofthe 7th International Workshop on Expressiveness in Concurrency（EXPRESS81-104146M. Bundgaard等人理论计算机科学电子笔记128（2005）131σσσσσσA减少前置正如第4节所解释的，我们的编码需要在荷马中进行多次通信，以便模拟π演算中的单个反应。 我们把π演算中对应于一个反应的步骤称为反应步骤，把附加步骤称为簿记步骤。从编码中我们看到，对于输出前缀，在反应步骤之前只有簿记步骤，而对于输入前缀，在反应步骤之后也有簿记步骤。我们索引我们的编码的π演算前缀捕捉的直觉，一个π演算前缀对应于一个序列的荷马过程。我们将索引0作为前缀的原始翻译（在编码 中 发 生 任 何 簿 记 减 少 之 前 ） ， 即 <$n<$m<$.P ）0=<$n<$m<$.P），然后定义<$nm.P）k，使得我是说，我是说，我是... P）6=σn θ <$σm）θ。 （P）。σ σ更精确地说，给定一个代换σ，我们定义<$nm.P）k，其中0≤k≤ 6，作为<$nm.P）0=<$nm.P）<$n<$m<$.P）1=（a）（a<$σn）<$<$mJdy . asvy ascP） as（xJJ）. a（z）。 xJJ）<$n<$m<$.P）2=（a）（a <$σn）<$asv<$<$σm）<$。 ascP） as（xJJ）.a（z）。 xJJ）σ。ΣP）3=（a）（a s）c（y）. σ n<$σm）。 yr接收σnσP.P. as（xJJ）. a（z）。 xJJ）.Σ<$n<$m<$.P）4=（a）（a s<$σn<$σm）<$.<$P）接收σn（xJJ）. a（z）。xJJ）σ。Σ<$nm.P）5=（a）（ar接收σna（z）.σn<$σm）。（P））P）6= σn θ <$σm）θ。（P），在这里，我们强调了同步前缀，并强调了一些可读性的资源边界。请注意，在索引0中，我们需要环境中的位置nJ，在索引1中，位置mJ，在索引6中，我们需要环境中的匹配共同作用，以便能够执行反应。M. Bundgaard等人理论计算机科学电子笔记128（2005）131147σσσσσE/ME/M我同样，我们定义n（m）。 P）k，对于0 ≤ k ≤ 5，（m）. P）0=（m）.P）（m）. P）1=（a）（mJ）（a ∈ σn）n =（a）（m j）（a ∈σn）n =（a）（m j）（a ∈ σn） arc（P） ar（xJJ）. a（z）。 xJJ）σ。（m）. P）2=（a）（mJ）（asSend σnrc（y）.σn（z）。（a）（a）（a）Σ[咒语] a（zJ）。（yzJ））.P.A. ar（xJJ）. a（z）。 xJJ）（m）. P）3=（a）（mJ）（a联系我们Σr∈σn（z）. （a）（a）（a）对任何人有约束力。a（zJ）。（<$P）zJ））ar（xJJ）. a（z）。 xJJ）.Σ（m）. P）4=（a）（mJ）（a sa（z）.σn（z）。（a）（a）（a）[咒语] a（zJ）。（<$P）zJ）（m）. P）5=（mJ）（σn（z）. （a）（P）z/））σm0E/M（P）1=（mJ）（a）（aBind mave）。a（zJ）。（<$P）zJ））=（mJ）（a）（amJe）a（zJ）。（<$P）zJ）），E/MJ J式中，<$P）z/m = aBind mavz。a（z）。（<$P）n（z）。 再次注意，在index 0我们需要环境中的一个位置nJ，在index 5中我们需要在周围环境中的一个匹配的共同作用。<$P）0和<$P）1表示在输入名称e）之后的绑定步骤（到本地名称m）。B通信证明为了简化证明，我们考虑π演算过程的（前）正规形式。定义B.1π演算过程P的标准形式定义如下.ΣP=（νn）I1|·· ·|Ik|O1|·· ·|噢，其中每个I i都是x（y）形式的。P i和每个O i的形式为xy。PJ，对于x，y，其中P1，...，P k和PJ，.，PJ都是正常形态。1m命题B.2每个π-演算项P在结构上全等于一个项PJ的标准形式。（P）148M. Bundgaard等人理论计算机科学电子笔记128（2005）131πσ（C、P）L定义B.3 π演算过程P的预规范形式定义如下。ΣP=（νn）I1|·· ·|Ik|O1|·· ·|Om|P1|·· ·|Pl，（*）其中每个I i都是x（y）形式的。PJ，并且每个O i的形式为xy。 PJJ，我我对于一些名字x，y，其中PJ，.，PJ和PJJ，.，PJJ是正规形式1千1百万而P1…，P1处于正常形式。很容易证明，如果P是一个在预正规型上的π -演算过程且σ<$P→PJ，则存在一个PJJ<$πPJ，且PJJ是在预正规型上的.因此，我们只需要考虑预正规形式上的过程，带有显式替换的π演算及其在荷马中的编码，并且我们不会因此丢失任何行为。处理P1，.，Pl将对应于编码中的输入前缀，其已经接收到值，但是还没有完成以下簿记-ing.更详细地说，我们将预正规形式（*）上的过程转化为以下荷马过程..<$σP）（i，o，p，e，m）=（m）（nJ）<$I 1）i1·· · <$I k）ik <$<$O1）o1···<$Om）omp11e1/m1σ···el/mlσn∈nσnjn）σΣ但是，（**）Wherem={mJ|m∈ dom σ和mσm}，n={n，n}|n∈n{\displaystylen}，r=<$n∈domσnJ<$$>σn）<$. 我们引入了旋转数<$−）（i，o，p，e，m），• i是输入前缀的索引列表，i1，.，ik（例如，对于每个ij，0≤ij≤6），• o是输出前缀的索引列表，o1，...，0mm（例如对于每个0j，0≤oj≤5），• p是预成型件的索引列表，p1，...， pln（例如， 对于每个pj，0 ≤pj≤1），并且列表e和m是名称列表，分别由输入中接收的名称和本地名称组成。注意，列表p、e和m必须相同，l。定理5.2定义一个关系R，使得对于所有形式为（*）的π-演算过程P，所有替换σ，以及对于所有可能的列表i，o，p，e，m（关于P），σ [m <$→e] PR <$σP）（i，o，p，e，m）.我们证明了R是一个匹配的倒钩互模拟。我们分别证明了定义5.1的四个条件。在下面的情形中，假设我们从R中取了一个任意对（例如σ [m<$→e]<$PR <$σ<$P）（i，o，p，e，m））。M. Bundgaard等人理论计算机科学电子笔记128（2005）131149σM1kJg/m第一个条件：这里有四种可能的情况需要考虑。唯一可能发生的同步类型是在输出和输入前缀之间，其中任何一个都可以是预成型的。我们只考虑两个前缀都不在预成形中的情况之一。• 我们有一个输入前缀Ii，1 ≤ i ≤ k，形式为n（m）.PJ，输出前缀Oj，1≤j≤m，形式为h∈f∈ f。QJ.不失一般性，假设Q j 的形式为（νn <$）。Q|···|I Q|O Q|···|O Q和The.QI11mJPJ的形式是（νn<$P）I P| ··· |I P|O P| ··· |O Pσn=σh，σf=1kJJ1mJJG. 在同步之后，我们有以下关于预正规的表达式形式.σ[m<$→e][m<$→g]<$（n<$n<$Pn<$Q）I1|I i −1|我|I一期+1| ··· |I k|···|I Q|I Q| I P |I P|I P|···|O j − 1|O j+1