1网址：http://www.elsevier.nl/locate/entcs/volume70.html20页策略和终止的近似方法AartMiddeldorp1;2筑波大学情报电子学研究所邮编：305-8573摘要Huet和Levy的定理指出，对于正交重写系统（i）每个可约项包含所需的redex，以及（ii）如果所考虑的项具有范式，则所需的redex的重复收缩导致范式，形成了正交重写系统的最佳归一化策略的所有结果的基础然而，所需的赎回一般是不可计算的。在本文中，我们说明，在[6]中介绍的框架的基础上，如何使用近似及其相关的树自动机的结果允许一个简单而优雅的方式获得可判定的条件。我们进一步展示了如何使用相同的思想来改进[18] Arts和Giesl [1]的依赖对方法，以自动证明重写系统的终止性更确切地说，我们展示了近似和树自动机技术如何提供更好的依赖图估计该图确定了为了得出终止结论而必须解决的排序约束。此外，我们提出了一个新的依赖图，不依赖于计算昂贵的树自动机技术的估计。1引言和摘要本文研究一阶项重写的策略和终止问题。 乍一看，这两个主题似乎没有什么共同之处。策略的研究关注的是术语重写系统（简称TRS），它允许使用Nite重写序列，并解决如何以最佳方式计算范式等问题。终止的研究是关于开发方法，可以用来显示没有在nite重写序列。在本文中，我们认为，近似的概念是非常1 日本文部科学省科学研究补助金（C）（2）13224006资助2 电子邮件：ami@is.tsukuba.ac.jp。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。2它有助于（1）刻画可判定的大类TRS，并给出计算范式的最优策略;（2）改进Arts和Giesl的依赖对方法，自动证明TRS的终止性。本文的其余部分组织如下。在第2节中，我们简要介绍了按需呼叫策略。在第3节中，我们对依赖对方法做了同样的事情。第4节介绍了各种近似和树自动机的结果，解释他们的用处。我们在第5节和第6节分别将这些结果应用于按需呼叫策略和自动终止证明的研究第6节还包含对依赖图的新估计，该估计不依赖于第4节的结果。除了后一部分，本文的所有结果都出现在Durand和Middeldorp [6]（策略）和Middeldorp [18]（终止）中。2按需求策略我们假设熟悉术语重写的基础知识（例如[2]）。 我们假设重写规则！ r满足l~2=V和Var（r）Var（l）。如果不施加这些条件，我们认为使用扩展的TRS（eTRS）是有用的。当我们近似TRS或从右向左定向重写规则时，这样的系统自然出现，如第4节所解释的。 请注意，不是TRS的eTRS永远不会终止，但在第6节中，我们将清楚地表明，这样的电子税务登记系统是非常有用的自动证明，终止TRS。在整个论文中，我们假设所有（e）TRS都是晚安。此外，我们只考虑重写基本条件。所以我们假设基项的集合是非空的。这些要求不失一般性。例2.1考虑由重写规则组成的TRSR0+ y！ yb！ f（s（0）; s（0））s（x）+y！ s（x + y）f（x; y）！ x：f（y; x + y）nth（0;y：z）！ ynth（s（x）;y：z）！ n（x; z）计算斐波那契数列的方法项t =nth（s（s（0））;b）允许标准形式s（s（0））：3t！ nth（2; f（1; 1）） nth（2; 1：f（1; 1 + 1））！ nth（1; f（1; 1 + 1））！nth（1;f（1;s（0 + 1）））！nth（1;f（1; 2））！nth（1; 1：f（2; 1 + 2））！nth（0;f（2; 1+ 2））！nth（0;f（2;s（0 + 2）！nth（0;f（2; 3））！nth（0; 2：f（3; 2 + 3））！2但是急切（最内部）策略将产生一个夜间重写序列。3 在重写序列中，我们用n表示sn（0），其中n= 1; 2;3。3如果一个项t有一个范式，那么我们总是可以通过以宽度- rst的方式计算t的约简来计算t的范式，直到我们遇到一个范式。然而，这是一种非常低效的计算范式的方法。在实践中，通过采用适当的策略来选择在每一步中要收缩的赎回来计算范式。如果一个策略成功地计算出所有允许范式的项的范式，则该策略被称为范式化。对于正交TRS类，已知若干归一化结果（参见例如，Klop [14]）。例如，O'Donnell [20]证明了并行最外层策略（在单个步骤中并行收缩所有最外层的赎回）对于所有正交TRS都是标准化然而，并行最外层不是最优策略，因为它可能执行无用的步骤。例2.2考虑由重写规则组成的TRSR0+ y！ 嘿！0s（x）+y！s（x+ y）s（x）y！（x）y）+y面对项t=（0s（0））（0+s（0）），并行最外层策略通过在两个步骤中收缩三个赎回来计算其范式0（0个s（0））（0 + s（0））！ 0 s（0）！0标准形式0也可以通过收缩两个赎回来达到s（0））（0 + s（0））！0s（0）！0因此，t中的redex 0+s（0）不需要达到标准形式。最优策略只选择需要的赎回。形式上，如果在从t到范式的每个重写序列中，收缩的后代，则需要项t中的例2.1（续）在显示的重写序列中，第n（2; b）！2不需要的赎回被收缩。例如，在项nth（0;f（2; 1 + 2））中的redex 1 + 2是不需要的：nth（0; f（2; 1+ 2））！ nth（0; 2：f（1 + 2; 2+（1 + 2）！2Huet和Levy [11]证明了以下重要结果。定理2.1设R是正交TRS。(i) 每个可约项都包含一个所需的redex。(ii) 只要所考虑的项有一个标准形式，所需的赎回的重复收缩就会产生一个标准形式因此，对于正交TRS，总是选择所需Redex的策略4收缩是正常的和最佳的。[4]不幸的是，所需的赎回通常是不可计算的因此，为了获得可计算的最优策略，我们需要找到（1）可判定的需要性近似和（2）重写系统的（可判定的）类，这些重写系统确保每个可约项都有由（1）标识的需要的redex。从Huet和Levy [11]关于强序列性的开创性工作开始，这些问题在文献中得到了广泛的研究（例如[3，12，13，14，15，22，28]）。在所有这些著作中，休特和勒维的索引概念！- 还原，并将其序列化。 基本上，为了确定是否需 要 项t=C[]中的最外层的redex，被一个新的符号代替，并且t中的所有其他最外层的redex被表示未知项的符号代替。然后研究是否可以从结果项t0中消失 通过使用一些可计算的部分还原的概念。如果情况不是这样，那么我们可以得出结论，t中的redex是必要的。因为redex在t中的必要性仅仅取决于它在t中的位置（参见引理5.1），在t中用替换redex不会损失一般性。然而，通过用基本信息替换所有其他最外层的赎回可能会丢失用于确定的必要性。这在下面的示例中进行了说明，该示例显示所需的兑换并不独立于其他兑换。例2.2（续）在（0 +s（0））项 中 需 要 任 意 的 redex ， 但在 （ 0s（0））项中不需要：（0s（0））！0分！0的情况。在第5节中，我们提出了Durand和Middeldorp [6]的可判定按需调用计算框架，其中问题（1）和（2）直接解决。3独立对在术语重写领域，终止已经研究了几十年，并且已经开发了许多强大的技术（参见[5，24，30]的调查）。由于终止是重写系统的不可判定属性，因此没有方法在所有情况下都有效。传统的自动终止证明的TRS的技术是简化的顺序，如递归路径顺序，Knuth-Beneficiary顺序，和（大多数）多项式顺序。最近，Arts和Giesl的依赖对方法显著地扩展了这些技术的终结性证明能力。在该方法中，TRS被转化为一组排序约束，使得TRS的终止等价于约束的可解性。生成的约束通常由传统的简化命令来解决。Arts、Giesl、Ohlebusch和Urbain [1，8，9，21，29]的一系列论文充分说明了依赖对方法的威力。4 这里我们忽略了（需要的）赎回的重复问题，如果共享公共子项，这个问题就可以解决。5在本节中，我们回顾与依赖对技术相关的基本概念和结果。 我们参考[1，8，9]的动机和进一步的要素。设R是签名F上的TRS。定义符号的子集DF由重写规则的左手侧的所有根符号组成。 设F]表示F和f [f]jf2Dg 的 并 ， 其 中 f] 与 f 具 有 相 同 的 元 数 . 给 出 一 项 t=f（t1; ：;tn）2T（F;V），其中f被定义，我们将项f]（t1; ： ：;tn）写成t ]。 如果我！ r2R和t是r的子项，其中r ot（t）2D，则重写规则l]！ t]称为R的依赖对。R的所有依赖对的集合表示为DP（R）。在例子中，我们写F为f]。示例3.1由重写规则组成的TRS Reven（x）！ （x; 0）int n=0（x; s（0））odd（x）！ （0;s（0））！虚假不（真）！ falseeo. getString（s（x）; s（0））！0= 0（x; 0） 真正有ve个依赖对：EVEN（x）！ EO（x; 0）（1）EO（x;0）！ NOT（eo（x; s（0）（3）ODD（x）！ EO（x; s（0））（2）EO（x; 0）！ EO（x; s（0））（4）EO（s（x）; s（0））！ EO（x; 0）（5）一个预序是一个传递和自反关系。重写前序是在上下文和替换下封闭的项上的前序&一个约简对由一个重写前序和一个相容的良基序>组成，它在替换下是封闭的。&这里兼容性意味着包含>>或包含>>成立。&&定理3.2（Arts和Giesl[1]）签名F上的TRSR是终止的当且仅当存在约简对（;>）使得R和DP（R）>.&因为重写规则只是成对的项，所以R&是&每个重写规则l的l r的简写！r2 R和DP（R）>表示对于每个依赖对l > r！ r 2 DP（R）.根据定理3.2，R的终止相当于终止一个约简对（; >），使得even（x） eo（x;0）eo（x;0） not（ eo（x; s（0）&&odd（x） eo（x; s（0））eo（0; s（0）） false&¬（ true） false eo（ s（x）; s（0）） eo（x;0）&¬（ false） true EO（x;0）> NOT（ eo（x; s（0）&EVEN（x）> EO（x;0）EO（x;0）> EO（x; s（0））ODD（x）> EO（x; s（0））EO（ s（x）; s（0））> EO（x;0）6R为了从约简对的第二分量在上下文下不需要闭合的事实中受益，由定理3.2生成的约束可以通过应用所谓的参数过滤来简化。签名F的参数筛选是一个映射，它将每个n元函数符号与参数位置i 2 f1;：; n g或具有1 6 i 1的参数位置列表[i1; ：;im]（可能是空的）相关联 <<我是6号。签名F由所有函数符号f组成，使得（f）是某个列表[i1; ：;im]，其中在F中f的arity是m。每一次迭代都引起从T（F; V）到T（F; V）的映射，也表示为：t如果t是变量（t）=（ti）ift=f（t1; ：;tn）and（f）=if（（ti1）; ：;（tim）） 如果t=f（t1; ：;tn）并且（f）=[i1; ：;im]因此，一个参数过滤被用来替换函数符号的一个参数或消除函数符号的某些参数定理3.3（[1]）签名F上的TRSR是终止的当且仅当存在F的一个变元迭代和一个约简对（; >）使得（R）和（DP（R））>.&例3.1（续）即使我们应用任意的参数筛选对于前面给出的排序约束，所得到的约束不能被&具有>一个简化阶的约简对（; >）满足。这可以从以下几点看出。约束E0（x; 0）>E0（x;s（0））只能在（s）=[]时满足。但是，约束EO（s（x）;s（0））>EO（x; 0）简化为 EO（ s;s）>EO（x;0），因此我们必须具有（ EO）2f[2];2g。 因此，两个约束EO（x; 0）>EO（x;s（0））和EO（s（x）;s（0））>EO（x; 0）简化为EO（0）>EO（s）和EO（s）>EO（0）或0>s和s> 0，与>的充分性相矛盾。与其像前面的定理那样同时考虑所有的依赖对，分开处理依赖对的组是有利的。 这些组对应于R的依赖图DG（R）中的循环。DG（R）的节点是R的依赖对，并且有一个从s开始的箭头！t你！v当且仅当存在替换和这样测试！ 联合(By重命名变量的不同实例我们可以假设依赖对=.）一个循环是依赖对的一个非空子集C，如果对于每两个（不一定是不同的）依赖对s！ t和u！v在C中存在一个非空路径从s！t你！v.定理3.4（[9]）TRS R是终止的当且仅当对DG（R）中的每个圈C都存在一个变元迭代和一个约简对（&; >）使得（R）&，（C）&[>]和（C）[>]=？.定理3.4中的最后一个条件表示对于至少一个依赖对s！ t 2 C.7、RPO例3.1（续）依赖图DG（R）有六个箭头：（1） z（3，），，（4）、、s（5）、r （二）对应于唯一循环C = f（4）;（5）g的约束由规则约束even（x） eo（x;0）eo（x;0） not（ eo（x; s（0）&&odd（x） eo（x; s（0））eo（0; s（0）） false&¬（ true） false eo（ s（x）; s（0）） eo（x;0） not（ false） true&&&依赖对约束EO（x;0）>0 EO（x;s（0））EO（s（x）;s（0））>00 EO（x;0）>0;>00 2f>;&g> >00 equals>. 让>0个 =&，>00 =>，并使用定义为（E0）=1的迭代，（eo）=（not）=（0）=[ ]，并且（s）=（even）=（odd）=[1]，这些约束简化为even（x）eo notfalse eonoteo s（x）> xodd（x）eo nottrue eofalsexx&&&&&&&并且满足递归路径顺序（即，>= with precedenceeven;odd eo not false; true.RPO和&==）的文件因为它是不可判定的是否存在替代，这样t！R u，则一般不能计算出DEP图。因此，为了机械化定理3.4的终止准则，必须近似依赖图。为此，Arts和Giesl提出了一个简单的算法。定义3.5设R是一个 TRS。估计的依赖图EDG（R）的节点是R的依赖对，并且存在来自s的箭头！ t你！v当且仅当 REN（ CAP（t））和u是uniable。这里CAP用不同的新鲜变量替换所有最外面的子项，REN用不同的新鲜变量替换所有出现的变量。引理3.6（[1]）设R是TRS。(i) EDG（R）是可计算的。(ii) DG（R）EDG（R）.容易验证，对于实施例3.1的TRS R，EDG（R）与DG（R）一致。8R一RRR例3.7考虑由著名的Toyama重写规则[27]组成的TRSRf（a; b; x）！ f（x; x; x）有一个依赖对：F（a; b; x）！ F（x; x; x）. 因为没有条款s 且t使得F（s; s; s）！F（a;b; t），DG（R）不含箭头，因此R终止是定理3.4的一个平凡的推论。然而，由于REN（CA P（F（x;x;x）=F（x1;x2;x3）与F（a;b;x）一致，EDG（R）包含一个圈. 由于求解得到的约束f（a; b; x）&f（x; x; x）和F（a; b; x）> F（x; x; x）与直接证明R的终止性一样困难，因此使用依赖对方法自动证明终止性似乎是不可能的。在上面的例子中，TRS不是DP准简单终止的。 DP类准简单终止TRS（Giesl和Ohlebusch [10]）假设“捕获所有TRS，其中使用依赖对的自动终止证明可能是可行的”。在第6节中，我们将看到，通过用依赖图的更好的（可计算的）近似替换估计的依赖图，自动证明例3.7的TRS的终止变得微不足道。4近似值我们开始这一节回顾一些基本的定义和结果有关树自动机。更多的信息可以在[4]中找到。一个（nite bottom-up）树自动机是一个四元组A=（F ; Q;Q f;），包括一个nite签名F，一个nite状态集Q，与F不相交，一个子集Q fQ的nal状态，和一组转换规则。每个转移规则都有f（q1; ：;qn）的 形式！ 其中f2F和q1; ：;qn; q2Q。 所以树自动机A=（F ; Q;Qf;）仅仅是一个有限基TRS（F[Qf;），其重写规则具有特殊的形状，以及Q的子集Qf。T（F[Q]）上的诱导重写关系表示为y！A. 一个基本术语t 2T（F）被A接受，如果t！对于某个q2. 所有此类的集合项表示为L（A）。一个子集LT（F）称为正则的，如果存在一个树自动机A =（F; Q; Q f;）使得L = L（A）. 众所周知，线性项t的基实例集（t）是正则的。此外，左线性TRSR的基正规形集NF（R）是正则的。下面我们利用一个众所周知的事实，即一个给定的树自动机是否接受空语言是可判定的设R是签名F上的eTRS，LT（F）.在下文中我们表示所有项s 2T（F）的集合，使得s！对于某项t 2 Lby（！）[L]。需求的不可判定性和需求图不可计算的事实的原因仅仅是简化（！）是根据-9SSR可食用的更确切地说，一个术语是否重写为属于某个集合的术语是不可判定的。在needededness的情况下，这个集合是范式的集合（不包含，参见下一节的精确状态）。由于NF（R）对于左线性TRS R是正则的，因此集合（啊！）[NF（R）]不是正则的。决定性的关键在于延伸！to！R R S对于一些合适的eTRS，例如（！）[NF（R）]是正则的。定义4.1设R和S是相同签名上的eTRS我们说Sapp roximatesRif！R！且NF（R）=NF（S）。的近似映射是从eTRS到eTRS的映射，具有（R）对于所有eTRS R近似R的性质。我们说是正则性保持的，如果（啊！）[L]对于所有eTRSR和正则L都是正则的。在本节的剩余部分中，我们定义了三个已知是正则性保持的近似映射。我们的定义与文献中的定义略有不同，因为我们必须处理可能的非左线性TRS（当近似第6节中的依赖图时）。定义4.2设R为eTRS。强应用R肟化Rs 通过用不同的新鲜变量替换每个重写规则的右手侧和左手侧中的所有出现的变量，从R获得，即，俄.西 =f REN（l）！zj l！ r2 R和z是一个新的变量。实施例2.2（续） 由以下规则组成：0+ y！ z0y！ zs（x）+y！ zs（x）y！ z通过忽略重写规则的右侧来近似TRS的想法是由于Huet和Levy [11]。通过保留重写规则右侧的n个非变量部分，获得了更好的近似定义4.3苯甲酸肟化反应 通过用不同的新鲜变量替换重写规则中的变量的所有出现，从R获得： =fREN（l）！ REN（r）j l！ r2R g.实施例2.2（续）eTRSR3 由以下规则组成：0+ y！ y00y！0s（x） +y！ s（x0+y0）s（x）y！（x0y0） +y00通过忽略重写规则右侧的变量来近似TRS的想法是由于O yamaguchi[22]。注意，R 当R是左线性和右接地时。定义4.4 eTRS被称为增长，如果对于每个重写规则l！ r中的变量V ar（l）\V ar（r）出现在l的深度1处。增长近似10G00sGRRg被定义为任何左线性增长的eTRS，它是从R通过线性化左侧并重命名右侧中出现在对应左侧中的深度大于1的变量而获得的。例2.2（续）eTRSR包括以下规则：0+ y！ 嘿！0s（x） +y！ s（x+y） s（x）y！（xy） +y注意，在R的规则的右手边出现的y没有被重命名，因为它们出现在对应左手边的深度1处。由Jacquemard [12]引入的生长TRS是Comon [3]考虑的浅层TRS的适当扩展。上面定义的不断增长的近似值源于Nagaya和Toyama [19]。它扩展了[12]中的增长近似，因为右线性要求被丢弃。作为另一示例，考虑包含重写规则f（x;g（x）;y）的TRS R！ f（x;x;g（y））. 则R conn tainsf（x;g（x0）;y）！z，R贡坦f （x;g（x0）;y）！f （x00;x000;g（y0）），和Rconn tainsf （x;g（x0）;y）！ f（x;x;g（y））或f（x0;g（x）;y）！ f（x00;x00;g（y））. 前者是首选，因为它更接近原来的规则。在定义的Rg的歧义不会导致问题的续集。定理4.5逼近映射s，n，g是保正则的.Nagaya和Toyama [19]证明了上述结果的增长约-imation;识别（！G）[L]定义为极限一个夜间饱和的过程。这种饱和过程与定义在Comon [3]和Jacquemard [12]中，但是通过专门使用确定性树自动机，可以处理非右线性重写规则。对于强近似和弱近似，使用基树换能器的更简单的构造是可能的（[6]）。Takai等人 [25]介绍了左线性逆尼特路径重叠重写系统，并证明了上述定理对于相应的近似映射是正确的。生长重写系统构成逆尼特路径重叠重写系统类的适当子类。由于这类的定义相当复杂，我们在这里不考虑逆路径重叠近似。然而，我们注意到，我们的结果很容易扩展。另一个复杂的正则性保持近似映射可以从Seki等人最近的论文中提取。[23]。5策略的近似设R是签名F上的TRS。我们假设存在一个常数不出现在F中，我们将R视为扩展签名11R0F = F[ f g.所以NF（R），R的基正规形式的集合，由T（F）中所有正规形式的项组成。设R为TRS R[f！G.请注意，NF（R）与NF（R）\T（F）一致，即不包含符号的基范式的集合下面的简单引理给出了需要的另一种定义，不依赖于后代的概念。引理5.1设R是签名F上的正交TRS。 需要C[] 2 T（F）中的Redex，当且仅当不存在这样的t2 NF（R）项这个C[ ]！ t.这个引理的一个直接后果是民间传说的结果，即只有一个redex在一个术语中的位置对于确定needededness是重要的。所以，如果需要在项C[ ]中redex，那么在C[0]中redex 0也是如此。定义5.2设R是签名F上的TRS，近似映射。我们证明了C[ ]2T（F）中的redex是-neded，如果C[]2=（啊！）[NF（R）]。 所有such项C[]的集合由NEE D（R）定义。R所以redex在C[ ]中，- 需要当且仅当C[] 2需要（R）。在例子中，我们将讨论！R to！ .例2.2（续）设1和2为赎回，并考虑t =（0 +s（1））+2|{z}3所有三个Redex都需要（因为R是非擦除的）。下面的重写序列表明1和2是不需要的：（0+s（））+2！0 +2！s0（0+s（1））+！s0 +！s0Redex3是s-需要的，因为所有的s-约简形式为+t0。F或近似的情况是一样的。Redexes 1和Redexes 2不是必需的|上述s-重写序列也是s-重写序列|但3是。对于增长近似，1不是g-所需的：（0 +s（））+！s（） +！s（0 +）！s（）！ 不2克2克2克2克对于某个正规形式t0（whi chde p在redex2上结束）。howwever，2 是需要的。这是因为在（0 + s（1））+项中不能去掉，因为+的第二个表达式不能被Rg中的规则消去.引理5.3设R是一个正交TRS和一个逼近映射。所有需要的资料都需要。只有在引理5.3中我们才需要正交性。对于可判定性问题，左线性假设。12NV斯沃格伊什引理5.4设R是左线性TRS，近似映射如果是正则保持的，那么NEED（R）是正则的。由于正则树语言的成员资格是可判定的，我们得到以下结果。推论5.5设R是左线性TRS和保正则逼近映射。是否需要一个术语的redex是可判定的自然，更好的近似可以识别更多需要的赎回。引理5.6对于每个TRS R，NEED（R s）NEED（R）NEED（R g）。引理5.3和推论5.5考虑了第一个问题，在定理2.1之后的段落中，找到了可判定的需要性近似。在下文中，我们解决第二个问题，以确定类的TRS的属性，每个可约项有一个可计算的需要redex。定义5.7设是一个近似映射.使得每个可约基项都有一个必有的归约的一类TRS记为CBN。以下定理的证明依赖于正则树语言和基树转换器的标准属性定理5.8设R是左线性TRS和保正则逼近映射。R2是否CBN是可判定的.更好的近似覆盖更大类的TRS，这并不奇怪这在下一个引理中得到了正式的表达。引理5.9CBN（CBN （CBN。值得注意的是，CBN类正确地包括Huet和Levy引入的强序列TRS类（参见[7，示例1]）。CBN类TRS远大于Oyamaguchi [22]介绍的NV顺序TRS类。例如，CBN包含所有右接地TRS。因此，证明前一个引理中的第一个包含是严格的是非常容易的。由三条规则组成的TRSf（a; b; x）！ af（b; x; a）！ b f（x; a; b）！C属于CBN（因为它是右接地），但不属于CBN，因为在f（; ;）项中没有出现redex是s-需要的：f（;;）！sf（;a;）！sf（;a;b）！是一个f（;;）！sf（b;;）！sf（b;;a）！是一个f（;;）！sf（a;;）！sf（a;b;）！是一个相比之下，NV-序贯TRS类正确地包括所有强序贯TRS的证明是相当复杂的（参见。[22]）。的关系13'NVsequentialit y&“#强大$顺序性CBNS！%CBNNVRRRCBNG在图1中总结了几类TRS之间的关系，这些TRS允许通过需要计算来判定调用到范式。感兴趣的读者可以参考Durand和Middeldorp [6，7]，以获得关于可判定的按需调用计算的进一步结果Fig. 1. 对比6终止的近似值回想一下，依赖对s中有一个箭头！测试依赖性对你！v在DG（R）中当且仅当t！ 一些替代品和。由于t2（t）和 u2（u），这等价于（t）\（！）[（u）]6=？如果我们想用树自动机来判定（t）和（！）[（u）]，最明显的思想是用包含它们的正则树语言来近似这些集合。 众所周知，如果u是非线性项，则（u）不必是正则的。然而，REN（u）是线性项，并且包含（u）（REN（u））显然成立。结果的基础上第4节，很自然地要评价（！）[（u）]b（！）[（RE N（u））]用于R R保正则逼近映射 . 但是，没有必要用（REN（t））近似（t），以获得可判定性。原因在下面的结果中表示。定理6.1（Tison [26]）下面的问题是可判定的：实例：树自动机A，项t问题：（t）\L（A）=？？这个结果对于自动证明14（1R）的方式R（1R）的方式依赖于非线性的TRS的终止（即，通过线性化重写规则，TRS变为非终止的）。为了正确理解下一个定义，that（t）！）[（u）]6 =？ 等于（u）\（！） [（t）]6 =？.R（R1）定义6.2设R是一个TRS和一个逼近映射. 近似依赖图DG（R）的节点是R的依赖对，并且有一个来自s的箭头！t你！v当且仅当（t）\（！）[（RE N（u））]6 =？ 和（u）\（！）[（RE N（t））]6 =？.所以我们从s画箭头！ t你！v，如果t的基实例在R中重写为REN（u）的基实例，并且u的基实例在（R 1）中重写为REN（t）的基实例。 具有这两个条件的原因是（1）为了可判定性，t或u应该是线性的，以及（2）取决于并且R，R可以比（R1）更好地近似R1，或者反之亦然。此外，施加的条件越多，就越接近真正的依赖图。定理6.3设R是TRS，近似映射(i) 如果是正则性保持的，则DG（R）是可计算的。(ii) DG（R）DG（R）.自然地，更好的近似映射导致依赖图的更好的近似。因此，我们有以下结果。引理6.4 DG（R）DG g（R）总干事（R）DG s（R）对于每个TRS R。现在我们将我们的近似依赖图与Arts和Giesl的估计依赖图进行比较。前两个例子表明，s-近似依赖图和估计依赖图在一般情况下是不可比的。例6.5考虑TRSR= f f（g（a））！f（a）; a！湾有两个依赖对：F（g（a））！F（a）（1）F（g（a））！A类（2）因为REN（ CAP（ F（ a）））= F（x）与 F（ g（ a））一致，所以 EDG（R）包含两个S（一）z（2，）（R1）=ff（a）！x;b！ xg. 因此（！）[fF（a）g]由以下组成：Sfn（a），fn（b），F（fn（a）），F（fn（b））形式的所有项，其中n>0。术语F（g（a））显然不属于这个集合，因此在DGs（R）中没有箭头。例6.6考虑TRS R = f f（x; x）！ f（a; b）g. 我们有DP（R）= f FS箭头：15俄.西（x; x）！ F（a; b）g. 因为REN（CAP（F（a; b）= F（a; b）和F（x; x）是EDG（R）不含任何杂质。 然而，bth（F（a;b））\（！）的方式16（1R）Rz，[（REN（F（x;x）]和（F（x;x））\（！）[（REN（ F（ a; b）]非空，S如项F（a; b）和F（f（a; b）; f（a; b））所证明的。前面例子中的非线性是必不可少的。引理6.7对于每个左线性TRS R，DGs（R）ED G（R）。下一个结果表明，近似依赖图总是估计依赖图的子图。定理6.8DG（R）对于每个TRS R，EDG（R）。下一个例子表明，近似依赖图通常是估计依赖图的真子图实施例3.7（续） =ff（a;b;x）！f（x1;x2;x3）g和（REN（F（a;b;x）=fF（a;b;t）j t是基项mg。 Consequee ntl y，（！）的方式[（REN（F（a; b; x）]等于（REN（F（a; b; x），并且由于F（x; x;x）项的实例不属于这个集合，所以DG（R）不包含箭头。我们注意到，依赖对方法的各种修改（细化、重写、实例化;参见Giesl和Arts [8]）不适用于例3.7的TRS。下一个例子显示了一个TRS，它不能被证明终止于近似值，但它的（自动）终止证明变得容易与增长的近似值。例6.9考虑由三个重写规则f（x; a）！ f（x; g（x; b））g（h（x）; y）！ g（x; h（y））g（a; y）！ y有三个依赖对：F（x; a）！ F（x; g（x; b））（1）G（h（x）; y）！ G（x; h（y））（3）F（x; a）！ G（x; b）（2）我们很容易证明DG_n（R）包含两个循环：S（一）z（2，）z（3，），r特别地，F（a;g（a;b））！R F（a;a），它解释了从（1）到（2）的过程。(1)和（2）。有问题的循环f（1）g在DGg（R）中不存在，因为没有F（x;g（x;b））的基础实例在Rg中重写为 F（x;a）的基础实例（一）（二）（3），r因此，由此产生的排序约束f（x; a） f（x; g（x; b））g（ a; y）y&&17g（ h（x）; y） g（x; h（y））G（ h（x）; y）> G（x; h（y））&181（111很容易满足（例如，通过取（f）= 1，结合具有优先级G h和g h的字典图形路径顺序）。5为了比较我们的近似依赖图与Kusakari和Toyama [16，17]定义的依赖图的近似，我们参考[18]。最后，我们介绍了一个新的近似的依赖图，它不依赖于树自动机技术。回想一下，近似依赖图中两个依赖对之间存在箭头有两个条件现在的想法是将引起第二个条件的对称性考虑纳入Giesl Arts的估计依赖图中定义6.10设R是签名F上的TRS。用D1中的根符号替换项t的所有最外子项的结果表示为CAP（t）。这里D1=f root（r）j l！ r2 Rg，如果R是非折叠F，否则是eTRS R 1的指定符号集。估计的依赖图EDG（R）的节点是R的依赖对，并且存在来自s的箭头！t你！v当且仅当REN（CAP（t））和u都是uniable，且t和REN（CAP（u））都是uniable。引理6.11设R是TRS。(i) EDG（R）是可计算的。(ii) DG（R）EDG（R）.证据第一部分是显而易见的。第二部分是下面引理6.4和定理6.17的直接结果。2接下来的两个例子显示了新近似优于EDG的优点。例6.5（续）我们有REN（CAP（F（g（a）= F（g（a）），因为D1= f b; f g。因为这一项不与F（a）统一，EDG（R）不包含箭头。例3.7（续）由于REN（CAP）（F（a;b;x））=F（a;b;x1）若与F（x;x; x）不一致，则EDG（R）不含箭头.只要R包含具有变量右侧的重写规则，EDG（R）和EDG（R）就重合。引理6.12对于每个坍缩的TRS R，EDG（R）= EDG（R）。5再次，TRS不是DP准简单终止。19111（1R）的方式（1R）的方式（1R）的方式SREN（CAP 1（F（a; b; x））= F（x; b;x），EDG（R）包含循环。一个容易证据 显然EDG（R）EDG（R）. 假设有一个箭头从s！不敬你！EDG（R）中的v。所以REN（CAP（t））和u是唯一的。我们需要证明t和REN（CAP（u））是唯一的。设F是R的签名.我们有一个ver oot（t）=r oot（u）2F ]。 令u=f]（u1; ：;un）. 因为R是坍缩的，D1 =F. 当u; ：; u2T（F;V）时，对于1n1n一些新鲜的变量x1; ：;xn. 因此，REN（CAP（u））与任何以f]为根符号的项，特别是以t为根符号的项。2至于与DGs的比较， 关于DG 就这一点而言，对于EDG建立的结果延续到EDG，除了我们必须在引理6.7中将左线性加强为线性。这可以从下面的两个例子和随后的结果中得出。例6.13考虑由两个重写规则组成的TRS Rf（g（a））！ f（a）a！g（b）有两个依赖对：F（g（a））！F（a）（1）F（g（a））！A类（2）因为REN（ CAP（ F（ a）= F（x）与 F（ g（ a））一致，并且 F（ a）与 REN（ CAP（ F（ g（ a）= F（x）一致，所以 EDG（R）包含两个箭头：（1） z（2，）然而，由于F（g（a））2=（！）[fF（a）g]，D Gs（R）不含任何负整数。S例6.14考虑由两个重写规则f（a; b; x）组成的TRS R！ f（x;x; x）c！ 一有一个依赖对：F（a; b; x）！ F（x; x; x）.因为F（a; b;x）与REN（CAP（F（x; x; x）= F（x 1; x 2; x 3）一致，并且F（x;x; x）与1 2证明危险货物（注册商标）不包括任何货物。2015年05月05日（）[（REN（t））]（REN（CAP 1（t），S折叠TRSR和项t。证据 设F是R的签名.我们对t的结构使用归纳法。如果t是一个变量，或者如果root（t）2 D1，则CAP1（t）是一个变量，因此 （1）（1）（2）（3）（3）（4）（5）（4）（5）（5）20S（REN（CAP1（t）。 设t =f（t;：：;t），其中f2 F] n D 1. 因为R是（R1）i（5）（6）（5）（6）（6）（6）（7）（7）（7）（8）（8）（8）（9）（）[（REN（t））]S1N非折叠，R中规则的每一个右手边，因此也是每一个左手边，（R1）中规则的手侧以D1中的符号开始。 因为r ot（t）2=D 1 并且REN（t）的参数不共享变量，则可以得出：（R1））[（REN（t））] =ff（s1;：：：;sn）j si2（）[（REN（t））]g.明确S（一）S
