偶图匹配的归纳特征的研究及双图反应系统调研

理论计算机科学电子笔记175（2007）3-19www.elsevier.com/locate/entcs偶图的匹配拉尔斯Birkedal1 Troels Christo Dumgaard1阿恩约翰Glenstrup1丹麦哥本哈根IT大学罗宾·米尔纳2英国剑桥大学摘要我们分析了偶图的匹配问题。特别是，我们提出了一个健全的和完整的归纳特征的匹配绑定偶图。我们的研究结果铺平了道路，一个可证明正确的匹配算法，需要实施的双图反应系统。保留字：双图，双图反应系统，匹配，完全归纳特征。1引言在过去的十年中，双图反应系统的理论已经发展[9，13，14]。双图反应系统（BRS）提供了一个图形化的计算模型，其中局部性和连通性都很突出。本质上，一个二图由一个位置图、一个森林和一个链接图组成，森林的节点表示各种计算对象，链接图是连接节点端口的超图。双图可以通过反应规则来重构。广义地说，一个双图反应系统由一组双图和一组反应规则组成 BRS的开发主要有两个目标：（1）通过关注移动连接（链接图）和移动位置（位置图），能够直接建模无处不在系统的重要方面，以及（2）通过开发通用理论，提供现有理论的统一，其中许多现有的并发1 电子邮件：{birkedal，tcd，panic}@itu.dk2电子邮件：Robin. cl.cam.ac.uk1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.04.0134L. Birkedal等人/理论计算机科学电子笔记175（2007）3和流动性可以用统一的行为理论来表示。 后者是通过用反应规则的抽象定义来表示双图的动力学来实现的，从反应规则中可以导出一个标记的转移系统，使得相关的互模拟关系是一个同余关系。统一恢复了π演算[9]和环境演算[8]的现有行为理论，并为Petri网[11]做出了贡献。 因此，对第二个目标的评价迄今为止是令人鼓舞的。在[2]中，Birkedal等人开始了对第一个目标的评估，特别是它展示了如何给出上下文感知系统的双图模型。正如[9，1，2]中所建议和论证的那样，实现双图反应系统的动力学以允许实验和模拟是非常有用的在IT大学的Biographical Programming Languages研究项目中，我们正在努力实现这样的实现。实现偶图反应系统动力学的核心问题是匹配问题，即对于给定的偶图和反应规则，确定反应规则是否以及如何用于重写偶图。本文的主题是分析匹配问题。在图1中，我们展示了几个双图。考虑名为a的双图。它的目的是模拟两个建筑物，一个属于一个公司，一个属于一个咨询集团。在建筑物内是笔记本电脑与数据嵌套在文件夹。 嵌套结构描述了位置图。 链接用于命名建筑物，此外，还用于建模哪些文件夹可以在公司和咨询小组之间以及公司内部共享。因此，图中所示的笔记本电脑是为该公司工作的一位顾问准备的- 顾问拥有包含属于顾问组的数据的文件夹（左侧显示的链接）和包含属于公司的数据的文件夹（右侧显示的链接属于公司的文件夹不应离开公司的事实通过将这些文件夹链接到公司大楼上的所谓绑定端口（由圆圈指示）来表示。匹配的抽象语义定义，如双图理论[ 9 ]中所定义的，大致如下（省略许多细节）：给定具有redex R和reactum RJ的反应规则（其中R和RJ都是双图），以及双图a（要被重写的主体），如果a=C（RjidZ）d，则可以将新的重写为 C （ R j id Z） d。这里，d表示双图的合成，Z是d的全局名的集合。换句话说，如果反应规则匹配a，在a可以被分解为上下文C、redex R和参数d的意义上，则a可以被重写。再次考虑图1中的示例。有一个反应规则表示通过redexR和reactumRJ;反应规则的目的是允许在相同嵌套层次结构中的连接文件夹之间复制数据（注意两个文件夹之间的R中的链接和所谓的本地名称y）。施事a可以写成C、R和d的组合-形式上，a=C（Ridz）d。合成的工作原理是：（1）将R和d的根分别插入C的孔（又名位点）;（2）将folder和z（在d中）以及z和folder（在C中）之间的连接融合在一起，在这个过程中删除z这个名字;（3）融合在一起L. Birkedal等人/理论计算机科学电子笔记175（2007）35建筑建筑文件夹0y笔记本数据顾问公司a=顾问公司C=zyR=yRJ=zD=Fig. 1.接地剂的例子a=C（idzR）d。反应规则R→RJ在连接的文件夹之间复制数据。本地名称y和R中的两个文件夹之间的连接以及名称y和C中的绑定端口之间的连接，在该过程中删除名称y注意在组合a=C（Ridz）d中使用了idz;它允许参数d中的名称z“通过”redex并附加到上下文C中的某个reactumRJ包含R中编号为1的站点的副本，表示数据在共享文件夹之间复制R中编号为0和2的站点允许反应规则也适用于笔记本电脑包含其他文件夹而不是连接的两个因此，可以使用反应规则将a重写为另一个代理aJ，如a，但在最右边的膝上型计算机中具有两个数据项（代理aJ未示出建筑建筑文件夹文件夹文件夹文件夹笔记本笔记本笔记本数据数据数据数据文件夹文件夹0123笔记本笔记本文件夹文件夹0123 4：=1笔记本笔记本文件夹数据数据数据6L. Birkedal等人/理论计算机科学电子笔记175（2007）3在图1中）。本文给出了当a=C（RidZ）dholds时，通过引入na和R（输入为一个线性映射）的一个归纳特征. 这是一个精确的表征，因为它对于抽象的定义来说既合理又完整。这提供了对匹配问题的详细分析，并且为开发和证明正确的实际匹配算法铺平了道路（其中，gich，givenaanddR，mustdC，d，anddZ满足a=C（Ri dZ）d成立）。我们还包括一个讨论如何可以从我们的归纳特征得到匹配算法。我们将在随后的论文中报告我们在匹配的实际实现方面的工作。我们的归纳特征是基于双图的标准形定理[13，5]，它表达了一般的双图如何被分解为简单图的本文给出的规范形定理和归纳特征是基于偶图的离散分解离散双图是具有简单形式的链接的双图在很大程度上，这使我们能够分析匹配的一般偶图考虑其链接图和位置图分开。当然，匹配问题与NP完全图嵌入问题密切相关。因此，我们分析了一类受限图的嵌入问题，并且我们的归纳刻画很好地利用了这类图的代数表示[13，5]。 人们希望匹配实现在实践中是有效的，因为redice通常很小。此外，对双图进行排序[3]可能是早期搜索消除的一个来源本文的其余部分组织如下。在第2节中，我们给出了一个非正式的描述绑定双图。本文的主要贡献是在第3节中，我们提出了我们的归纳特征匹配。第四节讨论了归纳特征如何保证匹配的正确性和有效性。在最后一节中，我们讨论相关工作并总结。定理3.15的详细证明，说明了特征的完备性，可以在Damgaards的硕士论文[ 4 ]中找到2绑定双图在这里，我们非正式地提出了双图;关于正式定义，见[9，5]。2.1具体双图一个由一个平面图GP和一个平面图GL组成的概念。位置图是指示位置的树的有序列表，根为r0，.，r n，节点v0，.，vk，以及一些特殊的叶子s0，...，s m称为站点，而链接图是节点集v0，.，v k扩展为内部名称x0，. ，xl，并且配备有指示连通性的超边。我们通常通过嵌套节点来说明位置图，如图2的上半部分所示（现在忽略由“：· → ·”表示的接口）。链路L. Birkedal等人/理论计算机科学电子笔记175（2007）37BigraphG：3，[{}，{}，{x0，x2}]， X→2，[{y0}，{}]， Yy0y1y2X={x0，x1，x2}Y={y，y，y}012放置图GP：3 →2X1链接图GL：X→Y根：姓名：y0y1y2研究中心：v0内部名称：v2v1ev3eJx0x2x1图二、示例二图说明了嵌套和作为位置和链接图。链接图的超边，内部边e或名称y。 作为名称的链接被称为开放，否则它们被关闭。名称和内部名称可以是全局的或局部的，后者分别位于特定的根或站点。在图2中，y0位于r0处，由小环表示，x0和x2位于在S2处，通过在站点内写入它们来指示。 像y1和y2这样的全局名称是在顶部的任何地方绘制，而像x1这样的全局内部名称在底部的任何地方绘制。一个链接，包括像图中的eJ这样的内部边，有一个活页夹（环），在这种情况下，它是一个绑定的链接，否则它是自由的。然而，绑定链接必须满足范围规则，这是一个简单的结构要求，即链接的所有点都位于其位置（在位置图中），除了绑定器本身。这可以防止例子中的y2和e被绑定。2.2控制每个节点v都有一个控制K，它决定了一个绑定和自由元，用v：K表示。在图2的例子中，我们可以有vi：Ki，i= 0， 1， 2， 3，其中K0：0→ 1，K1：0→ 2，K2：0→ 3，K3：1→ 2。这些arity确定节点的绑定和自由端口的数量，绑定和自由链路分别连接到这些端口端口和内部名称统称为点。2.3抽象的双图虽然具有命名节点和内部边的具体双图是双图理论的基础[9]，但我们的主要兴趣是抽象双图，即仅在节点和内部边的名称中区分的具体双图的等价类3。抽象双图用它们的节点控件来说明，如图1中所示的Building、Laptop等[3]在形式上，我们也忽略了空闲边，这些边没有连接到任何东西。1v0v10v2v32eJex0x2r10的v0v2s0R1v3s2s18L. Birkedal等人/理论计算机科学电子笔记175（2007）31我2.4接口每个偶图G有两个接口I和J，记为G：I→J，其中I是内函数，J是外函数。一个整数face是一个整数plem，X→，Xn，其中r em是宽度（站点或根的数量X是本地和全局名称的整个集合AndX→ 表示每个本地名称的位置，参见图2. 我们令=0，[]，{};当m=1时，该中间函数是局部的，并且如果所有x∈X都由X→表示，则该中间函数是局部的。在[12]中，我们写G：→J或G：I→，因为G：I→J，当我们不是分别关注I和J一个偶图G：I → J，如果I = 0，则称为基，或施事，如果I是局部的且J是素数，则称为素，如果m = n = 0，则称为布线，其中m和n是I和J的宽度，r是p。对于I=λm，X→，Xλ，bigaphidI：I→Icns是mrots，eacrot的sri只包含一个站点si，以及一个将每个内部名称x∈X链接到名称x的链接图。2.5离散和正则偶图我们说一个偶图是离散的，如果它的每一个自由链都是一个名字，并且只有一个点。离散双图的优点是，任何内部边的连通性必须是有界的，并且节点端口可以通过外部面的名称单独访问。在图1中，只有R、RJ和d是离散的，因为a和C的自由内边有两个点。此外，一个双图是名字离散的，如果它是离散的，并且每个有界链要么是一条边，要么（如果它是一个外部名字）只有一个点。请注意，名称离散意味着离散。一个偶图是正则的，如果对于所有的节点v和站点i，j，k，其中i≤j≤k，如果i和k是v的后代，则j也是v的后代。 此外，对于根riJ和rjJ，以及其中i是riJ的后代的所有站点i和j， 和j，如果i≤j，则iJ≤jJ。 图中的双图都是正则的，表1中的排列并不自由正则双图的优点是，当从基本双图组成它们时，可以避免排列。2.6张量积、平行积和复合对于没有名字或内名的双图G1和G2，通过并置它们的位图，构造它们的联图的并，使G2中的点的指数增加G的点的数目，可以使张量积G1 ≠ G2.例如，图1的偶图d是四个素数的张量积。我们将迭代张量G0<$··<$G n−1记为n G i，在n= 0的情况下，它是id<$。平行积G1||G2类似于张量积，除了全局名称可以共享：如果y是共享的，则G1和G2中y的所有点都成为G1中y的点||G2.我们可以合成偶图G2：I→IJ和G1：IJ→J，得到偶图G1<$G2：I→J，通过用G2的根插入G1的位置，消除两者，并将G2的名称与G1的内部名称连接起来，如图1所示，其中a=C<$（idz<$R）<$d。在下文中，我们将省略''，并简单地将L. Birkedal等人/理论计算机科学电子笔记175（2007）39我^2.7主动、被动和原子控制除了arity，每个控件都被分配了一种类型，原子，主动或被动，并根据它们的控件类型描述节点。我们要求原子节点除了站点之外不包含任何节点;任何作为被动节点的后代的站点都是被动的，否则它是主动的。如果一个偶图G的所有点都是活动的，则G是活动的。对于图1，我们可以有Data：atomic（0→ 0），Folder：passive（0→ 1），笔记本电脑：激活（0→ 0），建筑物：激活（1→ 1）。2.8双向反应系统双图本身模拟了上下文的两个基本部分：局部性和连通性。为了对动态进行建模，我们引入了双图反应系统（BRS）作为规则的集合。每一条规则R→R_J由一个正则的redexR：I→J，a正则reactumRJ：IJ→J，以及实例化Q，将Rj的每个位点映射到R的位点。I=xm，X→，X_j和I_ J=xm_J，X→J， X_j是局部的，并且通过X_J= X_j（i）相关。如图1所示，每当Q（i）= j / = i时，我们通过“i：= j”来说明Q。给定一个实例Q和一个具有素数di的离散偶图d= d0···dk，设Q（d）= d0（0）···dk，允许复制、丢弃和重排序d的部分.给定一个主体a，redexR的匹配是一个分解a=C（idZ<$R）d，具有活动上下文C、离散参数d和一些名称集合Z。通过将a转换为新的代理aJ=C（idZ<$RJ）dJ来实现动力学，其中dJ=Q（d）-图1中示出了示例。匹配的定义与[9]相同，只是这里我们还要求R是正则的。 对规则的还原反应R（和离散参数d）的这种限制并不限制可能的反应集合。 我们把注意力限制在正则R2.9记法、基本双图和抽象接下来，我们将使用以下符号： 表示所需tobed是joint;我们为Y0Yn−1写{Y→}，其中Y→= Y0，. Y n−1，类似地{→y}对于{y0， . . ，yn−1}。对于射频，我们将进行一次测试，[1] ， .. . ，X]，X，Xtomean = 0，[ ]，X，X到mean= 1，[{}]，X和（X）到mean = 1，[X]，X。任何双图都可以通过将合成、张量积和抽象应用于恒等式（在所有接口上）和一组基本双图来构造，如Tabl e 1 [5]. 对于一般的计算，当在任意条件下使用时，πX→G或GπX→，X→ 给出由G的整数fey如π。给定一个素数P，抽象操作定位其外部名称的子集。请注意，作用域规则是必须遵守的，因为素数P的内面必须是局部的，所以P的所有点都位于它的根内。抽象运算符用（·）·表示，并尽可能向右延伸当α：X→Y时，α '不等于（id 1 α）X '，当σ：U→ Y时，σ =（Y）（σ i d 1）U '. 我们写了一个新的标题，y/[x， . . ，]：→Y作为Y。10L. Birkedal等人/理论计算机科学电子笔记175（2007）322002合并合并n：n→1merge3=012符号示例浓度X'：（X）→ <$X <${ x 1，x 2 } '=抽象（Y）P（{y， y}）（{y}）{y， y， y， z}：I→Y1， [Y]，Z±Y123123年1年2年3年子序列y→/X→：X→Y[y1，y2，y3]/[{x1，x2}，{}，{x3}]=σx1x2x3年1年2年3年重命名α，βy→/→x：X→Y[y1，y2，y3]/[x1，x2，x3]=x1x2x3Closure/X：X→{}/{x1，x2，x3}=x1 X2 X3布线（id/Z）σ（id{y1，y2}{z1，z2}）一年二年=ω：X→YK→y（X→）[y1，z1，y2，z2]/[{}，{x1，x2}，{x4，x5}，{x6}]x1x2x4y1y2x5 x6离子：（{X→}）→<${→y}<$K[y1，y2]（[{x1}，{x2，x3}，{}]）=yx置换{i> →j，.. . }{0<$→2，1<$→0，2<$→1}=πX→：πm，X→，Xπ→πm，π（X→）， Xπ表1[{x}，{y}]基本双图，抽象运算，以及双图上的变量不是t[]/[]=π0=id1，dme1=π' = π 1 = id 1，其中π i是宽度为i的无名置换。作为一个例子，图2的偶图可以写成：G=（ω（（{y0}）（y0/Yid1）Yω=（/eid{y，y}）[y1，y2，e]/[{y1}，{y2，yJ，yJJ}，{e，eJ}]， Y={y0，yJ，yJJ}122 2 0 0P1=（id{y0，y1，yJ，e}}merge2）。（id{y0，e}<$K0[yJ]）K1[y0，e]<$K2[yJJ，y1，yJ]merge0<$P2=（id{eJ，yJJ}merge2）（K3[eJ，yJJ]（[{x0，x2}]）m2 2对于图1，我们有a =（id{consultation，corporation} n/z）（p1||p2），其中p1=（idzBuilding[consultancy]（[{}]）Laptop）Folder[z]Datamerge0p2=（idzBuilding[corporation]（[{y，y}]））（{y1，y2}）（id{z，y，y}merge2）（pJpJJ）1 21 22 2pJ=（id{z，y}Laptopmerge2）（Folder[z]Datamerge0Folder[y]Datamerge0）21 1pJJ=（idy笔记本电脑）文件夹[y]数据合并20x1x20 x1x2y1y2y3z0y1y2y3zKx1 x2x312 0y x2L. Birkedal等人/理论计算机科学电子笔记175（2007）311最后，一个分子是一个只有一个最外节点的素数12L. Birkedal等人/理论计算机科学电子笔记175（2007）3.^^我 我我我我我→y（X）我3匹配的归纳表征在本节中，我们提出了我们的匹配归纳特征。为了简化表示，我们将忽略匹配中的上下文必须是活动的要求（扩展以下表示以包括活动要求是直接的）。3.1预赛在这一小节中，我们将介绍一些有用的符号，并建立一些关于如何分解双图的命题。为了简化符号，我们将简单地写id为单位双图，没有下标显示接口，当它是明确的，从上下文的接口是什么。下面的命题表达了如何把双图分解成简单的构成成分。从文[5]中定理的标准形式可以很容易地得出这些证明.请注意，ω、α、σ和π的范围涵盖布线、重命名、替换和置换，参见。表1.命题3.1任何偶图G都可以分解成以下形式的合成图G=（ω_id）（D_idY），其中D是离散的并且具有局部内面。 G在此形式上的任何其他分解都采取G=（ωJid）（DJidY）的形式，其中ωJ=ω（αidY）且DJ=（α−1id）D，对于适当的α。命题3.2任何具有局部内面的宽度为n的离散偶图D都可以被分解，使得nD=（σiπid）Pi π，我其中Pi是名称离散的素数。这张表上还有其他的分解吗D把S从M身上拿走。n（σ^jid）PJπJ，其中，对于某些α^i，ρi，对于所有i，PJ=（α^i−1α ^id）Piρi（nρi）πJ=π，且ndσ^J=σ^iα^i。对于素数和分子，标准形式可以在loc中找到。前引书关于K中的ECANDECOMPOS E B→intoKy→（u→）n（ui）/（Xi）。Suchdecom-立场将是有用的，因为下面的命题，这是一个必然的结果，[5]中的定理1，第1项（专门用于自由离散离子）。支持3. 3任意自由度的离散分子方程M：I→（{→y}Z）可表示为M=（K→y（→u）idZ）P，其中P是离散素数。 M在这种形式上的任何其他分解都有式m（K→y（→x）<$i dZ）PJ，其中存在 由ui<$→xi给出的单位u e α，使得K→y（→u）α^=K→y（→x）且dP=（α^<$idZ）PJ。L. Birkedal等人/理论计算机科学电子笔记175（2007）3133.2匹配句子我们现在定义匹配句子和规则，用于导出有效的匹配句子。定义3.4匹配句是连线和双图之间的7位关系，其中ωa，ω R，ω C是连线，R<$→C，d，满足其中ωa，ωR，ωC是连线，a，R，C，d是离散双图，R和C有局部内面，R是正则的。定义3. 5一个矩阵表示序列ωa，ωR，ωCa，R<$→C，d，其中ωR：→Y，并且具有一个全局变量Z，i是可变的，表示dωa，ωR，ωCa，R<$→C，d，i（idωa）a=（idωC）（CidYidZ）（ididZωR）（RidZ）d. 不合格的身份是本地的，并根据上下文确定。对于 任 意 给 定 的 ωa，ωR，ωCa，R<$→C，d，i，则aJ=（idωa）a，C J=（idωC）（CidYidZ），dRJ=（idωR）R，naJ=C J（RjidZ）d。相反，如果对于一般的aJ，CJ，RJ，d，我们有一个匹配aJ=CJ（RjidZ）d，则通过命题3.1，我们可以分解aJ，CJ和RJ，并得到相应的有效句子。因此，有效的句子准确地捕捉了匹配的抽象定义。3.3匹配规则在图3中，我们给出了一组用于推断匹配句子的规则。在PAR中，我们进一步要求定义所有离散分量的张量积。此外，在规则PERM和ION的前提下，以及在规则MERGE、ION和SWITcH的结论中，我们要求id的这完全是由上下文决定的。我们现在解释规则。PERM规则简单地将上下文内部的置换通过redex，置换离散素数，并产生一个pushed-through置换π，取决于π和redex的内表面，如push-through引理[5]所述。PAR规则解释了如何匹配一个产品，给定两个有效的匹配，如果redex的两个部分共享一个（必须是全局的）名称，那么这两个匹配共享一些上下文连接ω图4.LSUB规则允许我们匹配任何离散素数（参见命题3.2），通过匹配一个潜在的自由（名称）离散素数与连接的代理和上下文扩展与潜在的全球替代σa和σC。换句话说，这个规则表达了我们可以通过匹配相应的自由偶图（忘记名称是局部的）来匹配具有局部名称的偶图，然后记住让正确的名字再次出现在本地。MERGE规则简单地说，要匹配具有外部merge和全局id的bigraphs，我们必须能够匹配底层的bigraphs。14L. Birkedal等人/理论计算机科学电子笔记175（2007）3KL我我染ωa，ωR，ωCa，mPπ−1（i）<$→C，（πid）dωa，ωR，ωCa，mPi<$→Cπ，dPARωa，ωR，ωC||ωb，S<$→ D，e ωa||ωS，ωC||ωa b，R S <$→ C D，de||ωS,ωC||ωD||ω►a⊗b,R⊗S‹→C⊗D,d⊗eσa<$ωa，ωR，σC<$ωC<$p，R<$→P，dσa：Z→WσC：U→Wωa，ωR，ωC<$（σ^a<$id）（Z）p，R<$→（σ^C<$i d）（U）P，dωa，ωR，ωCa，R<$→C，d aglobal合并ωa，ωR，ωC<$（mergemid）a，R<$→（mergemid）C，d离子ωa，ωR，ωC<$（（→v）/（X→）id）p，R<$→（（→v）/（Z→）id）P，dα=y→/→uσ：{→y}→σ||ωC <$（K → y（X →）ε id）p，R <$→（K → u（Z →）ε id）P，d||ωC►(K→y(X→)⊗id)p,R‹→(K→u(Z→)⊗id)P,d斯维特ωa，id<$，ωC（σ<$ωR<$id）<$p，id<$→P，dP：→<$WY <$σ：W→Uωa，ωR，ωC<$p，（σ^<$id）（W）P<$→Uα：X→β：Z→p：XXZ素公理ω，id<$，ω（α−1<$β−1）<$p，id<$→α布线公理y，Y，y/Y id，id<$→id，idcLOSEσa，σR，idYR<$σC<$a，R <$→C，dσC：→Y YCσR：→U YR（id/（YRYC））σa，（id/YR）σR，（id/YC）σCa，R<$→C，d图三. 绑定双图ωaωbxw1y1y2w2zaBYC={w}YD={w，z}ωCCidYCωRRvy1LSUBL. Birkedal等人/理论计算机科学电子笔记175（2007）315xw1y1ωwy2 zy2w zy2w2zωDidYDDωSS见图4。 使用平价规则xy1KL16L. Birkedal等人/理论计算机科学电子笔记175（2007）3yy离子规则直观地通过将结合离子分裂成自由的、离散的离子和潜在的局部替代来工作。对于任意给定的离散素数匹配，我们可以用K→y（X→）或K→u（Z→）来表示，如果我们对这些离散素数匹配的值和与此同时，我们的客户端名称→y和d→u之间的关系也比较复杂;通过以下方式确定状态其中，re α = y → f→u，reα具有hσy和dσyα两种形式。对于一个例子，如果我们考虑年龄nta=（idK→y （ X→ ） ）pyieldactxtc=（idk→u（ Z→ ） ）P，则必 须 考 虑 A J=（→v）/（X→）pyieldactxtc J=（→v）/（Z→）的定义，如如图5所示。J J J121σyJ2σyα一年二年u1u2v1v2v3v1v2v3aC aJCJ图五. 通过匹配产生上下文CJ的aJ来匹配产生上下文C的给定一个代理并考虑自下而上的推理树，规则指定如何分解代理，同时构建相应的上下文（参见，例如，在一个实施例中，IONRule）。在匹配redex的根时，应用SWITcH规则，将redex切换到上下文位置，以便代理的进一步分解检查redex是否匹配。因此，当推断匹配时，除了SWITcH之外的每个规则都可以在两种模式下使用：一种是给定agent和redex，从而产生上下文和参数;另一种是给定agent和上下文，从而产生参数。素公理和布线公理是我们的基本情况，并且直观明了（后者用于匹配零宽度的偶图cLOSE规则允许我们推断所有全局链接都打开的双图的匹配，并通过用边替换连线中的名称来图6.施事中的内部边不需要与其在redex或上下文中的对应物具有相同的身份，因此α。a RuCK 1K 2L1L2M1 M2K1K2L1L2M1 M2yz1z2u友友z1z2K 1K 2L1L2M1 M2K1K2L1L2M1 M2尤aJRJCJ见图6。 匹配redex和上下文内部和之间的封闭链接Kx1 x2 x3x4pKz1z2z3z4Px1x2x3x4pz1z2z3z4PyyL. Birkedal等人/理论计算机科学电子笔记175（2007）317我我我定理3.6图3中的匹配规则是合理的，也就是说，任何可以导出的匹配语句都是有效的。证据 简单，但繁琐，标准的代数运算。Q完整性定理将通过归纳法证明有效句子的大小，其定义如下。定义3. [7]化学键的大小为ωa，ωR，ωC→ωa，R<$→C，d中的离子数。下面的引理表达了一个有效的句子是如何通过将推理规则应用于较小或相等大小的有效句子而得到的。证明首先分解给定的有效句子的成分，然后定义声称存在的有效句子的成分，最后验证（1）声称存在的句子确实是有效的，（2）给定的句子确实可以像声称的那样导出。分解是通过命题3.1，3.2和3.3得到的，验证过程使用[5]中找到的这些标准形式和引理的引理3. 8Eve ryva alidsenten ceωa，ωR，ωCa，R<$→C，d可用于形式为σa，σR，σCa，S <$→nP i，e的等长有效句子的封闭性和perm规则。引理3.9每个有效句子σa，σR，σC<$a，R <$→P<$nPi，d，其中 P和Pi素数和离散的，是可证明的使用标准普尔规则的有效句子，或相等大小，形式为σP，σP，σP||σS► p，S <$→P，e和σC，σC，σC||σSaJ，RJ<$→nP i，eJ.aR C CaR C C引理3.10每个有效句子σa，σR，σCa，R <$→ id，d都可以用PAR和WIRING-公理证明。引理3.11Everyvalidsentenceωa，ωR，ωCp，R<$→P，d，其中p和P是独立的在一个有效的句子上使用LSUB规则是可证明的，大小，形式为ω J，ω J，ω J<$p J，R <$→ P J，d，其中p J和P J是离散自由素数。aR C引理3.12每个有效句子σa，σR，σC<$p，R<$→Q，d，其中 p和 Q是离散和自由素数，可以使用合并，PAR（迭代）和SWITcH规则在有效句子上证明，每个句子的大小较小或相等，并且每个句子都有两种形式之一• σJ，σJ，σJ<$pN，id<$→PN，e，其中pn和PN是自由离散素数，aR C• σJ，σJ，σJ<$m，S <$→ M，e，其中m和M是自由离散分子。aR C引理3.13每个有效句子σa，σR，σC<$m，R<$→M，d，其中m和M是自由的离散分子，是可证明的使用离子规则对一个有效的句子σJ，σJ，σJ，p，R <$→ P，d，小一点，其中p和P是离散素数。aR C引理3.14每个有效句子σa，σR，σC<$p，id<$→P，e，具有 p和 P自由离散素数，可以使用合并和PAR（迭代）规则在大小相等或更小的有效素数公理的实例，要么是规则素数公理的实例。形式为σJ，σJ，σJ<$m，R <$→M，d。a r M18L. Birkedal等人/理论计算机科学电子笔记175（2007）3定理3.15图3中的匹配规则是完备的，也就是说，任何有效的匹配语句都可以从这些规则中导出。证据归纳出句子的大小。通过上面的引理，我们得到所有长度为n的有效句子都可以从形式为σa，σR，σC<$m，R <$→M，d的有效句子导出，其中m和M个自由离散分子的长度小于或等于n。根据引理3.13，这些可以从长度小于n.Q4匹配算法研究完备性定理告诉我们，我们可以通过应用匹配规则找到所有有效的匹配句子。因此，匹配的规则定义了一个匹配的算法，例如很容易用Prolog表达，它只是通过使用规则搜索推理树来操作。虽然我们可以（例如，在Prolog中）直接将匹配算法建立在匹配规则的基础上，我们并不主张高效的匹配算法必须如此。我们引入匹配规则有两个目的：第一，从结构上和归纳上解释匹配，以便理解它（特别是理解与基于范式的表示的关系，并理解在匹配过程中可以在不同匹配之间进行精确选择）;第二，提供一个点，从这个点开始寻找真正有效的匹配算法，并验证它们。在我们看来，这种严格的匹配方法是合理的，因为匹配将是任何偶图动力学实现的主力在实践中，人们当然对最小化不必要的盲搜索感兴趣事实上，可以证明，考虑所谓的正常推理树是可行的，它对推理规则的应用顺序进行了限制（例如，总是以cLOSE规则结束我们在这里不包括正规推理树的正式定义，而是讨论定义正规推理树的一些可能性我们首先注意到，为了保持完整性，任何正规推理的定义当然都必须确保不损失可证明性。通过研究导致完备性定理的引理的公式，我们可以看到正规推理树的定义确实有几种可能性。例如，从引理3.8中我们可以看到，我们可以自由地用cLOSE然后PERM来结束每个推理树，反之亦然。此外，在一些规则中，我们允许传播闭合链接，即使cLOSE直观地使其不必要。我们选择在规则系统中保留这种自由，而是评论如何扩展规则集，以便在选择正规推理树的定义时有更多的自由在考虑实现时，这一点很重要，因为正常推理树的每个定义都对应着不同的匹配算法。可以说，当前的规则集自然会产生正常的推理，这些推理是“懒惰地”或“急切地”匹配链接图之间的混合而不是L. Birkedal等人/理论计算机科学电子笔记175（2007）319如果不考虑破产规则，人们本可以修改平价规则（||在结论中），这样它们也将处理闭包的匹配。这将允许真正的“按需”链接匹配。相反，我们可以修改cLOSE来比较替换，从而允许我们考虑离散双图的匹配，直到在它们的外表面上重命名isos。如果我们修改LSUB和SWITc H规则以相应地工作，则这实际上将排除对martachin g s中的w iringωa、ωR、ωC的需要。 因此，我们可以看到，这些规则中增加的复杂性意味着我们从整体上消除规则的复杂性所获得的好处很少。无论如何，这些变化将使我们能够定义一个正常推理的变体，它在链接图中是“严格的”，因为我们将立即能够基于链接图（而不是位置图）拒绝可能的匹配。另一种可能性是添加一个规则GLOB，允许我们将来自单个素数的所有这个想法似乎表明，在局部双图[12]中的匹配（其中没有全局链接，而是多位置名称）可以类似地处理，通过重铸规则以在局部链接上工作，并且仅在它们出现的所有根处定位名称4.1图的表示当然，匹配的实现必须以某种方式表示双图。一种可能性是直接用位置图和链接图来表示偶图，然后实现范式引理，范式引理表示如何将偶图分解成更简单的偶图;然后匹配可以通过分解图上的归纳来进行。 然而，一般来说，排列(For例如，merge（M1<$M2）=merge（M2<$M1）。匹配的实现需要探索所有可能的分解。这是可以做到的明确的形式，通过措辞的归纳特征匹配不是双图，但双图表达式（语法），定义在[13，5]。这样做迫使我们添加一个推理规则，它允许我们通过[ 5 ]中的等式公理 来替换匹 配序列 中的任 何表达式 ωa ， ωR ， ωCa，R<$→C，d，saya，byanotther，sayaJ，thatisprovably equal。这样做显然会产生一套完整的规则，传记式的表达当为这些定义正规推理树时，人们当然要限制等式公理的应用。正规推理树的定义将正式解释匹配算法需要探索的所有可能性。本文给出了用于匹配位置图表达式的正规推理树的定义，并证明了它是完备的。基于这些经验，我们相信找到绑定偶图表达式的正规推理树的合适定义并证明它是完备的应该不会太难。5结论和相关工作本文给出了联结偶图匹配的一个完整的归纳刻画我们目前正在努力实现匹配20L. Birkedal等人/理论计算机科学电子笔记175（2007）3基于特征。双图反应系统与图转换系统相关;图转换系统的最新综合概述见[6特别地，双图匹配与一般的图模式匹配（GPM）问题密切相关，因此一般的GPM算法可能是适用的[17，7，10，20]。由于偶图的特殊结构，一般的GPM算法预计是低效的，尽管一些GPM工具[19]使用启发式搜索策略，可能能够发现和利用偶图结构。双图的一个特殊方面是，我们可以匹配一组子树与Redex中的单个节点（站点），并匹配Agent中不同位置的多个Redex根。Fu [7]处理这样的节点和多个模式，但直接应用他的算法并不简单，因为他攻击了展开到无限深度的有根图的树同构问题。子树同构问题[15，18，16]比GPM简单，但直接将其应用于双图的位置图不会利用链接图所施加的约束。更确切地说，双图匹配的有效实现应该通过试验不同的正规推理树定义并将其与子树同构算法相结合来从初始实现中获得。这里提供的归纳特征将更容易证明实际算法的正确性。确认这项工作部分由丹麦研究机构资助（批准号：2059-03- 0031）和哥本哈根IT大学（LaCoMoCo项目）。引用[1] 伯克达尔湖，Bigraphical Programming Webages-a LaCoMoCo research project，in：SecondUK UbiNet Workshop，Cambridge，2004，position paper.[2] 伯克达尔湖，S. Debois，E. Elsborg，T. Hildebrandt和H. Niss，上下文感知系统的Biographical模型，in：L。 AcetoanddA. Ingo'lfsd'otir，editors，FOSSACS'06：Proceedingingof9thInternationalConferenceonFoundationsofSoftwareScienceandComputationStructures，LNCS3921（2006），pp. 187-201.[3] 伯克达尔湖，S. Debois和T. Hildebrandt，Sortings for reactive system