π-演算中的移动过程和开放互模拟的组合和完全抽象语义

理论计算机科学电子笔记106（2004）105-120www.elsevier.com/locate/entcs移动过程尼尔·加尼1部数学和计算机科学，地址：University Road，Leicester，LE1 7RH，United KingdomKidaneYe mane2，3 BjöornVictor2，4部信息技术，乌普萨拉大学，信箱337，S-751 05乌普萨拉，瑞典。摘要我们应用最近发展起来的高阶抽象语法和函子操作语义技术，给出了具有开放互模拟的π-演算的组合和完全抽象语义.在我们的工作中，关键的新颖性是实现开放互模拟的复杂性，要求我们从通常的语义域的集合的子类别上的预层移动到Rel的子类别上的预层。这种额外的结构在控制挤出名称的重命名和提供各种不同的动态分配操作符来模拟π演算的不同绑定器方面至关重要。关键词：过程演算，抽象代数，代数，余代数1介绍π-演算是由Milner、Parrow和Walker [9]引入的，作为以前分布式和并发计算范例的扩展，1电子邮件：N. mcs.le.ac.uk2欧洲联盟PROFUNDIS项目支助的工作，合同号IST-2001- 33100。3电子邮件：Kidane. it.uu.se4电子邮件：Bjorn. it.uu.se1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.027106N. Ghani等人理论计算机科学电子笔记106（2004）105结构不仅要反映信息的局部性，还要反映信息的流动性，ity。因此，除了进程代数的常用组合子，如前缀、并行组合、非确定性选择、输入和输出之外，π演算还包含形式为（νx）P的过程，这应该是具有局部信息x的过程P。关键是，π演算允许局部的拓扑动态地演变，使得在某点处局部的信息可以在以后变成全局的。这种现象被称为挤出，是π演算的核心创新π演算允许进程随时间改变它们的连通性因此，它被称为移动过程。进程代数研究的一个关键进展是互模拟的概念，它是一种证明进程等价性的方法。虽然这个概念在CCS [8]中引入时相当简单，但在具有变量绑定的进程代数中，由于存在各种不同的位置，这个概念变得更加复杂。较简单的例子，如早期互模拟和晚期互模拟[9]，则不是同余。另一方面，开放互模拟[15]是一种同余，但由于以下事实而变得复杂：互模拟关系不仅在转换下必须闭合，而且在某些替换下也必须闭合，并且这些替换随过程而这使得整体定义比早期和晚期互模拟的定义更加复杂和微妙。π演算的成功，以及它支持的各种不同的互模拟，使它成为程序语言语义中一些令人兴奋的最新发展的理想案例研究，特别是高阶抽象语法（HOAS）[4]和函子操作语义（FOS）[18]。HOAS的目标是扩展初始代数语义的高度成功的范例，涉及变量绑定的语言，而FOS寻求一个统一的框架，在其中的原因操作和指称模型之间的关系。因此，我们的目标是通过使用以下策略来处理π演算中的开放互模拟：• 由于π演算包含变量绑定，我们采用HOAS方法，用一类预层上的内函子的初始代数来建模π• 人们对一个过程的观察是由一种前缀语言给出的，这种前缀语言是由同一类前缀上的一个共点内函子建模的这个内函子称为行为函子。转移系统是这个行为函子的余代数，互模拟由余代数互模拟给出。• 我们将操作语义建模为语法在行为上的分布性，从中我们获得组合性和完全抽象N. Ghani等人理论计算机科学电子笔记106（2004）105107结果因此，本文的贡献是• 我们给出了一个干净的介绍开放互模拟，并得出结果，如组合性和充分的抽象。这是通过使用抽象的概念，如余代数，自然性和索引，以避免出现在标准定义中的关于自由和束缚名称的各种技术方面的条件[16]来实现的。• 开放互模拟的复杂性来自于它在不同类别的重命名下的封闭性我们的方法的新颖之处在于，我们通过从Set的一个子范畴上的预层（如[5]中所述）移动到Rel的一个子范畴上的预层（我们称之为关系预层）来捕获这个特征。本文把Rel作为以关系为对象、单调函数为态射的范畴。这些关系预层比通常可用的更动态的分配操作符来模拟π演算中的绑定器。• 正如我们在结论中所评论的，关系预层的这种额外能力似乎正是处理其他复杂互模拟所需要的，例如Fusion演算中的超互模拟[11]。相关工作：这个研究程序在[5]中被应用于π演算，但只应用于早期和晚期的互模拟。然而，开放双模拟的复杂性意味着这些方法无法应用-我们使用关系预层的解决方案似乎正是提供适当额外结构所需的。开放互模拟已经在并发文献中被广泛地描述[16，12]（例如关于其公理化，导致有效特征的符号转换系统，以及用于决定等价性的实现算法）。有趣的是，在这些论文中，有些结构是由关系索引，而其他人没有。因此，我们围绕关系预设集构建语义的想法但是，人们随后看到了与其他互模拟（如超互模拟）的联系，这一事实为我们转向更抽象的环境提供了强有力的理由。本文将呼吁那些coalgebraists谁是感兴趣的HOAS和FOS，为了使这个理论完全成熟，更复杂的例子需要处理。这正是我们所做的。例如，我们想知道我们在这里考虑的关系预层是否适合Power此外，本作者中有两人在108N. Ghani等人理论计算机科学电子笔记106（2004）105α：：=a（x）（输入）P：：=0（未采取行动）ax（产出）α。Q(Pre fix）a（x）（绑定输出）Q+R（总计）τ（沉默）Q|R（νx）Q（组成）（限制）[x=y]Q（匹配）！P（复制）Fig. 1. π-演算同时，他们来到这个主题，因为他们对更抽象地处理他们的主题的可能性感兴趣。鉴于扩散的不同进程代数和众多相关的互模拟，这肯定是一个越来越感兴趣的领域，我们希望其他并发理论家对这项工作感兴趣。总之，在我们提供的高阶函子操作语义框架内，开放互模拟的发展有很好的理论和实践理由。本文的结构如下：我们在第2节中提供了π-演算的具体语法和语义，然后在第3节中提供了π-演算的抽象语法。第4节包含相关的行为函子和π演算的组合和完全抽象语义的关键结果。我们在第5节中总结了一些结论和进一步工作的想法。2π演算在本节中，我们回顾了π演算的语法和语义以及开放互模拟等价的定义。由于这是标准材料，我们建议读者参考标准文本了解一些技术细节，例如。[16 ]第10段。我们假设一个无穷大的名字集合N，范围是a，b，. x，y，.. . .这些表示通信信道以及发送和接收的值定义2.1（π演算）原始π演算过程的集合，由P、Q、R等和前缀α组成，由图1的规则归纳定义。0代表空进程，它什么也不能做。过程α.Q可以执行相关的输入、输出或静默动作，然后成为过程Q; Q + R是Q和R的非确定性选择; Q |R是N. Ghani等人理论计算机科学电子笔记106（2004）105109αPREF−α 。 P−α→PP−α→PJRESP−α→PJ（νz）P−α→（νz）PP−α→PJJifz/n∈（α）总和P+Q−α→PPARJP|Q−α→PJ|Qifbn（α）/f∈n（Q）P−α→PJP−u−（x→）PJ， Q−u→yQJ匹配网αJτJ J[x = x] P −→ PP |Q −→ P {y/x}|QP−x→yPJP−u−（→y）PJ， Q−u−（→y）QJ开放（νy）P−x−（→y）PJifx/=y关闭P|Q−→τ（νy）（PJ| QJ)P−α→PJP−u→yPJ，P−u−（y→）PJJ代表！ P−α→PJ|！P公司简介！P−→τPJ | PJJ{y/x}|！ PP−u−（→y） PJ， P−u−（→y）PJJREP-关闭τJJJ！P−→（νy）（P|P）|！P图二. π-演算的转移规则过程Q和R并行运行;（νx）Q是局部发生且有界于Q中的过程Q ; [x = y]Q是当名称x和y相等时的过程Q，否则为0。终于来了！P是复制操作符，它可以被看作是P的无限拷贝，可以用来编码递归。前缀产生了过程在演化过程中所表现出的可观察行为。观察结果根据想要研究的互模拟而变化，但对于开放互模拟有四个，即i）a（x）表示通道a上未知名称x的输入; ii）ax表示通道a上全局名称x的输出; iii）a（x）表示通道a上局部名称x的输出; iv）τ表示无声的内部动作。在上面的动作中，我们称a为动作的主语，x为宾语。输入前缀和限制运算符是绑定器（绑定输出前缀a（x））。 P是（νx）ax的短缩。 P）。 因此，在一个过程或前缀中，有许多自由名和束缚名的概念，记为fn（P）、fn（α）、bn（P）、bn（α）;我们把过程或前缀中的自由名和束缚名记为n（P）和n（α）。 然后，结合物在过程上引入了明显的α-等价概念，π-演算的项是由α-等价表示的过程。在定义了π演算的语法之后，我们转向它的运算语义。定义2.2跃迁族P−→Q是最不满足的族。简化图2中的定律，其中SUM、PAR、COM和关闭已被省略。110N. Ghani等人理论计算机科学电子笔记106（2004）105关于我们∼∼开放式互模拟最初由Sangiorgi [15]定义，比早期和晚期互模拟[9]更精细;与早期和晚期互模拟不同，开放式互模拟是一种一致性，尽管它的定义乍看起来似乎更复杂，但它具有自动化工具中利用的开放互模拟被定义为一组由区别索引的关系，用于表达名称的永久不平等定义2.3区分是关于名称的有限对称和不相关关系。我们可以写（x，y）为（x，y），（y，x）等，省略对称对。一个替代是一个功能的名称，有明显的行动过程和区别。如果（a，b）∈D表示σ（a）/=σ（b）。区分关系用于记录由绑定输出挤出的名称;这些名称最初是绑定的，因此必须与所有其他名称保持不同-区分关系的使用允许我们只考虑那些保持挤出名称不同的重命名。定义2.4对称过程关系的区别指标集S={SD}是一个开互模拟，如果对于每个SD和每个关于D的σ，无论何时（P，Q）∈ S D(i) 如果Pσ−a−（x→）PJ有hx/∈fn（Q），则n∈e是aQJsuchthatQσ−a−（x→）QJ且（PJ，QJ）∈SDJ，其中DJ=Dσ<${{x}× fn（P σ，Qσ）};(ii) 若Pσ−α→PJ有hbn（α）/∈fn（Q），则nQJex是tss.t. Qσ−α→QJ且（PJ，QJ）∈SD.P和Q是开D-双相似的，记作P<$DQ，如果存在开互模拟S. t. （P，Q）∈SD，其中SD∈ S.作为一个简单的激励示例，考虑以下过程P = x。0 |y. 0Q= x.y。0 + y。X.0P0=（νx，y）zx. z y . PQ0=（νx，y）zx. z y . Qττ其中，显然P/Q，因为P{x/y}−→PJ但Q{x/y}−→QJ。然而，在这方面，均p00，因为x和y永远不可能被识别。 这信息被记录在开放互模拟关系的区别索引中;在前两个有界输出z（w）和z（y）之后，我们只需要验证P{（x，y）}Q，从而排除识别x和y的所有替换。更多的例子和动机见例如。[16、15]。稍后我们将看到这些关于绑定和自由名称等的技术条件是如何包含在HOAS中的，以提供更令人满意的N. Ghani等人理论计算机科学电子笔记106（2004）105111C C →C→定义。3抽象语法在2.1节中给出的π演算语法的具体定义的问题在于，它是作为商数据类型来表示的。用这样的商数据集进行推理是非常困难的，因为要么必须有效地为等价类选择代表，要么直接使用等价类本身。因此，当发现如何不仅表示原始项，而且表示项的α-等价类作为自由或初始数据集时，这是一个突破[4]。这种方法可以总结如下：不是定义一组原始项，然后用α-等价来表示它们，而是为每一组自由变量定义一组项，该组项在这种情况下可以定义。这些上下文也称为阶段。因此，对于每个上下文或阶段，我们都有一组术语。允许在上下文中重命名变量意味着上下文形成一个范畴，然后术语应该由函子Set给出。通常被选择为有限集合和所有函数的范畴[5]，或有限集合和内射函数的范畴[5]。我们的核心见解和我们的方法的新颖性是，为了解决更复杂的情况，如π演算中的开放互模拟和Fusion演算中的超互模拟，需要更多的阶段结构，特别是阶段形成Rel的子类别。开放互模拟不仅在转换下是封闭的，而且在重命名下也是封闭的，这些重命名必须在已被挤出的名称上是单射的。因此，每个阶段不应该只由一组自由变量组成，而应该包括一个关系，说明何时不能将名称重命名为相同。因此，我们的预层将覆盖Rel的某些子范畴，而不是Set。对于开放互模拟，这个子范畴就是我们现在定义的区别关系范畴。3.1区分关系为了解释开放互模拟，我们使用由区别关系组成的阶段。因此π-演算项将形成一个预层D集，其中D是区别关系范畴。定义3.1（范畴D）区别关系范畴D是Rel的全子范畴，其对象是区别关系，即，关系是不相关的，对称的，有一个有限的载体集。因此，区别关系（n，dn）和（m，dm）之间的态射是函数的。112N. Ghani等人理论计算机科学电子笔记106（2004）105→→−f：n m，保持区别关系。直觉上，区分关系是一个集合和一个关系，使得相关元素被认为是明确不同的，决不能被重命名为相同的正如我们前面所讨论的，找到一种数学形式，以确保挤出的名称被注入地重命名，而其他名称可以被非注入地重命名，这是理解开放互模拟的关键。如上所述，这里的主要观点是我们在预层范畴集合D中工作。这个前层范畴的许多必要结构都是从D继承的，正如我们现在所描述的。引理3.2（D的结构）范畴D有三个不同的动力学联系函子Id，δ+，δ-：D→D证据 动态分配算子Id是单位元，而δ−只是与一元集上的区别关系的余积。 δ+：D的作用Donojesgivenyδ（n，dn） =（n+1，dn+1）其中dn+1是对称闭包dn<${（i，i）|i∈n}对态射的作用正如预期的那样，而函子性是一个简单的计算。Qδ−和δ+bb是一个额外的元素，用于描述不同的关系，以表示不可见的数据。 然而，δ+还表明，这个新元素与其它元素是不同的。的函子δ+将使用d来绑定带有限制的类，以确保挤出的名称不能重命名为其他名称，而δ−函子用于不需要此类限制的绑定输入。上面写着+，设计的目的是为了解决这一问题，即δ+和δ−bot在一个外部元素中已经定义，δ+在外部元素中添加。他的存在一个以上的动态分配操作符是我们移动到关系预层作为语义域的直接结果。我们使用的身份作为一个动态分配操作符，只是为了避免案例分析后。引理3.2中的结构提升到D-预层范畴的结构如下.注意，对有限区别关系的限制意味着在讨论D-预层范畴时不存在大小问题。我们将使用相同的符号，但要确保读者有足够的信息来推断我们正在研究的类别，而不是为提升的结构发明新的符号。引理3.3（集合D的结构）范畴集合D有积、余积、名的集合、三个D的代数运算函子Id、δ-、δ+和aN. Ghani等人理论计算机科学电子笔记106（2004）105113P P→有限幂集函子定义如下：• 名称N ∈集合D的预层，作用N（n，dn）= n。• 与函子范畴中的所有极限和上极限一样，积和上积是逐点计算的。因此（P×Q）（n，dn）=P（n，dn）×Q（n，dn），对于余积也是如此。• D上的每个动态分配函子κ∈{Id，δ+，δ−}定义动态分配算子κ：SetD→SetD。• 如果f是Set上的有限幂集函子，则f：SetDSetD定义了D -预层上的有限幂算子。我们现在可以给出基于区别关系的π演算的初始代数语义3.2作为初始代数的π-演算预表集D的范畴提供了一个合适的类型论域来建模具有开放解释的π定义2.1中给出的π-演算的语法被一个内函子：SetD→SetD（定义在图3中）捕获到α-等价。X=K1（未采取行动）+N× N×X（输出前置）+N×δ+X（绑定输出）+N× δ− X（输入前缀）+X× X（总计）+X× X（组成）+δ+X（限制）+N× N×X（匹配）+X（复制）图三. 内函子模型π-演算项函子的构造正如预期的那样，是语言的每个特定语法类别例如，0进程总是添加一个进程，而自由输出前缀进程由两个名称和一个已经构造的进程组成另一方面，绑定输出由114N. Ghani等人理论计算机科学电子笔记106（2004）105a（）a（）要在其上传输先前本地名称的通道的名称，以及具有由δ +的用户声明为与所有其他名称不同的挤出名称的进程。与输入前缀的情况相比，此处输入通道中预期的名称不会被挤出，因此不会通过使用δ −强制与其他名称区分开。π-演算的语法是我们写为ππ的初始π-代数。这是因为：i）集合D有ω-上极限和一个从集合D继承的初始对象; ii）和与积保持过滤上极限，而对于任何函子F，F总是保持过滤上极限。证明了ππ（X）是π-演算项与自由名直到α-等价的集合通过与[5]中相同的论证可以很容易地看到，以建立无类型λ-演算的高阶抽象语法方法的正确性。注意，由于ππ是一个D-预层，我们也可以重命名π-演算项。然而，究竟哪些名称可以等同于这样的更名是由阶段或区别关系的过程生活。回想一下，实现这一点是解决开放互模拟的关键一步。4标签转换系统在给出了π-演算的语法的初始代数语义之后，我们转向对开放转移关系的处理，从而转向开放双模拟。我们的方法是定义一个行为函子，使得一个开放的转换系统仅仅是行为函子的一个余代数，并且开放的互模拟是一个余代数互模拟。当然，我们希望利用HOAS的优势来达到α等价，因此第一步是将定义2.1中包含约束变量的前缀替换为α-等价的版本。因 此 ，我们定义集合Act ={a（），a（），ab，τ}，并注意到如果σ：N → N是名称上的任何函数，则在集合Act上存在明显的作用。接下来，我们使用这些动作来定义过渡系统的概念。在HOAS框架中，过程是在特定的阶段中给出的，因此变迁系统的节点必须是成对的阶段和抑制它们的过程。定义4.1（D-变迁系统）D-变迁系统由一个预层X：集合D和一个图组成，使得• 节点由对（p，d）标记，其中p∈X（d）• 边由集合Act的元素标记，使得如果·（p，d）−→·（p，d）−→（pJ，dJ）则dJ=δ−d且a∈d（PJ，DJ）THENDJ=δ+d且a∈dN. Ghani等人理论计算机科学电子笔记106（2004）105115AB∃B→P·（p，d）−→·（p，d）−→（PJ，DJ）则DJ=d且a，b∈d（pJ，dJ）则dJ=d• If（p，d）−α→（pJ，κd）其中r eκ∈{Id，δ−，δ+}且σ：d→DJn（pσ，DJ）−α→σ（pJσ，κDJ）.FOS方法的本质是表示过渡系统，如定义4.1中的行为函子的余代数。我们定义行为函子如下：定义4.2（行为函子）函子：集合D集合D定义如下BP=Pf（P+N×N×P+N×δ+P+N×δ−P）为了理解上面的定义，可以把BP看作是过程P的一个前层的可能演化。非决定论意味着有许多可能的演化，因此存在幂型函子f。这些可能的演化中的每一个都由可观察的行为和结果过程silent和free输出操作是前两种可能性-请注意，结果进程处于同一阶段。对于绑定输出，我们观察发送输出的通道，结果进程的名称为extruded，因此stage由extruded名称扩展，该名称必须与所有其他名称保持区别。最后，对于绑定输入，情况大致相同，只是在结果过程中，新名称不需要与其他名称不同。引理4.3 D-变迁系统与B-余代数一一对应.证据余代数的结构映射精确地给出了变迁关系，而余代数结构映射的自然性直接对应于保区别改名下开变迁的封闭条件。QB-coalgebraic互模拟定义如下：定义4.4（共代数互模拟）B-共代数X上的B-互模拟由X上的关系R给出，使得R上存在B-共代数结构，使得以下图可交换。X（R）X.....v. VVBX（BR）BXτ116N. Ghani等人理论计算机科学电子笔记106（2004）105B引理4.5下列数据是等价的：• 预层X：D）集上的B• 对称关系{Rd<$X（d）×X（d）}d∈D使得· 若σ：d→DJ且p Rdq，则pσ RdJqσ· p Rd q意味着如果p和pJ Rd qJp和pJRδ−dp和 pJRδ+dQJq J.p和p JR dq J。引理4.5给出了-互模拟作为开放互模拟的一个优雅的特征，但这真的与定义2.4中的开放互模拟概念相同吗？与绑定名相关的条件已经通过使进程驻留在特定的区别关系中而隐式地实现，通过使用动态偏置运算器δ−和δ+。只有其他的才有用定义2.4在保持区别的重命名下不是立即封闭的，但这实际上是一个众所周知的性质[16]。4.1分类规则在本节中，我们将展示图2中给出的π演算的运算规则是如何通过某种形式的自然变换来建模的，这种自然变换意味着具有完全抽象属性的组合语义，前提是行为函子是无穷的，并且保持弱回调。这种自然的转换产生了一种组合的和完全抽象的语义，这可以追溯到开创性的论文[17]。最近的工作[7，13]已经根据分配律更优雅地重新塑造了抽象理论，但是，由于我们的目标是建立这种分配律的存在，我们坚持原来的具体形式。由于这里的材料正如人们所期望的那样，我们只处理限制算子的下列定律。P−a→bPJP−x→yPJRES（νz）P−a→b（νz）PJifz/∈a{，b}O笔（νy）P−x−（→y）PJ如果x/=y一般来说，我们试图将这种操作定律建模为X(1)集合D中的X（X× BX）→ BTXτ- →pJ则有aτqJhthatq−→QJa（）- →pJ则有aa（）qJhthatq−→QJa（）- →pJ则有aa（）qJhthatq−→QJAB- →pJ则有aABqJhthatq−→QJN. Ghani等人理论计算机科学电子笔记106（2004）105117+⎪⎩◦PBρ（a，b，q）=（aJbJ，（vz）qJ），如果a是old（aJ）andb=old（bJ）在上述两个 限制规则的情况下，我们从自然变换δ+（X×BX）→BTX 导出正确的自然变换，它由下式生成：δ+N×δ+ N×δ+X−→ρPf（N×N×TX+N×δ TX）ρ的定义可以使用[3]中定义的内部语言给出。如果a是旧的（aJ）andifb=新的 （bJ）ifa=new（aJ）当新老注入D）δ+D和1）δ+D。自然性很容易被检查。[17]中的结果显示了与自然变换建模相关的语义，操作规则诱导具有完全抽象属性的组合语义，即，具有相同语义的两个进程是B-双相似的。引理4.6通过类型（1）的自然变换建模的图2的操作规则引起具有完全抽象属性的组合语义。证据行为函子的大多数构造函数已经被证明是无穷的。Pf：Set）Set是无穷的是民间传说，因此幂型算子Pfff是无穷的，因为如果K是任何无穷的函子，那么K f是无穷的。保持弱回调的事实来自i）产品和副产品的事实f是; iii）如果K：D ）D是任何函子，则K：集合D）集合D保持弱拉回。 这可以证明如下。设P是η：S）Q和η：R的弱拉回 ）Q（假设下面的图是弱回调）。Pp）RpjV VS） Qη118N. Ghani等人理论计算机科学电子笔记106（2004）105◦◦◦◦ ◦ ◦◦◦◦我们必须证明P <$X是η <$X：S <$X的弱回调）Q X和ϵ◦X: R ◦ X)Q◦X.P<$Xp<$X）R<$XpJX v电子邮件*vS X）QXηX给定一个映射h：H）S X和hJ：H 利用（η X）h=（η X）HJ的性质，得到了满足平方交换的映射Lan XH）S和Lan XH）R。由于P是这个平方的弱拉回，我们具有映射Lan X H）P，因此根据需要具有映射H）P X。所有的交换都遵循自然规律。Q5结论本文利用最近发展起来的高阶抽象语法和函子操作语义理论，给出了π演算中开放互模拟的一个清晰的表示。开放互模拟比以前在这个框架中研究的早期和晚期互模拟更复杂，因为挤出的名称必须被记录并与重命名下的所有其他名称区分开。我们以一种优雅的方式解决了这个技术挑战，从Set的一个子范畴上的预层转移到Rel的一个子范畴上的预层，即区分关系的范畴。这种关系预层的额外结构使得可以选择动态分配操作符来模拟语言中出现的不同绑定操作符。通过验证函子操作语义框架的前提条件，我们得到了π演算中开放互模拟的组合和完全有一些未来的方向，我们希望采取这项研究。首先，关系预层似乎提供了对复杂的互模拟（如开放互模拟）建模所需的额外结构。融合演算[11]是π演算的变体，其中通信规则网 P−u−（x→）PJ，Q−u→yQJ，P|Q−→τ被通信规则所PJ{y/x}|QJP−u→xPJ，Q−u→yQJ网P|Q−{−x=−y→}PJ|为|y|y|| Q这可以被认为是一个明确的替代，并与所有相关的JN. Ghani等人理论计算机科学电子笔记106（2004）105119在这样的演算过程中，定义的上下文中不仅包括一组自由名称，而且还包括由上述通信规则产生的名称上的等价关系。这表明使用具有由有限等价关系给出的阶段的预层来模拟融合演算我们已经勾勒出了细节，并将在即将出版的期刊版本中包括它们。从长远来看，我们有各种各样的方向。对从理论上讲，将这些技术扩展到更高阶的进程演算将是非常有趣的，并且许多语义基础设施已经存在并等待使用。我们还想考虑这些技术是否可以扩展到Milner此外，测试Power最近在计算方面的工作的适用性将是有趣的[13]这是一个很好的例子。一个更实际的研究方向是HD-自动机[10]。HD-自动机试图通过用相关信息（进程的自由名）修饰自动机的状态并建立不同状态中的局部信息之间的对应关系来给出历史依赖演算的操作模型。这些自动机可以被看作是更抽象的框架的具体实现[12，2]。 通过自动提取一个具体的，最小化的过程表示作为一个历史相关的自动化，我们可以期待沿着[1]的路线引用[1] Gianluigi Ferrari，Stefania Gnesi，Ugo Montanari，Marco Pistore，and Gioia Ristori. HAL环境中的可移动进程。在Alan J. Hu和Moshe Y. Vardi，编辑，Proceedings of CAVSpringer，1998年。工具海报。[2] Gianluigi Ferrari，Ugo Montanari，and Marco Pistore.名称传递演算的最小化转换系统：一个共代数公式。在Mogens Nielsen和U. Engberg编辑，2002年FoSSaCS会议记录，LNCS第2303卷，第129-143页。Springer，2002年4月。[3] 马塞洛·菲奥雷、欧金尼奥·莫吉和大卫·桑吉奥吉。π演算的完全抽象模型（扩展抽象）。在LICS '96会议记录IEEE，计算机社会出版社，1996年7月[4] Marcelo Fiore，Gordon Plotkin和Daniele Turi。 抽象语法和变量绑定（延伸抽象）。 在proc 第14届LICS大会第193IEEE，计算机社会出版社，1999年。[5] 马塞洛·菲奥雷和丹尼尔·图里。名称和值传递的语义。在第16届LICS会议上，，第93-104页。IEEE，计算机社会出版社，2001年。[6] Ole Hogh Jensen和Robin Milner双图和转换。SIGPLAN不。，38（1）：38-49，2003.120N. Ghani等人理论计算机科学电子笔记106（2004）105[7] Marina Lenisa，John Power，and Hiroshi Watanabe内函子的分配性，点内函子和共点内函子，单 子 和 共 单 子 。 In Horst Reichel ， editor ， Proceedings 3rd Workshop on CoalgebraicMethods in Computer Science，CMCS爱思唯尔[8] R.米尔纳 通信系统的微积分，LNCS第92卷。Springer，1980年。[9] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。 移动过程的演算，第一部分。Journal of Information and Computation，100：1-77，September 1992.[10] 乌戈·蒙塔纳里和马可·皮斯托雷历史相关自动机。 技术报告，《计算机科学与设计》，联合国出版社，1998年。 TR-11-98[11] Joach i mPowanddBjüornVictor. FUSION计算：在移动过程中，Ex是必需的，并且是简单的。在LICS'98的会议记录IEEE，计算机社会出版社，1998年7月。[12] Marco Pistore和Davide Sangiorgi。π-演算的一个分区精化算法。 Journal of Information andComputation，164（2）：264一个扩展的摘要出现在CAV'96：38-49的会议记录[13] 约翰·鲍尔数学运算语义学的理论。In H. Peter Gumm，编辑，电子笔记理论计算机科学，第82卷。Elsevier，2003年。[14] 约翰·鲍尔变量绑定的统一范畴理论方法。2003年MERLIN会议记录，瑞典乌普萨拉，2003年8月。[15] 大卫·桑吉奥吉。π演算的互模拟理论。Acta Informatica，33：69早期版本发布为报告ECS-LFCS-93-270，爱丁堡大学。一个扩展的摘要出现在CONCUR '93，LNCS 715的会议记录[16] 大卫·桑吉奥吉和大卫·沃克。π演算：移动过程理论。剑桥大学出版社，2001年。[17] D.图里和动力局普洛特金数学运算语义学。在第12届LICS会议上，第280-291页IEEE，计算机社会出版社，1997年。[18] 丹尼尔·图里。函子操作语义及其指称对偶。博士论文，阿姆斯特丹自由大学，1996年6月。[19] 比约恩·维克托和法隆·莫勒。 对于π -计算器，M b i i ityW或kbenc-atol。在David Dill编辑的Proceedings of CAVSpringer，1994年。