理论计算机科学电子笔记162（2006）135-139www.elsevier.com/locate/entcs融合演算1Maria Grazia Buscemi2 乌戈·蒙塔纳里3意大利比萨大学信息学系摘要这项工作是进一步探索标记的过渡和互模拟融合结石。 我们遵循的方法开发的图里和Plotkin提升过渡系统的句法结构双代数，因此，我们提供了一个组成模型的融合演算明确的融合。 在这样一个模型中，由唯一态射到最终余代数所诱导的双相似关系与融合超等价一致，并且它是关于微积分运算的一个同余。在我们的工作中，关键的新颖性是通过标记的过渡给出一个明确的融合。在这篇短文中，我们将重点讨论没有递归和复制的融合演算的一个片段保留字：进程演算，代数/共代数模型1介绍融合演算[6]已经被引入作为pi演算[4]的变体，其使输入和输出操作完全对称，并且在同步期间启用更通用的名称匹配机制融合是一种名称等价，允许在一个术语中互换使用同一等价类的所有名称在计算上，融合是由于两个互补动作之间的同步而产生的，并且它被传播到与活动动作并行运行的融合是理想的代表，例如，转发器的对象之间的位置或形式的模式匹配对消息之间的迁移。在融合演算中，一个融合一旦生成，就立即应用于整个系统，并且它具有一个（可能是非内射的）名称替换的效果。另一方面，显式融合演算[3]是一种变体，旨在保证融合到环境的异步广播。显式1欧盟IST-FP 6 16004综合项目SENSORIA部分支持的研究。2电子邮件地址：buscemi@di.unipi.it3 电子邮件地址：ugo@di.unipi.it1571-0661 © 2006由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.12.109136M.G. 布谢米大学Montanari/Electronic Notes in Theoretical Computer Science 162（2006）135融合是与系统的其余部分同时存在的过程，并且能够自由地使用两个名称中的一个。一个coalgebraic框架[7]有几个优点：余代数之间的态射（余同态）享有“反射行为”的性质，因此它们允许例如将互模拟等价作为态射的核，并将双相似性作为最终余代数的态射的核。 此外，适当的时态逻辑和通过共归纳的证明方法也很好地适应了这幅图景。然而，在普通的共代数框架中，转移系统的状态双代数模型在这个方向上向前迈出了一步：它们的目标是捕获组合的交互系统。粗略地说，双代数[8]是可以看作代数范畴上的余代数而不是范畴Set上的余代数的结构，或者对称地看作余代数范畴上的代数。Turi和Plotkin在[8]中证明了具有句法结构的变迁系统lts可以提升为双代数，只要lts的SOS规则是GSOS规则格式.因此，lts上的双相似性是一致的，即抽象语义的组合性被自动保持。我们应用在[8]中开发的一般方法来提供没有递归和限制的融合演算的片段的组成煤-地质模型这项工作的一个关键贡献是通过标记的过渡给出了明确的融合，据我们所知，以前是缺席的我们认为，我们的结果不仅涉及融合演算，但它可以适合基于模式匹配的语言的理论基础。我们专注于融合演算的一个片段，因为在这篇短文中，我们只对解决名称融合的关键问题感兴趣。限制的引入需要处理名称的动态创建，这是名称融合的正交方面，并且在[1]中已经考虑了pi演算。在任何情况下，限制和递归都可以在我们的理论中建模。 我们指 到[2]的完全融合演算的共代数模型我们首先介绍了一个代数，其操作是构造的calculus加上常数建模显式融合。然后，我们定义了一个配备了该句法结构的转换系统，并得出结论，相关的双相似性是一个同余。值得注意的是，显式融合使我们能够在融合演算中模拟名称融合的全局效果，即使我们的代数不包含替换操作。 事实上，可观察到的替代效果是由特殊的SOS规则来模拟的，这些规则使进程行为饱和，同时仍然保持显式融合典型的异步传播的良好特性。我们声称，在我们的代数融合剂的翻译是完全抽象的融合hyperequivalence。由于篇幅有限，我们省略了证明;它们可以在[2]中找到M.G. 布谢米大学Montanari/Electronic Notes in Theoretical Computer Science 162（2006）1351372聚变演算fusion演算是pi演算的一个变体。π演算和融合演算之间的关键区别表现在同步上：在融合演算中，同步的结果不一定是局部的。例如，两个代理uv.P和ux.Q之间的相互作用导致v和x的融合。这种融合也会影响并行运行的任何进一步的进程RR| UV.P|ux.Q{x= v}› −→R|P|Q.在这项工作中，我们考虑一个一元版本的微积分没有限制和复制。对于融合演算的完整处理，我们参考[6]。设N ={x0，x1，x2，.. . }是无限的，可数的，全序的名称集，并让x，y，z.表示名称。融合是N上的一个全等价关系，只有有限个非奇异等价类。融合的范围是由，，. τ表示身份融合。我们用+表示比和更粗糙的最细融合，即自反和传递闭包（）;用[x]表示x在中的等价类;用±表示比更细，即对所有x∈N，[x][x];我们写{x=y}来表示{（x，y），（y，x）}。定义2. 1L etAb e initia lalge. braT. with... π。.|.. x=y，其中，将预修复定义为π：：=x<$y。 xy。- 是的请注意，即使代数不包含替换操作，签名中的显式融合x=y也允许对融合演算的替换效果进行建模。实际上，显式融合x = y允许表示由同步产生的名称融合的全局效果，而不需要在并行过程中用y替换x或反之亦然，即名称x和y可以在上下文x = y中一个用于另一个|.在实践中，而不是应用到一个代理的替代效果的融合，代理是并行运行的融合本身。融合剂可以如预期的那样被翻译成代数A定义2.2设L为标签集L=Λ× Φ，其中Λ ={x y，x y，，−| x，y，n（n）∈N}，Φ是N上所有融合的集合. 我们让α，β，. 在Λ上的范围。标签L的左侧分量对应于融合演算的自由作用，而右侧分量则表示在同一等价类中的两个名称可以在给定的术语中互换使用一个蕴涵关系定义如下：如果α，β/=β，σ（α）=σ（β），若σ+σ=σ+σJ，则σ=σ（ β）.定义2.3[transition specification Δ] transition specification Δ是一个元组，L，R，其中签名是定义2.1中的，标签L是定义2.2中的，R是表1中的SOS规则集。过渡的形式是（α，α）p−−→q，其中（α，α）的范围在L上。138M.G. 布谢米大学Montanari/Electronic Notes in Theoretical Computer Science 162（2006）135FJJ（PRE）（xJ yJ，J）xy.p−→ p |ϕϕJ±ϕ；ϕ►xy= xJyJ（J，J）（F US）.p−−→p|+（EXP）（−，x= y）x=y−→x=y x/=y（−，1）（−，2）（PAR）p1−→q1p2−→q2（−，）p1|p2−−−→q1|Q2J±（α，α1）（−，α2）（第1段） p1−→q1p2−→q2（β，β）p1|p2−−→ q1|Q2J±（α，α）（xy，n）（x<$z，）（PAR）p−−→q（α，α）p|r −−→ q |Rp1−→q1p2−→q2（COM）（y= z，m）p1|p2−→q1|Q2|y= z规则（PRE）与输出动作类似。表1结构操作语义学表1中的关键规则是处理显式融合的规则。通过规则（EXP）传播显式融合，并且通过规则（PARf）和（PAR1），它们分别并行地彼此组合以及与其他代理组合。规则（PRE）和（FUS）旨在确保相关的双相似性通过关于并行运行的融合的闭合来保持。所有的边条件都确保了显式融合过程行为的饱和。实施例2.4• 设p为项p = x y.y w。0的情况。 根据规则（P RE），p可以经历以下任何一种转变：（x y，τ）（z y，τ）（xJyJ，n）p−→yw。0p−→yw。0|z=xp−−−→yw。0|你好，对于所有的xJ，yJ，使得xj=xJyJ，以及对于所有的x j，使得xj±x j。• 假设p1=（x=y）|（y=k）|p和p2=（x=y）|（x=k）|p. 项p1和（α，y= k）p2有相同的跃迁。 例如，如果p1−→，则根据规则（EXP）和（α，α）（PARf），p2−−→，对于任意的x±x=y+x=k，特别是对于x=y=k。（y= k，k）• L etp=x<$y.p1|zk. p2beaterm. Byrules（PRE）andd（COM），p−→p1|p2|ψ|y=k，对于所有的π和π，使得x=z±π和π±π+（y=k）;换句话说，在p中的同步可以发生在任何上下文中，其中x和z可以彼此使用，并且，此外，可以观察到任何定理2.5设lts是转移系统lts = λA，−→ λ，其中−→由表1中的SOS规则定义，并且设λ是与lts相关联的双相似性。M.G. 布谢米大学Montanari/Electronic Notes in Theoretical Computer Science 162（2006）135139双相似性是一个全等性。定理2.6设P和Q被两融合剂.然后，P埃什河Q[P]][[Q]]，其中，[[ P ]]表示融合超等价[6]，[[·]]是融合因子到A项的转换。3结论为了本文的目的，我们考虑了融合calculus的片段。在[2]中，我们提出了一个全微积分的双代数模型，这使得一个更复杂的场景。例如，限制操作引入了动态名称创建的问题。因此，在loc.cit. 作者定义了一个置换代数[5，1]，它丰富了微积分和显式融合的运算，并配备了公理化。在这种更一般的情况下，双相似性被证明是一个同余，通过利用提升结果[1]，该结果将图里和普洛特金的方法推广到具有结构公理的微积分引用[1] M. Buscemi和U.蒙塔纳里Pi演算早期观测等价性的一阶共代数模型。在CONCUR '02，LNCS 2421的程序施普林格，2002年。扩展版本可作为TR-02-14，Dipartimento di Informatica -比萨大学。[2] M.Buscemi 和 U. 蒙 塔 纳 里 融 合 演 算 的 复 合 余 代 数 模 型 。 曼 恩 角 可 查 阅http://www.di.unipi.it/BUSCEMi/Fusion.pdf 。 发 表 在 JournalofLogicandAlgebraicProgramming上。[3] P. 加德纳和L.维斯奇克明确的融合。Theoretical Computer Science，340（3）：606[4] R. Milner，J. Parrow，and D.沃克移动过程的演算（第一部分和第二部分）。信息与计算，100（1）：1[5] 联合Montanari和M.皮斯托雷 π演算的结构余代数和极小HD自动机Theoretical Computer Science，340（3）：539-576，2005.[6] J. Parrow和B.维克多融合演算：移动过程中的表达性和对称性在1998年LICS会议记录IEEE Computer Society Press，1998.[7] JJM拉顿泛余代数：系统理论。Theoretical Computer Science249（1）：3-80，2000.[8] D. Turi和G.普洛特金数学运算语义学。在Proc.of LICS计算机社会出版社，1997年。
我的内容管理
展开
