高阶移动嵌入式资源的双图语义演算及其局部名称特点

理论计算机科学电子笔记154（2006）7-29www.elsevier.com/locate/entcs具有本地名称的高阶移动嵌入式资源的双图语义1托马斯·希尔德布兰特（Thomas Hildebrandt）哥本哈根大学编程、逻辑和语义丹麦摘要双图已经被引入，目的是提供一个地形元模型的移动，分布式代理，可以操纵自己的链接和嵌套的位置，概括的π演算和移动环境演算的特点。我们给出了第一个具有嵌套位置、非线性活动过程移动性和局部名称的非线性高阶过程演算的传记式表示，即高阶移动嵌入式资源（Homer）演算。该演示文稿是基于米尔纳非线性主动过程移动性和本地名称的组合需要参数反应规则的新定义和名称位置的表示。我们建议本地化的双图作为一个概括的本地双图中的链接可以进一步本地化。关键词：双图，局部名，非线性进程迁移率介绍双向反应系统（BRS）[13]的理论已经被提出作为移动的拓扑元模型，分布式代理可以操纵自己的链接和嵌套位置。一个偶图由两种结构组成：位置图和链接图。位置图是表示系统拓扑的无序树的元组 树木的根部1由丹麦研究机构资助：2059-03-0031（LaCoMoCo）和IT-Vest网络大学：国家教学网络：基于模型的并发设计2 电子邮件地址：mikkelbu@itu.dk3 电子邮件地址：hilde@itu.dk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.0298M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7被称为区域，节点通常被称为地点，并且可以表示位置或其他过程构造器，例如，动作前置一些叶子可能是使偶图成为（多孔）上下文的位点（也称为孔）每个非站点位置都有一个控件，并且有许多通过链接图链接在一起的端口链接图表示系统中的连通性，对应于π演算中的共享名称。自由名由连接到双图的（外部）接口中的一组名称的链接表示在所谓的纯偶图中，位置和链接图可以被认为是正交结构，因为位置的嵌套和链接的连接没有相互关系。纯双图足以表示演算，如纯MobileAmbient演算。当我们转向所谓的绑定和局部双图时，正交性被打破。在[ 12 ]中引入了绑定双图，以捕获在π演算中发现的绑定和名称范围的概念。在绑定双图中，我们允许一个节点有绑定端口，并要求任何其他端口链接到相同的链接作为绑定端口在绑定端口的节点内。在[15]中，Milner将bindingbigraphs定义为局部bigraphs。在局部双图中，自由名（即，接口中的名字）都明确地位于双图的区域，同一个名字可能位于几个区域。相应地，孔（即，站点）由连接到链接的一组名称明确地注释局部双图被用来方便λ演算的表示[16]，它演示了如何使用显式替换在双图框架中表示高阶过程（过程传递）。在本文中，我们给出了第一个bigraphical表示的组合的嵌套位置的活动过程中，目前在移动的Ambients，非线性高阶过程通过（通过显式替换）目前在λ演算，和本地名称目前在π演算。事实证明，非线性、主动进程移动性和本地名称的组合需要特别注意，即：我们不能简单地将移动环境、λ-演算和π-演算的先前我们以（异步）高阶移动嵌入式资源（Homer）的演算为出发点[9]。Homer是一种纯粹的高阶演算，其灵感来自于之前的高阶演算，如PlainCHOCS [18]和HO π [17]，并且可以被视为λ演算的扩展，以包含嵌套的活动位置和（嵌套的）命名通道上的并发同步。它也是研究嵌套位置中的活动移动过程的双图的自然子类。基本上，异步Homer有两个用于定位资源的构造函数δ[r]（被动）和δ [r]（主动），其中δ是表示资源地址的名称序列。这两个构造函数对应M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）79分别连接到具有连接到链路δ的端口的无源和有源双图控制。相互作用由两个相应的构造器控制，用于移动定位资源δ（x）.p（receive）和δ（x）.p（take），分别表示通常的输入预固定过程等待在通道δ上接收（被动）过程，以及从位置δ采取主动过程的输入动作，在两种情况下，用移动的资源代替p中的x。我们允许通过简单地组合地址与任意深度嵌套的活动进程进行交互在下面的例子中，我们将资源r向下发送到嵌套地址ab（由a和b组成），并在位于位置a的地址b处接收资源阿卜勒河|a[b（x）.q |qJ]\a[q [r/x] |qJ]。（一）我们还可以从嵌套位置获取资源，如a[b [r] |p] |ab（x）.q\a [p] |q [r/x]。（二）像往常一样，我们让（n）p表示一个进程p，其中n是局部的。对于本地名称，我们还需要处理范围扩展。对于大多数进程构造函数，作用域扩展是预期的，但是当资源被移动时，可能需要将名称的作用域扩展到位置的边界，例如，如果资源r包含名称nfree，我们将预期反应a[（n）（b [r]|（p）] |ab（x）.q\（n）（a [p] |q [r/x]），（3）其中，我们垂直地通过位置边界扩展了n的范围，以覆盖名称n的所有可能出现。在Mobile Ambients演算中，垂直范围扩展在结构一致性中执行（以及通常的范围扩展）m [（n）p]<$（n）m [p]，如果nm.（四）然而，正如在[6]中所发现的，当移动进程可能被复制时，这条规则并不合理。这个问题有几种解决方案，它们都排除了结构同余式（4）中的垂直范围扩展，而是在反应关系中扩展范围这个扩展要么是急切地完成的，这意味着我们总是扩展范围，或者当且仅当名称n在r中是自由的。在《荷马史诗》中，我们选择了后一种解决方案，例如，HOπ的通常语义。与嵌套位置相结合，它的结果是上下文可以测试名称在进程中是否空闲，因此对于任何非平凡同余相关进程必须具有相同的自由名称集合（参见，例如，[9]详细讨论。然而，有时候能够从自由但不可访问的名称中抽象出来是有用的，例如。10M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7在完美防火墙方程（n）（n[p]）中，说明计算资源在本地位置的行为为了方便这一过程，我们使用了一个不包含名字的名称索引。类型pedperfectt满足nbecomes（n）（n[p]）：nn0：n为fn（p）\{n}<$n<$. 实际上，它证明了这个方程的成立性还需要用一种类型来显式地注释所有定位的子资源，这不需要通过将该类型扩展到δ[r]n和δ[r]n。相关工作在[9]中引入了Homer演算以及标记的转移互模拟同余，并且在[3，4]中给出了同步π演算的Homer编码发送和接收前缀中的复合名称也可以在具有多进同步的π演算中找到[5]，但是，不考虑活动进程的双重前缀在[13，12]中，Jensen和Milner建立了BRS的基本理论，给出了异步π演算Aπ的双图表示，并证明了导出的LTS及其双相似性与传统的LTS及其双相似性密切匹配。Milner在[14]中给出了条件事件Petri网的双图表示，Jensen在他即将发表的论文中给出了Mobile Ambient演算[11]。米尔纳改进了绑定双图的理论[15，16]，给出了具有显式替换的λ-演算的双图表示本论文的几个方面受到了这一现状的启发除了双图之外，还有几种图形形式适合于表示并发性和移动性的演算：solo图，同步超边替换，瓦片系统等，参见例如参考文献[2]显式替换在函数式编程语言中被广泛应用，主要是为了弥合编程语言的抽象定义和具体实现之间的差距。在阿巴迪等人的开创性工作中，[1]在λσ上，一个具有显式替换的λ-演算本文中选择的方法与此解不同，与Milner的λ -演算相同 一段距离。显式替换也出现在并发性和移动性的进程演算中。特别是π演算已经增加了明确的替代在几个变种，例如。使用全局环境进行替换[8]或使用De Bruijn索引并使用术语重写系统处理名称实例化[10]。该文件的结构如下：在第二节。1.1我们简要地回顾了局部双图的主要概念，并在第二节。1.2给出了微积分Homerσ。秒2包含了荷马σ作为BRS的介绍，结尾是《圣经》-M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）711局部双图的概念是局部双图的推广，其中链接可以进一步局部化。1预赛在这一节中，我们首先简要回顾了局部双图理论[15]的主要概念，并给出了参数反应规则的一个新定义然后，我们提出了在[9]中引入的演算荷马的异步变体，但扩展了显式替换，以在双图框架中呈现荷马的高阶1.1局部双图我们建议读者参考[13]的基本静态和动态理论（纯和绑定）的双图和[15]和[16]的其余细节有关局部双图。在本文中，我们将主要使用一个简单的术语语言，在上述文件中介绍，而不是图形表示的bigraphs。 术语语言由以下构造函数组成：h||G和h |g分别是两个偶图h和g的平行积和素平行积。而素平行积合并两个单区域（素）双图的区域，平行积并置区域。闭包构造函数/ng是偶图g，其中我们通过将外部名称n替换为g中的边来移除外部名称n。−→局部偶图的外表面是一个对m，X，其中m是数−→区域的集合，X是长度为m的向量，使得Xi是局部名称的集合连接到第i个区域。同样，内面是一对−→n，Y，其中n−→是站点的数量，|Y|=n且Yi是附加到iJth绝佳的价钱如果G的外表面和内表面都是对称的，则可以构造两个双图H和GH的面匹配，从而产生偶图H<$G，其中G的区域的内容已被插入到H的相应位置，并且对应的局部名称的链接已被融合在一起。双图签名K是一组控制，并为每个控制K提供一对有限序数，绑定端口和自由端口的数量，绑定元数h和自由元数k，写作K：h→k。它还确定哪些控件是原子控件，哪些非原子控件是活动控件。基础反应规则是一对（r，rJ）具有相同外表面的基础双图（没有洞的双图）给定一组基本规则，反应关系D是使得对于每个活动上下文D和每个基本规则（r，rJ），D<$rD D<$rJ的参数化反应规则允许规则包含参数，这些参数可以被复制、丢弃或只是移动。12M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7m，Xm，X参数反应规则具有redexR和reactumRJ，并且采取以下形式：（R：I→K，RJ：IJ→K，η），内表面I=π−→且I J=J−→J，而η：mJ→m是一个序数映射，它导出了下面定义的实例化η。对于每个参数d：I，参数反应规则生成基本反应规则（Rd，RJη（d））。与最初的定义不同在[15]中，我们要求显式指定参数的所有外部名称通过参数反应规则，以确保我们处理范围扩展正常实例化将redex的一个参数映射到reactum的一个参数，并允许规则复制它们的一些参数−→抛弃其他人 更准确地说，一个基偶图a：m，Xm，跨区域的闭链可唯一分解为素偶图a = c0|| · · · ||cm−1，其中ci：Xi。对于映射η：mJ→m，我们将实例化η定义为J−→JdefJdefJη（a）：λm，Xλ=cη（0）||c η（m j − 1），其中r e Xj||cη(mJ−1),whereXj=Xη（j），对所有j ∈ m.1.2高阶移动嵌入式资源我们假设n是由m和n组成的名称N的有限集合，并且n是由名称的有限集合组成的我们让γ在（可能是空的）名称序列上取值，让δ在非空的名称序列上取值，称为地址，让|δ|表示地址δ的长度，我们也让δ：：= δ |δ。我们假设一组无限的过程变量V，其范围为x和y，letx范围为v个有限的变量集。概率表达式的集合P对于（异步）高阶移动嵌入式系统的演算Homerσ具有显式替换的资源定义如下进程：p、q、r =0..π。p..p|Q.....（n）p..p[x：=q：n]..X.δ⟨r⟩n˜.δ[r]n前缀：π：：= δ（x） 。δ（x）复作用量δ_（x）和δ_（x）是Plain的一般预取CHOCS [18]或HOπ，除了我们允许名称序列作为地址而不仅仅是名称，并且我们显式输入资源r。如在引言中所描述的，动作δ[r]n和δ（x）可用于添加动作对微积分来说是很难的。 Weewritee[r]n对于δ[r]n或δrn。 THE过程p[x：=q：n阶]是一个合法的策略子过程，表示在一个可以在x中替换q（或q的）的坐标xt中处理p。下面定义的规则确保了q是封闭的，并且自由名M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）713xp：n1xq：n2x0：nxp|q：n1n2x（−）n：nxxp：n► q：mxp：nnxxx：nxp[x：=q：m]：nmx（n）p：nxxp：nx（x）. p：nfn（n）xr：mx[r]m：mfn（）表1Homerσ的打字规则的q都包含在n中。通常，我们将约束算子（n）b设为n，并使预取算子（x）和p[x：=q：n]约束可变x。上下文C的定义是采用过程的语法，并用一个称为hole的符号written（−）nnn n来扩充它。请注意，孔是类型化的，只有具有类型化的孔才能在孔（-）中进行处理。我们定义了一个有效的判断，即通过Tab中的规则1.一、从现在开始，我们将只考虑类型良好的进程。请注意，对于变量x和变量n的有限集合，当且仅当p的变量（变量s）为在集合n（x）中包含d，并且对于每个子项[r]m和q[x：=r：m]在这种情况下，可以使用这种方法进行检索。我们定义了一个新的名字和自由度是可变的，因为除了自由度之外，p[x：=r：n]定义为fn（n）n和fn（p）n，r是p的。我们说一个没有自由变量的过程是封闭的，并让Pσc表示封闭过程的集合。设Pσ/α（和Pσc/α）表示（闭）过程表达式的α -等价类的集合，并考虑α-等价过程. 我们省略子跟踪0，将ttttp：nt用于tttp：nt和ttprefixing和restriction是右结合的，比显式替换更强，让显式替换比并行组合更强。 对于名称sn={n1， . . ，nk}，其中t（n）p表示（n1）·· ·（nk）p。我们将mn写成mn，也就是假设mn=。1.3反应语义学我们为Homerσ提供了一个使用结构一致性、求值上下文和反应规则定义的反应语义在良型进程上的二元关系R称为良型的当且仅当它将进程p和q与相同的ypen（x）相关联，其中xpRq：n。本文只考虑良型关系一个关系R被称为同余当且仅当它是一个完全等价关系，并且满足x∈PRq：n∈Sx∈J∈C（p）RC（q）：n∈J∈C。结构同余定义为良型14M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7γγγєєγ可以使用以下规则导出gxpσq：n，ifxp：n，xq：n和dpσq中的关系式p|0 σp（p|pJ）|pJJ<$σp|（pJ|pJJ）p| q<$σq|p（n）p|q<$σ（n）（p|q），如果n/∈fn（q）π . （n）p <$σ（n）π。p，如果n/∈ fn（π）（n）（m）p<$σ（m）（n）p<$σp，如果n/∈fn（p）（n）（p[x：=r：n<$]）<$σ（n）p[x：=r：n<$]，如果n/∈n<$由于荷马σ允许位置层次结构中任意深度的反应，也允许进程与任意深度嵌套的子资源之间的反应一个求值上下文E是一个没有自由变量的上下文，它的漏洞没有被前缀保护，也没有作为发送构造函数的对象出现。E：：=（−）n|E|p|（n）E|δ[E]n∈Pσc。我们定义了一个多小时的家庭，通过一个特定的地址，γ∈N∈N，∅n˜m˜m˜C：：=（−）n和Cδγ：：=δ[（n）（Cγ|（−）n<$J）]m< $ J 、whenvern请注意，在所有上下文资源的集合中，都可以使用估计值extδ[E]n，并且对于一个extCn，路径地址γ指示在其下找到上下文漏洞的路径的名称表示该孔的已命名名称。中的侧条件路径上下文的定义确保了孔的路径地址中没有名字是绑定的。在路径上下文的定义中，需要使用本征名称s（n），因为结构一致性不允许垂直范围扩展，如引言所述。我们使用一个open操作符来处理垂直范围扩展和位置类型注释的更新，定义在路径上下文上。我们通过以下方式定义路径约束条件下的运算符：mC=CmCn1n2 =δ[（n1\m）（mCn2|（−）n<$J）]m< $ J<$m<$ 、δγγ若Cn<$1 n<$2 =δ[（n<$1）（Cn<$2|（−）n<$J）]m< $ J和m<$$>n<$1n<$2<$$>f n（Cn<$1 n<$2）=<$。我也是，不是吗δγγδγ操作员在管理层中将名称更改为从绑定的孔，并将它们添加到位置的类型注释中，这些位置是M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）715γγσσ``（sendσ） γδrn |Cm（δ（x）. p，−→p）\ifm（δn）=（取σ）<$Cm<$（δ[r]，−→p）|γδ（x）。p\n<$$>Cm<$（p[x：=r：n<$]，−→p）：n<$J，（nCm（0，−→p）|Jγnσm<$）n<$ γp[x：=r：n]：n 、ifm（δfn（p））=（applyσ）C（x）[x：=r：n]\nC（r）[x：=r：n]：nJ，如果Cdoes不是bi nn表2Homerσ的反应规则当在反应规则中应用时，开放操作符的后一个条件总是可以通过α转换来满足，该条件确保我们可以通过使用开放操作符来扩展范围并将限制放在顶层，而无需任何名称捕获。对 于 结 构 同 余 ， 我 们 定 义 了 Homerσ 的 反 应 关 系，其中σ是零，使得所有闭合过程的闭合关系满足表1中的规则。2，在所有评价背景下均已关闭结构一致性（sendσ）规则表示如何将被动资源r发送（向下）到（子）位置γ，在该位置γ处，在地址δ处接收被动资源r。边条件确保位置路径在上下文中不受约束，并且在移动过程中没有r的自由名受到约束。open运算符只扩展构成位置路径的位置的类型注释，而不解除任何限制。（takeσ）规则捕获计算资源r是从（子）位置γ获取的，其中计算资源r在地址δ处运行。同样，当我们取消限制时，副条件确保位置路径在上下文中不受约束，并且没有自由名称受约束开放运算符可能既解除限制又扩展位置的类型注释。规则（applyσ）用显式替换的内容替换变量的一次出现（在上下文中任意深度）。注意，我们重载了xin（applyσ）的使用，将该操作符应用于一般上下文，而不仅仅是路径上下文。但是，运算符的结果是相同的，它扩展了包含变量的规则的后一个条件总是可以通过上下文的α转换来满足（garbageσ）规则负责垃圾收集超连续替换。这些类型确保在反应期间，没有名称可以从位置的自由名称或顶层中接收资源r的进程中的位置或发送构造函数可以通过尚未出现在其注释中的r的类型来扩展其类型注释σ16M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7defxδ δXnt名称图1. Homerσ的离子和原子2荷马史诗σ的传记语义学在这一节中，我们给出荷马σ作为BRS的传记介绍荷马。 首先给出了Homer σ-项的签名，并给出了Homer σ-项到偶图的完全合成翻译.第二，翻译路径语境和反应关系。提出的一个重要标准是表明Homerσ与其作为BRS的表示之间存在静态和操作对应，这意味着结构一致性Homerσ对应于双图表示中的图同构，并且反应一致签名具有代表两个输入前缀的控件rece和take，以及代表两种（被动和主动）定位资源的控件send和loca控件var、sub和def分别表示变量和用于显式替换的构造最后，签名还具有原子控件tname（typing的缩写）和ann（annotation的缩写）来表示resource和send构造函数的显式类型注释在介绍了双图框架中的反应规则之后，我们将更详细地讨论这一点。请注意，由于路径地址是用序列中每个元素的一个端口表示的，因此我们有一个由地址长度索引的无限系列控件。总的来说，'Homerσ的签名定义如下。• var：0→1和tname：0→1是原子控件• 控件系列：rece|δ|：1 → |δ|，take|δ|：1 → |δ|，并发送|δ|：0 →|都不活跃|are all inactive• 控件家族loca|δ|：0→|δ|处于活动状态• 控件def：0→1、sub：1→0和ann：0→0处于非活动状态请注意，我们对限制和非活动进程没有控制这是为了确保静态对应，如Thm中所述2.2.在图1中，我们描述了在翻译中使用的离子和原子，我们省略了take和loca控件，因为它们分别类似于rece和send。我们选择将控件tname描述为一个点，以便能够以图形方式区分tname和var控件。遵循Milner的约定[16]，我们为X子varXrece安发送M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）717原子，我们将离子表示如下sub（x）_idZdefx_idZann_idZreceδ（x）_idZsendδ_idZ.我们将绑定端口名写在括号和最后。我们使用了一个带有单位连线的双图的扩张算子，从而扩张了双图的内面和外面。所以离子sendδδidZ有Z作为内部名称，Zδ作为外部名称。2.1翻译我们有一个从荷马σ到双图的完全合成翻译定义2.1（Homerσ-terms到bigraphs的转换）我们在x{\displaystylex{\displaystylex}p的推论中归纳地定义了Homerσ-termsp的变换：<$x0：n）=nx分x分|q：n1n 2）=<$xp：n1）|分xq：n2）<$x（n）p：n）=/n（<$xp：nn））<$xxx：n）=varxnx<$xp[x：=r：nJ]：nnJ）=（sub（x）idnn'，x）（<$xxp：n）|（defxidn'）（r：nJ）|（annidn'）<$nJ）<$xδ[r]n'：njfn（δ））=（locaδidn'，x）（<$xr：nJ）|（annidn'）<$nJ））<$xδrn'：njfn（δ））=（sendδidn'，x）（<$xr：nJ）|（annidn'）<$nJ））<$xδ（x）. p：nfn（δ）） =（receδ（x）idn，x）<$xxp：n）<$xδ（x）. p：nfn（δ）） =（takeδ（x）idn，x）<$xxp：n）并且我们将这种类型的数据分为以下几个部分： （1）=|n∈n名字;我们将0表示为具有正确外表面的空偶图，平行合成由素积表示，并且我们使用闭包/n来表示名称n的限制。 变量x表示为控制变量var的一个节点，该节点连接到名称x。我们以与[16]相同的方式表示Homerσ中的显式替换，除了我们用类型注释扩充了显式替换这两个结构δ[r]n表示为一个包含资源r的表示和类型注释的表示的相应控件的一个位置，作为一组由具有控件ann的位置包围的tname节点。 两个前缀δ（x）。 p和δ（x）。 P由相应控制的节点直接编码，其中变量x被绑定在P的加密编码中，并且我们要求x和x′是分开的。作为从Homer σ-项到偶图的转换的一个例子，我们在图2中描绘了n r的转换结果。|rJ{m}|n（x）。X.静态对应，由下面的定理所述，在应用程序中证明B.18M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7γJγMn<$r）<$rJ）发送安瓦尔雷图2. 名词名词翻译例|rJ{m}|n（x）。x转化为双图2. 2（Staticccorrespondence）x<$xp：n）=<$xq：n）。► pσq：n=0当且仅当为了给出Homerσ的反应规则，我们首先给出了路径上下文和开运算。我们定义了路径上下文的翻译n表示为某种形式的偶图，称为路径偶图，C_（n+1）结构吉吉<$C：n）=idnJJnmjJmjJCδγ：n）=（locaδidnJJ）（/n（Cγ：n）|idnJ）|（ann idm J）<$m））恩·姆·姆·杰如果Cδγ =δ[（n）（Cγ|（−）n<$J）]m< $ J.WeletF，F路径双图上的范围。并且如对于Homerσ，我们有时会用下标来表示孔的地址和上标表示孔的绑定名称。本文定义了路偶图的一个开偶图，m∈BF，用m∈B扩展了以往的符号mbidn=idnm姆吉mbF=（locaδidnJ，m）（/（n\m）（（mb<$Cγ：n））|idnJ）|（annidmJ，m）<$mm））mjJ若F=（locaδidnJ）（/n（<$Cγ：n））|idnJ）|（annidm J）<$m））. 注意我们不能只判断一个符号的位置，|si nce用一个节点显式地表示类型注释的各个元素在注解中每个元素都有一个集合，因为这会导致我们的注解是多集合而不是集合。在App.A中，我们给出了一个描述对应于Homerσ过程的偶图的排序.2.2Homerσ的反应规律在这一小节中，我们提出了'Homerσ的反应规则。定义2.3（'Homerσ的反应规则）我们定义'Homerσ的四个反应规则如下发送：``R=（sendγδidn）idn|（annidn）|Fγ（rec eδ（x）idn'）CM. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）719γγγRJ=（n<$$>bFγ）<$（sub（x）<$idn<$'）（idxn<$'|（defxidn）（idn|（annidn）η={0<$→2，1<$→0，2<$→1}采取：R=Fm（locaδidn）（idn|（annidn））|（takeγδ（x）idn'）RJ=/（m<$$>n<$）<$（（n<$$>bFm<$）<$0）|（sub（x）idn'）（idxn'|（defxidn）（idn|（annidn）η={0<$→2，1<$→0，2<$→1}适用范围：R=（sub（x）idn'）（Cvarx|（defxidn）（idn|（annidn）RJ=（sub（x）idn'）（nbCidn|（defxidn）（idn|（annidn）η={0，1<$→0，2<$→1}垃圾：``JR=（sub（x）idn'）idn'|（defxidn），R=idn'，η={0 <$→0}在所有的规则中，我们选择了在表示双图的项中从左到右枚举洞，但省略了k+1-洞中的最后k个洞pathcontextsFγ和Fm实例化在其上充当身份。在发送和取路径双图Fγ的规则都不绑定名称在δ中。在这两个规则中，ann节点的内容都用在开运算符中，这就是setn。 这两个规则都模仿了Homerσclosely中的其他规则。请注意，我们显式地输入了参数化反应规则的参数，并且我们不允许参数包含规则中未显式提及的外部名称，这一在规则Apply中，我们使用了一个满足排序要求的通用HomerσcontextC，并且它不会关闭变量链接x。反应规则垃圾，丢弃[16]这是一个明确的替代定义[16]。下面定理中所述的运算对应的证明在附录D中给出。定理2.4（操作对应）对于每一个良型进程► p：n.我们有► p\σpJ：n<$当且仅当<$p：n<$）D<$pJ：n<$）.现在，让我们仔细看看类型注释的使用。正如在介绍中提到的，我们在组合本地名称和非线性进程传递时必须小心。由于这两个过程（n）m[P]和m[（n）P]（假设n=m）（5）一般情况下，它们不是结构全等的，它们在平移下不应该产生如果我们考虑没有类型注释的编码，那么（5）中的两个过程将产生同构双图，因为我们没有办法检测闭包是发生在位置外部还是在复制参数的BRS中，这将导致与介绍中提到的相同在图3中，我们已经说明了类型注释如何帮助我们区分两个双图。 如果20M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）7mnmnloca安loca安（n）m[（−）n]n<$nm[（n）（−）n]n<$图3. 限制的位置name出现在类型注释中，则闭包必须在该位置之外，并且参数的每个副本都将共享此链接。另一方面，如果受限制的名称没有出现在类型注释中，则参数的每个副本都将具有不同的链接。对于类型注释的一个直接建议是将名称闭包显式表示为具有绑定端口的控件然而，通常的作用域条件要求（n）p表示中绑定端口的位置在进程p周围，这将破坏通常的结构同余等式如（n）（m）p<$σ（m）（n）p和（n）p|q<$σ（n）（p|q），其中n/∈ fn（q）.最近，Jensen和Milner提出了一个解决方案，以同样的问题复制参数与封闭链接明确。在他们的解决方案中，他们使用一个原子resplace来限制一种新的向外绑定端口。resplace的唯一目的是方便这个绑定端口，但与正常绑定双图中的绑定端口相反，这个端口不绑定在节点内部，而是绑定在父节点内部除此之外，端口的行为与传统的绑定端口相同。这种对每个限制使用一个resplace的限制的显式表示表现得很好。上面的结构等式，但它打破了等式：π。（n）p <$σ（n）π。p，若n/∈fn（π），（n）p <$σp，若n/∈fn（p）.更重要的是，这种解决方案没有提供所需的互模拟一致性。恩塞。仅当fn（p）≤ { n }时，引言中给出的类型pedperfwalequation（n）（n[p]）：n≤0：n才成立。原因在于，如果没有活动子位置内的链接的明确本地化，我们就会丢失本地信息当我们把一个进程放在一个上下文中时，它的外部名称2.3具有局部链接的双图由于Homerσ中的类型注释是集合，我们需要一种方法来以无序的方式将任意数量的名称关联到一个地方在图的左侧4我们已经勾勒出一种情况，其中我们有3个位置代表Homerσprocessδ[0]{m}|δ[0]{m，n}|δ[0]{m，n}，这里 我们省略了链接δ。本文所采用的解决方案，同时也应用于M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）721J JJm n m n安安安图4. 原始表示和使用本地化链接[ 7 ]中的“生命游戏”将名字标注到地点，暗示了对局部双图的扩展，在局部双图中，人们可以以无序的方式将名字直接与地点相关联，如图11右侧所4，我们称之为本地化链接。这种扩展的直接结果是，我们可以从编码中删除控件tname和ann，而是直接使用本地化链接来表示类型我们不建议将本地化链接作为传统链接的替代品，而是作为对这些链接的扩展，因为我们仍然希望能够将链接连接 到有序端口，例如。当表示元素m[p]{m}时，名称m将连接到与所述位置的地址相对应的端口，以及由于类型注释而被本地化形式上，我们建议引入一个新的函数来定义局部→−→−双图 对于局部偶图G：n =m，X= n →n，Y= n，其中边集E，位置集V ，我们 让函数 localise 将边缘 和外部名 称映射到 一组位置 ，localise：EY→Pow（V）。我们要求这个映射满足与传统链接相同的作用域条件我们定义了两个双图的合成−→−→F：m，X→ n，Y，位置为V，边为E，函数为localiseG：→−l，Z→→−m，X表示位置V、边E和函数localise对于局部双图来说是一样的。F∈G的局部化函数localiseJJ：EEJY→ P（V）P（VJ）定义如下（使用F的链接映射link）.如果x∈EJ，本地化(x) 为 localize（x）xJ∈X和link（xJ）=x局部化J（xJ），如果x∈EY.EJ中的边的位置保持不变，而对于Y中的名称或E中的边，如果X中的名称分别链接到名称或边，则我们可能需要组合localise和localiseJ22M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）73结论和进一步工作本文给出了一个具有非线性活动过程和局部名的高阶微积分，Homerσ是一个双图反应系统'Homerσ.证明了Homerσ的结构同余对应于<$Homerσ的图同构，Homerσ的反应关系与<$Homerσ的反应关系之间有紧的运算对应.该演示强调了明确跟踪免费双图反应规则中参数的名称。它还解决了本地化的名称（链接）的问题，建议扩展到本地的bigraphs称为bigraphs与本地化的链接。从本文所做的工作中产生了几个有趣的问题首先，我们计划研究使用双图的一般理论可导出的标记转移互模拟同余，并将其与[9]中Homer的标记转移互模拟同余进行我们还计划进一步研究本地化链接的扩展，无论是在方便介绍作为双图反应系统和双图反应系统的行为理论方面，特别是如果扩展保留相对推出。本文中使用的参数化反应规则不同于现有的参数化反应规则，因为我们也参数化的规则与某些上下文（路径上下文）。研究这种参数化本身是很有趣的。目前存在几个建议，用于表达对节点可能嵌套的，端口之间的链接等。看看应用程序A中的排序是否可以在这些设置中表达，特别是如果我们可以对封闭自由链接的移动和位置因此，捕获一些与向外绑定节点相同的信息，但不引入表示限制的显式确认作者要感谢国际电联双图编程语言小组的成员，他们就如何在双图中表示某些属性和构造进行了有益的讨论。我们还要感谢Robin Milner和Ole HøghJensen提供了他们论文的早期草稿引用[1] Abadi，M.，L. Cardelli，P. L. Curien和J. - J. Levy，Explicit Substitutions，Journal ofFunctional Programming1（1991），pp. 375-416.M. Bundgaard，T.Hildebrandt/Electronic Notes in Theoretical Computer Science 154（2006）723[2] 布 鲁 尼 河 和 I. Lanese ， On graph （ ic ） encodings ， in ： B. Koenig ， U. Montanari 和 P.Gardner，编辑，用于建模分布式和移动系统的图变换和过程代数，Dagstuhl研讨会论文集（2005年），编号04241。[3] Bundgaard，M.，T. Hildebrandt和J.C. Godskesen，高阶移动嵌入式资源中名称传递的CPS编码，在：J。Baeten和F.Corradini，editors，Proceedings of EXPRESS131-150.[4] Bundgaard，M.，T. Hildebrandt和J.C. Godskesen，高阶移动嵌入式资源，理论计算机科学（2005）。接受在TCS特刊上发表。[5] Carbone ， M. 和 S