理论计算机科学电子笔记104（2004）199-215www.elsevier.com/locate/entcs一个图形化的融合演算伊万·兰尼斯1Dipartimento diInformaticaUniversit`adiPisa意大利比萨乌戈·蒙塔纳里2Dipartimento diInformaticaUniversit`adiPisa意大利比萨摘要我们分析了融合演算和同步超边替换（SHR）风格中定义的图形变换之间的关系。特别是，我们表明，基本的代数结构是相同的同步时，在SHR是米尔纳同步。我们看到的主要区别是Fusion Calculus具有交错行为，而SHR本质上是并发的。在本文中，我们介绍了交错语义的SHR与Mil- ner同步，并表明，有一个完整的对应关系之间的操作语义的融合演算和SHR系统。关键词：融合演算，图变换，同步超边替换，迁移率1介绍本文比较了两种不同类型的模型，它们对研究并发、分布式和移动系统是有用的。这类系统在实践中非常重要，因为它包括互联网，互联网*研究得到MIUR项目COMETA和EU-FET项目AGILE的IST-2001-32747。1 电子邮件地址：lanese@di.unipi.it2电子邮件地址：ugo@di.unipi.it1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.08.026200I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-数以亿计的用户，但也有其他类型的网络，如局域网和无线通信网络。在这种环境中开发大型系统的问题是复杂的，因为传统的因此，需要能够在适当的抽象级别上处理这种情况的强大的正式模型和工具。在文献中出现了一些建议，其中一些被广泛使用，但没有一个单一的形式主义已经成为这种系统的最佳模型。在这种情况下，分析和理解不同模型之间的关系非常重要，以便找出处理这种系统所需的功能，哪些是可能的选择，哪些是每个模型的优点和缺点。本文研究了融合演算[11]与同步超边替换[1，3]之间的关系。融合演算遵循过程演算的方法，其中，如在CCS [9]中，系统由合适的代数中的项建模，操作语义由结构归纳指定CCS的后继者，π演算[10]，允许在简单的数学框架中研究广泛的流动性问题融合演算是π演算的一种演化，它是通过简化π演算并使其更加对称而获得的。实际上，π演算的输入前缀已经被分解成一个新的输入前缀，它相对于输出前缀和一个标准的π演算限制是对称的此外，融合演算有一种新的动作，融合动作，它合并名称，从而允许对π演算无法处理的移动性的某些方面进行建模。进程演算方法在应用于分布式系统时的一个已知限制是，进程演算缺乏直观的表示，解决这类问题的一种不同方法是基于图变换[12]。在这种情况下，配置由一个图显式表示，该图既具有清晰的、固有的并发数学语义，又具有暗示性表示。在图形变换的各种建议中，我们选择同步超边替换（SHR）[2，1，6，3]。在我们的方法中，我们表示计算实体，如进程或主机与超边（边连接到任意数量的节点）和通道之间的共享节点。就动态方面而言，我们使用生产指定的行为，通过暴露在节点上的动作同步的单个超边。由同一节点上的不同hyperedges公开的操作必须兼容。什么是兼容的I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 201平均值取决于同步模型的选择。例如，我们可以有Hoare同步，其中所有的边缘必须暴露相同的动作（在CSP风格中），以及Milner同步，其中两个相应的动作（我们使用具有移动性的SHR扩展[5，3]，允许hyperedges将节点引用与操作一起发送。在同步期间，其参考被匹配的节点被融合。如[4]所示，这种方法非常有表现力，因为它可以使用多个同步来定义仅使用局部规则的全局重写步骤。在文献中，SHR已经被用作元模型来研究其他形式主义，如π-演算[4，5]和Ambient演算[3，8]。我们的工作特别是扩展了[5]关于π演算的工作，以应对Fusion演算的表达能力。我们表明，融合演算（与保护和递归）是严格对应的SHR的一个子集。对应关系是基于两个模型中存在两个类似的算子，即。e.用于构建系统的并行组合运算符和用于声明局部名称的限制运算符。此外，我们认识到流动性的各个机制之间的密切关系主要的区别是Fusion Calculus具有交错语义，并且在每一步只允许一个同步，而SHR是并发模型，并且允许多个同步。因此，为了有一个完整的对应关系，我们必须强制一个inter-leaving语义也为SHR，我们所做的使用一组特定的推理规则。通过使用正常的推理规则，我们有对应于许多融合演算步骤的转换第2节包含所需的背景，特别是融合演算（2.1）的语法和语义，图的代数表示和SHR（2.2）的规则。第3节包含本文的主要贡献，即交织Milner SHR（3.1）的规则和从融合演算到交织Milner SHR（3.2）的映射。最后，第4节包含了一些结论和未来工作的痕迹2背景2.1融合演算Fusion Calculus [11]是一种用于建模分布式和移动系统的演算，它基于融合和范围的概念。它是π-微积分[10]的一个发展，有趣的是它是通过简化微积分得到的。事实上，用于通信的两个动作前缀是对称的，而在π演算中它们不是，我们只有一个称为范围的绑定运算符，而π演算有两个（限制和202I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-Σ输入）。如[11]所示，π演算在语法上是Fusion演算的子演算（关键点是π演算的输入是使用input和scope获得的）。为了具有这些特性，必须引入熔合作用。我们将详细介绍融合演算的语法和SOS语义。在我们的工作中，我们只考虑融合演算的一个子演算，它没有匹配（但我们稍后将讨论如何重新引入它），也没有失配算子，只有保护求和和递归。在我们的讨论中，我们区分顺序代理（其中有一个总和作为最高的运营商）和一般代理。我们假设有一个无限集合N的名称范围由u，v，...，z.名称代表沟通渠道。我们用x表示一个名称向量，用φ表示N上的一个等价关系，它可以用一个有限的等式集来表示（我们用1表示恒等关系）。定义2.1自由行动的定义如下：α：：=ux（输入）ux（输出）φ（融合）定义2.2代理人的定义如下：S：：=αi.Pi（保护和）我P：：= 0（不采取行动）S（顺序代理）P1|P2（组成）（十）P（范围）recX.P（递归）X（代理变量）作用域操作符是名字的绑定器，因此x被绑定在（x）P中。类似地，rec是代理变量的绑定器，此外，我们只考虑相对于代理变量封闭的代理，并且在recX.P中，X的每次出现都在顺序代理（保护递归）中。我们定义函数fn，bn和n，给定一个代理或一个动作，分别计算自由，绑定和所有名称的集合（融合中的名称是非单例等价类中的名称）。过程是被认为符合如下定义的结构公理的主体I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 203≡−→P|{}−−→定义2.3施事之间的结构同余是满足α-转换律（对于名称和施事变量）、求和和合成的阿贝尔幺半群律（结合性、交换性和0作为单位元）、作用域律（x）0 <$0、（x）（y）P <$（y）（x）P、关于LawP的可拓性的最小同余|（z ）Q（z ）（P|Q）当z∈/fn（P）时，给出了递推律rec X.P<$P{recX.P/X}.注意，fn可以简单地扩展到进程。定义2.4约束作用量的形式为（z）ax，其中|z|> 0且z中的所有元素也都在x中。z中的名称是绑定名称。动作由自由动作和约束动作组成。为方便起见，我们将φ\z定义为φ（N \{z}）2<${（z，z）}。我们现在可以呈现SOS语义。定义2.5[融合演算的SOS语义] PREF−α。P−→αPP→−αPJ总和P+Q−→αPJPAR网P−u→xP→−αP|Q→−αPJ，QuyPJPJ|QQJ，|X|为|y|x=y−−−−→ PJ|QJ范围φP→−PJ，zφx，z x（z）Pφ\z PJ{x/z}P→−αPJ， z∈/n（α）通过（z）P→−α（z）PJ开放(y) axP−→PJ， z∈x\y， a∈/{z，z}（zy）ax(z)P−→PJP−→αPJP<$QPJ<$QJSTRUCTQ→−αQJ我们在这里展示了一个有用的分解，可以定义为融合剂。204I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199---定义2.6代理P的标准分解被定义为：P=σPP其中reσP是标准subs t，Pt是P的标准年龄nt。这种分解满足：P=σQ意味着P=QσP=σσQ我们用fnarray（P）表示P中出现的自由名的数组，根据P的结构所规定的固定顺序进行排序。特别是σP={fnarr ay（P）/fnarr ay（P）}。标准分解可以很容易地扩展到流程。2.2同步超边缘替换同步超边替换[2，1，3]是一种（超）图变换的方法，它允许使用局部产生来定义全局变换因此，通过组合条件相容的不同产生式，得到了全局变换。兼容的确切含义取决于我们使用的同步模型。可能的模型是例如Hoare [7]和Milner [3]同步模型。此外，重写系统还使用节点移动性，即在转换期间，可以传输对节点的一些引用，并且合并对应的节点我们用标号转移系统给出了SHR的形式描述，但首先我们需要超图的代数表示超边，或简单地说是边，是具有标签的原子项（来自排序字母表LE= LEnn=0，1，. ），并与其标签的等级一样多的有序触角。一组节点，连同一组这样的边，形成一个超-图（或简单的图），如果每个边都通过它的触角连接到它的附着节点。图配备有一组由不同名称标识的外部节点。 外部节点可以看作是图及其环境（i. e.上下文）。我们认为图的同构保持边缘和节点，外部节点和边缘标签之间的连接。现在，我们将图的定义作为句法判断，其中节点对应于名称，外部节点对应于自由名称和边到形式L（x1，.，xn），其中xi是任意名称，L∈ LEn.I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 205N≡|⊆∪定义2.7[作为句法判断的图]设 是一个固定的， 一组名称，LE是一组排序的标签字母表。一个句法判断的形式为ΓG，其中：(i) “N”是一个有限的名称集合（图的外部节点）。(ii) G是由语法生成的术语G：：= L（x）|G|G| νy G|无其中x是名称的向量，L是具有rank（L）= |X|和Y是一个名字。我们把ν定义为一个绑定器，所以在νy G中，y的所有出现（也是G中的出现）都是绑定出现。我们像往常一样定义函数fn、bn和n。我们要求fn（G）<$r。我们用记法Γ，x来表示将x加到Γ上所得到的集合，假设x∈/Γ。类似地，我们写Γ1，Γ2以说明名称的结果集是Γ 1和Γ 2的不交并。定义2.8[结构一致性]我们定义了句法判断的结构一致性，它遵循以下公理：(AG1)（G1）|G2）|G3-G1|（G2）|G3）（AG2）G1|G2-G2|G1(AG3)G|nil G(AG4)νx νy Gνy νx G（AG5）νxG<$G如果x∈/fn（G）（AG6） νxG<$νyG[y/x]ify∈/fn（G）（AG7）νx（G1|G2）（νxG1）|G2，如果x∈/fn（G2）公理（AG1）、（AG2）和（AG3）分别定义了算子的结合性、交换性和诣零上的恒等式。公理（AG4）和（AG5）指出，图的节点只能以任何顺序隐藏一次。公理（AG 6）定义了图关于其束缚名的α-转换公理（AG7）定义了隐藏和平行合成之间的相互作用由于公理（AG4），我们可以写为νX，其中X = i=1. n{xi}，来计算νx1νx2. vxn. 注意，通过使用公理，我们总是可以将正规形式的任何判断，其中G是只包含边的合成的子项。我们也可以使Γ和X是不相交的节点集。注意n（G）ΓX.我们可以陈述下面的对应定理。定理2.9（图与判断的对应）直到结构公理的良构判断同构于图206I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-∈Λ，πΛ，π1−−→2 1−−−→2到同构。我们在这里介绍SHR计算的步骤。定义2.10[SHR transition]设Act是一组排序的动作。法的等级是ar（a）。SHR转变的形式为：Γ<$G−−→Φ<$GJ其中，Λ ∈ Γ ×Act× N∈，使得Λ在其第一个参数中是全函数（即Λ（xi）=（ai，yi），我们将yi表示为n Λ（xi）），并且我们要求ar（ai）= |y i|π：Γ→ Γ是幂等代换。我们定义：• n（Λ）={z| <$x.z ∈ n Λ（x）}• Φ =π（Γ）π（n（Λ）\Γ）我们要求<$x∈n（Λ）.π（x）=x（这意味着我们只传达由π定义的等价类的代表）。如果π是恒等式，我们可以去掉它。我们通常有一个零元的平凡动作n，因此当没有其他说明时，我们假设Λ（x）=（n，n）（如果这对所有x都发生，我们写Λ = Λn）。我们从基本产生式中推导出SHR转换，这些基本产生式使用一些推理规则来定义单个超边的可能性，这些推理规则取决于同步模型的选择。定义2.11[SHR生产]生产是SHR的一种过渡形式：x1， . . . ，xnn=s（x1， . . ，xn）−−→ΦG其中所有xi都是不同的。产生式必须被认为是模式，也就是说，如果我们有一个产生式，我们也有通过应用内射重命名可以从它获得的所有产生式。本文给出了Milner同步模型的推理规则集定义2.12[Milner同步规则]GΛ，π公司简介ΓJ<$GJΛJ，πJΦjGJΓ，ΓjG |GJ−Λ−−Λ−J，−π−→πJΦ，Φj |GJ1122其中（Γ<$ Φ）<$（ΓJ <$ ΦJ）=<$。（面值）I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 207Λ，π⎧−−−−→ifσ（x）=σ（y）=z<$x=/y<$Λ（x），Λ（y）/=（τ，τ）−−−→−−→（合并）ΓG−−→ΛJ，πJΦφGJσ（Γ）<$σ（G）−→ΦJ <$νUρ（σ（GJ））其中σ：Γ→ Γ是幂等替换，并且：• σ（x）=σ（y）<$Λ（x）/=（，）<$Λ（y）/=（，）<$x/=y<$（<$z∈ N \ {x，y}.σ（z）=σ（x）<$Λ（z）=（n，n））Λ（x）=（a，v）• ρ = mgu（{σ（v）= σ（w）|σ（x）= σ（y）<$Λ（x）=（a，v）<$Λ（y）=（a，w）}σ（x）= σ（y）|π（x）= π（y）}）• ΛJ（z）=ρ（σ（Λ（x）如果σ（x）=z<$ Λ（x）/=（λ，λ）其他智慧• πJ= ρ|σ（Γ）• U=ρ（σ（Φ））\ΦJΛ，πΓ，x<$GΦφGJ其中：τ νx GΛ|Γ，π|ΓΦjv Z GJ• （π（x）=π（y）<$x/=y）<$π（x）/=x• Λ（x）=（τ，π π）Λ（x）=（τ，π）• Z={x}如果x∈/n（Λ|r）， Z= 10° e r wi s e（空闲）ΓGΛc，idGMilner同步模型的规则假设动作可以是正常动作（此外，我们有两个特殊的作用量，即无作用量和内部作用量。规则（par）允许使用不相交的名称集合组合转换。 规则（merge）处理非内射的重命名，规则（res）限制没有通信发生的名称，规则（idle）保证每个边总是可以进行显式的空闲步骤。（res）208I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-⟨⟩⎧⎨·⎩−−−→−−−→11223融合演算到同步超边缘替换的映射在本节中，我们提出了从Fusion Calculus到SHR的映射，该映射扩展了[5]针对π演算的工作，并将Fusion Calculus映射到一种特殊类型的SHR，该SHR使用Milner同步并具有特殊规则以强制交织行为。这是必要的，因为融合演算的语义本身就是交错的。这种映射具有自然的优点（存在一对一的映射，其将并行组合映射为并行组合并且将作用域映射为限制）并且实现两个模型之间的完全对应。3.1交错米尔纳SHR为了定义Milner交织SHR的推理规则，我们需要将自己限制在两种转换中：• 通信转换：对于每个x，它们具有π=id和Λ（x）=（π，只有一个（我们用行为表示这种Λ）;• 聚变跃迁：它们具有Λ = Λπ。我们现在介绍在这种情况下使用的一套特殊的推理规则。定义3.1[用于交织米尔纳同步的规则]（人）Λ，πΓG−−→ΦφGJΓJ，σ（Γ）<$σ（G）-Λ-J-，→πJΓJ，ρ（σ（Φ））<$ρ（σ（GJ））其中σ：Γ→ Γ是幂等替换，并且：• ρ= mgu（{σ（x）= σ（y）|π（x）= π（y）}）ΛJ（z）= ρ（σ（Λ（x）如果σ（x）=z<$ Λ（x）/=（λ，λ λ）（λ，λ λ） 否则• πJ= ρ|σ（Γ）G第一幕，本剧Φ φGJG第二幕，身份证ΦjGJG|GΛc，πρ（Γ）νU ρ（GJ|GJ）其中：12−−→1 2(com/close）I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 209Λ，π−−−−→112−−→Λ，π• 对于某个节点x和对作用-相互作用a和a，act1=（x，a，y1）和act2=（x，a，y• ρ= mgu（{y1=y2}）• π = ρ|Γ• U=ρ（Φ<$ ΦJ）\ρ（Γ）（面值）GΛ，π1−−→ Φ1000mmΓ-G2G|G −−→ Φ φGJ|π（G）Λ，πΓ，x<$GΦφGJ其中：τ νx GΛ|Γ，π|ΓΦjv Z GJ• （π（x）=π（y）<$x/=y）<$π（x）x• Λ（x）=（λ，λ λ）• Z={x}如果x∈/n（Λ|r）， Z= 10° e r wi s e规则（ren）处理接口中名称的重命名，并且还允许创建新的隔离节点，规则（com/close）将两个通信转换暴露在同一节点上的互补动作以给出融合转换，规则（par）将系统的空闲部分添加到转换，并且规则（res）处理限制。注意，关于使用2.12我们去掉了τ作用量（它被τ作用量所代替），并且我们从一组通信和融合产生出发得到的所有转移要么是通信转移，要么是融合转移，也就是说它们都只有一个效应。这使得语义交织。我们可以陈述正常SHR和交织SHR之间的以下对应定理。定理3.2给定一组通信和融合产生式P，从raphΓ <$G开始，我们可以利用这一公式导出变换Γ<$G−−→Φ<$GJ在定义3.1 i中，我们可以推导出转移Γ <$GΛJ，π Φ►GJ，其中reΛ（x） =（τ，τ ε），如果ΛJ（x） =（τ，τ ε）且Λ（x） =ΛJ（x），否则i−s−e→使用定义2.12中的规则以及在某个节点上同步的一个或两个通信产品。2（res）210I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-（Ⅲ）（Ⅲ）（Ⅲ）（Ⅲ）<$（x）P）=νx<$P）（）（）（）（2）3.2将融合映射到交织SHR融合演算和SHR之间的区别之一是，在一种情况下，融合由等价关系表示，而在另一种情况下，使用替换。这两种表示之间的关系如下。定义3.3一个融合φ的代换效应是一个符合φ（i）的幂等代换σ。e. σ发送每个等价类的所有成员， φ为类中的一个代表）。我们现在定义Fusion Calculus和具有Milner同步的交错SHR之间的转换。定义3.4[动作的翻译]我们现在定义融合演算的动作和SHR的同步之间的关系。这个关系是一个函数，在通信动作的情况下，我们用−表示（当y=0时，我们有一个自由动作）：（y）ux =（u，inn，x），id其中n = |X|（y）ux =（u，outn，x），id其中n = |X|我们将inn和outn定义为互补的动作，即： e. inn=outn，outn= inn.Fusion Calculus的φ作用在SHR设置中对应于作为φ的替代效应的任何替代π。请注意，在翻译自由名称和绑定名字消失了，但对于一个nytransitionnP−→αPJbn（α）=n（α）\fn（P），可以在必要时检索绑定名称集。由于我们需要有限数量的产生式来描述每个过程的演化，因此我们只对标准形式的顺序过程使用边和产生式。特别地，每个边具有封装对应进程的标签。定义3.5[代理人的翻译]我们现在定义代理人的翻译<$0）=零S=LS（fnarray（S）），其中S是符合标准的概率代理SP1|P2= P1|P2recX.P =P{recX.P/X}我们不需要转换代理变量，因为它们只发生在顺序进程中。I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 211（2）|（三）|我 我−−→我我 我我我翻译也在等价类上有很好的定义，即。e. 因为如果P1≠P2，则P1≠P2。 请注意，如果在顺序代理内部应用一致性规则，则两个代理的转换是相同的，因为边由进程本身标记。此外，对应于规则（AG1），（AG2）和（AG3）的阿贝尔幺半群定律，（x）0 = 0对应于（AG5）的实例，（x）（y）P=（y）（x）P对应于（AG4），范围扩展定律对应于（AG7）。最后，名称的α转换是（AG6）。递归定律成立，因为递归定义的主体的平移与使用递归定律的扩展的平移一致请注意，即使这部分定义不是通过结构归纳，终止仍然是允许的，因为我们只使用了保护递归。因此，在一次应用该规则之后，我们得到一个顺序代理，其翻译被直接定义。最后，代理变量的+和α转换定律只能在顺序代理内部应用。还要注意，规则（AG5）对应于可以从P0 =P（作用域扩展定律）和（x）0 = 0获得的规则。因此，这两种形式主义有相同的底层结构，即一个平行的复合操作符和一个名的绑定器，由等价的同余来统治。作为最后一步，我们需要展示SHR系统中使用的产品定义3.6我们只为标准序贯代理人定义iαi.Pi. 设r为fn（iαi.Pi）。制作形式如下：<$<$.P）<$αi）<$P）如果αi是一个通信动作（注意，这是一个通信产生），<$α.P）→−ππ（<$$><$（P））如果αi=φ，π是φ的融合产物（注意这是一个融合产物）。请注意，由于在SHR计算中，节点永远不会被删除，因此我们在计算期间获得的图具有更多未使用的节点。在两个系统中用于计算融合的不同方法之间的对应关系由以下引理给出引理3.7设S是表示融合φ的等式集合，σ是置换。那么下面两个命题是等价的：• σ是φ的代换式;• σ是S的mgu。我212I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-α（Ⅲ）−−→► （1）−−→（2）φ（1）−−−−→||1231231−−−−−−−−−→23123123−−−−−−−−−→123聚变作用(i)无论P→− PJ，α=（Λ，id），π = id，PJ = ΓJ<$G且 ΓJ =Γ， ΓE从融合演算得到的图的一个重要特征是，我们没有生成新的名字，如下面的引理所示（但我们可以有绑定名字的挤出），然而，我们可以有无限多个名字，因为递归公理允许无限代理的有限表示（它可能包含无限多个名字）。Lemma3. 8F或每个过程P如果P−→PJ对于某个作用α，则所有出现在α中的自由名也是 P.我们现在可以陈述两个定理，证明翻译的正确性和完备性。定理3.9（正确性）对于每个融合过程P和每个Γfn（P））如果P−→αPJ和Γbn（α）=则：(i) 其中，如果α是通信，则Γ = bn（α）E E行动;(ii) 如果α是a，则对于α的任意置换π，（Γ π、P）→ − π π（Γ）π、（Pj））Λ，π定理3.10（完备性）对于每个融合过程P，如果则存在PJ使得：其中，ΓE = bn（α）;（ii）或P→−PJ，π是φ的代换项，Λ =Λ，π（PJ） =G和r J= π（r）。我们也可以通过将匹配算子分布在顺序代理上，然后向SHR添加一个特殊的规则来处理与匹配的顺序进程相对应的边。我们展示了一个如何使用翻译的例子。例3.11让我们考虑聚变跃迁：（z）（P|uxy.Q|（Uzw.R）{y=w} （P |Q|R）{x/z}。将起始过程转换为图是：νz LPLx1x2x3.Q（u，x，y）Lx1x2x3.R（u，z，w）我们可以选择Γ = u，x，y，w。此外，我们还有以下产品：x x xL（x，x，x）（x1，out2，x2，x3）x x xLx，x，xL（x，x，x）（x1，in2，x2，x3）x x xL通过应用rule（ren），我们可以得到：αx1x 2x3.QQx1x 2x3.RRI.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 213−−−−−−−→−−−−−−−→--------→−--||u，x，y，z，w=Lx1x2x3.Q（u，x，y）（u，out2，nx，yn）u，x，y，z，wLQu，x，y，z，w=Lx1x2x3。R（u，z，w）（u，in2，z，w）u，x，y，z，w然后我们可以应用规则（com/close），（par）和（res）来获得：u，x，y，z，w<$Lx1x2x3.Q（u，x，y）|Lx1x2x3.R（u，z，w）x/z，y/w−−→u，x，y<$（LQ|LR）{x/z，y/w}u，x，y，z，w|Lx1x2x3.Q（u，x，y）|Lx1x2x3.R（u，z，w）x/z，y/w−−→u，x，y<$（LP|LQ|LR）{x/z，y/w}u，x，y，wv z LP|Lx1x2x3.Q（u，x，y）|Lx1x2x3.R（u，z，w）y/W−→u，x，y <$（LP|LQ|LR）{x/z，y/w}因为{y/w}是{y=w}的替代项。在这里，我们将展示如何使用SHR在一个步骤中执行许多Fusion Calculus转换。例3.12让我们考虑融合过程（xy）（ux.P|yx.Q|yz.R）。我们可以有以下两个计算：（十）ux（xy）（ux. P|yx. Q|yz。R）−→（y）（P|yx. Q|yz。（R）X=z−→（y）（P|Q|（R）（xy）（ux.P yx.Qyz.R）uz（y）（（ux.P |Q|R）{z/x}）−→（y）（（P|Q|R）{z/x}）使用定义3.1的转换和推理规则，我们有两个相应的转换序列：u，z<$v x，y Lx1x2.P（u，x）|Lx1x2.Q（y，x）|Lx1x2.R（y，z）（u，in1，x）−→u，z，x<$νyLP|长x1x2。Q（y，x）|长x1x2。R（y，z）z/x−−−→ u，zνy（LP|LQ|LR）{z/x}u，z<$v x，y（Lx1x2.P（u，x））|Lx1x2.Q（y，x）|Lx1x2.R（y，z））→u，z<$v y（Lx1x2.P（u，x））|LQ|LR）{z/x}（u，in1，z）−→u，z<$νy（LP|LQ|LR）{z/x}请注意，在这种情况下，两个结果是相等的，即使观察是不同的，因为不同的顺序的过渡。此外，如果我们选择定义2.12的推理规则集，我们也可以有这样的过渡：1214I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-u，z<$v x，y（Lx1x2.P（u，x））|Lx1x2.Q（y，x）|Lx1x2.R（y，z））（u，in1，z）−→u，z<$νy（LP|LQ|LR）{z/x}其对应于两个转换的并发执行。我们用一个简单的模式来结束这一节，这两个模型之间的对应关系。融合SHR融合SHR过程图过渡过渡顺序过程边缘并行压缩并行压缩名称节点范围限制Prefix执行生产0无4结论我们分析了Fusion Calculus和SHR之间的关系，表明它们都依赖于相同的底层代数结构和Milner同步（但SHR也可以使用其他类型的同步模型），主要区别是Fusion Calculus相对于SHR并发性质的交织行为。因此，我们设计了一种带Milner同步的交错式SHR模型，并证明了这两种模型之间的一个对应定理。在文献中，我们有两个类似的著作，分别映射π-演算[5] 和Ambient演算[3]到SHR。关于[3]，我们使用相同的移动机制（即我们允许任何节点的融合），但我们不需要多个同步。此外，环境有不良的通信机制，只使用树结构的过程，而我们有一般的图形。关于[5]和π-演算，我们允许名字的一般融合。这一点很重要，因为这与逻辑编程中使用的移动性相同，如[7]所示，因此这项工作是从融合过程演算到逻辑编程的第一步。作为未来的工作，我们希望继续在这个方向上，特别是分析Hoare同步（这是在逻辑编程中使用）和Milner同步（这是在最流行的过程演算中使用这将弥合融合演算和逻辑编程之间的差距。未来发展的另一个方向是融合演算和SHR之间的技术转移。特别是，I.兰尼斯群岛Montanari / Electronic Notes in Theoretical Computer Science 104（2004）199-215 215将超等价的概念扩展到SHR（保持作为同余的性质），并且在相反的方向上，使用SHR以便为融合演算提供并发语义。引用[1] Pierpaolo Degano 和 Ugo Montanari 基 于 图 重 写 的 分 布 式 系 统 模 型 。 Journal of the ACM（JACM），34（2）：411[2] H. Ehrig，H.- J. Kreowski，U. Montanari和G.罗森伯格，编辑。图文法和计算手册的图变换，卷3：并发性，并行性，和分布。世界科学，1999年。[3] GianLuigi Ferrari，Ugo Montanari，and Emilio Tuosto.基于移动性的图同步的环境语义。载于Simona Ronchi Della Rocca Antonio Restivo和Luca Roversi，编辑，《国际贸易和消费者委员会Springer，2001年10月。[4] 丹·赫希。软件架构风格的图形转换模型。PhD thesis，De partamentodeCom putaci'on ，FacultadeCienciasExactasyNaturales，UniversidadeBuenos Aires，Argentina，2003.[5] 丹·赫希和乌戈·蒙塔纳里同步超边缘替换与名称移动。Springer Verlag，编辑，Proc. of CONCUR[6] 酒吧酒吧酒吧OB服务器为同步化数据组重写提供了有效的资源。Springer Verlag，编辑，Proc.TACS[7] 伊万·兰尼斯。分布式系统中基于Horn子句的进程同步。比萨大学计算机科学系硕士论文，2002年。从http://www.di.unipi.it/~lanese/tesi.ps下载。[8] 伊万·兰尼斯和乌戈·蒙塔纳里通过逻辑编程的软件架构、全局计算和图形转换。Leila Ribeiro，编辑，Proc SBESAnais，2002年。[9] 罗宾·米尔纳通信系统的演算。In Lect. Notes in Comp. Sci. ，第92卷。施普林格，柏林，1989年。[10] 罗宾·米尔纳，约阿希姆·帕罗，大卫·沃克。 移动过程的演算。 告知。的Comput。，100：1[11] Joach i mPowanddBjüornVictor. FUSION计算：在移动过程中，Ex是必需的，并且是简单的。在LICS'98的会议记录中IEEE，Computer Society Press，June 1998.[12] G. 罗森伯格编辑图文法与图变换计算手册。世界科学，1997年。
我的内容管理
展开
