基于规则的编程语言中的终止问题的证明环境

188理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html20页最外侧接地终端奥利维耶·费索1，伊萨·贝勒·格纳迪格1，和H'el'eneKirchner1LORIA-INRIA LORIA-CNRS，54506V和o euv re-l`es-Nancy，BP239 C edex，France.摘要我们提出了一个半自动的归纳过程来证明基项代数上最外层重写该方法是基于一个抽象机制，图式规范化的子项，并缩小，图式减少地面条款。归纳排序不需要先验，而是沿着证明的约束集的解决方案我们的方法特别适用于标准策略的非终止系统，甚至也不适用于懒惰策略。关键词：重写，终止，最外层，策略，基于规则的1介绍问题重写的终止性是自动演绎中的一个关键问题，对于等式逻辑，以及在程序设计中，对于基于规则的语言。该性质本身很重要，但它也需要决定的性质，如一致性和充分完整性，或允许证明的一致性。现有的大多数证明项重写系统（简称TRS）终止性的方法本质上是解决通用终止性问题：它们在自由项代数上工作，并证明标准重写（没有任何策略的重写）的终止性许多是基于句法或语义的诺特[2019 - 05 - 15][2019 - 05 - 15][2019 - 05][2019 - 05 - 15][2019 - 05 - 15]其他方法包括将TRS R的终止问题转换为另一个TRS RJ的终止问题，可以用以下技术证明：前一类。[25]这是一个很好的例子。dency pair方法[2]。在 本 文 中 ， 与 [16] 一 样 ， 我 们 解 决 了 基 于 规 则 的 编 程 语 言 （ 如ASF+SDF[17]， Maude[5]， Cafe-OBJ[13]或ELAN[4]）的证明环境中的终止问题，其中程序是1电子邮件：{fissore，naedig，Helene.Kirchner}@ loria.fr2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。菲索尔、格内迪格和基什内尔189−→→→ →−项重写系统和查询的评估包括重写基础表达式。在这种情况下，需要比前面引用的更具体的终止证明工具，允许在具体的约简策略下证明在这一领域取得的成果仍然很少，尽管这一需要很重要。 据我们所知，方法只给出了最内层策略[1，14]，上下文敏感重写包括特定类型的局部策略[21]和一般局部策略[10]。在编程环境中计算表达式的最外层策略主要用于当人们知道计算可以是非终止的时候。直觉表明，重写一个项在最高可能的位置比另一种策略有更多的机会导致一个不可约形式。实际上，当最内层失败时，最外层重写可能成功，如表达式second（dec（1），0）所示，重写规则为second（x，y）y和dec（x）dec（x1）整数。最内层的重写无法终止，因为它首先将dec（1）求值为dec（0），dec（1），依此类推。然而，最外层的重写在一个重写步骤中给出0。此外，最外层的推导通常更短：在我们的例子中，为了减少second（u，v），不需要减少u，这可能导致无限计算，或者至少导致无用的求值。这种优势使得最外层策略成为基于规则的语言的有趣策略，因为它允许解释器更高效，以及定理证明，因为它允许基于重写的证明更短。最外层的计算对于Miranda、Haskell或Clean这样的函数式语言特别感兴趣，其中解释器或编译器通常涉及按名称调用的策略通常，使用惰性求值来代替：将操作符标记为惰性或渴望，它包括仅当它们的减少允许在项中更高的减少步骤时才减少渴望子项[23]。然而，惰性计算可能会在最外层计算终止时发散，这为研究最外层终止提供了额外的动机。例如，让我们考虑用以下两个规则计算表达式inf（0）：cons（x，cons（y，z））big，inf（x）cons（x，inf（s（x）.以惰性方式求值，inf（0）被还原为cons（0，inf（s（0），然后，由于第一个规则的应用失败，在考虑整个表达式之前，必须对子表达式inf（s（0））求值，这导致无限求值。以最外层的方式计算，inf（0）也被简化为cons（0，inf（s（0），但随后inf（s（0））被简化为cons（s（0），inf（s（0），然后整个表达式被简化为big。虽然通常不与基于规则的评估过程一起使用，但出于前面的效率原因，最外层的策略可能对Maude，OBJ或ELAN等语言感兴趣更好地了解这一战略w.r.t. 在这种情况下，更常见的策略，如最内部或局部策略，会很有趣，并且可以帮助在编程时选择好的策略菲索尔、格内迪格和基什内尔190X T FF∈T F X在这些语言中。特别是研究这些不同策略的终止问题，我们已经指出了这样一个事实，即它对于最内层、最外层和懒惰策略是不同的：这些策略之一的终止并不意味着它们中任何其他策略的终止[12]。函数语言的延迟终止已经被研究过了（例如[24]），但据我们所知，没有终止证明工具可以专门证明重写的最外层终止。我们在这里提出了一个证明方法检查终止最外层的计算，即使重写没有策略或与其他策略分歧。我们的终止证明方法最外层重写地面条款是基于一个明确的诱导机制的终止属性。其主要思想是使用归纳法的终止性质，以证明任何元素t的一个给定的一组条款T终止，即。没有从t开始的无限衍生链。因此，这种方法需要对归纳原理中使用的术语进行诺特与经典归纳证明不同，在经典归纳证明中，排序是给定的，我们不需要先验地定义它。我们只需要通过确保沿着终止证明递增地设置的排序约束的满足性来检查它的存在性由于归纳的力量，生成的约束往往很容易解决。该方法是基于抽象机制，图式规范化的子项，并缩小，图式减少地面条款。它是半自动的：它可以在成功时停止，然后建立给定TRS的外部终止;它可以在失败或发散时停止，在这种情况下，无法对终止做出任何结论约束求解可以由过程本身处理，也可以留给用户或委托给外部自动约束求解器。第2节介绍了背景情况第三节介绍了归纳证明机制的基本概念。第4节建立在这些概念的基础上，提出了最外层终止的证明技术。 可以在[12]中找到证据。2背景我们假设读者熟悉例如在[9]中给出的项重写的基本定义和符号。 （，）是从给定的有限的一组具有元数nN的函数符号f和一组表示为x，y..的变量构建的项的集合。. .（）是基本项的集合（没有变量）。由一个零元符号组成的项称为常数。项中的位置表示为整数序列。空序列表示顶部位置。设p和pJ是两个位置。位置p被称为pJ的（严格）prefix（和pJsuf x ofp）ipJ=pλ，其中λ是一个非空的整数序列给定一个项t，Var（t）是t的变量，O（t）是t的位置集合，归纳定义如下：如果t∈ X，则O（t）={<$}<${i.p|1 ≤i≤n且p∈ O（ti）}如果t =菲索尔、格内迪格和基什内尔191|∈OOTF X›→›→XTF X›→›→ T F XFR→ T F XRT F X→R↓↓T F∈ TF X>>>F X>F联系我们联系我们>>F> T F Xpf（t1，.， tn）。我们将V（t）表示为t中变量位置的集合。符号tp代表t在位置p处的子项。如果p（t），则t[tJ]p表示通过将位置p处的子项替换为项tJ而从t获得的项。替换是从到 （，），写作σ=（xt）. （y u）。它唯一地延伸到一个自同态（ 、）.我们确定了一个代换σ=（xt）. （年u）用有限方程组（x=t）...（y=u）。 将σ应用于项t的结果（，）记作σ（t）或σt。σ的定义域，记作Dom（σ），是X的有限子集，满足σx/=x。 σ的范围，记作Ran（σ），由y定义Ran（σ）=x∈Dom（σ）Var（σx）. 我们还得到了Dom（σ）<$Ran（σ）=R. 一基替换或实例化是从X到T（F）的赋值。的置 换 σ1 后 接 σ2 的组合表 示 为 σ2σ1。 给 定 两 个 代 换 σ1 和 σ2 ， 我 们 记 为σ1≤σ2[X]i∈θ，使得σ2=θσ1[X]i. e.σx∈X，σ2x=θσ1x（σ1比σ2更一般）. 对于X的一个子集X1，我们把σ限制在X1的变量上，记为σX1，即： 置换条件是Dom（σX1）<$X1且<$x∈Dom（σX1）：σX1x=σx.给定一组重写规则（一组 （ 、 ），表示为l r，使得V ar（r）V ar（l））或项重写系统on（，），a 函数符号在中被称为构造函数，如果它不出现在规则左侧的顶部位置，则称为定义函数符号否则，请执行以下操作。F对于R的定义函数符号的集合由Def R表示（当没有歧义时，R被省略）。由R诱导的重写关系表示为→R（→如果R上没有歧义），并且由s → t i定义，在s中存在替换σ和位置p，使得s|p= σl，且t =s [σr] p. 记为s →p ， l→r ， σt，其中p或l→r或σ可以省略 ;|p称为redex。transitive（传递）表示R诱导的重写关系的一个（自反传递的）by+R （分别）→A）。如果t→tJ且tJ不能再重写，则tJ为称为t的标准形式，用t表示。注意，给定t，t可以是不是唯一的。在（，）上的一个排序被称为noetherian，因为对于这个排序，没有无限下降链它对任意一对项t，t，J都是-稳定的，（、），对于任何上下文f（. .. . ），ttJ意味着f（. t.. . ）f（. tJ.. . ）.它具有子项性质i，对于（，），f（. t.. . ）t。注意，因为和有限，如果是- 稳定且具有子项性质，[19]这是一个很好的例子。如果，另外，通 过 替 换是稳定的（对于任何替换σ，任何一对项t，tJ（、） ， ttJ 蕴 含σt ，则称之为简化序。让t是（）的一个项;让我们回想一下t终止于i，从t开始的每个重写派生（或派生链）都是有限的。我们说，最外层的s在位置p重写为t，s→out tis在位置p重写为t，并且没有prefix位置pJ使得s在位置PJ重写。设t为T（F）的一个项，如菲索尔、格内迪格和基什内尔192↓R→∩ ∪∅⊆∪RT F X>∈ D>T F>∈DT F在标准重写中，我们说toutermost终止i，从t开始的每个最外层重写派生都是有限的。从现在开始，t表示t的最外层（重写）范式。现在让我们回顾一下缩小的定义。让一个TRS上（ 、）.项t在不可变位置p处被缩小为tJ，使用重写R的规则l → r和置换σ，i ∈ σ是t的最一般的单位元|p和l，且tJ= σ（t [r] p）.这表示为t p，l→r，σtJ，其中p或l r或σ可以省略。 我们总是假定规则和项之间没有共同的变量，即。e. Var（l）=Var（t）=V a r（t）。不相交变量的要求很容易通过适当的在执行缩小时重命名规则中的变量注意，对于上述定义中使用的最一般的单位元σ，Dom（σ）Var（l）Var（t），我们可以选择Ran（σ）（Var（l）Var（t））=，从而在σ的范围内只引入新的变量。3终止妊娠诱导主要的直觉是观察从作为项g（x1，.，xm），对于某些定义的函数符号g ef，以及变量x1，...，x条纹鲈证明在基项上的终止等于证明所有这些最外面的重写导出树只有有限个分支。为了证明（）的每一项t最外终止，我们继续通过归纳（）与诺特序，假设对于任何tJ，使得t tJ，tJ最外终止。我们首先证明了一个基本的最小元素的最外层终止。正如我们将看到的，假设子项的终止来证明项本身的终止是很自然的所以>的subterm属性是必需的，然后是>是F的常数集的子集。然后，我们从g（x1，.， xm），对于所有的gef，证明所有分支都是有限的。每个导出树由从g（x1，.，xm），并通过交替使用两个主要概念，即缩小和抽象来开发。更确切地说，由于所有可能的窄化单位，窄化图式化了推导中基础项的所有最外层重写可能性 抽象过程根据最外层策略模拟派生中的子项的正规化。这个抽象步骤是在可以假设为最外终止于归纳假设的子项上执行的。因此，证明过程相当于开发抽象树，其节点由可能具有变量的当前项和由约束适当表示的一组基础替换组成。这个约束是由用于缩小的连续单位器的合取产生的，从g（x1，...， xm）到目前为止。每个节点模式化一个可能为空的菲索尔、格内迪格和基什内尔193∈ D{} TF {}RT F基础项的集合，即由作为约束的基础解的替换给出的当前项的所有实例显然，归纳排序>必须沿着证明是相同的：对于每个抽象树中具有根g（x1，.， xm），g ef，和所有的抽象树然而，重要的是要指出证明方法的灵活性，它允许使用不同的技术与辅助终止证明相结合：当归纳假设不能应用于项u时，有时可以通过另一种方式证明u的每个基实例的最外终止在下文中，我们将使用一个谓词TERMIN（u），它是真的，i表示u的每个基础实例最外面终止。本文给出的终止证明过程由一组采用特殊策略S. 为了证明R在每个项t ∈T（F）上的终止性，我们进行如下：对于每个定义的符号g ∈ Def，我们考虑所谓的参考项tref= g（x1，...，xm）和一个平凡的约束集T.将根据策略S的规则应用于初始状态（g（x1，...， xm），）构建一个证明树，其节点是由推理规则产生的状态分支是通过对所有可能的重写规则进行不同的收缩步骤来获得的不同类型的约束出现：过程中的等式、不等式和约简约束以及过程结束时的排序约束如前所述，终止证明程序的行为有三种情况。好的情况是当策略终止时，因为规则不再适用，并且所有证明树的所有终端状态都有一个空的项集当规则不再适用于具有非空项集的状态时，该策略也可以以失败而停止最后，如果对其中一个参考条款的规则的应用次数无限，则该规则不得终止在最后两种情况下，我们不能对终止做出任何结论4最外端接让我们以更详细的方式重新考虑以前的想法。考虑下面的例子，它是最外层终止的，但对于标准重写关系，也不是最内层策略，甚至也不是惰性求值策略。f（g（a））→af（x）→bg（x）→f（g（x））让我们先用“手”来证明，最外层终止于（）（=f：1，g：1，a：0，b：0），以如下方式。 首先，考虑常数a和b：它们显然是最外层终止的。那就让我们菲索尔、格内迪格和基什内尔194>>↓↓/∈F研究f（t）型基本项的终止问题。如果t=g（a），f（t）最外层重写为a，这是正常形式。类似地，如果t的形式为f（tJ），则f（t）重写为b。否则，f（t）在顶部位置不可约。利用一个具有子项性质的序作为归纳序，我们得到f（t）t.所以，通过归纳假设，我们假设t在最外层终止。现在，要么t是不可约的，然后，由于f（t）在顶部位置不可约，f（t）是正规形式，要么t正规化为 t.设tJ是从t到t的最外归约链的任何中间项。或者f（tJ）在最上面的位置最外可约为a或b， 或者最外面的redex在tJ中。在第二种情况下，tJ被简化为另一个中间项，我们可以在其上应用相同的推理。由于t被假设为终止的，中间项的数量是有限的，这允许得出f（t）最外面终止的结论。最后研究了g（t）型基项的终止性。任何g（t）形式的基项首先重写为f（g（t））。然后，如果t=a，则f（g（t））归一化为a。如果t=a，则f（g（t））最外层重写为f（f（g（t）的第三条规则。最后，得到的项用第二条规则重写成b，证明结束。让我们展示如何形式化和自动化这样一个推理与狭义-抽象和抽象。4.1感应如前所述，我们观察到从t_ref= g（x1，.，xm），对于每g，其中x1，...，xm是变量，可以由任何基项实例化最外层的重写关系通过如下的缩小和抽象来模拟：• 首先，我们观察到从g（x1，.， xm），遵循x1，.，xm，直接在顶部或还原后在顶部的subterms。实际上，g（x1，...，xm）可以直接在顶部可约化，或者在变量x1，...， x条纹鲈因此，为了精确地对基础项上的最外层重写关系进行建模，我们首先要替换x1， .. . .. ，xJm定义如下。给定任何基实例αg（x1，...， xm）的g（x1，...，xm），XJ1， . ，xJm表示αx1， .. . 的 第 一 个 约 化 形 式 。 ，αxm生成项中较高的最外约简（此处，在顶部），在任何从αg（x1，...， xm）。我们记住这个替换，并对g（XJ1，...，xJm）以所有可能的方式得到项v。这是缩小的步骤。• 然后，我们的想法是尽可能有效地将归纳假设应用于每个所得的窄项v。为此，我们试图将这种归纳假设应用于大小）v的子项vi，用变量yi代替它们，表示它的任何正规形式。其实，当菲索尔、格内迪格和基什内尔195>↓↓↓↓vi越小，满足排序约束的机会就越大tref> vi.根据最外层策略，只有当在它们的标准化期间，vi不引入在项v中更高的最外层赎回时，才能做到这一点。更正式地说，归纳假设适用于子项v|p1，...，v|当前项v的p n，前提是αt>αv|p1，...，αv|pn，对于归纳序>，对每个基代换α，给出s=v[y1]p1... [yn]pn对于最外层的窄化关系来说是不可窄化的，定义如下：下面这意味着项s最外层的每个基实例都终止。这是抽象步骤，这是它应用于证明树的分支上的最后一步如果v不能被抽象，我们再次尝试一个缩小的步骤。• 我们的机制还包括归纳假设可以直接应用于当前项v的情况，当αtrefαv对于每个基替换α，这结束了对v的分支的证明，因为t的导出树中从v开始的每个导出都被假设为通过归纳终止。实际上，这种情况是抽象步骤的一种特殊情况。4.2最外侧狭窄我们首先正式定义在缩小步骤之前执行的变量替换。定义4.1设t ∈ T（F，X）是一项，其变量在t中从左到右出现次数为x1，.，x条纹鲈t的归约重命名包括重新-把xi放在t中的新的和所有不同的变量xJi上，并由所谓的归约公式表示R（t）=（x1→nxJ1， . ，xm→nxJm）[t]。应用于t的归约重命名的结果表示为Ren（t）。通过交替使用归约重命名和缩窄步骤来模拟最外层的归约关系，给出了归约公式的满足性定义4.2设t ∈ T（F，X）是一项，其变量出现次数从左到右为x1，. xm，在位置p1，.，pm分别。基替换θ满足公式R（t）=（x1→nxJ1， . ，xm→<$xJm）[t]i <$存在从θt开始的最外重写链，使得t[θxJ1]p1.. . [θxJm]pm是θt=t[θx1]p1的 第 一 个 约 化 形 式 。 . [θxm]pm在该链中具有在t的不可变位置处的最外重写位置，如果该位置存在，或者θxJ1=（θx1），.，θxJm=（θxm），如果没有这样的位置。在继续之前，可以对这个定义做一些评论。在第二个满足条件的情况下，t[θx1]1。 . [θxm]misinnormalform. 此外，R（t）总是令人满意的：取一个基础假设就足够了菲索尔、格内迪格和基什内尔196{→ →}∈T F X联系我们∧{→ →}tionθ使得t[θx1]p1.. . [θxm]pm在t的非变量位置处有一个最外重写位置，然后将其定义域{x1 ， . ， xm}到 x1 ， . ，xm ，xJ1 ， . ，xJm我是 一 个 很 好 的 朋 友 ，1、... ，m，θxJi=θxi. 如果sucha替换不存在，则t的每个基实例都没有最外层在t的非变量位置重写位置，取一个基替换θ使得θx1=... = θxm= θxJ1 =.=θxJm=u，其中u为正规形式中的任何基项然而，可能存在这样的约束的几个替代解决方案。让我们考虑例如重写系统R =f（a）f（c），b a和归约公式R（f（x））=（x→nxJ）[f（x）]。代入θ1（x）=θ1（XJ）=a和θ2（x）=b，θ2（XJ）=a是两个不同的解。 与代入θ2，f（a）是f（b）的第一个约化形式，其最外重写位置在f（x）的不可变位置（这里在顶部）。最后，通常情况下，简化公式可以简化为简单的重命名。设t（，）是一项，其变量为x1，.，xm，在位置p1， . ，pmres pecti vel y.让我们考虑R（t）=（x1→nxJ1， . ，xm→nxJm）[t]设It={i ∈ [1. m] |t在预定位置进行最外层重写pi的pJi}。则R（t）是等价的（在同一组基的意义上），替换满足这两个公式）到R（t）i∈ItxJi=xi。对于任何θ满足R（t），对于任意i∈It，t[θx1]p1. . [θxi]pi.. . [θxm]pm有一个值在t的不可变位置处的最外重写位置：位置pJi或者是pJi的一个预置位置。那么我们有θxJi=θxi。为了说明这一点，让我们考虑系统g（x） x，f（x，x）x（规则的右边在这里并不重要），以及约简公式R（f（x，g（y）=（x →xJ，y →yJ）[f（x，g（y））]。那么既然f（x，g（y））在g的位置处最外重写，R（f（x，g（y）等价于借给RJ（f（x，g（y）））=（x→nxJ）[f（x，g（y））]y=yJ.实际上，无论基实例θy如何，g（θy）最外层项只在顶部位置重写，θy没有最外层约化。然后，根据定义4。2,θyJ=θy。最 后，注意，如果It={1，.， m}，则R（t）等价于在t中重命名。Mi=1 xi=xJi，其中xi是从左到右的可变出现次数为了在基本项上对最外层重写进行模式化，我们需要引入一个新的特定窄化关系。定义4.3一个项t∈ T（F，X）的最外端缩窄为一个项tJ∈T（F，X）在非变量位置p，使用规则l → r ∈ R，最一般的单位元σ，p，l→r，σ tJi(i) σ（l）= σ（t|p）和(ii) tJ=σ（t[r]p），(iii) 不存在p的预定位置PJ，不存在R的规则LJ→RJ，也不存在使σJ能统一σt的置换σ j|pJ和lJ。菲索尔、格内迪格和基什内尔197它总是假设规则之间没有共同的变量菲索尔、格内迪格和基什内尔198|→|/∧和术语i。e. Var（l）=Var（t）=V a r（t）。上述定义的第三点并没有出现在经典的缩小的定义。这里需要这个特殊的条件来定义一个最外层的缩窄机制，该机制对基项上的最外层重写应用于给定项t的最外面的缩小步骤以下面的方式计算。我们观察t的每个位置p，使得tp与使用替换σ的规则的左侧一致。位置p是t的最外面的窄化位置，根据定义4.3，如果没有t的prefix位置pJ使得σt|p是左手边规则的单位。然后，我们寻找p在t中的每个prefix位置pJ，使得σtpJ随着一些替换σJ和一些规则lJrJ，并且我们设置一个约束来排除这些替换。让我们考虑前面的系统{f（g（a））→a，f（f（x））→b，g（x）→f（g（x））}。在最外层位置使用标准缩窄关系时，f（g（x1））仅使用第一规则和替换缩窄为aσ=（x1= a）。利用上面定义的最外层缩窄关系，f（g（x1））利用第一规则和σ =（x1= a）缩窄为a，利用第三规则和满足不等式x 2 = a的替换σ =（x1=x2xJ= x2）缩窄为f（f（g（x 2）。注意xJ来自于规则中变量的重命名如这个例子所示，根据定义4.3，用来缩小一个项的替换一般必须满足一组不等式。为了使这句话精确，我们需要一些符号和定义。设σ是T（F，X）上的一个代换，用公式i（xi=ti）表示其中xi∈ X，ti∈T（F，X），其中=是句法等式。我们表示用σ表示公式i（xi/=ti）。定义4.4替换σ有助于满足公式i ji（xji/=tji），i i ∈所有基实例化α，i ji（ασxji/=ασtji）。在证明过程中，我们记住先前定义的变量的归约替换约束公式中连续缩小步骤中使用的不等式的替换（也称为约束替换定义4.5替换约束公式（简称S CF）是一个for-mulal（xl1 →∗ xJl1，.，xlm→ xJlm）[ul]i（xi=ti）j（kjxkjtkj），其中xl1，xJl1...， xlm，XJLM，xi，xkj∈ X，ti，tkj∈ T（F，X）. 空公式记为T.然后证明树的节点由当前项和由替换约束公式表示的一组基替换组成。每一个节点图式化一个可能为空的基项集合，即由替换给出的当前项的所有实例，所述替换是替换约束公式的基解。菲索尔、格内迪格和基什内尔199>>> >∅> T F>∈∪∩定义4.6一个替换约束公式l（xl1 →∗ xJl1，.，xlm →∗xJlm）[ul]i（xi=ti）j（kjxkjtkj）被认为是可满足的条件是，存在一个假设nθ，使得i（θxi=01-02kjθxkj/= θtkj）和θ满足l（xl1 →∗ xJl1，.，xlm→ xJlm）[ul]。在实践中，可以解决约束的等式和不等式部分，然后检查解θ是否满足约化公式。这在θ仅实例化xJi的情况下是微不足道的，因为它可以通过设置θ（xi）=θ（xJi）来扩展不幸的是，当θ也实例化xi时，我们得到了一个不可判定的问题：给定两个基项t和tJ，不能通过重复应用一组给定的重写规则转换为tJ但幸运的是，我们的过程是合理的，即使在证明树的节点上应用推理规则表示空的术语集[12]。因此，在收缩步骤中，我们不试图检查约束的满足性尽管如此，我们保持跟踪的累积约束沿着一个分支的缩小步骤。如果在任何一点上，约束可以被证明是不满足的，那么分支可以被切断。对于抽象步骤，SCF的满足性必须与排序约束的满足性相结合。定义4.7设t，u1，...，um∈ T（F，X）和自洽场.约束（t，t > u1，...，如果存在一个F-稳定序，则称为满足- ing on（）具有子项性质使得θt θui，i [1.m]，对每个基代换θ满足π，且其定义域包含t和ui的变量，i ∈ [1. m]。 这样的排序>被称为满足（n，t > u1，.， um）。满足（t，t > u1，...，m）是不可判定的。但是满足这个约束的一个充分条件是，它通过替换是稳定的（归纳序是一个简化序），并且u1，...，嗯。注意，因此，（t，t > u1，.，也许是可以的，也许是不可以的。如前所述，我们将在缩小步骤之前执行的变量的归约重命名和在每个缩小步骤处使用的受约束替换存储在SCF中，用于将当前项u与规则l的左手侧统一，并且其域是Var（u）Var（l）。，我们不需要知道与出现在l中的变量相关的信息，因为我们只对应用于u的变换感兴趣。所以只有σ对V ar（u）的限制和每个σJ（见定义4.3）对V ar（σu）的限制的否定，分别表示为σVar（u）和σJV ar（σu），存储在存储器中。4.3抽象现在让我们形式化我们的抽象机制。术语的抽象u依赖于泛化的概念菲索尔、格内迪格和基什内尔200∃|||||∈TF X {}∈ T F X ∈ T F X- -T F X- -定义4.8术语t（、）是u的概括（、）iu是t的instance（即，σ，使得σt=u）。给定项u的两个推广s和t，称t大于si，s是t的推广。推广t称为线性推广，如果t是线性的。然后，抽象一个项u包括找到最大的线性广义化t，其中变量位于位置p1，.， pm这样，• 归纳假设适用于up1，即（t，tref> up1，.，m）是令人满意的，• 一般化nt=u[y1]p1.. . [ym]下午，当y1， .. . ，y，m是新的不同变量，是不可缩小的。下面的明显引理允许我们得出结论，如果u可以抽象为项t，则u的任何基实例都是终止的。引理4.9设u（， ）.设t是u的推广，并且p1，...， pm是t中变量位置的集合如果t不是可缩小的，则：(i) 在t的每一个基实例中，仅有的redex位置是pi，i的子集，[1] m]，(ii) 因此，如果Up1，...，upm最外端，则u最外端的每个接地实例终止。4.4推理规则表1中给出的最外层终止的推理规则适用于对（T，T），其中：• T是（，）的项的集合，包含当前项，其基实例必须被证明是最外终止的。这是单例或空集。• SCF是一个SCF，通过表达要缩小的项的变量的归约重命名和每次执行缩小步骤时的新约束替换的公式来丰富推理规则的工作原理如下：• 窄化步骤由应用于（u，n）的规则Narrow表示：u的变量被重命名为定义4.1中指定的。然后，Ren（u）在一个步骤中以所有可能的方式被最外缩小，其中所有可能的方式都是最外缩小的。将重写系统R的规则重写为项v。对于任何可能的v，（{u}，n）被（{v}，n∈R（u）nσVar（Ren（u））表示iσJiV ar（σRen（u），其中σVar（Ren（u））iσJiV ar（σRen（u））是定义约束子空间u的SCF使Ren（u）最外层缩小为v。• 抽象步骤由应用于（u，n）的规则Abstract表示：我们寻找当前项u的最大可能推广t，如4.3节所要求的。If（t，tref>u|p1，...，u|pk）对于{p1，...，pk}=V（t）和TERMIN（u|i）对于i∈ OV（t）\ {p1，.，pk}∈菲索尔、格内迪格和基什内尔201|||∈T F XRT F X，如果存在u最大线性推广检验，使得t不是最外面可变窄的，（，tref> u|p1，...，u|pk）对于{p1，...，pk} ≠ 0V（t），TERMIN（u|i）对于i∈ OV（t）\ {p1，.， pk}摘要：{u}，窄：{u}，{v}，R（u）我如果Ren（u）不含v，其中σVar（Ren（u））σ我σJiV ar（σRen（u）） 是受约束的置换允许Ren（u）的最外窄化为σ。表1最外层t引用终止的那么，通过第一种情况下的归纳假设，以及第二种情况下的假设，u p1，.u pk和u i终止。通过引理4.9，u的每个最外层的基实例终止，这结束了当前推导链上的证明。故（{u}，）由（，）代替。• 如前所述，我们也可以测试当前项u，（t，tref> u）是否满足或TERMIN（u）是否满足。然后，如前所述，通过归纳假设或通过假设，u的最外层的每个基础实例终止，这也结束了当前推导链上的证明这是抽象规则的一个特例，其中u的推广是变量y。为了确定TERMIN（u）为真，在某些情况下，[1]可以使用。给定TRS对（、）和项u（，），可用规则被定义为重写规则的可计算超集，其可以应用于u的任何基实例，对于标准重写关系，直到达到其基范式（如果存在）证明u的任何基础实例的终止性然后归结为证明其可用规则的终止性，这通常比定向整个TRS容易得多可用的规则可以用经典的终止方法如简化排序来证明终止-然后我们得到标准重写关系的终止，这意味着u的最外终止-或者用我们的归纳方法本身：然后我们直接证明u的最外终止。这种方法的一个有趣之处在于，用于证明可用规则的终止性的排序，无论是经典方法还是归纳法，都完全独立于主要的归纳排序。注意，我们的方法考虑了初始TRS可以用其他众所周知的方法（通过简化排序或使用依赖对来定向规则）证明终止的情况：菲索尔、格内迪格和基什内尔202{}T∅{} TF F>联系我们RT F Xg（x1，.，xm）组成的初始TRS，然后可以用前面提到的方法证明它们的终止性。还需要注意的是，为了证明常量的终止性，也可以使用可用的规则。可用规则的概念、它们的计算和它们的性质在[14]中得到了充分的发展。根据定义4.2后面的注释，在[1]中的归约在这种情况下，Abstract仅包含变量重命名和受约束的替换，可用于表明应用Abstract所需的排序约束是可满足的（参见[12]中的示例B.1和B.4）。还可以建立以下引理。它允许在当前项是变量或不可缩小项时应用Abstract引理4.10设（{ti}，T i）是通过在（{ t ref }，T）上应用策略S而获得的导出树的任何分支的第i个状态，并且>具有子项性质的F-稳定序.如果每个约简公式都可以简化为公式jxj=xJj，则我们有：f∈Var（ti）：（fi，tref>x）满足于>。为了证明R在每个项t∈ T（F）上的最外终止，对于每个定义的符号g∈Def，我们将规则应用于初始项集T = tref= g（x1，...，xm）和平凡约束。这些规则必须使用策略S：尝试使用抽象。如果抽象不适用，则应用窄。然后重复这个过程，直到没有规则适用。让我们强调一些关于推理规则的要点• Narrow是一种非确定性规则，可以产生几种结果：它与所有可能的重写规则一起应用于所有最外面的位置。• 在抽象之后，不再有任何规则现在可以更精确地描述终止证明程序的行为的三种情况该策略适用于初始状态（tref）可以在具有非空项集的状态下停止，如果存在无限数量的Narrow应用，则它可能不会终止。好情况是当策略终止时，因为规则不再适用，并且所有状态都是（，）的形式。让我们写SUCCESS（g，>）i来表示推理规则在（ g（x1，.， xm），），其条件满足，给出了在派生树的所有分支的末尾形成（，）我们可以说，的主要结果。定理4.11设是（，）上的一个TRS，使得的常数是最外终止的. 如果存在具 有 子项性质的稳定序，使得对于每个非常数定义符号g，SUCCESS（g，>），则T（F）的 每 一 项 最外终止。菲索尔、格内迪格和基什内尔203FR、、我们现在开发例子，给出证明树的状态其他例子可以在[12]中找到。例4.12考虑前面的例子R= {f（g（a）） →a，f（f（x））→ b，g（x）→ f（g（x））}，这是最外终止的，但不是标准重写关系的终止。本文证明了R是T（F）上的最外终止的，其中F ={f：1，g：1，a：0，b：0}.for的定义符号是f和g。 应用f（x1）的规则，我们得到：f（x1）T =T，，窄一得双曲余切值.、、、，，N箭头，zbn =（（x1→nxJ1）[f（x1）]nxJ1=g（a））（σ=（xJ1=g（a）））摘要Jn=（（x1→n=xJ1）[f（x1）]（xJ1=g（a））n =（（x1→nxJ1）[f（x1）]（f（x2））（σ=（xJ1=f（x2）<$xJ=x2））摘要Jn=（（x1→n=xJ1）[f（x1）]（f（x2））变量xJ来自规则左边的x的重命名对于第一个摘要，a被推广到x3，因为（f，f（x1）> a）是满足的。能够通过字典式路径排序（简称LPO）>具有优先级（F上的排序）f>Fa。对于第二个摘要，b被推广到x4，、、菲索尔、格内迪格和基什内尔204>由于（f，f（x1）> b）可由具有附加优先级fFb. 我们记得归纳排序必须是相同的所有的分支的所有衍生树。应用g（x1）的规则，我们得到：菲索尔、格内迪格和基什内尔205. .. .、、>/打开/关闭g（x1）=T窄Jf（g（xJ1））n =（（x1→nxJ1）[g（x1）]）（σ=（xJ=xJ1））. . .不，不。. ..a.，c、、、，，N箭头，，zf（f（g（xJ1j）n =（（x1→nxJ1）[g（x1）]n =（（x1→nxJ1）[g（x1）]n（xJ1→nxJ1J）[f（g（xJ1））]n（xJ1→nxJJ）[f（g（xJ1））]xJ1J=a）a）（σ=（xJ1J=a））摘要J=（（x1→n（xJ1→nxJ1J）[f（g（xJ1））]xJ1J=a）（σ=（xJ=xJ1J）满足（xJ1J/=a））窄JBn =（（x1→nxJ1）[g（x1）]n（xJ1→nxJ1J）[f（g（xJ1））]n（xJ1J→nxJ1JJ）[f（f（g（xJ1J）]xJ1J/=a）（σ=（xJJJ=g（xJ1JJ）摘要J=（（x1→n（xJ1→nxJ1J）[f（g（xJ1））]n（xJ1J→nxJ1JJ）[f（f（g（xJ1J）]xJ1J/=a）抽象应用于a和b，具有额外优先级gFa，b的先前LPO。当缩小f（g（xJ1））时，我们首先尝试顶部位置，并使用第一个规则（左分支）找到可能的统一。还必须考虑第三条规则，如果xJ1j使得xJ1J=a;因此，如果xJ1J=a，则f（g（xJ1J））在位置1处用第三条规则（第二分支）缩小..、、菲索尔、格内迪格和基什内尔206例4.13设R为引言中引用的TRS，建立在F={cons：2，inf：1，big：0}：cons（x，cons（y，z））→biginf（x）→cons（x，inf（s（x）对inf（x1）应用推理规则，我们得到：菲索尔、格内迪格和基什内尔207111111111111Inf（x1）窄Jcon