网址：http://www.elsevier.nl/locate/entcs/volume51.html12页代数的一个双重推出变换M. Llabr es，F. Rossello1部巴利阿里群岛大学西班牙帕尔马摘要本文是对文献[9 ]中结果的综述，在文献[9]中建立了发展任意签名（型）的部分代数和全代数的DPO变换的基础。 特别地，我们在这里描述了相应代数范畴的胶合条件和唯一性条件，这是保证规则可以应用并且其应用结果是唯一的（直到同构）的必要和充分条件。1引言双推出（DPO）的方法，图转换是在七十年代初，现在已经成为一个完善的重写形式主义。它被用作软件系统的基于规则的形式化规范技术，其中系统的状态由图表示，并且两个状态之间的转换由相应图的DPO变换来建模。虽然DPO方法已经在几个不同的一元和关系结构的categories中得到了发展，但直到我们的工作，还没有任何尝试将这样的代数方法推广到任意类型的部分和全代数。本文综述了文[9]的结果，其中建立了任意型上部分代数和全代数的DPO变换的发展基础。这样的发展将允许一个基于规则的正式规范的软件系统与复杂的代数建模的状态。让我们提到它的至少一个可能的应用：1 这项工作得到DGES的部分支持，拨款PB 96 -0191-C 02 -01和BFM 2000 -1113-C 02-01。M. Llabre es也通过技术得到了欧盟TMR网络GETGRATS的部分支持。柏林大学和比萨大学。电子邮件：merce.llabres@u ib. es，c esc. r os sel lo @ui b. esc 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2我...，，l0动态抽象数据类型（DADT）对具有动态行为的系统建模的兴趣，其中动态操作通过代数之间的变换来建模，导致了DADT概念的发展，其中代数变换和ADT规范的概念，需要以自然的方式进行任意签名，相互作用。指定这些动态操作的一种建议方法是通过属性图转换系统：属性图对DADT的即时结构进行建模，即时结构的转换由属性图转换系统中的规则指定，[6]。但是，尽管属性图转换的单推出（SPO）方法已经很好地建立起来（例如，参见[10]），但到目前为止，只有一种非常限制性的DPO方法在[1]中引入了属性图转换。此外，属性图不能表示递归结构，如对象堆栈或对象引用。为了解释文[9]中的主要结果，我们必须首先简要地回忆一下任意范畴C中变换的DPO方法的基本概念，为了方便起见，我们假定C具有所有的推出。在这次改写中L r形式主义，C中的产生式规则是态射P =（L K！R）在C中，并且它可以通过态射m：L应用于对象D！D如果存在一个图表L Kr Rmgg0J J JDBr0H使得两个正方形都是C中的推出正方形（双推出图）。如果存在这样一个图，则对象H被称为通过应用规则P到m从D导出，对象B被称为该导出的上下文对象。因此，在发展范畴C中的DPO变换之前，必须解决以下三个问题。应用问题：什么时候给定的产生式规则可以通过给定的态射应用？如果C有所有的推出，解决这个应用问题相当于确定经典上所谓的胶合条件：两个态射l：K上的一个必要和充分条件！L和M：L！D在C中，因为它们的推出补数的存在，即，对象B和两个态射g：K！ B和10：B！ D满足D与m和l0一起是l和g在C中的逆.唯一性问题：哪些产生式规则是这样的，当它们通过给定的态射应用于一个对象时，所有派生对象都是同构的？ 由于推出在同构上是唯一的，所以通常通过在C中定义唯一性条件来解决这个问题：关于态射l：K的必要和充分条件！ L的唯一性，直到l的推出补（如果有的话）和每个态射m的同构：L！D.3B描述问题：通过态射将产生式规则应用于对象的结果叫什么为了解决这个问题，我们给出了一个明确的描述终端派生对象的应用程序的规则，通过态射（粗略地说，派生对象是一个epimorphic图像的所有其他派生对象）。注意，如果规则中的左手态射满足唯一性条件，则通过给定态射应用该规则所导出的所有对象将是同构的。本文总结了文[9]中在任意签名（型）的部分代数范畴Alg（同态为态射）和范畴Alg（-总- 代数（部分-代数，使得其中的所有运算都属于对于一组固定的运算符号是全的;我们一般称它们为部分全代数），同态是态射。 如果中所有运算符号的集合 ，然后是Alg;是通常的总类别TAlg- 代数由于本文是对[9]的综述，这里只回顾其中最相关的结果，我们建议读者参阅上述文献。前引书给出了部分代数的所有定义和基本概念，以及这些概念和结果的例子和证明。本文所回顾的一些结果已包括在[8]和[3]中。2Alg中的推出补数在这一节中，我们提出了解决方案的应用程序和唯一性问题的算法。首先，我们回忆一下这个范畴中的推出结构（+）表示从一个签名中去掉所有零元运算得到的签名，对于每个部分-代数A，我们用A（+）表示它的（+）-约简.2.1Alg的推出式施工命题2.1设f：K！ A和G：K！ B是的两个同态局部代数LetA（+）+B（+）=（AtB;（'A（+）+B（+））'2（+） ）be the partial带载体的（+）-代数以A和B的不交并2为集，其运算定义如下：对每一个2（+），A（+）+B（+）=AtBdom'A（+）+B（+） =dom'Atdom'B 如果2dom'A （具体而言，2dom'B），则'A（+）+B（+）（a）='A（a）（具体地，'A（+）+B（+）（b）='B（b））。设（f; g）是A（+）+B（+）上包含以下关系的最小同余E（f;g）=f（f（x）;g（x））j×2Kg [f（'A;'B） j'2（0）;'A;'B定义g：0 000 0设nallyD是其（+）-约简是商的偏代数2 形式上，A和B的不交并AtB被定义为Af1g[Bf2g，但为了简化符号，我们将A和B与它们在A t B中的图像等同起来。一40000（A（+）+B（+））=（f; g），其空值运算定义如下：每'0第2条（0）款，“D”当且仅当A或B a rede n ed，其中case'Disits（ortheir）等价于类模（f;g）。则D，to与同态g0 A！D和F0 B！D由商映射A t B的A和B的限制给出！（AtB）=（f; g），是f和g在Alg中的推出。2.2Alg中的胶合条件和唯一性条件作为上面解释的推出构造的推论，我们得到了闭同态和内射同态的以下继承性质。推论2.2Let（D;g0：A！ D; f0：B！ D）e是f：K的推出！ A和G：K！B在Alg。如果f是闭内射的，g是内射的，则f 是一个简单的d和内射，g0 是注射性的。因为在范畴Alg中，对（E ; M），其中E是所有满同态的类，M是所有闭的和内射的同态的类，是一个因子分解系统，所以每对同态f：K！A和M：A！在Alg中具有推出补码的D具有一个推出补码（B0; g：K！ B0; d：B0，！ D）suchthatd：B，！ D是闭子代数的边，我们称它为自然的。由于这样一个自然的推出补完全由代数B 0确定，为了简化符号，我们通常将在续集中将它与这个代数等同起来。定理2.3设f：K！A和M：A！D是偏序代数R的两个同态。 设B0=CD（（Dm（A））[mf（K）），d：B0，！ D是相应的闭嵌入，令g：K！ B 0是m∈f与目标代数B 0的合成.如果f和m在Alg中有推出补数，则（B0; g：K！ B0; d：B0，！D）是它们唯一的自然推出补数，并且它在以下意义上是终结符：如果（C;m0 K！C; f0 C！ D）是它们的另一个推出补，则存在唯一的同态h：C！B0，它是在满射上，使得h∈m0=g和d∈h=f0。事实上，F：K！A和M：A！ D在Alg中有一个推出补当且仅当B 0是它们的自然推出补可以转化为具有推出补的同态对f和m的集合论特征，从而产生Alg中的粘合条件（见下一个推论）。但是，与一元情况相反，我们对这种粘合条件没有推论2.4设f：K！A和M：A！D是偏序代数R的两个同态。设B0=CA（（Dm（A））[mf（K）），并设#（f;m）为5一00A（+）+B（+）上包含关系的f（f（k）;mf（k））jk2Kg [f（'A;m（'A）） j'2（0）;'Ade ned g：0 000然后，f和m在Alg中有推出补当且仅当它们满足以下性质（在Alg中统称为胶合条件）：GC 1）若a;a02A使得m（a）=m（a0）62B0，则（a;a0）2#（f;m）. GC2）若m（a）2 B 0，则（a; m（a））2 #（f; m）.GC3）F或每个'2，如果d2dom'D D62B！（'）则d = m（a），两个多姆拉。就唯一性条件而言，根据定理2.3，由于（E; M）是Alg中的一个因子分解系统，这个条件是同态f：K的一个充要条件！A保证了在Alg中任何顶同态为f的推出方中，底同态是闭的和单射的。特别地，唯一性条件必须包括闭性和内射性。但是，与一元偏代数的情形相反，这里的闭性和内射性是不够的，还需要下面的附加条件定义2.5偏代数A的子代数C满足最小同余扩张性质（简称mce性质），当对于C上的每一个同余，如果是A上包含的最小同余，则：（一） \（CC）=.ii) 如果（a; ：; a）2dom'A和（a; c）; ：;（a; c）2，1n1 1n nc1; ：; cn2C，则存在 c0; ：; c0 2C满足（a1;c0）; ： ;（an;c0）1n1n2和（c0; ：;c0）2dom′C.1N同态f：K！当A是闭的内射的，且A在f（K）上支撑的闭子代数满足mce性质时，A是mce同态.换句话说，A的子代数C满足mce性质当且仅当对于C上的每一个同余，商集C=嵌入到A =的闭子集。 当是一元签名时，每个闭子代数都满足mce-性质。定理2.6设f：K！A是部分代数的同态.a) 如果f：K！A是mce-同态，m：A！D是部分-代数的同态，使得它们在Alg中有一个推出补，则它在K和D上同构是唯一的，自然推出补由D在（Dm（A））[mf（K））上支撑的闭子代数给出.b) 如果对具有源代数A的部分代数的每个同态m，使得f和m在Alg中有一个推出补，6互补是唯一的同构，那么f：K！A是一个mce-同态。3Alg中的推出补语;3.1- 共计- 代数在这一节中，我们引入-全-代数范畴Alg ;， 部分代数的自由完备化和自由核是解决这类应用问题的两个让=（S; ;）是任意签名，并让是一个非-操作符号的空集合 . 我们将表示为副签名=（S;; （j） ，并给予任何 - 代数A，我们将始终表示其减少A。A-代 数 A 称 为 e- 全 的， 当'A 对每 个'2 是 全 的， 即 ，当它的 -reduceA是全的时候。Alg的全子范畴，对象为all- 全-代数用Alg表示。特别地，当所有运算符号的集合在中时，则全代数恰好是全代数。- 代数，因此Alg; = TAlg。 此外，在下面的例子中，我们展示了如何将属性超图理解为特殊类型的全代数的一种特殊情况。例3.1设0=（S0;0;0）和1=（S1;1;1）是两个签名，其中S0\ S1 =0\1= ;.设=（S;;）是具有S = S0[ S1，为0[1[A，其中A\（0[1）=;，并且：！SS使得j0 =0，j1 =1，（）2 S0S1为每凌晨21-全代数则是由0-代数组成的结构，其元素可以在全1-代数中具有属性（由对应于A中的运算符号的可能部分属性映射给出）。另一方面，一个（1[A]）-全-代数将是一个类似的结构，除了属性映射必须是全的。这将是两种不同类型的可以称为1-属性0-代数的代数，推广了属性超图的概念（参见。[10]）。当然，通过修改集合我们还可以在0为总计，以及1、可能是局部的。对于任何对（;），全全-全-代数类是[2，x6.1]意义下的E-簇，即，它是某个存在方程组的所有模型的类：这些存在方程是那些强制要求中的特别地，它在闭子代数和同态像下是闭的。部分代数A的一个自由补是满射`A：A！A，具有A-全，满足以下普适性质：对每个同态f：A！B与B-全，存在且仅存在一个同态f：A！ Bsuch chthatf∈`A=f. 由于这种7不'2一Im一'2DI1泛性质，如果f：A！B是部分代数的一个且仅有一个同态 全代数f：A！Bsuch的f`A =`Bf.这种单向性也意味着，部分-代数A的-完备化在A上总是同构的。部分代数A=（A;（'A））的自由完备化可以如下得到.设T（A）为自由- 由A生成的带载波的S-集T (A)在A中有变量的项。 让一个=（T （A）;（'A）'2 ）是总数- 代数，使得对于每个'2和每2 T（A）！（'），'A（t）=：'A（t）if2dom'A'T（A）（t）否则设A=CA（A），设A是A的闭子代数 在A.A的-约化A是A的相对子代数，嵌入A，！ A是A的自由完备化.设A是其-约简为A的部分-代数，其中每个运算'A与'2被定义为等于相应的运算'A.当我们说一个全代数B是一个部分代数A的自由完备化时，我们的意思是A是B的一个相对子代数，而它的边是A，！ B是一个自由完备化.设nwA是一个带有载体A=（As）s2S的偏代数. 让+be关系的传递闭包A在Ss2SASDENEDBYA0 一 一个等离子体a='A（a ; ：;a0; ：;ai对于某个操作符号“2”和某个元组，（ai1; ：;a0; ：; a）2dom‘A. 对于每一个XA，让初始部分由X生成的集合存在某个x2X满足a+ xg：X是A的初始部分当且仅当偏代数D=（D;（'D））的-f-紧性c（D）是初始段#DK0（D），其中K0（D）=（DS'2'（dom'D））[（S'2' （dom'D））[fd2Dj存在';2; b2dom'D; c2domD其中D（b）=d=D（c）且（6=或fd 2D j d+ dg：不BM而A A！A和B B！B是自由完备，则存在DD86= c）g[我们有下面的重新制定[2，Th。5.3.7，Prop. 5.5.2]。9引理3.2设A是一个全代数，B是它的相对子代数，则A是B的自由完备化当且仅当B是A的包含K（A）的初始段并生成A。3.2Alg中的胶合条件和唯一性条件;在这一节中，我们解决了Alg中的应用和唯一性问题。首先，我们回想一下Alg;中的pushout结构。命题3.3设f：K！ A和G：K！ B是两个同态对于-全-代数ras，设（H;g~A！H; f ~：B！H）是f的推出在Alg中有g，让HH！ H是H.然后（H;`Hg~：A！ H;`Hf~：B！ H）是Alg中f和g的推出。由于我们已经给出了Alg和自由完备化中推出的显式描述，所以这个结果提供了Alg中推出的显式描述。此外，作为前一命题的结果，我们有以下结果。命题3.4全代数f：K的两个同态！A和M：A！D在Alg中有推出补，当且仅当存在D0的相对子代数 且D是D0的自由完备集且f：K！ A和M：A！D0有一个推出完成在Alg。如果D0是D的这样一个相对子代数a，如果B0是f：K的自然推出补！ A和M：A！D0在Alg中，若B=CD（B0），则B是f：K的自然推出补！ A和M：A！D在Alg中;下面的结果是这个命题和定理2.3的一个推论。命题3.5设f：K！ A和M：A！ D是的两个同态在Alg中有一个推出补的-全-代数。然后，它们在Alg中有一个且只有一个自然推出补，并且这在定理2.3的意义上是终结 的。现在，下面的结果是我们的胶合条件的基础。定理3.6设f：K！ A和M：A！ D是全同态--------------------algebras，D0=K（D）[#Dm（A），且 D0=CD （D0）。然后，f：K！ A和M：A！D在Alg中有一个推出补数，当且仅当a) f：K！ A和M：A！D0 在Alg中具有推出完成;并且b) 如果B0 是 f ： K 的 自 然 推 出 补！ A 和M ：A！ D0 和B0=CD（B0），则B0，！ D0和D0，！ D在Alg ;中有一个推出补数。这个定理中的条件（a）被前一节中给出的Alg中的胶合条件所覆盖。如果D是a 夜间生成总数10;- 代数，或者如果是一个分层签名，则证明D由K（D）生成，并且条件（b）是超连续的。在一般情况下，就条件（b）而言，很容易证明D0是D的初始段，然后我们可以应用下面的结果。在它和在续集中，给定一个-全-代数D和它的两个闭子集B0; D0，使得B0 D0，我们设H（D0; B0）= D0 [fx2 DD0 j每个链条w.r.t. D从一个元素D0B0到x涉及B0 g的某个元素：引理3.7设D是-全-代数，D0是D的闭子集，也是它的初始段，B0是D0的子代数。 设H = H（D0; B0）。a) H是D的初始段。b) B0，！ D0和D0，！ 我在阿尔及利亚有一个推出的完成。c) 如果D0 是D的一个包含D 0的初始段，使得B0，！ D0和D0，！D0 在Alg有一个推出完成，然后D0H。现在，利用这个引理的记号，如果D是H的自由完备化，那么由命题3.4和p（b）我们得到，边界B0，！ D0和D0，！ 在Alg;中有一个推出互补。如果B0，则是相反的！ D0和D0，！在Alg中有一个推出补设D0是D的一个包含D 0的相对子代数，且D是它的自由完备且B0，！ D0和D0，！D0在Alg中有一个推出补，则D0 H，其中h意味着H生成D，因此，根据引理3.2，D是H的自由完备化.这个论证与命题3.4一起，摘自定理3.6在Alg中的以下胶合条件。定理3.8设f：K！ A和M：A！ D是的两个同态-total-algebras. 设置D0 =K（D）[#D m（A）和D0=CD（D0），设m：A！D0 be同态m理解为ta rgetalgebr a D0.然后，f：K！A和M：A！D在Alg中有一个推出补数;森林论坛a) f：K！ A和M：A！D0满足条件2.4中的条件（GC 1）至（GC3）;以及b) 若B0=CD（（D0m（A））[mf（K）），则H（D0;B0）基因表示D。如果f和m满足条件（a）和（b），则D-根的子代数d由B0，！ D0和D0，！Alg中的H（D0;B0）是f：K的自然推出补数！A和M：A！D在Alg中;就唯一性条件而言，命题3.5和与Alg中相同的对（E ; M）也是Alg中的因子分解系统;11我...，r暗示这个条件又是同态f：K上一个充要条件！A保证在Alg中的任何推出方中，顶同态f，底同态是闭的和内射的。命题3.3可以用来证明Alg中的胶合条件; 与Alg中的相同，即，是一个mce同态最后，我们想在这里提到，当=时，这对应于考虑任意的全代数，前面定理形式中的条件（a）和（b）也是TAlg中的粘合条件，它们不能被大大简化。但是，定义2.5中的条件（ii）总是满足的，因此，Alg中的唯一性条件被简化为全代数的通常的同余扩张性质（定义2.5中的条件（i））。4Alg中的DPO转换和Alg;在这一节中，我们在任意类型的部分代数和部分全代数范畴中引入DPO变换。部分代数和部分全代数的DPO变换如何在DADT的精神下用于指定一些过程的例子在[9]中详细解释。定义4.1设P =（ LLK！rR）是代数中的一个生产法则（分别）Alg;）且令m：L！G是部分-代数的同态（分别为. - 全-代数）满足关于L的胶合条件。 设（D; d：D，！ G; G：K！ D）是定理2.3中描述的l和m的自然推出补（分别为定理3.8）：我们称之为规则P通过m应用于G的上下文代数设nallyH，连同同态g0 R！H和R0 D！H是r：K的推出代数！R和G：K！D在命题2.1中描述（分别为提案3.3）。我们称H为终端导出的部分代数（分别为. G的终端导-全-代数）的方法。L KrRmgg0JzJJGdDr0H现在，作为前几节中某些结果的直接结果，我们得到下面的定理。定理4.2在上一个定义的意义下，设H是任意的一部分，- 代数（resp.- 共计（代数），使得存在双推出12我...，，GDAlg中的图表 （分别） Alg;）L KrRmf f0J J J0d0r00 H0设H为终端导出偏导数 - 代数（resp. - 共计 - 代数）通过应用在定义4.1中描述的P到m。a) 存在一个满射e：H0！ H使得e∈f0=g0。b) 如果我：K！L是mce-同态，或者如果l：K！L是闭单射的，m是单射的，那么e：H0！ H是同构。5结论本文总结了文[9]中关于DPO变换在范畴中的应用、唯一性和描述问题（这些问题在发展DPO变换之前必须解决）的主要结果任意类型的部分代数、部分全代数和全代数。 当然，由此得到的部分和全代数的DPO变换推广了（众所周知的）一元部分和全代数的DPO变换。在[9]中有一些进一步的结果至少值得指出。一方面，全代数的DPO变换严格包含了全代数的DPO变换的实现过程，- 代数，然后计算导出代数的-free完备化。另一方面，证明了任意类型的部分代数和全代数的DPO变换完全独立于它们的利用拟同态和闭域拟同态的SPO变换，并且不完全被M所包含. Gro e-Rhode的代数变换系统，[7]，尽管后者具有更大的表达能力。我们在引言中提到，任意类型的部分代数和全代数的DPO变换可以用于具有复杂状态的软件系统的规范，特别是DADT。虽然这里回顾的结果为这种DPO变换的发展奠定了基础，因此至少在理论上为这样的规范打开了大门，但我们的感觉是它们在实践中不会很有用：Alg和TAlg中的应用条件太复杂而难以实现，并且这些类别中的唯一性条件不允许为每个规则找到满足它的等价规则。引用[1] M.贝特霍尔德岛 菲舍尔，M。 科赫 具有部分属性的属性图变换及其在神经网络中的应用“程序。13APPLIGRAPH/GETGRATS图形转换系统研讨会，GRATRA'2000，（柏林，2000），171{178.[2] 伯迈斯特。面向模型论的部分代数方法。Mathematical Research vol. 32，Akademie-Verlag（1986）.[3] P. Burmeister，M. Llabr es，F.罗塞洛部分全代数的推出补计算机科学中的数学结构（Mathematical Structures in Computer Science，2000）[4] P. Burmeister，F. Rossello，J. Torrens，G. Valiente. 一元部分代数的代数变换I：双推出方法《理论计算机科学》184（1997），145{193。[5] H. 埃 里 希 图 文 法 的 代 数 理 论 导 论 “Proceedings 1st Workshop on GraphGrammars and Their Application to Computer Science and Biology ，LectureNotes in Computer Science 73（1979），1{69.[6] H. Ehrig，F.奥雷哈斯Dinamic抽象数据类型：一个非正式的建议。“Bull.EATCS 53（1994），pp. 162{169.[7] M. Gro e{Rhode.基于状态的系统的代数重写系统和元素规范技术报告99-04，柏林工业大学（1999年）。[8] M. Llabr es，F.罗塞洛任意部分代数的推出补“Proceedings 6th InternationalWorkshop on Theory and Application of Graph Transformation TAGT'98 ，Lecture Notes in Computer Science 1764（2000），pp. 131{144.[9] M. Llabr es. 代数的双推出变换。博士论文，Illes Balears大学（2001年）。[10] M. L哦，M。Kor，A. 瓦格纳属性图变换的一个代数框架“在术语图重写：理论与实践，约翰威利父子有限公司（1993年），185{199。
