粘着范畴与图形形式主义的研究

理论计算机科学电子笔记127（2005）43-56www.elsevier.com/locate/entcs作为粘着范畴的项图Andrea Corradini1 和法比奥·加杜奇2DipartimentodiInformatica，Uiversita`diPisa，Italy摘要最近的兴趣互模拟同余约简系统，刺激了研究一般（通常是图形）框架的名义演算，提出了许多建议的范畴形式主义，其中相关性质的观测等价可以自动验证。有趣的是，这些形式主义中的一些也确定了合适的类别，其中为图转换的双推出方法开发的标准工具和技术可以被重新设计，从而为高级替换系统范式提供了有效的替代方案[11]。在本文中，我们考虑了项图范畴，我们证明了它（部分）适合于在[19，26]中发展的粘合范畴的一般框架，在[12]中扩展并应用于[24]中的约化系统。主要的技术成就涉及的证明，类别的长期图实际上是准粘合剂，通过证明存在适当的范坎彭广场。保留字： 术语图，粘合剂类别，图重写。1介绍通过归约系统[4，22]表示名义演算的操作语义激发了人们对图形形式主义的新兴趣，其中包括（抽象）过程及其行为的表示。同时，它提出了一个调查之间的关系约简形式主义，通常由一组国家简单地配备* 这项工作得到了欧盟在项目IST-2001-32747 AGILE（移动性架构）和项目HPRN-CT-2002-00275 S E-GRAV IS（可视化建模技术的语法和语义集成）中的部分支持。供资机构不对可能使用此处所列结果的任何行为负责。1 电子邮件地址：andrea@di.unipi.it2电子邮件：gadducci@di.unipi.it1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.02.01444A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43转换关系和标记转换系统，以恢复归约语义框架中的行为等价概念[21，25]。在图转换社区中也提出了类似的问题。一方面，通过对图及其变换的归纳（读作：公理化）表示的研究[15，16];另一方面，通过在SOS风格[8]中用运算规则发展变换关系的表示，以及通过对图上下文的表征，讨论互模拟（在[13]中引入的借用上下文一个很有前途的工具，为这些股高兴的是由粘合剂类别，以及他们与双推出（DPO）的重写方法的联系，作为介导的cospan类别（即类别的对象是对箭头具有相同的目标）。首先，如[19，26]所示，并在[12]中推广，粘附性属性几乎涵盖了所有的高级替换（HLR）条件[11]，一个类别必须满足这些条件，以确保DPO重写的并发性和并行性标准定理的有效性与此同时，与粘合剂范畴相关联的cospans的（双）范畴提供了一个框架，在该框架中，可以通过标准归约系统来重铸与DPO重写相关联的操作语义，通常通过匹配态射来给出;此外，该（双）范畴可以定义一个标记的转换系统语义，这与通过借用上下文获得的语义一致[24]。术语图是粘合性能的合适测试用例。一方面，它们与约简语义有着天然的联系，因为它们最初是作为有效项重写的实现设备引入的;另一方面，它们的图形表示允许讨论粘合剂框架是否可以包含不同的图形形式主义。本文的主要结果证明了项图的范畴是拟粘着的，从而补充了我们在[5，6，7]中的工作在那里，我们提出了排名的术语图，配备了对它们的操作，作为重铸术语图及其在归纳设置中重写的工具（如稍后在[15，16]中对图所做的那样）。即使我们没有明确地说明这一点，我们也意识到它们代表了余跨度的范畴，这驱使我们直觉地认为这些操作应该如何表现。不幸的是，即使我们能够证明项图的准粘附性，我们仍然远远没有提出一组连贯的结果。事实上，术语图重写并不适合粘合语法[19]或粘合语法系统[12]的框架分歧有两个来源。首先，文献中用于项图重写的规则的格式比[12，19]中用于HLR风格结果的可接受格式第二，即使不对规则施加限制，粘合剂中允许的匹配A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4345GGG用于恢复互模拟和借用上下文的结果的框架对于术语图重写文献中通常允许的匹配来说限制太多。尽管如此，这些负面的结果可以被认为是进一步扩展粘附范畴和语法理论的建议，因为术语图重写代表了一个众所周知的和相关的案例研究，这将是难以简单地忽视。本文的结构如下。在第2节和第3节中，我们分别介绍了可能循环的有限项图的范畴，以及关于粘着范畴的主要定义。在第4节中，我们证明了项图的范畴满足拟粘着的相关条件，在第5节中，我们讨论了这个结果的（有限）适用性。最后，我们得出了一些结论，并提出了进一步的工作方向2（循环）项图本节根据[2]（后来在[7，23]中修订）介绍（可能是循环的，有限的）项图。定义2.1（项图）设k是一个（单排序）签名，即，运算符符号的排序集合，并且令arity为返回运算符符号的arity的函数，即，arity（f）= ni <$f∈ <$n.一个项图G（环G）是一个三元组G=N，l，s，其中N是有限个节点集，l：N~ n是称为标号函数的偏函数，s：N~N是偏函数函数调用后继函数，并且• dom（1）=dom（s），即，标号和后继函数定义在N的同一子集上;如果n /∈ dom（l），则节点a∈N称为空;• 对于每个节点a ∈ dom（l），arity（l（a））= length（s（a）），即，每个非空节点具有与其标签的arity一样多的后继节点如果s（n）= n1，. ，nk∈，ni是n的第i个后继，记为s（n）i.一个项图是离散的，如果它的所有节点都是空的。对于一个项图G，我们通常分别用NG，lG和sG表示它的分支. 此外，N和N分别表示G的空节点和非空节点的集合。定义2.2（项图态射，范畴TG）设G，H是两个图。一个（图）态射f：G→H是一个函数f：N G→N H，它保持了标记和后继，即， 使得对于任意a ∈ N∈ N，l H（f（a））=l G（a），且s H（f（a））i= f（s G（a）i），对于每个i∈ {1，.，arity（1G（a））}。图上的项图和图态射形成了一个范畴，记为TG图。在本文的其余部分中，我们利用了从项图范畴到项图范畴的基础集函子U：TG→Set46A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43、、，J、、J，CJ，fJmC，，fM、一个J，o，，，，zJ，，zBJ、、、得双曲余切值.A，，，，zBgJ，D ，n，o，，Cg，z，nsDJB，C，，fJ，，O，M一，，zJ得双曲余切值.，zJ，，o，，n，GD，，图1.一个外推正方形（i）（左）和一个交换立方体（ii）（右）。将每个项图G=<$NG，lG，sG<$映射到它的节点集U（G）=NG，将每个态射f：G→H映射到它自身U（f）：NG→NH，看作是一个函数.可以直接检查函子U有一个左伴随，它将集合X映射到以X为节点的离散项图。3粘合剂和准粘合剂类别我们在这里回顾粘合剂类别的定义[19]。我们不提供任何基本范畴结构的介绍，如产品，回撤和推出，请读者参考[3]的第5节和第9定义3.1（粘合剂类别）一个类别称为粘合剂，如果• 它沿着单声道有推力;• 它有回调，• 沿着mono的推出是Van Kampen（VK）平方。参考图1，VK正方形是类似于（i）的推出，使得对于具有（i）作为底面并且其背面是拉回的每个可交换立方体，如（ii），当且仅当顶面是推出时，正面是拉回。对于粘合剂类别，存在至少两种感兴趣的性质。第一个是粘合范畴服从于HLR范畴的许多性质[12]。换句话说，如果重写系统的规则由monos的跨度给出，这确保了关于并发性和并行性的几个结果对于粘附范畴中的DPO重写也是有效的[19]。第二个事实是关于线性余跨度的相关类别（即，具有共同目标的成对箭头，其中第一个是单声道）。正如在[ 15 ]中已经提出的，任何DPO规则都可以由一对cospans表示（更明确地说，规则L← K→ R是由对描述的（L→L<$K，R→R<$K <$），以及由、DA. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4347rules忠实地表示使用monos作为匹配获得的所有派生[16]。此外，所得到的双范畴具有相对推出[21]，因此可以自动导出行为良好的行为等价[24]，即互模拟等价，它也是（合适的）上下文下关于闭包的同余3.1胶粘剂分类就HLR系统的理论而言，已经观察到并不是所有已知的HLR类别的例子（根据[11]）都是粘性的。主要原因是hlr类别的定义是关于一组独特的箭头参数化的：在几个具体的例子中，这样的集合与mono的集合一致，但并不总是如此;粘附性是通过要求沿着mono的所有是VK平方），这是在若干HLR类别中不成立的性质。前面的观察导致了两个自然的普遍性的粘附性。在[12]中，粘附HLR范畴是关于一组独特的mono参数化的范畴，满足适当的闭包性质，并且只有沿着这些mono的推出需要是VK平方。独立地，LackanddSobcinn′skinttee（lessgeneral）准粘附范畴[19，26]，其中，本质上，monos被正则monos所取代。定义3.2（正则单声道）A单声道m：A <$→B是正则的，如果它是两个合适的箭头的均衡器。更明确地说，m是正则的，如果存在一个对象C和两个箭头fJ，fJJ：B→C使得fJ<$m = fJJ<$m，并且满足以下普适性质：对于每个对象AJ和箭头mJ：AJ→B使得fJ<$mJ=fJJ<$mJ，存在唯一的中介箭头k：AJ→A使得mk= mJ。如果一个范畴满足定义3.1的条件，并且用规则的mono代替mono，那么这个范畴是准粘着的。有趣的是，大多数针对粘合剂类别的构造也适用于这种更一般的背景[26]。4项图范畴的粘着性很容易认识到以下事实。事实4.1TG类粘合剂不是粘合剂。原因很简单，基本上在[10]中阐明：类别TG对于所有箭头跨度都没有推出，即使其中一个箭头是单箭头。例如，假设C、A和B是各自具有单个节点的三个项图，使得C的节点为空，而A和B的节点为空。48A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43一由两个不同的0元运算符符号a和b标记。而C→A和C→B的显（内射）态射的跨距没有推出。通过荒谬性，假设箭头A→D←B闭合了跨度，形成了一个推出;通过交换性，A在D中的唯一节点的像必须与B的唯一节点的像重合：但是由于态射保持标签，D的那个节点必须有a和b作为标签，这是不可能的。文[10]利用项图与标准项之间的密切关系，建立了无圈项图范畴中存在推出的一个充要条件事实上，每一项图态射f：C→B都导出一个与C的每一个空节点x相关联的替换σf，该替换σf是通过从节点f（x）解开图B而获得的则两个态射f：C→B和m：C→A有推出当且仅当伴随的置换σf和σm一致。因此，上面的例子没有推出，因为项a和b没有统一。本文的主要结果是下面的定理，本节的其余部分致力于它的证明。定理4.2范畴TG是拟粘着的。在证明定理的过程中，我们将研究基本范畴的结构，为正则单调、推回和拉回找到合适的刻画。让我们从常规的单声道开始。命题4.3 TG中的mono是正则的，如果它保留空节点，即，如果每个空节点的图像也是空的对于if的情况，让我们假设m：A <$→B是单声道，并且它保留空节点。设NC=NB（{1}×NB\m（A））（其中表示不交并）是包含B的节点和B的每个节点的不在m的像中的附加副本的集合。设函数f：NB→NC定义为f（b）=b，若b∈m（NA），否则f（b）=n ∈ 1，b∈ n.设C是项图C=<$NC，lC，sC<$，其中部分函数lC和sC扩展了那些B的，并且以这样的方式定义：f：B→C是一个定义良好的项图态射：这是可能的，因为m保留空节点。然后很容易检查m是f的均衡器，并且B到C的注入：如果mJ：AJ→B使得f<$mJ=in<$mJ，则必然f（mJ（a））∈m（NA），这决定了唯一的中介态射k：AJ→A使得mJ=m<$k。反之亦然，让我们假设m：A <$→B是两个箭头的均衡器fJ，fJJ：B→C，让我们荒谬地假设m不保持空节点，即， 存在节点x ∈ N ∈N，使得对于某些操作者symbolg∈N。现在，令Ae由Ae得到，令lA（x）=g，为B的每个节点添加一个空节点，该节点是m（x）的后继节点，以及A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4349BB一C一CBD而不是在m的年龄中，并定义为A_a_cc_rding_y。此外，在m的两个扩展中，letmk：At→Bt mk =fJtmk：At →Atm k= mk，并不存在任何形式的mk：At→Atmk=mk，M是均衡器。Q接下来，我们证明了范畴TG沿着正则monos有推出（以及正则monos在推出下是稳定命题4.4设f：C→B，m：C <$→A是TG中的两个态射，使得m是正则单射。然后存在如图1（i）中的推出。此外，态射n也是正则单射。证明给定f：C→B和m：C <$→A，如陈述中所述，3令D=nD，lD，sD，且态射g：A→D，n：B→D定义为：• 集合ND和函数g：NA→ND，n：NB→ND是函数集合f：NC→NB和m：NC<$→NA中的推出.更明确地说，ND=（NA<$NB）\n，其中n是上的最小等价关系，NA<$NB使得m（c）<$f（c）对所有c∈NC;g（a）=[a]<$对所有a∈NA;且对所有b∈NB，n（b）= [b]n.注意，函数n：NB→ND是单射的，因为集合中的mono在推出下是稳定的。• 对于所有d∈ND，部分函数lD：ND~∞被定义为：⎧如果n ∈ N，则n =a。 l A（a）= t a⎪⎨lD（d）=⎪一t b ，如果nb ∈ N nd. l B（b）= t b在其他方面，让我们证明函数lD是定义良好的，即d中的所有节点都是（NN）具有相同的标签（在相应的术语图中）。以来A Bn：NB→ND是单射的，在d<$N <$N中至多有一个节点，因此它是考虑以下两种情况就足够了：· 设a ∈ d，b ∈ d. 由于a是单射的，n是单射的，所 以 有aA Bc∈NC使得m（c）=a和f（c）=b;m是正则的，所以a∈N<$蕴涵c∈N∈ N，由于m和f是图态射，l A（a）= l C（c）= l B（b）.· 设a，aJ∈ d <$N <$，其中aaJ.根据n的内射性和n，在N C中存在c，CJ使得m（c）= a，m（CJ）= AJ，且f（c）= f（ CJ）; m是正则的，所以c， CJ∈N <$，且由于f是项图态射，f（c）∈ d <$N <$. 通过两次应用前面的情况，我们得到lA（a）=lA（AJ）。• 定 义 了 偏 函 数 s D ： ND~N， 对 所 有 d∈ND ， i∈ {1 ， … ， arity （ ID（d））}，作为[3]不失一般性，我们假设NB<$NA= N。50A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43BD一DBD一一B⎧n[aJ] n，如果 na ∈ d <$N <$. s A（a）i= aJsD（d）i=⎨⎪A[bJ]如果<$b ∈d <$N <$. s B（b）i= bJ⎪在其他方面，sD的良定性：ND→N可以证明，对于上述的lD，利用m的正则性和n的内射性。通过构造，n：B→D和g：A→D都是定义良好的图态射，并且g<$m=n<$f。让我们证明n：B→D是正则的。让x∈N，并荒谬地假设[x]。因为n是内射，所以存在B Da∈NC，其中m（c）=a，f（c）=x，但m的正则性意味着c∈N，因此f（c）=x∈N，产生矛盾。C B我们现在证明了由此产生的平方是TGε中的推出。 因此，设nJ：B→DJ和gJ：A→DJ，其中gJ<$m= nJ<$f：我们必须证明存在恰好一个态射k：D → DJ使得nJ= k <$n和gJ= k <$g。由于Set中的基础正方形是一个推出，因此只有一个中介函数k：ND→NDJ：我们只需检查它是否是态射k：D→DJ，即，它保留了标记和后继函数。设d∈N<$是D在n的像中的非空节点;由于n是正则的，我们有n−1（d）∈N<$且l D（d）=l B（n−1（d）），因为n是态射。由于nJ也是一个态射，我们推出l D（d）=l DJ（nJ（n−1（d）= l DJ（k（d））。如果d∈N<$n不在n的像中，则通过构造它是唯一a ∈ N <$n的像;则l D（d）=l DJ（k（d））遵循观察g和gJ都是态射。k保持后继函数的事实可以类似地证明。Q下面关于TG函子中沿着正则幺半群的推出的刻画是前面证明中给出的显式构造的直接结果。推论4.5给定图1（i）中的TG中的一个交换正方形，其中有m和n个正则monos，该正方形是TG中的推出当且仅当Set中的基础正方形是推出。现在，我们提供了回调的一个特征，从而证明了范畴TG具有所有回调（以及monos和正则monos在回调下都是稳定的）。命题4.6设g：A→D和n：B→D是TG中的两个态射。然后，存在如图1（i）所示的回调此外，如果态射n是（正则）单射，那么m也是。证明拉回由项图C和态射m给出：C→A和f：C→B使得NC={∈NA×NB|n（a）= n（b）;lC（a，b）=lA（a），如果a∈N<$且b∈N<$，否则定义A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4351一DJ一CBJBJC同样地，对于sC;和m（分别地，第一个是（）。（二）投影。对于第一部分，例行检查m：C→A和f：C→B是否形成回调。对于第二点，这适用于任何类别，因为限制（例如，回撤）与其它限制（例如，均衡器）。Q至于推出，下面的特征拉回在TG的证明是一个直接的结果，明确的建设在前面的证明。推论4.7给定图1（i）所示的TG函数中的一个交换正方形，如果这个正方形在TG函数中是一个回调，那么Set中的基础正方形也是一个回调;此外，假设m和n是正则单偶，如果Set中的基础正方形是一个回调，那么这个正方形在TG函数中也是一个回调。现在，我们通过在VK平方上证明下面的命题来结束定理4.2命题4.8所有沿着正则monos的推出都是TG中的VK平方。证明假设一个交换立方体如图1（ii），其中底面是推出，背面是拉回，态射m和n是正则monos（根据命题4.6，mJ也是正则monos）。我们必须证明，顶面是一个推出，而前面是拉回。为此，我们利用了Set是粘附的[19]这一事实，以及上面将TG中的推回和拉回与Set中的相应图相关联的结果。事实上，根据假设和推论4.5和推论4.7，Set中的底层立方体具有作为底面的推出，其中m和n是单声道的，并且背面是拉回。现在对于if情况，如果原始图的正面是TG图中的回撤，那么对应的面是Set中底层图中的回撤，并且由于Set是粘附的，我们推断顶部正方形是Set中的推出。然后，由推论4.5得出原始图的顶部正方形是外推的事实，观察到由命题4.6也nJ是正则的。对于唯一的如果情况，让我们假设顶面是一个推出在TG方程;因为mJ是正则的，所以根据命题4.4，nJ也是正则的。顶面下面的正方形是推论4.5中的推出，因此前面是粘附性设置那么，根据推论4.7和n和nJ的规律性，右边的正面是TG 函数中的一个拉回。事情稍微复杂的正面向左，因为它不是沿着定期单声道。荒谬地假设它不是TG中的回调：因为它是Set中的回调，所以必须有存在x∈N<$J使得gJ（x）∈N<$且a（x）∈N<$。 由于顶面是一个TG中的推出，且mJ，nJ是正则的，则必存在z∈N<$J，使得MJ（z）= x，FJ（z）∈ N∈ N，NJ（FJ（z））= GJ（x）. 因为背面朝左对易且m是正则的，c（z）∈N<$.总而言之，存在z∈N<$J，CCfJ（z）∈N<$且c（z）∈N<$，因此意味着右侧的背面是52A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43，r，~f，~，jzzx，，a，<$，，布雷尔x，，a<$，r，~，g~，，Jvzx∈r，~，b~，，，，a，⁄，图2.规则编码f（x，a）→g（x，b）。而不是TG的回调，这与假设相矛盾Q5讨论为拟粘着范畴设计的应用，以及在第3节中简要描述的应用，能用于项图范畴吗？所有的DPO陷阱都可以被改写，只要规则是常规单声道的跨度不幸的是，这并不适用于应用程序中出现的大多数规则格式。如在引言中所回顾的，术语图重写最初被引入作为有效术语重写的实现设备。因此，在文献中考虑的术语图重写规则通常是从术语重写系统的编码中获得的。现在，如果我们考虑DPO规则编码标准（左线性，非折叠）项重写规则，两个箭头是单声道，但不是常规单声道。如果规则是坍缩的，比如I（X）→X，那么右边的态射甚至不是单射。事实上，编码这样一个项规则S→T的标准DPO规则（其中我们假设S和T都不是变量，T的所有变量都出现在S中，并且没有变量在S中出现两次）具有形式（LK→R），其中[6，18]• L是表示 S的项图;• K是由 L通过使 S的标有top算子的结点为空而得到的，称之为 r， K<$→L是相应的包含;• R通过将右侧 T的表示加到 K上而获得;K→R将节点r映射到T的顶节点，对于其余部分，它是包含。因此，两个包含都不是规则的，因为空节点r分别映射到由规则左侧和右侧的top运算符标记的非空节点。这是必要的，因为它允许在任何上下文中应用该规则：所有指向S的指针都被重定向到T。作为一个例子，让我们考虑图2中描述的规则。左边的图表示项f（x，a）的语法树（注意节点标识符x是任意的，它仅用于标识形成规则的两个态射）;中间的图有两个空节点：由r标识的节点映射到左边标记为f的节点上，并映射到右边标记为g的节点上;最后，右边的图A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4353表示g（x，b）的语法树，加上标记为a的附加节点。如果它在应用规则的图中没有共享，那么后一个节点可能只是某种垃圾。事实上，上述考虑极大地限制了术语图规则的格式，而术语图规则可以应用关于并行性和并发性的良好结果。事实上，为了确保左手边态射是正则单射，规则或者不移除任何东西（左手边是同构），或者它实现一种头归约，因为它移除的算子不能是归约所保留的任何节点的后继对称地，右手边态射要么是同构，要么它可以添加任意子图，这些子图变成垃圾，因为它们不能通过有向路径从左手边的任何节点到达。遵守这些约束的规则包括那些实现分布式垃圾删除的规则（如[7]所示，重写规则删除垃圾也删除顶部节点，因此它们是规则的），但通常这些规则似乎与应用程序无关更有趣的是，头减少约束是通常在过程演算的图形编码中采用的一种约束，其中通常重写步骤必须仅在顶层执行[14，20]。我们计划在以后的工作中继续这一主题同样关于相关的cospan约化系统，我们有一个中间状态的一个矩阵。事实上，cospan框架已经足够通用，允许基于任意（甚至不是mono）规则和任意匹配来模拟DPO此外，在此框架中，并发派生的概念与DPO集合[15，16]中采用的概念一致。然而，相对推出的存在性似乎只对左线性余跨度是确定的，这意味着，具体地说，匹配态射被约束为单射。不幸的是，这种假设在现阶段看起来与标准定义相比过于严格最成功的例子尽管如此，最近对图变换理论的贡献[10，17]表明，规则和匹配之间的相互作用存在一些这些考虑值得深入分析，但这超出了本文件的范围。54A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）436结论在这篇文章中，我们研究了项图重写在多大程度上可以被改写到粘附语法的框架中，粘附语法是最近被引入的，作为DPO方法的推广，用于任意类别的图重写，这些类别配备了“行为良好”的主要的技术结果是证明了项图的范畴是准粘性的。这意味着关于并行性和并发性的标准定理对于其规则是正则单元的跨度的术语图重写系统是有效的。不幸的是，正如上一节所讨论的，应用程序中使用的标准规则不享有此属性，因此这些结果并不广泛适用。尽管如此，头部简化的建模规则确实是由一系列常规的mono构成的，它们在建模过程演算时自然出现：这是我们计划在未来探索的主题还需要进一步的研究，以了解在相关的cospan双范畴[24]中关于双相似性的结果在多大程度上适用于项图重写，可能限于内射匹配。 这里值得强调的是，在这个框架中识别的互模拟的概念与[1]中研究的双相似关系非常不同，后者基本上将那些展开为同构树的项图联系起来。最后，让我们提到一个可能的替代方法来证明并行性和并发定理的有效性，由Detlef Plump向我们提出。我们的想法是将项图视为满足某些附加条件的超图（如[10，18]），并在超图的超范畴中执行DPO构造：这可以在证明给定规则后安全地完成然后，上述定理的有效性应该遵循超图范畴的粘附性[26]，只需检查相关规则的适当闭包性质。我们发现这种方法非常有趣，值得进一步研究，即使它与本文的主要技术结果没有直接关系致谢我们非常感谢匿名的审稿人，他们的建设性批评帮助我们改进了我们的论文。引用[1] 阿里奥拉， Z.， J. 克洛普 和 D. 丰满， 联系我们 重写 的 双相似的 term 图表，在：C. Palamidessi和J.Parrow，编辑，并发中的表达性，A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）4355理论计算机科学7（1997）。[2] Barendregt，H.，M.作者：J. Kennaway，J. Glauert，M. Plasmeijer和M.睡眠，术语图简化，在：J. de Bakker，A. Nijman和P. Tziaven，编辑，欧洲并行架构和语言，Comp. Sci. Lect.Notes。259（1987），pp.141-158.[3] Barr，M.和C. Wells，“Category Theory for Computing Science，”Les Publications CMR，1999.[4] 卡尔代利湖和A. Gordon，Mobile ambients，in：M. Nivat，编辑，软件科学和计算结构的基础，Comp.Sci. 1378（1998），pp. 140-155[5] Corradini，A.和F.Gadducci，术语图重写的2分类表示，在：E. Moggi和G. Rosolini，editors，Category Theory and Computer Science，Lect. Notes in Comp.Sci. 1290（1997），pp. 87比105[6] Corradini ， A. 和 F. Gadducci ， An algebraic presentation of term graphs ， via gs-monoidalcategories，Applied Categorical Structures7（1999），pp. 299-331[7] Corradini，A.和F.Gadducci，重写循环结构：Equivalenceetwentheoperationalandtheecategoricaldescription，InformatiqueTh′eoriqueetApplications/Theoretical Informatics and Applications 33（1999），pp. 467-493.[8] Corradini，A.，R. Heckel和U. Montanari，图形操作语义学，在：A. Corradini和R. Heckel，editors ， GraphTransformationsandVisualModeling Techniques ， ProceedingsinInformatics8（2000），pp. 411-418[9] Corra d ini ，A. 、乌桕属 U.我 不知 道 ， F.Rossi ， H.Ehrig 、R.他 叫 M. Lüwe，Algebraicapproaches to graph transformation I ： Basic concepts and double pushoutapproach，in：G. Rozenberg，editor，Handbook of Graph Grammars and Computing by GraphTransformation，I：Foundations，World Scienti fic，1997，pp.163-246。[10] Corradini，A.和F. Rossi，Hyperedge replacement jungle rewriting for term rewriting systemsand logic programming，Theor.比较科学109（1993），pp. 7-48[11] Ehrig，H.，A. Habel，H. J. Kreowski和F. Parisi-Presicce，高级替换系统中的并行性和并发性，计算机科学中的数学结构1（1991），pp. 361-404.[12] Ehrig，H.，A. Habel，J. Padberg和U. Prange，胶粘剂高级替代类别和系统，在：G。Engels和F.Parisi-Presicce，editors，Graph Transformation，Lect. Notes in Comp. Sci. （2004年）。[13] 好的，好的。和B。König，DerivvingbisimimulationgruencesintheDPOapproachtographrewriting，in：I.Walukiewicz，编辑，软件科学和计算结构的基础，Comp.Sci.Lect.Notes。2987（2004），pp. 151-166。[14] Gadducci，F.，项图重写和π-演算，在：A。Ohori，编辑，Programming Languages andSemantics，Lect. Notes in Comp. Sci. 2895（2003），pp. 37比54[15] Gadducci ， F. 和 R. Heckel ， An inductive view of graph transformation ， in ： F. Parisi-Presicce，编辑，《代数发展技术的最新趋势》，Comp. Sci. Lect. Notes。1376（1998），pp.219-233[16] Gadducci ， F. 、 R.他 叫 M. 在 这 种 情 况 下 ， Bi-Categoricalaxiom ationofconcurren tgrarewriting，in：M. H ofma nn，D. 帕弗罗维奇和G。土壤学，编辑，计算机科学，电。笔记在TheorComp. Sci. 29（1999）。[17] Habel，A. ，J. Müller和D. 加油，DoubLe-普寿T格拉普赫为我准备的Revisited，Mathematical Structures in Computer Science 11（2001），pp. 637-688.[18] HoMushmann，B.和D.Plump ， 通 过 丛 林 评 估 实 现 术 语 重 写 ，InformatiqueTh′eoriqueetApplications/TheoreticalInformaticsanddApplications25 （1991 ），pp. 445-472[19] Lack，S. 和P. 我的孩子们都很好，而且他们都很聪明。王文，软件科学与计算结构的基础，计算机科学学报，2000年第1期。2987（2004），pp. 273-288.56A. Corradini，F.Gadducci/Electronic Notes in Theoretical Computer Science 127（2005）43[20] Laneve，C.，J. Parrow和B.Victor，Solo diagrams，in：N.Kobayashi和B.皮尔斯，编辑们，计算机科学的理论方面，计算机科学讲义。第2215（2001）号来文，第2215（2001）页。第127-144页。[21] 雷法 J. 和 R. 米尔纳， 导出 互模拟 同余 为 反应性 系统，在：C. Palamidessi，编辑，Concurrency Theory，Lect. Notes in Comp. Sci. 1877（2000），pp.243- 258[22] 米尔纳河，多元π演算：教程，在：F. Bauer，W. Brauer和H. Schwichtenberg，editors，Logicand Algebra of Specification，Nato ASI Series F94，Springer，1993 pp.203-246[23] Plump，D.，项图重写，在：H。Ehrig，G.恩格斯，H. J. Kreowski和G. Rozenberg，editors，Handbook of Graph Grammars and Computing by Graph Transformation，II：Applications，Languages and Tools，World Scienti fic，1999，pp. 3-61[24] 很 好 ， 小 维 。和 P.Sobocin′ski ， Congruencesforcor ontextualgraphh-rewriting ，TechnicalReportRS-04-11，BRICS ，Department of Computer Science， University of Aarhus（2004）.[25] Sewell，P.，从重写规则到互模拟同余，Theor。 比较科学 274（2004），pp. 183-230[26] Sobocin'ski，P. ，“从可执行系统中确定业务组“，P h. D. thesis，BRICS，Department ofComputer Science，University of Aaurhus（2004）.