术语图重写：基于图的函数表达式计算模型

P网址：http://www.elsevier.nl/locate/entcs/volume51.html13页术语图重写精要计算机科学系，约克大学Heslington，约克YO105DD，英国det@cs.york.ac.uk摘要项图重写是一种使用表示函数表达式的图进行计算的模型。图允许共享公共子表达式，这提高了空间和时间上的常规项重写的效率。本文从可靠性、完全性、终止性和连续性等方面综述了术语图重写的要点。1引言术语图重写是关于将函数表达式表示为图，并通过基于规则的图转换对其求值。使用图的动机是为了提高传统的基于字符串或树的项重写的效率例如，考虑以下术语重写规则，定义自然数上的阶乘函数（其中s表示后继函数）：事实（0）（0）fact（s（x））！ s（x）fact（x）评估术语1 fact（sn（0））通过这两个规则产生sn（0）（ sn1（0）（： s2（0）（ s（0） s（0））：））;n+22其是包含i=2i =（n +5n +4）=2个函数符号的项因此该评估所需的空间是输入项大小的二次方。的非线性行为是由第二规则引起的，该规则复制了与变量x匹配的子项。一般来说，每个项重写规则在其右侧比在其左侧更频繁地包含一些变量，可以增加项的大小，增加的量是非恒定的。在实现中，这个问题通常通过创建指向子项的多个指针而不是复制它来克服。1 这里sn（0）代表s（s（：s（0）：）），s不同时出现。c 2002年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。2这意味着从术语重写的计算模型转移到术语图重写的计算模型。例如，图1显示了使用上述规则重写项图对事实（sn（0））的评估该评估仅需要空间2n +3，因此在输入项的大小上是线性的2事实S个）s事实s个）Ss事实sSS）：）s.....s s s ss s s s s0 0 0 0 0图1.一、通过项图重写来评估事实（sn（0））使用术语图重写而不是术语重写|或者，如果你愿意，|其影响超出了提高效率。共享公共子项防止某些项重写序列，即那些相等的子项被不同地重写的序列。因此，先验地，项图重写在什么意义上（如果有的话）是项重写的合理且完整的实现是不清楚的。出于同样的原因，还不清楚重写系统的相关属性，特别是终止性和连续性，在两种计算模型之间切换时是否被保留下面的部分回顾术语图重写的要点，即。关于项重写的可靠性，等式证明的完备性，以及关于终止和连续的项重写的关系。该报告以调查为导向[15]。2项图重写设和X分别是函数符号和变量的不相交集合，其中每个函数符号f都有一个自然数arity（f）0，变量的arity为0。元数为0的函数符号称为常数。X上的超图是由两个结点集VG和EG组成的系统G = hVG;EG; labG;attG i2 还要注意的是，在这个例子中，项重写和项图重写都需要n+1个规则应用程序来达到结果，但是单个项重写步骤（在项的给定位置处）需要多于恒定的时间，因为它们必须复制非恒定大小的子项。3GH实验室G：EG ！[X]，以及附加函数attG：EG ！V而作为─将一串节点标记为超边e，使得attG（e）的长度为1 + arity（labG（e））。从现在起，超图和超边被简称为图和边。给定一个图G和一条边e，其中attG（e）= v v1：vn，节点v是e的结果节点，而v1;：; vn是参数节点。 结果节点v由res（e）表示。对于每个节点v，G[v]是由从v可达的所有节点和将这些节点作为结果节点的所有边组成的子图。定义2.1（项图）图G是项图，如果(1) 存在节点根G，每个节点从该节点根G可到达，(2) G是无环的，并且(3) 每个节点是唯一边的结果节点。图2示出了具有二元函数符号f、g和h以及常数a的三个项图。边被描述为带有内接标签的框，项目符号表示节点。一条线连接每条边及其结果节点，而箭头指向参数节点。参数字符串中的顺序由离开框的箭头从左到右的顺序给出。术语图的这种图形格式与引言中使用的更紧凑的格式是双射对应的在续集中，两个版本都将使用。一个在X上的项是一个变量、一个常数或一个字符串f（t1;：; tn），其中f是一个元素n 1的函数符号，t1;：; tn是项。定义2.2（术语表示）设v是术语图G中的节点，e是结果节点v的唯一边，并且attG（e）= vv1：vn。然后termG(v)为如果n = 0，： labG（e）（termG（v1）; ：;termG（vn））否则是由v表示的项。令项（G）是项G（根G）的缩写。图态射f：G！两个图G和H之间的H由两个函数fV组成：VG！ VH和FE：EG！这是一个很好的例子，到节点，即，labf= lab和attf=fHEGHEVG映射字符串v ：：vn至fV（v1）：：fV（vn））.态射f是单射的（满射）如果fV和fE是。 如果f是内射和满射，则它是一个同构在这种情况下，G和H是同构的，记为G= H。为了技术上的方便，同构项图在本文中将被认为是相等的。（这个惯例在[15]中正式成立定义2.3（坍缩）给定两个项图G和H，如果存在图态射G，则G坍缩为H！把根G映射到根H。这表示为G H，或者，如果态射是非内射的，则表示为G H。后一种崩溃被认为是正确的。一个项图G是完全折叠的，如果没有H与G H，而G是一棵树，如果没有H与H G。V14不RFH H一GGFGH一FG gH一一图2显示了两个折叠步骤，其中中间的图完全折叠。对于每个项图G ，存在树 MG 和完全折叠项图 OG ，使得项（G ）=项（ MG ）= 项（OG），其中MG和OG在同构下是唯一的 [12]。图二. 两个折叠步骤一个术语重写规则l！r由两个项l和r在和X上组成，使得l不是变量，r中的所有变量也出现在l中。术语重写规则的集合R是术语重写系统。假设读者熟悉术语重写的基本概念（参见[2]）。在下文中，R表示任意的项重写系统。与R相关联的术语重写关系表示为y！，它的n重组成由y！n，它的过渡性关闭，由！+，它的自反传递闭包由！，以及它的自反对称传递闭包。给定一项t，用t表示一个项图，它表示t，使得（1）每个入度大于1的节点v满足项t（v）2 X，（2）对于t中的每个变量x，都有一个唯一的节点v，其项t（v）= x。因此，t是从Mt通过合并标记为相等变量的边获得的在移除所有用变量标记的边之后，由t产生的图表示为t.一个项图G是t的一个实例，如果存在图态射！把根t发送给根G。定义2.4（项图重写）设G和H是项图，l！r是R中重写规则，v是G 中的节点，使得G[v]是l的实例。然后，存在预重写 步 骤G）v;l！R 如果H是由G通过以下构造得到的：(1) 移除结果节点为v的唯一边，得到图G1.(2) 从不交并G1+构造一个图G2，将v与根r合并，以及合并u与u0的图像，对于l中的所有n个u和r中的u0，项l（u）=termr（u0）2×。(3) 从G2中移除所有从根G（\garbage collection”）无法到达的节点和边，产生H =G2 [根G]。5vn这样的重写步骤也由G）H或仅G）H表示，并且G）H是G）H的reexi ve-transiti ve闭包。步骤（1）和（2）的组合效果也可以通过所谓的图变换的双推出方法中的规则来指定。通过将术语重写规则转化为合适的图转换规则，得到了一个无需垃圾收集的术语图重写模型，称为丛林评估[5，6]。详细信息可以在[12]中找到，其中术语图重写是通过使用垃圾收集扩展丛林评估来定义的。文[3]中提出了一种通过图重写对项重写进行建模的技术上有些不同的方法，并创造了“项图重写”这一名称该论文中重写步骤的定义涉及边的重定向和垃圾收集，并且在其效果（在非循环图上）等同于定义2.4。3可靠性和完备性事实证明，术语图重写相对于每个步骤G）v;l中的术语重写是合理的！rH对应于一系列应用程序|或并行应用程序|规则l！ r对应于子项G（v）在项（G）中的出现。定理3.1（合理性[7]）对于所有的项图G和H，G）H包含项（G）！术语（H）v其中n是从根G到v的路径数。这一结果也解释了使用术语图重写而不是术语重写时重写步骤数量的潜在加速。此外，紧接着，对于术语图重写步骤的每个序列，存在相等或更大长度的对应术语重写序列。因此，如果项或项图的最坏情况时间复杂度近似于从它开始的重写序列的最大长度3，则项图重写的最坏情况时间行为永远不会比项重写的最坏情况时间行为差。类似地，在最坏情况下项图重写所需的空间不能超过项重写所需的空间。这是因为重写序列的图最多与它们表示的项一样大，其出现在相应的项重写序列中。在考虑了术语图重写的合理性之后，一个自然的问题是它是否也是完整的。答案取决于我们所寻求的完整性的形式。如果完整性被认为是一种能力，3 这个度量是一个近似值，因为它忽略了在项和图形中确定可以应用规则的位置所需的时间，以及在规则的右侧包含重复变量的项重写步骤所需的额外时间6EQ模拟每个项重写序列，然后根据规则f（ x ）！g（ x; x ）aB和重写序列f（a）！g（a; a）！g（a;b）.从树Mf（a）出发，由于rst规则引入的共享，不可能通过项图重写达到Mg（a;b从Mf（a）可导出的图只有Og（a; a），Og（b; b）和Mf（b）. 为了克服这个问题，可以将复制步骤添加到重写关系中，其中复制是折叠的逆关系（关于复制项图重写的一些结果见[1]。）然而，复制与术语图重写以通过共享提高效率的思想相冲突。下面使用的方法是向重写关系添加适当的折叠步骤，这将使项图重写对于等式推理是完整的。术语图重写的完整性的第二个障碍是在其左侧具有重复变量的术语重写规则例如，规则eq（x; x）！ true不能应用于树Meq（0;0），因为没有图态射eq（x，x）！ Meq（0; 0）（见图3）。因此，Meq（0; 0）不能被）约化，尽管项eq（0; 0）是可约化的。图3表明，这个问题可以通过折叠来解决：合并标记为0的两条边使重写规则适用。）图三. 折叠以启用规则应用程序定义3.2项图上的关系定义为：）=）[：Coll因此，重写的方式是以任意的顺序重写和折叠。事实证明，这种关系是完整的一个中心应用的长期重写，即方程推理。把R的规则看成方程l00EQ0EQ真7r，R的方程理论就是所有方程t u的集合8Coll1212这样，t$ u。由伯克霍定理的方程理论符合一套方程是有效的所有模型的R（即在所有代数满足方程的R）。细节可以在[2]中找到定理3.3（完备性[11]）对所有项图G和H，term（G）$term（H）当且仅当G，H.Coll在这里，是的自反对称传递闭包）Coll. 因此，方程t u在R的模型中有效，当且仅当存在一系列步骤， 以及它在表示t和u的两个项图之间的逆。换句话说，项图的折叠重写对于证明方程的有效性是完全的，就例如，再次考虑系统R = ff（x）！（x;x）; a！bg。f（a）g（a; b）的有效性的证明如下：Mf（ a）CollOg（ a;a））Coll（b）（Coll（2）A（CollMg（ a; b）：注意，没有折叠的项图重写缺乏定理3.3的完整性，因为很明显，在上面的例子中，Mf（a）6，Mg（a;bR的方程理论是可判定的，如果存在一个过程，决定任意项t和u是否为t$u。存在方程理论不可判定的项重写系统[2]。定理3.3给出了一个条件为col是一致的情况下的判定过程，改进了经典的基于项重写的判定过程.调用二元关系！在给定的集合上终止，如果没有在nite序列a1！一个2！：：，然后，如果对于每个星座a a！ 一有一个元素b这一个！ b a .如果！既终止又同现，那么它是收敛的。推论3.4如果集合是一致的，则nite项重写系统的方程理论是可判定的.For，if）Coll则对所有项图G1和g2关于G1CollG 2 存在一个项图H使得G1CollCollG2. 一个代表输入项t和u由项图表示，比如Ot和Ou，并通过）coll到不可约图。 后者是可能的，因为）coll正在终止。 现在定理3.3意味着t $u当且仅当所得的不可约图相等。这个过程通常比基于项重写的相应过程更有效。此外，它是更广泛的适用性，因为类收敛项重写系统是适当地包括在类的系统，其中h）coll是connvnt。 后者将在接下来的两节中详细介绍。、）H（94终止从定理3.1（可靠性）和不存在适当的崩溃步骤的无限链（因为这些步骤减小了图的大小）的事实可以得出，无论何时项重写，项图重写都是终止的。定理4.1如果！ 是终止的，那么）coll是终止的，因为我们ll。因此，为证明项重写的终止而开发的综合机制（例如参见[2，4]）适用于项图重写。但是下面的例子证明了术语图重写在严格意义上比术语重写更多的情况下终止用两条规则重写术语f（a;b;x）！ f（x;x;x）a！ B不会终止，因为存在夜间重写序列f（a;b;a）！ f（a;a;a）！ f（a;b;a）！* *为了证明coll是终止的，考虑下列从项图到自然数的函数：对于任意项图G，de ne（G）= m + n + p，其中m是G中前两个角点不同的f-标号边的个数，n是G中a-标号边的个数，p是G中n个角点的个数. 人们很容易认为，G列H意味着（G）>（H），所以不可能有列步骤的不间断序列。项图重写的更好的终止行为提出了一个问题，即是否有一般的证明方法覆盖系统，如上面的一个是终止项图重写下，但不是项重写。这样的方法是项图上的递归路径顺序[14]，其将用于项重写系统的众所周知的递归路径顺序[4]推广到项图设置。由于篇幅有限，这里不讨论递归路径顺序。另一种可以覆盖非终止项重写系统的终止证明技术是终止系统的组合。Toyama[16]观察到，两个终止项重写系统的并集可能不会终止，即使系统具有不相交的函数符号集。他举了以下例子：R0nf（0;1;x）！f（x;x;x）g（x; y）！XR1：g（x; y）！ y这并不是要证明这两个系统都在终结，而是它们的结合。10GFGGFGFF在nite rewrite序列中承认以下内容：2f（g（0;1）;g（0;1）;g（0;1））！f（0;1;g（0;1））！f（g（0;1）;g（0;1）;g（0;1））！**相反，即使两个系统具有某些共同的功能符号，它们的联合也会保留colll的终止。 称两个项重写系统R 0和R 1是不相交的，如果Ri中规则的左手边的函数符号不出现在R 1 i中规则的右手边，其中i=0;1。 对于下面的定理， 也 可以用 （y）R表示（y）R与项重写系统R的关系。定理4.2（[10]）设R0[R1]是两个不相交项重写系统的并. 然后）R0[R1 是终止的当且仅当）R0 和）R1是终止的。再次考虑Toyama的示例，模拟上面所示的循环重写序列的尝试产生图4的终止重写序列。2）0 1 0 1 0 1F00 1g）0 1 0 11见图4。 两个终止重写序列定理4.2的一个推广在[9]中给出，它允许在R0和R1中有更常见的函数符号.5Conuence项图重写和项重写关于并发的关系正好与项重写关于终止的关系相反：并发项重写系统的类适当地包括项图重写在其上是并发的系统的类。下面的定理有一个直接的缺点，就是利用了（定理3.3）的完备性。定理5.1（[11]）若）coll是con uent，则！ 就像我们知道的那样。11G这个结果的逆被[11]中的一个反例所反驳：f（x）！ g（x; x）aBg（a; b）！ Cg（b; b）！ f（a）对项使用结构归纳法可以证明，每一项都可化为唯一的不可约项，因此项重写是连续的。但是图5表明）是不conuent，which显然为）coll一样好。这 里 的问题是由规则f（x）创建的共享！ g（x; x）防止重写步骤g（a; a）！g（a; b），这是将g（a; a）降为c所必需的。GFc（））（=ab b babFB图五. 项图重写尽管在一个并发项重写系统上的项图重写不需要是并发的，但没有一个图将减少到一个以上的不可约图。给定一个二元关系！在某些集合上，如果不存在带a的b，则称元素a为范式！B.关系！有唯一的范式，如果对所有范式a和b，a$ b意味着a = b。定理5.2（[12]）r）coll有唯一正规形当且仅当！有独特的范式。二元关系！在某个集合上是正规化的，如果对于每个元素a，存在正规形式b，使得a!B. 请注意，每个终止关系都是规范化的，但反之则不成立。定理5.2允许下面两个性质的简单证明。推论5.3（1）如果）coll是正规化的，那么）coll是连续的当且仅G一G12当！是一致的。(2) 如果！ 是conve rgent，那么）coll是conve rgentaswe ll。下一个例子反驳了推论5.3（2）的逆，因此收敛项重写系统类被适当地包含在系统13在这个条件下，图重写是收敛的。请考虑以下系统：f（ x ）！g（ x; x ）aBg（a; b）！ f（a）这里每个项都有唯一的范式，因此项重写是必然的。但是，鉴于在夜间重写序列，f （ a ）！ g （ a; a ）！ g （ a; b ）！ f（a）！**相反，通过上面提到的项图上的递归路径顺序，可以证明项图重写是终止的。由此推论5.3（1）。类似于项重写的情况[8]，项图重写的终止允许基于所谓的临界对的分析的一致性的判定过程。详情可参见[12，13]。定理5.4（[12]）有一个算法可以解决以下问题：实例：重写系统R的一个niteterm，使得）coll正在终止。问题：Is）collcon uent？最后，将考虑组合系统上项图重写的一致性和收敛性与项重写的情况相反[1 7]，不相交系统的并集不需要保留集合的一致性。事实上，仅仅通过扩展函数符号的集合就可能失去连贯性[11]。 另一方面，如果两个不相交的系统的左手边不相互重叠，则通过它们的并集来保持收敛。称两项重写系统R 0和R 1为非干扰的，如果R i的左手边与R 1 i的左手边没有重叠，其中i = 0; 1。[2]见《明史》。\overlap”.）如前一节所述，）R表示关系）collovera项重写系统R.定理5.5（[11]）设R0[R1]是两个互不相交且互不干涉的项重写系统的并. 如果）R0（1）R1 a reconvergent，then）R0[R1 就像我们想象的那样。这个结果与项重写的情况形成对比，在项重写的情况下，即使不相交的并集也不需要保持收敛[16]。另见[9]，定理5.5的一个放宽的不相交性的推广。引用14[1] 泽纳M. Ariola，Jan Willem Klop，and Detlef Plump.术语图重写中的双相似性。 信息与计算，156（1/2）：2{24，2000。[2] 弗兰兹·巴德尔和托拜厄斯·尼普科。重写和所有这一切。剑桥大学出版社，1998年。15[3] Henk Barendregt ， Marko van Eekelen ， John Glauert ， RichardKennaway ， Rinus Plasmeijer ， and Ronan Sleep. 项 图 重 写 。 在 Proc.Parallel Architectures and Languages Europe ， Lecture Notes in ComputerScience，第259卷，第141页{158}。Springer-Verlag，1987.[4] 纳彻姆·德肖维茨终止重写。Journal of Symbolic Computation，3：69{116，1987.[5] Annegret Habel，Hans-Jorg Kreowski，Detlef Plump.丛林评估。在Proc.Recent Trends in Data Type Speci cation，Lecture Notes in Computer Science的第332卷，第92页{112}中。Springer-Verlag，1988.[6] 贝托尔德·霍曼和德特勒夫·普朗普。丛林评估有效的长期重写。代数与逻辑程序设计。 Mathematical Research 49，第191页，柏林，1988年。学术出版社也在Springer Lecture Notes in Computer Science 343，191{203，1989。[7] 贝托尔德·霍曼和德特勒夫·普朗普。通过丛林求值实现术语重写。RAIRO理论信息学与应用，25（5）：445{472，1991。[8] Donald E. Knuth和Peter B.班纳特泛代数中的简单字问题。在J. Leech，编辑，抽象代数中的计算问题，第263页{297。北京：人民出版社，1970.[9] 马达拉克里希纳·拉奥术语图重写的模块化方面。理论计算机科学，208（1-2）：59{86，1998.[10] 德特勒夫·普朗普通过图归约实现项重写：组合系统的终止条件和类型重写系统，卷516计算机科学讲义，第307页。Springer-Verlag，1991.[11] 德特勒夫·普朗普折叠树重写：完整性，连续性和模块化。在Proc.Conditional Term Rewriting Systems，Lecture Notes in Computer Science，第656卷，第97页{112}中。Springer-Verlag，1993.[12] 德特勒夫·普朗普用超图改写法计算函数表达式。大学博士论文在不来梅，Fa chbe r eichMathematikundInformatik，1993.[13] 德 特 勒 夫 · 普 朗 普 术 语 图 重 写 中 的 临 界 对 。 在 Proc.MathematicalFoundations of Computer Science 1994，Lecture Notes in Computer Science的第841卷，第556页中。Springer-Verlag，1994.[14] 德特勒夫·普朗普项图重写的简化顺序。在Proc.Mathematical Foundationsof Computer Science 1997，Lecture Notes in Computer Science的第1295卷，第458页中。Springer-Verlag，1997.[15] 德特勒夫·普朗普项图重写。In H. Ehrig，G.恩格斯，H. J. Kreowski和G.Rozenberg ， 编 辑 ， Handbook of Graph Grammars and Computing by GraphTransformation，第2卷，第1章，第3页{61。WorldScienti c，1999.16[16] 富山义人。项重写系统直和终止性的反例。信息 处理信件，25：141{143，1987.[17] 富山义人。关于项重写系统直和的Church-Rosser性质 Journal of theACM，34（1）：128{143，1987.