特殊策略重写终止性的证明方法：算子上的局部策略

《理论计算机科学电子札记》58卷第2期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html34页采用当地策略OlivierFissorea，IsabelleGnaedigb和Hel eneKirchnercaLORIA-CNRS，P 239 F-54506 Vand uvre-l es-NancyCedex，电子邮件：Olivier.Fissore@loria.frbLORIA-INRIA，P 239 F-54506 Vand uvre-l es-Nancy Cedex，电子邮件：Isabelle. Gandeliadig@loria.frcLORIA-INRIA LORIA-CNRS，P 239 F-54506 Vand uvre-l es-Nancy Cedex，电子邮件：Helene.Kirchner@loria.fr摘要本文提出了一种特殊策略重写终止性的证明方法：算子上的局部策略。一个归纳的证明程序，提出了基于显式归纳的终止性。给定一个项，证明原理依赖于交替地将归纳假设应用于其子项，根据策略，通过用归纳变量抽象子项，并在一步中缩小所获得的项归纳关系是一个具有子项性质的F-稳定序，它不是先验地给出的，而是通过检验序约束的满足性来检验它的存在性。关键词：重写，终止，算子局部策略，规则语言，归纳，缩窄，排序约束。1介绍重写的终止是自动演绎中的一个关键问题，对于等式逻辑，以及在程序设计中，对于基于规则的语言。 由于它在一般情况下是不可判定的，因此在特定的上下文中，它是在充分条件下得到保证的。许多终止性证明技术已经被提出，其中大多数使用项的诺特序。但是他们通常处理标准重写关系的性质，本质上是在自由项代数上工作。在基于规则的语言（如ASF+SDF [14]、OBJ3 [13]、Maude [5]、CafeOBJ [10]、ELAN [20]或ELAN [3]）的上下文中，程序是规则集，执行包括重写基础表达式，拥有更具体的终止证明工具将是有用的：允许在特定归约策略下证明终止的方法，或证明c 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。菲索尔、格奈迪格和基什内尔2终止于基项代数，用于不终止于自由项1的项重写系统（简称TRS）。证明方法我们建议在这里，基于一个明确的归纳终止属性，使我们能够解决这些问题。在编程的上下文中，有一组规则，当考虑所有推导时，这些规则导 致 发 散 计 算 ， 但 对 于 特 定 策 略 终 止 。 一 个 著 名 的 例 子 是 用if_then_else_expression定义的递归函数的求值，如果rst参数不是rst计算的。运算符的局部策略用于这种情况，特别是强制表达式的计算终止。这种策略被OBJ3，CafeOBJ或Maude等语言所允许，并在[7]和[18]中进行了研究。它是这样定义的：对任何运算符f附加一个有序的整数列表，给出在给定项中要计算的子项的位置，其顶部运算符是f。例如该TRSf（i（x））！ if then else（zero（x）; g（x）;f（h（x）0！ 真正0（s（x））！false if then else（true; x;y）！Xifthen else（f alse; x; y）！ yh（0）（0）h（x）！s（i（x））使用条件表达式，对于标准重写关系，不终止，而是使用以下策略终止：LS（ite）=[1; 0]，LS（f）= LS（zero）= LS（h）=[1; 0]和LS（g）= LS（i）=[1]，其中ifthen else简称为ite。据我们所知，用策略重写的具体终止性证明工具只针对自由项代数的最内情形[1]和上下文敏感重写[17，16，21，11]，以及基项代数的最内在这里，我们提出了一个终止证明方法的情况下，局部战略的运营商，以下的归纳证明原则[12]。注意，我们的方法处理了最左最内和最内策略：最左最内策略是局部策略的一种特殊情况，并且如[15]中所证明的，重写的终止对于最左最内和最内策略是等价的。如上所述，对于一种称为上下文敏感重写的重写，也存在终止结果。在这种情况下，重写只允许在某些特定的位置上的条款，这是从本地策略，这是更具体的：在第二种情况下，不仅允许重写的位置是指定的，而且考虑他们的顺序。除了局部策略的特殊情况外，这两种策略是不同的。我们的证明方法的主要思想是使用显式归纳的终止性质，以证明任何元素t的一个给定的集合，菲索尔、格奈迪格和基什内尔3项T终止，即，不存在从t开始的无限导出链。我们的归纳原理使用了具有子项性质的基项的排序。 它基于一个简单的思想，即如果根据给定的策略rst减少一个项t需要归一化t的一个子项t0，则我们可以通过归纳推理来假设t0对于相同的策略终止。 如果我们用一个表示它的许多正规形的归纳变量X来代替t 0 y，那么就需要证明由t0yX在t中的推广得到的项u是终止的，从而证明t是终止的。然后，在X的不同可能值之后对u执行重写步骤：它通过缩小来计算。这个过程是迭代的，直到获得一个非窄项，或一个项的归纳假设适用。注意，归纳排序不是先验的，但在证明过程中通过设置排序约束。应用归纳假设，然后在于测试这些约束是否是satisable able。在前面的例子中，我们的方法在于证明对于前面给定的策略，常数和f（T）; zero（T）; ite（T1;T2;T3）; h（T）; i（T）; g（T）; s（T）形式的项的终止性，无论基项T;T1;T2;T3的值如何。显然，0; true;false是正规形式，然后终止。对于i（T）（类似于s（T）和h（T）），使用归纳排序使得i（T）T，通过归纳假设，我们可以假设T是终止的。i（T）也是如此，因为i是一个构造函数（即i不是规则左侧的顶部符号）。根据该策略的定义，归一化零（T）rst包括将T1归一化为它的任何范式T#（如果它存在），然后在顶部位置处归零（T#）对于与前面相同的排序，我们有零（T）T。然后，通过归纳假设，T终止。设T#是它的任意正规形（如果系统不连续，可以有几个正规形零（T）的终止然后被还原为零（T#）的终止，其只能还原为真或假。正规化h（T）rst也在于正规化T。与前面类似，归纳假设也可以应用于T。h（T）的终止于是被还原为h（T#）的终止，它只能还原为i（0），即正规形式，或还原为s（i（T#）），即也是正规形式。常化组（T1;T2;T3）rst包括常化T1。如前所述，可以假定T1是终止的，并且ite（T1;T2;T3）的终止被简化为ite（T1#;T2;T3）的终止。根据这一策略，ite（T1#;T2;T3）被还原为T2或T3，它们被诱导假设终止我们用同样的方法来研究f（T）如何归一化。我们的目标是提供一个实现这种推理的过程。第2节介绍了背景情况。第三节介绍归纳原理的基本概念。在第四节中，给出了一个基于规则的算法，将证明原理机械化，证明了它的正确性，并给出了例子。菲索尔、格奈迪格和基什内尔4表示为by！+（相应地） ！）的。如果它存在，则nitederivation的最后一项2背景我们假设读者熟悉例如在[6]中给出的术语重写的基本定义和。T（F;X）是从具有元数n 2 N的函数符号的给定集合F和表示为x;y：的变量的集合X构建的项的集合。T（F）是基项的集合（没有变量）。 由0元符号组成的项称为常数; C是F的常数集。项中的位置表示为整数序列;表示空序列。项t的顶部位置是，并且在t的顶部位置的符号被写作top（t）。 设p和p0是两个位置。如果p 0 = p，则位置p被称为p 0的前x（和p 0的后x），其中是非空整数序列。 给定一项t，O（t）是t中的位置集合，归纳定义如下：O（t）=fgif t2 X;O（t）=fg[fi：p j1我n和p 2 O（ti）g，如果t =f（t1;：;tn）. 该集合被划分为O（t）=fp2O（t）jtjp62Xg和OV（t）=fp2O（t）jtjp2Xg其中符号tjp代表t在位置p处的子项。 如果p2O（t），则t[t0]p表示从t通过用t 0项替换位置p处的子项而 获 得 的 项。替换是从X到T（F; X）的赋值，写作=（x7！t）：（y7！u）。它唯一地扩张到T（F; X）的一个自同态。我们确定替换=（x7！t）：（y7！u）与方程组（x = t）^：：^（y = u）。应用于项t2T（F; X）的结果写为 （t）或 t. 领域 表示为Dom（）是X的子集，满足x6=x。的范围，表示为Ran（），由yRan（）=Sx2Dom（）V ar（x）. 基替换或实例化是一种赋值从X到T（F）。 Id表示身份替换。 的组合物取代1后接2表示21。给定两个替换1和2，我们写12i9，使得2= 1。给定X的子集X1，记为X1 对于X 1的变量的限制，即，代换为Dom（X1）X1和8×2Dom（X1）：X1x=x：给定T（F; X）上的重写规则或项重写系统的集合R，F中的函数符号称为构造函数，如果它不出现在规则左侧的顶部位置，否则称为定义函数符号。F对于R的构造函数的集合用Cons R表示，F对于R的定义函数符号的集合用Def R表示（当没有歧义时省略R）。由R导出的重写关系称为标准重写关系，注！R（！ 如果在R上没有m bigui ty）。 我们注意到了！p; l！r;t（或s！p; l！r;t其中p或l！ r或m可以省略），如果s在位置p处用规则l重写为t！r和替换。项sjp称为redex，位置p称为redex位置，并且在位置p处的符号称为redex符号。transitive（传递）R诱导的重写关系的（自反传递）闭包是R R从t开始，被认为是正规形式，并且由t#表示菲索尔、格奈迪格和基什内尔51i 1在T（F ; X）上的一个序称为Noether序（或良基序），如果这个序没有无穷下降链。它对T（F ; X）的任意项对t;t0是F-稳定的i，对任意项f（： ：），tt0蕴涵f（：t ： ）f（：t0： ）. 它有一个子项proper yi，对于T（F;X）的n y t，f（：：：t：：：）t。注意，如果是F-稳定的且具有子项性质，则它是诺特的。此外，如果通过替换是稳定的（对于任何替换，一对项t;t02T（F;X）;tt0蕴涵tt0），那么它被称为单化序。设t是T（F）的一个项;让我们回想一下，t终止当且仅当从t开始的任何重写推导（或推导链）是nite。3采用当地策略我们现在解决用算子上的局部策略重写的终止问题，如[13]中所表达的和[7]中所研究的。局部策略的定义如下。定义3.1关于T（F; X）的LS重写策略（或LS-策略）（分别T（F）的函数LS）是从F到整数列表集合L（N）的函数LS，定义重写策略如下。给 出 了 一 个 LS- 策 略 ， 使 得 LS （ f ） =[p1; ： ;pk] ， pi2[0 ： ： arity（f）]，对所有i2[1：：k]，对某个符号f2F，正规化项t=f（t1;：;tm）2关于LS（f）= [p1;：;pk]的T（F; X）（resp2T（F）），在于根据该策略连续地将t在位置p1;：;pk处的所有子项如果存在i2[1：：k]，使得p1;：;pi1= 0且pi= 0（0是最高位置），则如果在归一化tj p;：;tj p之后获得的当前项t 0在顶部位置可约化为项g（u 1;：; un），则g（u 1;：; u n）相对于L S（g）被归一化，并且策略[pi+1; ：;pk]的其余部分被忽略，如果t0在顶部位置处不可约，则t0相对于pi +1;：; pk归一化。在重写步骤中，项t被称为LS-重写为项t0。 如果t不重写LS-策略，则称其为LS-正规形式（或如果没有歧义则为正规形式）。如果从t开始的任何LS重写链导致LS范式，则t被称为LS终止（或LS终止）。 如果t0的评价策略是empty表，则t0是LS-正规型.在下文中，我们将使用一个概念来表示t的任何实例化关于LS-策略的可能可约位置。定义3.2如果LS-策略允许在位置p重写t，或者如果LS-策略允许在位置p或在p的一个succumx位置重写t的任何基实例，则项t2T（F; X）的位置p是t中的LS-位置。菲索尔、格奈迪格和基什内尔6：Si2LS（f）fi：pjp2LSPOS（ui）gif 06 2LS（f）;fgSi2LS（f）n0fi：pjp2LSPOS（ui） gif 02LS（f）;项t的LS位置的集合LS P OS（t）可以以以下方式计算。LSPOS（f（u1;：;un））=LSPOS（x）=8fgifx2X;：; ifx2 N：3.1地方战略为了证明T（F）的一个项t LS-终止，我们在T（F）上用一个Noether序（更确切地说，是一个具有子项proper ty的F-稳定序）进行归纳，假设对任意t 0，t t 0满足tt0，t0LS-终止.首先证明了LS-极小元的一个基本集是终止的.由于需要的子项性质，极小元集是F的常数集的子集。然后我们考虑T（F）的任何项t的情况。为此，我们观察LS策略的重写导出树，从项tref=g（x1;： ;xm）开始，对于任何g2F，其中x1;：;xm是可以由任何基项实例化通过下面的两种机制来模拟基础项上的LS重写关系，以遵循从t_ref开始的导出树，并且其当前项是t。令LS（top（t））= [p 1;：; pn]，并且pk 是[p1; ：;pn]的 第 一 元 素 ， 使得pk=0。首先，子项tjp1; ：;t jpk1的值被LS归一化，通过对LS策略的定义。如果treftjp1; ：;t jpk1 通过归纳假设，我们可以假设这些子项是LS-终止的。然后，我们用抽象变量X i在t中替换它们，这些抽象变量X i分别表示它们的任何范式t i #：这些变量将仅由范式中的项实例化。 通过归纳推理允许我们只假设t i #的存在而不显式地计算它们;这一步骤将被称为抽象步骤或t的子项的抽象。我们还说t被抽象为项v。第二，在位置处重写结果项v，遵循v的所有可能的基实例。这是通过对v进行缩小步骤来计算的。可能发生两种情况：如果v在顶部位置不可描述，则v的子项vjpk+1; ：;v jpn必须LS归一化，并且我们尝试像上面那样抽象它们如果v在顶部位置处是可缩小的，则利用所有可能的规则和所有可能的替换1;：; 1来计算缩小步骤，以给出必须分别利用策略LS（top（w1））;：; LS（top（w 1））来考虑的项w 1;：; w 1。因此，上述两种机制再次应用于项w1;：; w1。此外，收缩不考虑的v的实例必须在以下位置减少：菲索尔、格奈迪格和基什内尔7p k+1;：; p n. 所以上面描述的两个机制也适用于v的位置p k+1;：; p n，对于v的实例不是iv; i 2 [1：：l]。该过程在具有空LS策略的当前项t上停止，或者在可以应用归纳假设的当前项上停止（即，使得t 参 考 t;在这种情况下，t被假定为LS终止）。注意，如果fp1; ：;png中不存在pk，则pk=0，则只处理t中的第一个p，从而抽象每个子项tjpi 的t;i2[1：：n]。3.2抽象我们现在给出一些新的定义来形式化上述机制。抽象需要使用表示LS-范式的特殊变量。定义3.3设N是与X不相交的一组新变量。N的符号称为NF变量。替换和实例化以如下方式扩展到T（F; X[ N]）。设X2 N ;对于任何替换（分别为实例化），使得X2Dom（），X（resp. （X）是正常的形式。注意，为了抽象当前项f（u1;：; um），对于已经是标准形式的基础项的uj引入抽象变量是没有用的，对于已经是NF变量的uj定义3.4项f（u1;：; um）在位置fi1;：;ipg[1：：m]处抽象为 f（U1;：; U m），如果：fi1; ：;ipg是[1：：m]的位置，使得ui1; ：;uip既不是正规形式的基项，也不是NF变量，其中Xj是一个新的NF变量，如果j2fi1; ： ：;ipg，则Ui=ui，否则。我们将证明T（F）上的LS-终止性，即关于T（F; X[ N]）的具有抽象变量的项的推理3.3约束现在让我们定义我们的证明过程所需的不同约束。与使用归纳的经典方法不同，归纳排序不是先验的。沿着证明设置约束，遵循必须应用归纳假设时出现的要求这样的排序约束被累积在一个集合C中，并且在必须应用归纳假设的任何时候测试C我们现在正式定义了排序约束的满足能力。定义3.5关于T（F;X[ N]）的排序const（t > t0）是可满足的，如果存在一个排序和至少一个实例使得tt0。 我们是这样的，并满足（t>t0）。菲索尔、格奈迪格和基什内尔8我如果存在满足所有合取的排序和实例，则排序约束的合取C是可满足的。空连词，总是满足的，用>表示。沿着我们的归纳过程，当抽象的子项t i的X i，我们的状态约束NF-变量表示，他们的实例只能是正常形式的相应实例的t i。它们的形式是t # =X，其中t2T（F; X），和X2N，或者更一般地形式是t#=t0，其中t;t02T（F;X[N）。 让我们把这种约束称为抽象约束.定义3.6一个抽象作用常数（t#=t0），其中t;t02T（F;X[N]）是满意的，如果存在至少一个实例满足t#=t0. 我们是一个满足es（t#=t0）的y。一个常数公式A是一个形式为V（ti#=t0）V（W（xk6= t0）的公式。iij kj jukj））， xkj2X[N;ukj2T（F;X[ N]）和（ti#=t0）是抽象的约束 空公式表示为>。 公式A是满意的，如果存在至少一种情况，使得V（ti#=t0）V（W（xk6= t 0））ukj））。我们说satis esA.iij kj j本文考虑由2-元组（A; C）组成的约束问题，其中A是约束公式，C是序约束的合取。定义3.7设A是一个约束公式，C是排序约束的合取如果A是可满足的，则约束问题（A; C）由一个排序满足，并且对于所有满足A的实例，和满足C.（A; C）是满意的，如果A是满意的，并且存在如上的排序。判定（A; C）的满足性需要表示满足A的所有实例。正如我们稍后将看到的，我们的方法的一个有趣之处在于，我们不需要描述所有这些实例化。展示其中一个就足以证明A的能力。 在这种情况下，一个序满足（A; C）的一个充分条件是它通过替换是稳定的（那么归纳序是一个单纯序），并且对于C的一个不等式t>t0，t0是稳定的.3.4缩小在将f（u1;：; um）项抽象为f（U1;：; Um）在位置fi1; ：;ipg之后，其中uij的基实例具有规范形式uij#，并用抽象变量Xij代替，通过对Xij的可能实例的句法形式的案例研究，检验了f（U1;：; Um）的基实例是否可约.该测试包括在位置处缩小f（U 1;：; U m），其中所有可能的替换实例化X i只有不可约项和所有可能的重写规则。现在让我们回顾一下窄化的定义菲索尔、格奈迪格和基什内尔9R定义3.8设R是T（F;X）上的TRS。使用重写规则l，项t在不可变位置p处被nar_din到t0！r和代换，其中n是t_p和l的最一般单位，t0=（t[r]p）. 这表示为t;p; l！r;t0其中p或l！ r或m aye省略。 总是假设规则和项之间没有共同的变量，即Var（l）\Var（t）= ;。不相交变量的要求很容易通过在执行收缩时对规则中的变量进行适当的重命名来满足 注意，对于在以上定义中使用的最一般的单位，Dom（）Var（l）[Var（t）]和we可以选择Ran（）\（Var（l）[Var（t））=1，这使得仅在新变量的范围内引入。ThusVar（t）\Var（t0）=;如果另外，Var（t）Dom（）的变量通过表示为仁正如我们将在下面看到的，在我们的证明过程中，我们还必须考虑替代的否定。定义3.9设是T（F; X[N]）上的一个替换，定义为Vi（xi=t i）xi2X[N，t i2T（F; X[N）。的否定，记为Wi（xi6=ti）。4基于规则的算法是公式4.1推理规则描 述 我 们 的 局 部 策 略 的 终 止 证 明 机 制 的 推 理 规 则 在 4 元 组 T=（fug;[p1; ：;pm];A;C）的集合上工作，其中：fug是T（F; X[ N]）的一组项，包含当前项u，其基实例必须证明是LS-终止的.不是一吨就是空的。[p1; ：;pm]是当前项u必须评估到的位置的列表。这是LS（top（u））的子列表A是一个约束公式，用于存储对当前项u执行的抽象和缩小替换。形式u# =X; u 2 T（F; X [N）;X2 N的子公式在每次当前项的子项u被新的NF变量X抽象时被陈述。C是由抽象步骤完成的排序约束的合取。现在让我们介绍推理规则。规则抽象处理抽象步骤。当存在k 2 [2：：n ] ; pk = 0且p 1 ;：;pk 1 6 = 0时，它适用于（f f（u 1;：：;um）g;[p1; ：：;pn];A;C）。项u=f（u1; ：;um）在位置i1; ：;i p2处被抽象fp1; ：;pk1g如果存在一个F-稳定序，其子项满足并证明（A;C^t=f >ui1; ： ：;uip）是令人满意的。事实上，B菲索尔、格奈迪格和基什内尔10T[f（ff（U1; ： ;Um）g; [0;pk+1; ：;pn]; A^（ui#=Xi）; C^tref>ui）抽象-停止：T[f（ff（u1; ：;um）g;[p1; ： ：;pn]; A;C）gMni=1我i=1我表1trefLS-终止的推理规则摘要：T[f（ff（u1; ： ： ;um）g;[p1; ： ：;pn]; A;C）g我我其中f（u1;：;u m）在位置：i2 f i1;：; i p g处被f（U 1;：：; U m）抽象fp1;：：：;pk1 g如果9k2 [2：：n]：p1;：;pk10;pk= 0且（A; C^i2fi1;：;ipgtref> ui）是满意的T[f（;;[];A; C^i2fi1;：;ipgtref> ui）g其中f（u1;：;um）可以由f（U1;：; Um）在位置：i1;：;ip2 fp1;：; pn g处抽象如果p1; ： ;pn6=0且（A;C^i2fi1;：;ipgtref> ui）是满意的N arrow-Y：T[f（ff（u1; ： ： ;um）g; [0;p1; ：;pn]; A; C）gT[i2[1：：l]f（f wig;return（i）;A^i;iC）g[ COM P L如果9使得f（u1;：; u m） ;w和A^令人满意其中wi;i2[1：：l];是使得f（u1;：：;um）;iwi和A^i满足的所有项;f（ff（u1;：;u）g;[p1：：p];A V;C）g如果（AV）满意：;否则：Narrow-N：T[f（ff（u1; ： ：;um）g; [0;p1; ： ;pn]; A; C）gT[f（ff（u1; ： ：;um）g;[p1; ： ： ;pn]; A; C）g如果f（u1;：;um）在顶部位置不可缩窄或f（u 1;：; um）在顶部位置的8个窄化替换;A^不满意：Stop-Ind：T[f（fug;[p1; ： ： ;pn]; A;C）gT[ f（;;[]; A; C^tref>u）如果（A; C^tref> u）满足Stop-A：T[f（ff（u1; ：;um）g;[p1; ： ：;pn]; A; C）gT[f（f）] g;[的];A;C）g如果p16=0且既不应用抽象停止也不应用抽象停止：停止：T[ f（ff（u1;：：：;um）g;[];A; C）gT[f（;;[的];A;C）g归纳hy命题，ui1的所有基础实例; ：; uipLS终止。 所以ff（u 1;：; u m）g被f（U 1;：; U m）替换。然后位置列表变成[0; p k+1;：; p n]。当当前术语的策略中没有位置0时，规则Abstract Stop如上所述处理抽象步骤。通过LS策略的定义，抽象后获得的项的任何基础实例都是不可LLCOM PL=菲索尔、格奈迪格和基什内尔11约的，这结束了当前推导链上的证明。菲索尔、格奈迪格和基什内尔121L我然后，包含当前项的集合被空集合替换规则Narrow Y在当前项u的位置0处处理缩小步骤。如果u可通过满足当前约束公式A的替换来缩小，则u在一个步骤中通过重写系统R的所有可能重写规则以及所有可能替换i，i，n到wi，i，2[1：：1]以所有可能的方式缩小。 然后（fu g;[0;p1; ： ：;pn];A;C）被替换为f（fwi g;LS（top（wi））; A^i;iC）;i2[1：：l] g，其中i是允许将u缩小为项w i的最一般的替换。此外，由于在A中，我们只记住对当前项u执行的抽象和缩小替换，并且由于Var（u）与TRS重写规则中出现的变量集不相交，因此我们可以在将i添加到A时将i限制为Var（u）。因此，在下文中，我们将i写成iVar（u）。这个缩小的步骤意味着，1u;：;lu是 u的所有实例，在顶部位置是可还原的它涉及到，如果=^：：^对于每一次替换，令人满意的是，u在顶部位置不可约。然后，由于这些u必须在位置处减少，[p1;：：; pn]， 如果满足，我们必须在前一个集合上加上这个集合：（fug;[p1; ：; p]; AVl;C）g. 注意，如果9isu ch，只是一个-ni=1i变量的命名，然后=;。让我们也精确地说，如果wi是一个变量x2 X，我们不能得出任何关于x的基实例的终止的结论。因此，我们强制证明过程停止，将LS（x）设置为特定符号]。然而，如果wi=X 2 N，LS（X）被设置为[]，这与X的任何基实例都是正规形式的事实是一致的。规则窄 N处理u在位置处0，或者可以用不满足当前约束公式A的替换来缩小。然后，不进行缩小处理，并在策略中顶部位置之后的位置处评估当前项。然后位置列表变成[p1;：：; pn]。我们还可以测试当前项是否存在具有子项性质的排序，使得（A; C^tref>u）是满意的。然后，通过归纳假设，u的任何基础实例对于LS-策略终止，这结束了当前导出链上的证明。然后，Stop Ind规则将包含当前项的集合替换为空集。规则Stop A允许在既不适用Abstract也不适用Abstract Stop时停止推理过程，用特定符号]替换u。规则Stop允许在位置列表为空时停止推理过程。表1中给出了推理规则集一旦应用了Abstract，求值列表的第一个元素就是0，所以唯一适用的规则就是fNarrow Y，Narrow Ng。当窄Y不适用时，窄N适用。当Abstract不适用，并且评估列表的第一个元素不为0时，菲索尔、格奈迪格和基什内尔13或者停止A适用，然后不再有任何规则适用。应用这些规则的策略是：重复 *（（抽象/抽象停止/停止A）;（窄Y/窄N）;停止;停止指示）其中“;”表示规则的顺序应用，r 1/：/r n表示规则r 1;：; r n是互斥的，并且其中一个将被应用，并且如果r 1 ;：; r n中的任何一个都不再应用，则repeat*（r 1 ;：; r n）停止。如果将推理规则应用于（fg（x1;：; xm）g; LS（g）;>;>），其条件由满足，给出状态在每一个分支上的形式（;;[]; A; C）。定理4.1设R是T（F; X）上的TRS，LS：F7！L（N）是LS-策略，使得F的常数LS-终止.如果存在具有子项性质的F-稳定序定义符号g，SUCCESS（ g;），则T（F）的每一项LS-终止。注意重要的一点，对于所有g（x1;：：; xm）2 Def，排序必须相同。还注意到的诺特性质是由F-稳定性和子项性质所隐含的。关于定理4.1的证明，以及下面的引理、命题和定理，见附录。在证明过程中，变量是NF-变量的信息对于得出结论非常重要：如果当前项是NF-变量，则其策略设置为[]，并应用Stop规则。当引入新的变量时，可以容易地推导出这些信息：通过定义，抽象过程直接对于窄化过程，其范围仅包含X的新变量的窄化替换可以通过将这些变量中的一些替换为NF-变量而转换为新的替换NF让我们考虑由窄化代换引入的形式X=u的等式，其中X是NF变量，并且u2 T（F;X）。由于X是一个NF-变量，u的任何基实例都必须是正规形式。所以u中可以被NF-变量替换的变量是出现在u中LS-位置的变量。现在设为替换（xi= xi; 8xi2 V ar（u）; xi出现在u; f中的LS位置或所有方程X= u of;X2N;u2T（F; X））。然后NF=.4.2归纳原理当归纳假设不能应用于项u时，归纳推理可以如下完成有时可以证明ui的任何基实例的终止（分别为（二）另一种方式。设项IN（u）是在u的任何基实例LS中为真的谓词菲索尔、格奈迪格和基什内尔14终止。在Abstract，Abstract Stop和Stop Ind中，我们可以将条件t >ui替换为某个i（resp. t > u）由替代谓词TERM IN（ui）（分别为项IN（u））。显然，在这种情况下，排序约束t > ui（resp. t > u）不加到C上。在[12]中，为了确定项IN（u）为真，在某些情况下，可以使用可用规则的概念。给定T（F; X）上的TRSR和项t2 T（F; X[ N]），对于标准重写关系，我们确定可能应用于其任何基础实例的唯一重写规则，直到达到其基础范式（如果存在的话然后，我们试图找到一个简化排序N，使这些规则是有方向的。因此，对于标准重写关系，任何基实例t都必然终止：事实上，如果t！ t 1！t 2！：，那么，由于前面的假设，tNt1Nt2N：并且，由于排序N是诺特的，所以重写链不可能是尼特的。更正式地说，给定一个TRS R，我们称一个项t 2 T [N]的可用规则为R的规则集的可计算超集U（t），该超集用于从任何t开始的所有可能的LS-推导，定义如下。 当t是X的变量时，t的可用规则就是R本身。同样，与NF变量相关联的可用规则集是空的，因为这样的变量的唯一可能实例是范式中的基础项 当t的形式为f（u 1;：：：; u n）时，则t的可用规则是u i的可用规则，其中i2L S（f）; i6=0并且，如果0 2 LS（f），则所有的规则l！ r具有符号f作为的顶部符号lhsl，连同项r的可用规则的集合U（r）。因为一般来说r包含X的变量，所以对U（r）和U（t）的求值很可能导致整个规则集R。为了计算一个较小的可用规则集，比如缩小替换，我们将尽可能多地用NF变量替换这个想法是，r中某些变量的可用规则可以省略，因为它们包含在ui的可用规则中。更准确地说，用l重写t！在顶部位置的r与接地替换导致术语r。设x是出现在l的lhs中的变量！ r在LS位置p处。 根据重写的定义，我们有x = tj p。此外，p是t中的LS位置，如果x出现在r中的位置p0，我们有rjp0 =t j p. 此外，我们需要U（x）（U（r）），仅考虑规则可以应用在Rjp0的推导中。但当rjp = tjp，并且对于某些i，可以应用于tjp的推导的规则被包括在U（u i）中，我们可以在U（r）的计算中抑制U（x）的计算。这些事实的正式证明可以在引理4.3的证明因此，为了计算t的可用规则，我们变换每个规则l！ R的一个规则NF（l！ r）= l！ 其中是取代基（xi=xi; xi2X;xi2N;8xi2 Var（r）并 且 xi在l中的LS位 置）。我们记NF（R）为集合fNF（l！ r）j l！ r 2 Rg.LS重写的可用规则的形式定义如下。菲索尔、格奈迪格和基什内尔150Rls（f）Si2LS（f）;i=0U（u）Sl！r2Rls（f）U（r）if02LS（f）定义4.2设R是符号集F上的TRS。设Rls（f）=f l！r2Rjtop（l）=fg，且Rls0（f）=fl！ r02NF（R）j top（l）=fg. F或nyt2 T（F;X[N]），t的可用规则集，记为U（t），由下式定义U（t）= R ift2 X，U（t）=;ift2 N，U（f（u1;：;un））=>我0 0：>Si2LS（f）;i6=0U（ui）否则：引理4.3L设R是一个符号集F上的TRS，R0=NF（R）且对每个L！r02R0，在LS-位置上没有变量Xoc在r0中出现. Lett2T（F;X[N]）。 不管结果如 何！p1;l1！R1 t1！p2;l2！r2t2！ “ ……”pn;ln！rntnLS-从r omt开始重写链，然后8i2[1：：n]：li！ r i2 U（t）.然后，我们可以给出一个足够的标准，以确保终止的标准重写关系（然后LS-终止）的任何基实例的一个条款t。命题4.4L设R是一个符号集F上的TRS，R0=NF（R）， 且对 每一个L！ r02R0 ， 在LS-位置上没 有 变 量 Xoc在 r0中出现. 设t = 2T（F;X[N]）. 如果存在一个简单的排序，使8 l！r 2U（t）：l r，则t的任何基实例都是终止的。注：如果存在一个单序，使得l Rfor任何重写规则l！r，则对任意给定的符号g2DefR和任意具有子项性质的F-稳定序0 ，有SU CCESS（g;0因此，定理4.1适用。事实上，对于任何tref=g（x1;：;xm），我们有U（tref）= R，每个规则都是由。最后，感谢命题4.4，我们有TERM IN（tref），然后应用Stop Ind这种方法的一个有趣之处在于，可以使用的确定可用规则的方向完全独立于归纳排序0的情况。现在让我们用引言中给出的例子来说明我们的完整方法。例4.5回想一下，规则是：f（i（x））！ite（zero（x）; g（x）;f（h（x）zero（0） ！真正0（s（x）） ！ 法阿尔塞int（true; x; y）！ Xite（f alse; x; y）！ yh（0）（0）菲索尔、格奈迪格和基什内尔16h（x）！s（i（x））菲索尔、格奈迪格和基什内尔17LS策略如下：LS（ite）= [1;0]，LS（f）=LS（零）=LS（h）=[1; 0]，LS（g）=LS（i）=[1]。让我们证明这个系统在签名F = ff：1; zero：1; ite：3;h：1;s：1;i：1;g：1; 0：0 g上的终止性。显然，常数0 LS-终止。在f（x1）上应用推理规则，我们得到：f（x1）[1; 0]A= >C=>摘要f（X1） [0]A=（ x1# =X1） C=（ f（ x1）> x1）抽象适用，因为C可以满足任何具有子项性质的排序A可以满足任何实例化使得x1=X1= 0。窄Yite（zero（X2）;g（X2）; f（h（X2）=（X1=i（x2）^x0=x2）N F=（X1=i（X2）^x0=X2）[1;0]A=（ x1#= X1^ X1= i（ X2）） C=（ f（ x1）> x1）f（X1）[]A=（x1#=X1）^（X16=i（X2））C=（f（x1）>x1）注意x0来自rst规则中x的重命名。 将x 2重命名为X 2是因为x 2出现在i菲索尔、格奈迪格和基什内尔18（x 2）的LS位置。这里，第一约束公式A可通过任何实例化来满足，使得X2= 0且x1=i（0）。第二个约束公式由任何实例满足，使得x1=X1=X2= 0。窄 Y表示这样一个事实， f（X1）是可约的，如果使得X1=i（X2），并且其他实例（0f（X1），其中0X16=i（X2））菲索尔、格奈迪格和基什内尔19不能减少。停止ite（zero（X 2）; g（X 2）;f（h（X 2）[1; 0]A=（ x1#= X1^ X1= i（ X2）） C=（ f（ x1）> x1）;[]A=（x1#=X1）^（X16=i（X2））C=（f（x1）>x1）停止应用，结束第二个分支。摘要ite（ X3; g（ X2）;f（ h（ X2）[0]A=（ x1#= X1^ X1= i（ X2）^ zero（ X2）#= X3） C=（ f（ x1）> x1）;[]A=（ x1#= X1）^（ X1 C=（f（ x1）> x1）i（X2））约束公式A对任何实例都是满足的使得X1 = i（0），X 2= 0