网址：http://www.elsevier.nl/locate/entcs/volume51.html12页两类高水平置换系统的基本结果？哈特穆特·埃里希1法国信息技术大学地址：D-10587 Berlin，GermanyAngret Habel2法赫贝里奇信息大学在OldenburgPostfach 2503，D-26111 Oldenburg，GermanyF. Parisi-PresicceUniversitdi Roma \La SapienzaDipartimento Scienze dell'InformazioneI-00198 Roma，Italy摘要高级置换系统的一般思想是将图变换系统和图文法的概念从图推广到计算机科学和数学中感兴趣的各种结构。在图变换的代数方法中，这是可能的，通过将图、图态射和图的推出（胶合）替换为适当类别中的对象、态射和推出。特别感兴趣的是各种标记和类型的图，超图，代数speci阳离子和Petri网的类别。在本文中，我们回顾了在对称情形下代数双推出方法中高级置换系统的基本结果，其中两个规则morphism都属于一个特殊类M. 此外，我们首次提出了非对称型的高级置换系统，其中只有左规则态射K！L属于M。？ 欧洲共同体在TMR网络GET-GRATS和ESPRIT工作组APPLIGRAPH下部分支持的研究。1 电子邮件地址：ehrig@cs.tu-berlin.de2 电子邮件地址：habel@informatik.uni-oldenburg.de3 Email：parisi@dsi.unir om a1. Itc 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2LRLRLR1介绍高级替换系统的一般思想是将图替换的概念从图推广到计算机科学和数学中感兴趣的各种结构（更多细节见[3，4，5在本文中，我们回顾的基本概念和主要结果的双推出方法。 这推广了相应的概念和结果在代数理论的图论（见[1，2]），也可以应用到代数speciations和Petri网（见[3，7，11]）。图文法的代数理论在[8]中被重新讨论了非对称规则，其中只有左手边是单射的。本文将这类图文法推广到DPO 0型的高阶元素系统，并给出了适当的DPO0-条件，以便能给出关于Church-Rosser性质和并行性的基本结果.这些基本结果是图论的代数理论的基础（见[1，2]），其中特别研究了抽象语义，并行性和并发性问题。这些更先进的结果中的一部分已经在DPO型中实现（参见[3，4，5]），但是对于DPO 0型研究它们仍然是必要的。2基本概念在本节中，我们回顾高级替换系统（HLR系统）的基本概念，包括产生式、派生式和系统。在下文中，CAT是一个具有一个特殊的态射类M的范畴L r定义2.1（规则和转换）规则p =（LK！右）由三个对象L，K和R组成，分别称为左手边，接口（或粘合对象）和右手边，以及两个态射K！ L和K！R具有态射l2M.l rp给定规则p=（LK！R）一个直接变换G=）H，在范畴CAT中，对象G到对象H的关系由下面的两个推出图（1）和（2）给出：L K Rg（1）c（2）hG C HGh态射L！ G和R！ H称为L在G和R中的出现在H中，分别。L在G中的出现的存在对于p的适用性是不充分的。为了将规则应用于给定对象，必须满足胶合条件（见[2]）。在我们的抽象框架中，如果存在一个对象C，使得给定的对象G成为一个推出对象，则胶合条件满足。3LR事实2.2（规则的适用性）给定规则p =（LK！R），一个G对象G和出现L！G中，则规则p适用于gG通过L！ G如果满足以下两个条件：(i) 有一个宾语C（称为推出补语宾语），C l态射K！ C和C！G，使得定义2.1中的平方（1）是一个外推正方形。h r(ii) 有一个对象H和态射R！H和C！H，这样定义2.1中的正方形（2）是外推正方形。如果这两个条件都满足，则直接变换Gp=）Hcan被建造。当且仅当推出补语结构是唯一的时，它在同构之前是唯一的。给定一个具体的范畴，胶合条件可以构造性地给出，图的胶合条件见[2]，代数的胶合条件见[3]，代数的高级网的胶合条件见[11]。现在，我们能够在任意的范畴中定义新的高级替换系统，从而在双推出方法中推广了图文法的概念。用一个起始对象代替初始图，由一对内射图态射组成的规则集被一组具有区别类M中的态射的定义2.3（高级替换系统）给定范畴CAT和一个特殊的态射类M，在（CAT;M）中有一个DPO0型的高级替换系统H=（S;P 由起始对象CT给出S2jCATj和一组规则P.系统H被称为DPO类型，如果L r对于所有p =（LC！R）2 P，l和r都属于M.例2.4（特殊范畴）（i）若CAT是[1]中考虑的有向图和图态射的范畴Gra，M是内射图态射的范畴，则（Gra，M）中的DPO（resp.DP O0）是文献[1]（resp. [6，9，8]）。(ii) 通过在集合和（全）函数的范畴Set中选择内射函数类M，得到了（Set，M）中的高级替换系统，其中变换后的高级结构是集合。这种情况很有趣，因为图和其他一些高级结构都是基于每个组件中的集合。(iii) 把CAT作为代数规范范畴Spec，使其具有合适的内射规范态射类M，得到了[7]意义下的代数规范文法。(iv) 设CAT是P=T的位/变迁网范畴，[10]，其中，然而，同态f：P ！P生成P1 2函数f P：P 1！P2（见[3]），我们得到了变换系统Petri网4R1 L2==HL1 L2==G所有这些结果都需要独立性。的直观含义(v) 将CAT作为代数高级网的范畴Ahl，得到了[11]意义下的代数高级网变换系统。3独立性和独立主义在这一节中，我们对DPO型和DPO 0型高级置换系统给出了顺序和并行变换独立性的概念，并给出了高级置换系统的两个C hur ch-Rosser定理和并行性定理，这些定理在图论中是众所周知的[6，9，2，8]。然而，对于大多数证明，我们需要额外的条件，分别对于范畴CAT，对于DPO和DPO0类型的系统，我们称之为条件和条件。 这些条件将在第4节中进行模拟 。首先，我们需要顺序和并行的p1 p2两个直接变换G=）H和H=）X的序列独立性通过规则p i =（L iK i！Ri）（i = 1; 2）是H中的R1和L2包含在H中的K1和K2的交集中。换句话说，第一条规则不删除第二条规则所需要的任何内容，第二条规则也不需要第一条规则产生的任何内容。在DPO型的高级置换系统的情况下，这等价于存在合适的态射R 1！C 2和L 2！C1，如以下序列独立性的定义所述（见[1]）。平行独立性的公式是类似的。定义3.1（序列独立性）给定两个直接变换，p1 p2如图所示，G=H和H=XL1 K1 K2 R2GC1p1p2C2X测试变换G=H和H=X是顺序独立。dent如果有态射R1！ C 2和L 2！ C 1，所以R 1！ C2！ H= R 1！ H和L 2！ C1！ H = L 2！H.定义3.2（并行独立性）给定两个直接变换p1 p2G=）H1和G=）H2，如图所示R1 K1 K2 R2H1C1p1p2c2h2型测试变换G=）H1和G=）H2是平行独立，如果有态射L1！ C 2和L 2！ C 1，所以L 1！ C2！ G = L 1！ G5L1在变换G=）H1和G=）H2中，re是对象X，并且是方向R1t变换H1=）X和H2=）X，使得t变换G=）p1+p2L2！ C1！ G = L 2！G.对于下面的局部Church-Rosser定理和并行性定理，我们要求DPO型的高级置换系统满足HLR条件，而DPO0 型的高级置换系统满足第4节所述的HLR条件，并给出了相应的主要思想. 注意，对于DPO0-ty pew ee不需要像[8]中的一些图的情况那样要求垂直态射在M中。定理3.3（局部Church-Rosser I）给定平行独立直p1 p2p2 p1 p1p2p2p1H1=）X和G=）H2=）X是完全独立的。定理3.4（局部Church-Rosser II）给定一个序列独立的变换Gp1=）H1p2=）X存在一个对象H2，且等价于独立变换Gp2=）H2p1=）X，使得变换p1 p2G=H1和G=H2是独立的。如果范畴CAT有二元余积，用+表示，我们就能够用公式表示并行的产生式和变换。定义3.5（平行规则）给定规则p1 =（L1K1！R1）和l2r2l1 +l2r1+r2p2 =（L2K 2！规则p1 + p2 =（L1 +L2K1+K2！ R1 +R2）在CAT中，由二元余积定义的规则称为p1和p2的并行规则。A变换t：G变换。=）由parallel规则定义的X被计算为parallel定理3.6（平行论）如果p1和p2是规则，p1+p2是相应的平行规则，则：(i) 合成：给定一个序列独立变换s：Gp1+p2p1=）H1p2=）X，re是一个pa ra ll e lt变换t：G=）X。(ii) 分析结果：给定一个平行变换t：Gp1+p2=）X，r是两个整数p1p2p2p1独立变换s1：G=）H1=）X和s2：G=）H2=）X。(iii) 双射对应：在顺序独立变换和并行变换之间存在双射对应，即给定一个顺序独立变换s，“综合”构造导致一个并行变换t，而“分析”构造又导致相同的顺序独立变换s（直到同构），反之亦然。604条件和条件在下文中，我们首先回顾的条件，所谓的HLR条件，这是必要的证明的Church-Rosser定理I和II和DPO型高级别更换系统的Cherch-Rosser定理。定义4.1（HLR-条件）给定一个范畴CAT和CAT中的一个不同态射类M，以下条件称为（CAT; M）的HLR-条件：(1) 半M推流的存在。对于所有对象A，B，C和态射CA！B，其中至少有一个在M中，存在推出C！D B：A B（一）C D(2) 存在M回调。对于所有态射B！ D和C！ D都在M中，存在回调C A！B如图（1）所示。(3) M-态射在推出和M-拉回下的继承。(a) 对于每个推出正方形（1），如上所述A！B 2 M意味着C！D 2 M。(b) 对于每个回调正方形（1），如上B！ D 2 M和C！ D 2M意味着A！ B 2 M和A！ C 2 M。(4) M-推出-拉回-分解。对于表单的每个图表：阿、B、E（1）（2）C D F如果（1+2）是推出方，（2）是拉回方，A！CBDE F，B！ E和D！ F是M-态射，则（1）也是推出方。(5) 二元余积的存在性及与M.(a) 对于每一对对象A，B，有一个余积A + B与泛态射A！ A+ B和B！ A + B.F(b) 对于每一对态射A！a0级GB！ b0的在M中，余积态射A + BF+G！a0级+ B0 也在M。7(6) M-推出是拉回。M-态射的推出方是拉回方。请注意，这些HLR条件的变体已经在[4，5]中陈述，以便在高级替换系统的框架中证明局部Church-Rosser定理和Chaelism定理事实上，上述条件意味着8在[4，5]中，它们被称为\HLR1”条件。DPO型在HLR条件下主要结果的证明思想 关于DPO型高级置换系统的定理3.3、3.4和3.6的证明分别见[5]，第380、377和382页。 特别地，局部Church-Rosser定理I和II的证明利用了（1）半M推的存在性，（2）M拉回的存在性，（3）推和M拉回下的M态射的继承，(4) M-推出-拉回-分解。 条件（5）二进制余积和与M的相容性确保了对于每一对（p1; p2）产生式，存在一个平行产生式p1 + p2，它也是2.1意义上的产生式。最后，假设满足DPO条件（1）{（5）}，则双射对应定理中的陈述（i）和（ii）成立，并且假设满足DPO条件（6）M-推出是拉回，则双射对应（iii）成立。如果左态射K！如果规则p的L在M中，且高层规则系统的类型p∈DPO0，则在局部Church-Rosser定理和并行性定理的证明中需要不同的条件，称为HL R 0 -条件.定义4.2（条件）给定一个（高级结构的）CAT和一个在CAT中的态射的区别类M，以下条件是（CAT;M）的一个条件：（1）存在任意的推顶。对于所有对象A，B，C和态射C A！ B存在一个推出C！D B.（2）半M-回撤的存在性。对于所有态射B！D和C！其中至少有一个在M中，存在回调C A！B如图（1）所示。（3 '）推出和拉回下的M-态射的继承。(a) 对于每个推出正方形（1），如上所述A！B 2 M意味着C！D 2 M。（b '）对于每个回调正方形（1），如上所述C！D 2 M意味着A！ B 2 M。（4 '）半M-推出-拉回-分解。对于上面的每个图（1+2），我们有：(a) 如果（1+2）是推出方，（2）是拉回方，B！E和D！ F是M-态射，则（1）也是推出方。(b) 如果（1+2）是推出方，（2）是拉回和推出方，A！CBD和E！ F是M-态射，则（1）也是推出方。(5) 二元余积的存在性及与M.（6 '）半M-推出是回调。9p1+p2在G中出现L1+L2，因为对于序列独立变换，态射的推出平方，其中至少有一个在M中，是拉回平方。对于DP O0型的高阶线性系统，Church-Rosser定理I和II及对偶定理成立，证明了HL R0-条件成立. Church-Rosser定理I和对偶定理的证明分别由文[5]第380页和第382页的证明来完成. F或DPO0型的HLR系统 我们需要一个单独的局部Church-Rosser定理II，它通过对称性从局部Church-Rosser定理I得出DPO型。对具有HL-R-0条件的DP-O-0型的主要结果提出了一些看法. 定理3.3和3.6的证明是通过检查[5]，第380页中的证明来进行的和第382页;定理3.4的证明类似于定理3.3的证明，但需要更强的条件：局部Church-Rosser定理I的证明利用了（1）推出的存在性，（2）M拉回的存在性，（3）推出和M拉回下的M态射的继承性和（4）M推出-拉回分解。局部Church-Rosser定理II的证明与局部Church-Rosser定理I的证明类似，但它要求（1 '）推出的存在性，（2'）半M拉回的存在性，（3 '）推出和拉回下的M态射的条件(5) 二元余积的存在和与M的相容性确保了对于每一对（p1; p2）产生式，有一个平行产生式p1 + p2，它也是2.1意义上的产生式。最后，对偶定理中的命题（i）和（ii）满足DPO0条件（1'）{（4'）和（5），而双射对应（iii）也成立，只要DPO0条件（6 '）的半M-推出是拉包.注意，对于typeDPO0的高级并行系统，步骤m可以通过直接测试产生几个不同的并行变换G=）Xp1 p2在定义3.1中，G=）H=）X可能存在几个态射L2！ C 1，所以L 2！ C1！ H = L 2！ H（参见[8]中的实施例6.9）。F法案4.3（满足以下条件的类别： 给定范畴CAT和CAT中的一个特殊态射类M，（CA T ; M）的HL R0-条件蕴涵了C 0-条件.特别地，对于在例2.4和事实4.8中讨论的下列范畴C A T和态射M的区别类，条件是满足的。M内射表示相应范畴中所有内射态射的类，索引“严格”解释如下（参见[3]第6.3节）：(i) (Gra; M内射），(ii) (Set; M内射），102(iii) （Spec; M严格;内射），(iv) （P=T; M内射），(v) （Ahl; M内射;严格;isom），(vi) (UGra; M内射）。证据在文献[3，4，5，11]中给出了具有HLR-条件的DPO型的证明，其中有些地方使用了稍微不同的符号。证明了对于t ∈ DPO0的范畴（i），（ii）和（iii）其中（iv）和（v）的证明是基于（i），（ii）和（iii）在相应分量中的证明.在本节末尾给出了类别（vi）的证明。在集合和Gra推出、回调和余积的类别中，它和它的构造是众所周知的。这意味着HLR0-条件（1 '），（2 '）和（5a），其中后两个仅在特定情况下需要这些构造内射态射在推出和拉回以及上积下的继承对于Set是众所周知的，并且蕴含条件（3 '）和（5b）。此外，对于集合和内射函数，很容易明确地检查条件（4 '）和（6'）的满足性这反过来又暗示了Gra的相应条件，因为图态射是单射的，图在Gra中是推出或拉回的当且仅当图态射的边和节点分量满足Set中的相应性质情形（iii）的证明是类似的，并且基于这样一个事实，即指定态射由两个满足附加结构约束的集函数（在排序集之间和在算子集之间）组成。更正式地说，一个代数特殊态射f：SP EC 1！代数规范SP EC 1 =（1; E1）和SP EC 2 =（2; E2）之间的SP EC 2是一个签名，物理因子：1个 ！2使得f#（e）2 E对于所有的e2E1，即.例如，的翻译E中的方程在E 它是严格的，如果，此外，（f #）1（E）埃岛例如，1 2 2 1如果SP EC2中的任何方程仅由图像中的运算符号形成，f为1是SP EC 1中已有的方程的平移。对于Set和Gra的情形，已知的推回、拉回和代数物种的余积的构造已经满足了条件（1 '）、（2'）和（5a）。条件（4 '）和（6'）从Set中的相应性质得出，因为它们基于内射性而不是态射的严格性最后，对于（3'a），考虑上面的推出平方（1）如果D包含一个仅由C的算子（的像）构建的方程，通过构造SPEC中的推出，该方程，如果不是C中的（方程的像），则只能是B中的（方程的像），因此仅使用来自B的算子。但是这些算子只有在（算子的映象）最初在A中时才能为B和C所共有。但如果A！B是严格的，B中的任何方程仅用A中的算子（的像）建立，必须已经是A中的（方程的平移），因此是C中的。其余的性质可以用类似的方法证明。11NE我们以另一个结构示例来结束本节，该结构示例产生了一个类型为DPO0的高级虚拟化系统 满足HL R0条件。框架是无向图，其中每个边与一组1或2个节点（其端点）相关联。定义4.4（无向图）无向图（U-图）G是一个三元组（G E; G N;end），其中G E和G N分别是边集和结点集，end：GE！ P2（GN）是将每个边e关联到基数为1或2的GN的子集end（e）的函数。对于有向图，无向图之间的态射必须保持结构不变.定义4.5（U-图态射）给定两个无向图G =（GE;GN;end），和G0 =（G0;G0 end0），一个U-图态射f：G！的g0E N是一个pair（fE：GN！的g0 ;fE：GE！的g0 ），使得end0（fE（e））=fN（end（e））（其中相同的符号用于表示fN到N的子集的明显扩展）。U-图态射的合成是按分量定义的。组合是明确的联想和对（id E：GN！G N; id E：G E！GE）是明显的同一性。事实4.6范畴UGra的对象是无向图，其态射是U-图态射，它在推出和拉回下是闭的。对于无向图，很容易修改原有的胶合条件[2]保证规则的适用性。命题4.7给定p =（L K！R）和g：L！G，设IDg=fx 2 L：9y 2 L; x 6= y; g（x）= g（y）g，DANGg =fn 2 LN：9e 2 GEgE（LE）使得gN（n）2结束G（e）g。则推出补数C存在当且仅当DANGg[ IDgl（K）.单射U-图态射是指两个分量fN和fE都是单射函数的U-图态射。利用与有向图[5]中所用的类似的论证，可以证明，（UGra）产生一个满足λ0-条件的高级代数系统。事实4.8具有特殊态射类M内射的范畴UGra构成了一个DPO 0型的高级表示系统，它满足DPO0-条件。证据任意U-图态射对的推出、回撤和上积的构造都是基于Set中相应的 基 础 集 函 数 的 构 造 ， 因 而 满 足 HLR0- 条 件 的 结 构 性 质 是 由（Set;Minjective）满足HL R0-条件这一事实得出的. 由于U-图态射是完全内射的，12当边和结点分量为时，M态射的继承性（3 '）和相容性（5b）也由Set的相应性质得到.5结论本文讨论了在双推出方法中如何获得高阶线性系统的Church-Rosser和并行性结果，即DPO的短高阶线性系统. 本文首次给出了一类DPO 0的H或HLR-系统的相应结果，其中只有规则的左手边属于一个区别类M。事实上，我们已经提出了适用于DPO 0型的HLR-条件，它比用于DPO0型的HLR-条件稍强。然而，我们所有的例子范畴不仅满足条件，而且还满足条件。 因此，它仍然是一个问题，是否有inter-numerous例子满足的条件，但不满足的条件。引用[1] Corradini，A.， 联合 Mo n tanari，F. Rossi，H. 埃里格河 He ckel和M. L图变换的代数方法第一部分：基本概念和双推出方法，G. Rozenberg，编辑，Handbook of Graph Grammars and Computing by Graph transformation，第1卷：基础，World Scienti c，1997 pp. 163{246.[2] Ehrig，H.，图文法的代数理论导论，在：V。克劳斯，H. Ehrig和G.Rozenberg，编辑，计算机科学讲义73，第一次图形语法研讨会（1979年），pp。1{69.[3] Ehrig，H.，M. Gaublsky和F. Parisi-Presicce，应用于代数规范和Petri网的高级替换系统，在：图文法和图变换计算手册，第3卷：并发性，并行性和分布，World Scienti c，1999 pp. 341{399.[4] Ehrig，H.，A. Habel，H. J. Kreowski和F. Parisi-Presicce，从图文法到高级替换系统，在：计算机科学讲义532，第四届国际图文法及其在计算机科学中的应用研讨会（1991年），pp. 269{291.[5] Ehrig，H.，A. Habel，H. J. Kreowski和F. Parisi-Presicce，高级替换系统中的并行性和并发性，计算机科学中的数学结构1（1991），pp. 361{404.[6] Ehrig，H.H. -J. Kreowski，多维信息结构中的操作，在：计算机科学讲义45，计算机科学的数学基础（1976年），pp。284{293.[7] Ehrig，H.和F. Parisi-Presicce，代数规范文法：模规范与图文法的结合，在：13计算机科学532，第四届国际研讨会上图文法及其应用到计算机科学（1991年），页。292{310.[8] Ha bel，A.， J. 微米的ller和D. 丰满，双推出graphtransformationrevisited，计算机科学中的数学结构11（2001），出现。[9] Kreowski，H. J.，Manipulationen von Graphmanipulationen，Dissertation，Technische Universitat Berlin（1977）.[10] Meseguer，J.和U. Montanari，Petri nets are monoids，Information andComputation88（1990），pp. 105{155.[11] Padberg，J.，H. Ehrig和L. Ribeiro，Algebras High Level NetTransformation Systems，Mathematical Structures in Computer Science5（1995），pp.217{256.
我的内容管理
展开
