懒惰和上下文相关重写及其对计算机终止性的影响

234理论计算机科学电子笔记64（2002）网址：http://www.elsevier.nl/locate/entcs/volume64.html21页懒惰重写和上下文相关重写Salvador Lucas萨尔瓦多·卢卡斯1，2DSIC圣保罗理工大学摘要延迟重写（LR）旨在改善TRS的终止行为。这是通过限制函数的选定参数的减少来尝试的。类似地，上下文敏感重写（CSR）禁止对这些参数进行任何缩减。我们证明了LR和CSR在一定条件下是一致的。在这个结果的基础上，我们还描述了一个变换，使我们能够证明终止的LR作为转化系统的CSR的终止。 因为有一个数字- 通过对CSR终止性证明的不同技术的比较，本文提供了一个证明懒惰重写终止性的1介绍语法注释（与符号的参数相关联）已经在诸如Lisp、Haskell、Clean、OBJ2、OBJ3、CafeOBJ、Maude等编程语言中使用，以提高计算的终止性和效率。惰性语言（例如，Haskell，Clean）将它们解释为严格的注释，以便变得“更渴望”和有效。渴望语言（例如，Lisp，OBJ2，OBJ3，CafeOBJ，Maude）使用它们作为替换约束来变得“更懒惰”，从而（希望）避免非终止。例如，[FW76]研究了Lisp的实现，其中列表运算符（cons）在计算的某 些 阶 段 没 有 评 估 其 参 数 。 此 外 ， 代 数 语 言 ， 如 OBJ2[FGJM85] ，OBJ3[GWMFJ00]，CafeOBJ[FN97]或Maude[CELM 96]，允许将策略注释显式指定为括号中的整数序列。它们被解释为替换限制，这些限制约束了底层的参数求值策略：函数调用f（t1，...，k）谁的1由CICYTTIC 2001 -2705-C 03 -01、Acciones Integradas HI 2000- 0161、HA 2001-0059、HU 2001-0019和Generalitat Valenciana GV 01 -424部分支持的工作。2电邮地址：slucas@dsic.upv.es，WWW：http://www.dsic.upv.es/users/elp/slucas.html2002年2月出版，电子科学和B。 V. 操作访问根据C CB Y-NC-N D许可证进行。卢卡斯235联系我们F联系我们F → Pindex i∈ {1，.，k}不出现在策略注释（i1i2···i n）中（其中i1，i2.，i n0，1，.，k）不被考虑用于评估。此外，即使在顶部应用规则也必须通过'0'明确表示[Eke 98]。这种“真正的”替换限制的存在示例1.1以下OBJ3程序：objEXAMPLE是sort排序。操作0 ：->排序。ops：Sort -> Sort.opcons：Sort Sort -> Sort [strat（10）]. 操作inf：Sort -> Sort.opnth：Sort Sort -> Sort.var X Y L：排序。eq nth（0，cons（X，L））= X.等式nth（s（X），cons（X，L））= nth（X，L）。等式inf（X）= cons（X，inf（s（X）。Endo为列表构造函数cons指定一个显式的策略注释（1 0），该注释禁止第二个参数4的归约。这样，表达式nth（s（0），inf（0））的求值总是结束并产生项s（0），即使上下文敏感重写（CSR [Luc98]）提供了一个合适的框架，用于证明使用这种策略注释的OBJ程序的终止性（参见[Luc01a，Luc01b]）。在CSR中，映射µ：（N）被称为重映射。布局图，如果µ（f）一，K对于每个k进制符号f，签名.替换映射用于区分允许替换的参数位置。以这种方式，获得重写限制（参见第3节）。 终止TRS是µ-终止（即，在μ下，没有任何项启动CSR的无限序列）。 然而，CSR可以通过在有限的重写序列中修剪（所有）来实现终止。 已经开发了几种方法来正式证明CSR的终止5[BLR02，FR99，GL02，GM99，GM02，Luc96，SX98，Zan97]，参见[GM02，Luc02c]这些技术中的大多数的比较。例如，可以证明与例1.1的OBJ3程序相对应的TRS对于CSR是终止的（参见下面的例3.2根据[Luc01a，Luc01b]，[3]在[GWMFJ00]中，OBJ指的是OBJ2、OBJ3、CafeOBJ或Maude。4其他符号被赋予默认策略注释（参见[GWMFJ00]）。5参见http://www.dsic.upv.es/users/elp/slucas/muterm获取工具（MU-TERM），它实现了大多数这些方法。第1.0版）卢卡斯236证明实际上确保OBJ3程序的终止。使用重写限制可能会导致不完整的计算。例如，某些项的标准形式可能无法通过受限计算来实现。示例1.2下面的CafeOBJ程序（从[NO01]借用）：mod！测试{ [T]操作0：-> T操作：T-> T{strat：（1）}操作cons：T T->T{strat：（1）}op 2nd： T-> T{strat：（10）}操作自：T-> T{strat：（1 0）}变量 X Y Z： T等式2nd（cons（X，cons（Y，Z）= Y。eq from（X）= cons（X，from（s（X）。}为列表构造函数cons指定一个策略注释（1），使程序终止;然而，计算2nd（从（s（0））到s（0）：2nd（from（0））→2nd（cons（0，from（s（0）→2nd（cons（0，cons（s（0），from（s（s（0）→s（0）不可能原因是不允许对cons的第二个参数进行约简;因此，第二个约简步骤不再可能。另一方面，使用局部策略（例如（1 2））进行评估是可能的，但获得以下无限约简序列：2nd（from（0））→2nd（cons（0，from（s（0）→2nd（cons（0，cons（s（0），from（s（s（0）→···例1.2显示了OBJ程序中语法注释的当前解释的局限性（可以使用CSR框架给出）。Fokkink等人的懒惰图重写[FKW00]提供了一个不同的（更自由的）操作模型，用于使用由替换映射μ指定的语法替换限制。在第4节中，我们改编了Fokkink et al.的框架，懒惰的长期重写（LR）。事实上，延迟重写也旨在“改善TRS的终止行为”[FKW00]。例如，使用延迟重写，我们可以计算2nd的值（从（0））（使用对应于例1.2的策略注释的替换限制），而无需jeopardizing非终止性。尽管（原则上）不允许在符号的非替换参数，它们仍然是可能的，如果它们甚至可以最终有助于应用关于符号的替换位置的规则，卢卡斯237Pterm.实施例1.3（继续实施例1.2）还原步骤2nd（cons（0，from（s（0）→2nd（cons（0，cons（s（0），from（s（s（0））可以使用延迟重写。事实上，它实际上有助于使以下（关键）步骤成为可能：第二个（cons（0，cons（s（0），from（s（s（0））→s（0）然而，减少步骤第二个（cons（0，cons（s（0），from（s（s（0））→···不允许潜在地“产生”无限重写序列，因为来自（s（s（0）的redex发生在非替换位置，而不便于在（平凡地）替换项2nd（cons（0，cons（s（0），from（s（s（0）上应用规则（即，例1.2中程序的第一个规则）。注1.4注意，例1.1和1.2中的程序可以通过使用其他技术给出最佳归一化策略。例如，不难看出这两个程序都是强顺序的。由于它们也是正交的，因此它们都允许可计算的归一化策略[HL91]。当然，这种策略与OBJ评估策略非常不同，并且（通常）不能模拟为OBJ计算。然而，也可能存在不能被给予标准化的OBJ通过使用上述技术，我们仍然可以在证明其终止性和使用程序转换技术的基础上实现规范化，参见[Luc02b]和[Luc02a]。不幸的是，目前还没有关于延迟重写终止的分析在第5节中，我们证明了在某些条件下（即，规则左侧的所有不变子项都是μ-替换的），CSR和LR重合。在这种情况下，LR的终止等同于CSR的终止，可以使用为CSR开发的技术进行研究。在第6节中，对于LR和CSR不一致的情况，我们提供了一个变换，该变换允许证明惰性重写的终止作为变换后系统的CSR的终止。这样，我们就可以利用证明CSR终止性的技巧来证明LR的终止性。该转换可用于在MU-TERM1.0中使用，其中还实现了用于证明CSR2预赛给定一个集合A，（A）表示A的所有子集的集合。给定一个集合A上的二元关系R，我们用R +表示它的传递闭包，6 事实上，它们在[Ant 92]的意义上是归纳顺序的;这些TRS是强烈的顺序，参见[HLM98]。卢卡斯238p∈|FX T FX{} F→F··XF± ∈ F <$±{}∈ F±pµµ和传递闭包。 元素aA是R-正规形式，如果没有比aR更好了。我们说b是a的R-正规形式（记为a R！b）如果b是R-正规形且R≠b. 我们说R在那里终止于ia1Ra2Ra3不是无限序列.在整个文件中，表示变量的可数集合，并且表示签名，即，一组函数符号f，g，.. . 每个人都有一个固定的arity，由映射ar：N给出。这组术语是从和是 （，）。一项被称为线性项如果一个变量没有多次出现术语通常被看作是有标签的树。 位置p，q，. 由用于寻址t的子项的正自然数链表示。 给定位置p，q，我们将其 级 联 表 示 为 p.q 。 如 果 p 是 一 个 位 置 ， Q 是 一 组 位 置 ， 则p.Q={p.q|q∈Q}。 We表示由yA表示的emp tychain。项t的位置的集合是Pos（t）。t中不可变符号的位置记为PosF（t），PosX（t）是变量的位置。t的位置p处的子项记为tp，t[s]p是具有子项的项t在位置P由S代替。标记t的根的符号表示为root（t）。重写规则是一个有序对（l，r），记为l→r，其中l，r∈ T（F，X），l/∈ X且Var（r）<$Var（l）。规则的左边（lhs）是l，右边（rhs）是r。TRS是一对R=（F，R），其中R是一组重写规则。L（R）表示R的lhs一个TRSR是左线性的，如果对所有l∈L（R），l是线性项。一个项t∈ T（F，X）重写为s（在位置p），写作t→Rs（或只是t→s），如果t|p=σ（l）和s=t[σ（r）] p，对于某些规则l→r∈R，p∈Pos（t）和代换σ.3上下文相关重写一个映射μ：F→ P（N）是一个替换映射（或F-映射），如果μ（f）≥1，.，ar（f）对于所有f[Luc98].订购在MF上，所有-maps，即：µμJif for all f、µ（f）µJ（f）. 因此，μJ意味着μ考虑的位置比μJ少（用于减少），即，比yj更严格。根据±，µ（resp. ”[10]“”是“”的意思。{1，...，} ar（f）}）是M F的最小（最大）元.t∈T（F，X）的μ-置换位置Pos（t）的成立为：Pos（t）={Λ}，如果t∈ X且Posμ（t）={Λ} μi∈µ（root（t））I. Pos µ（t|i），如果t/∈ X. 该组µ替换t的变量Var（t）为Var µ（t）={x ∈ Var（t）|Pos x（t）Pos（t）/={\fn方正黑体简体\fs18\b1\bord1\shad1\3cH2F2F2F}. 在上下文相关重写（CSR[Luc98]）中，我们（仅）进行跟踪替换Redexes：t µ-重写为s（写入t <$→µ例3.1考虑TRSR：第二个（x：y：z）→yfrom（x）→x：from（s（x））s）如果t→Rs和p∈ Pos μ（t）。µ卢卡斯239Z--R→关于我们RRRRRR和µ（：）= µ（2nd）= µ（from）= µ（s）= 1，它们对应于例1.2的CafeOBJ程序7（我们使用：用途：代替cons），有关此对应关系的更多详细信息，请参见[Luc01 a]。然后我们有：2nd（from（0））<$→µ2nd（0：from（s（0）其中μ-重写从1开始停止。2/∈Posµ（2nd（0：from（s（0）。<$→µ-正规形式称为µ-正规形式。 注意，除了平凡的情况μ =μT，μ-范式的集合严格地包括R的范式（例如，例3.1中的第二项（0：from（s（0）是一个非正规形式的μ-正规形式）。如果是终止，则TRS是终止。 作为正如在引言中提到的，许多技术可以用来证明CSR的终止是转换的TRS的终止示例3.2TRSR：nth（0，x：y）→x nth（s（x），y：z）→nth（x，z）inf（x）→x：inf（s（x））其中µ（：）=µ（s）=µ（inf）= 1和µ（nth）= 1，2对应于例1.1中的OBJ3程序使用Zantemanth（0，x：y）→xnth（s（x），y：z）→nth（x，activate（z））inf（x）→x：inf'（s（x））activate（inf'（x））→int（x）int（x）→activate（x）→x其中activate和inf'是由变换引入的新符号。这个TRS是终止的（使用递归路径排序，基于优先级nth>activate>in f，：，nil和inf>：，inf'，s，并给nth通常的字典状态）。因此，R是μ-终止的。正则替换映射µ可以R是最严格的替代品图，其确保图的左侧的不可变子项R的规则正在被取代。请注意，µcan很容易从R=（F，R）中获得R对于所有的f ∈ F和i ∈ {1，...， ar（f）}，i∈ μ can（f）i ∈ L（R），p ∈ PosF（l），（root（l|p）= f<$p.i ∈ PosF（l））设CMR={μ∈MF|[001 pdf 1st-31files]可以是替换映射的集合，R可以比µ R的限制性更小或与µR的限制性相同。例3.3例3.2中R的正则置换映射μcan是：µcan（：）=µcan（s）=µcan（inf）=且µcan（nth）={1，2}[7]由于对于每个常数符号c，μ（c）=μ，所以在本文的剩余部分，我们只对其他符号显式地给出替换映射卢卡斯240RFTF ×L X ×LTFX ∈ TFX∈P||✏注意，例3.2中的μ满足μ can±μ，即，μ∈CMR.4惰性重写在懒惰图重写[FKW00]中，在标记图上发布约简。我们适应的框架，懒惰的长期重写标记的条款。在[FKW00]之后，我们将区分术语的渴望和懒惰位置。因此，我们用e表示渴望的位置或l表示懒惰的位置来标记项t的每个节点（或位置）：设F是签名，L ={e，l};则F × L是标记符号的新签名。符号f∈ F的标号记为f e或f l，而不是f，e或f，l。 自然地，对所有f ∈ F，ar（f e）=ar（f l）=ar（f）。 然后，标记项是（，），我们记为（L， L）。给定t （L，L），pos（t），如果root（tp）=xe（=xl）或root（tp）=fe（=fl），则我们说，p是一个渴望（resp。lazy）的位置。例4.1考虑例3.1中TRS的签名和以下标记项：第2l❄：e✏✮✏zzzL0l从l❄Se❄0升因此，1和1。二、1是期望位置;位置Λ，1。1，1。2和1。二、1 .一、1、懒惰Fokkink等人使用惰性签名的概念，即， 一个签名F，在F×N上提供一个懒惰谓词ΛL，它对（f，i）成立当且仅当1≤i≤ar（f），并且f的第i个参数是懒惰的（[FKW 00]的定义3.1.1）。懒惰谓词ΛL实际上可以用替换映射μ来识别：f∈F， i∈{1， . . . ，ar（f）}，（i∈μ（f）惠<$ΛL（f，i） ）在下文中，我们使用μ而不是ΛL。给定μ∈MF，映射标签μ：T（F，X）→T（FL，XL）提供了项的以下预期标签：给定s∈ T（F，X），标签μ（s）的最高位置Λ总是急切的;给定位置p ∈ P os（标签μ（s））且i∈ {1，. ar（root（s|p））}，标号μ（s）的位置p.i是惰性的当且仅当i/∈μ（root（s）|p））;否则，它是渴望的（[FKW 00]的定义3.1.2）。形式上，标记为μ（x）=xe，如果x∈ X，且卢卡斯241∈R≤≤|la belµ（f（s1， . ，sk））=f e（la be lJf，l（s1）， . . . ，labelJf，k（sk）），如果f∈F，则如果i µ（f），则xe标签Jf，i（x）=xl否则ge（la belJg，1（u1）， . ，labelJg，m（um））ifi∈μ（f）la belJf，i（g（u1， . ，um））=1（u1）， . ，labelJg，m（um）），例4.2考虑例3.1中的和µ。然后，术语的预期标签s=2nd（0：from（s（0） ist=la be lµ（s）=2nde（0e：efroml（se（0e）.从图形上看：S第2❄中文（简体）labelµ（s）第二E❄：e✏✮✏zzL✏✮✏✏zzzL0从❄S❄00e从l❄Se❄0e这里，Λ，1，1。1，1。二、1和1。二、1 .一、1是t的渴望位置;位置1。二是懒惰。给定t∈ T（FL，XL），erase（t）是T（F，X）中去掉所有标签后（显然）对应于t的注意，erase_label_µ= idT（F，X），但label_µ_erase/= idT（FL，XL）。如上所述，给定t∈ T（FL，XL），位置p∈ Pos（t）是急切的（相应地，lazy）if root（t|p）用e（resp）标记。l）。t的所谓活动位置归纳定义如下：Λ是活动位置;如果p∈ Pos（t）是有效的，则p.i对于所有的急切位置p.i，1都是有效的我ar（root（t p））oft（[FKW 00]的定义3.1.3）。活动位置总是可以从项的根通过渴望位置的路径到达。急切的立场不一定满足这一点。示例4.3（继续示例4.2）位置Λ、1和1。1活跃于t=2nde（0e：efroml（se（0e）卢卡斯242位置1. 二、1和1. 二、1 .一、t中的1个渴望但不活跃，因为位置1。2、懒惰的T从图形上看：卢卡斯243µR第二E❄：e活动位置（✏✮✏✏zzzL0e从l❄Se❄0e设Act（t）是标号项t∈ T（FL，XL）的活动位置集.给定s∈ T（F，X）和μ∈MF，标签μ（s）的有效位置的集合与Posμ（s）重合。命题4.4设F是一个签名，μ ∈MF，s ∈ T（F，X）。然后 ，Act（标记µ（s））= Pos（s）。标签项上的延迟重写的一个重要特性是，活动节点的集合可以随着标记项的减少而增加标记项上的每个惰性重写步骤可能有两个不同的结果：(i) 在标记的术语内改变给定位置的状态（活动或不活动），或(ii) 执行重写步骤（总是在活动位置上）。在下文中，我们通过在标记项上使用两个不同的二元关系来正式描述它们。4.1激活职位以减少如果位置是“必要的”，则可以修改（标记）项内活动位置正下方的惰性位置的激活状态 ，即，‘its contractionmayleadtonewredexesatactive nodes’定义4.5[Matching modulo laziness [FKW 00]]设l∈ T（F，X）是线性的，t∈T（FL，XL），p是t的活动位置。然后，l匹配模惰性s=t|p如果(i) l∈ X，或(ii) l = f（l1，...，l k），s = f e（s1，...，s k），并且对于所有i∈{1，.，k}，如果p.i是渴望的，则l. i匹配模惰性s. i。如果t的位置p.i是lazy且li/∈ X，则位置p.i称为本质的。例4.6考虑例3.1的TRS。lhs2nd（x：y：z）匹配多个惰性，因此可以将dt=2nde（0e：efroml（se（0e）。A-根据定义4.5，位置1。2、T是必不可少的。卢卡斯244|一R一一→一一1KQ注意，如果l∈ T（F，X）匹配模惰性有效标记子项s=tp而不产生本质位置，则l匹配通常意义上的erase（s）。职位“活动”的变化通过以下方式正式化。定义4.7设R=（F，R）是左线性TRS。 激活关系-标记项之间的关系定义如下。设p在t∈ T（FL，XL）和l→r∈R使得l匹配模惰性不|p. 设q是t的本质位置，t|Q=f l（t1，...， t k）。然后，t→At[f e（t， . ， t）]。考虑例3.1中的TRS下图显示了与例4.6中的t项对应的激活步骤第二E❄：e✏✮✏✏zzzLA.第二E❄：e✏✮✏✏zzzL启动！/联系我们0e从l❄Se❄0e0e从e❄Se❄0e注意→A是一个终止关系：只有有限个关系（fromlazytooeager）ispossibleeforrifniteterms .（从懒惰到渴望）是有限的条款。一般情况下，→A例4.8考虑（接地）TRSR：f（c（d，a））→ab→ f（c（b，d））然后，我们有这不是巧合。fe（cl（bl，dl））→fe（ce（bl，dl））→fe（ce（be，dl））f（c（d，a））不匹配项，因此fe（ce（be，dl））是A -正规型fe（ce（be，dl））模惰性。然而，在这方面，fe（cl（bl，dl））→fe（ce（bl，dl））→fe（ce（bl，dee））这就导致了一个困难t→A-正规型。注4.9注意，激活关系式不使用替换映射μ中包含的信息。我们把这一事实明确地说出来，没有引用到µ在ow→A我们用它来代表它。注意以下明显的事实。卢卡斯245∈Xl，uL∈Xl，uL→V Vµ命题4.10设R =（F，R）是左线性TRS，t，TJ∈ T（FL，XL）.如果t→AtJ，则e rase（t）=e ras e（tJ）。下面的命题确定了，如果标号项t是通过使用替换映射μ∈CMR标号项s∈ T（F，X）而获得的，则激活新位置是不可能的。命题4.11设R=（F，R）是左线性TRS，μ∈CMR，且一s∈ T（F，X）. 因此，标号μ（s）是→-正规形式。4.2减少在职职位延迟重写减少了活动位置。在下文中，我们正式描述这样的过程。请注意，根据Fokkink et al.的表述，TRS规则的lhs因此，正如在定义4.5中一样，我们必须处理有标签和无标签的术语。由于这个原因，还原过程的描述比纯粹的重写稍微复杂一些定义4.12设l∈ T（F，X）为线性项，t∈ T（FL，XL），p∈Pos（t），u= t|p.若l匹配erase（u），则设映射σ l，u：Var（l）→ T（FL，XL）为σ l，u（x）=u|q对所有x∈ Var（l）.从定义4.12中的σl，u，我们得到了关于标号项（变量在Var（l）中）的替换σ，所有x∈ Var（l），如果σ（x）=yλ，则为yeσ（xe）=n（t1，.，（t k）若σ l，u（x）= f λ（t1，...，（tk）如果σ（x）=yλ，则为σ（xl）=如果l（t1，...，（t k）若σ l，u（x）= f λ（t1，...，（t k）对于λ∈ {e，l}。由于我们将把这样一个替换应用于（左线性）重写规则l r和ar（r）ar（l）的带标签的rhs标签µ（r），我们的定义满足我们的目的（见定义4.13）。这是根据[FKW 00]中的定义3.2.3：当标号项上的替换σ应用于标号项t时，对应于σ（t）中位置q上的符号的标号是q在t中的标号，对于每个变量位置q∈PosXL（t）。因此，我们给出以下结果。定义4.13设R=（F，R）是左线性TRS且μ∈MF。的主动重写的关系→Rbetwenlabelle d terms定义如下。设p是t∈ T（FL，XL）的活动位置，u = t|p和l→r∈R使得l匹配erase（u）。 设σl，u为相应的映射。然后，t→Rµt [σ（la be lµ（r））]p。卢卡斯2460eµµRµµµ下图显示了与示例4.6在活化步骤之后。第二E❄：e✏✮✏✏zzzL0e从eRµ第二E❄：e✏✮✏✏zzzLe✏✮✏✏zzzL斯堪的纳维亚Se❄100e0e从l❄Se❄Se❄0e注意，在 该 → R - 步 骤 之 后 获 得 的 项2nde（0e： ese （0e）：efroml（se（se（0 e）是→A-范式。例4.14考虑TRSf（b，x）→g（x）（1）（2）（3）（4）（ 5）（6）（7）（8）（9）（10）（设t=fe（be，al）;注意标记μ（g（x））=ge（xe）。然后，f（b，x）匹配erase（t）。我们有σf（b，x），t（x）=al。得到了由σ（xe）=ae和σ（xl）=al给出的置换σ.然后，fe（be，al）→Rge（ae）Remark4.15Example4.14显示t→R-步骤也可以单独激活µ在收缩（带标签的）redex后的惰性位置。 例如，我们可以认为t=fe（be，al）上的e→R-步作为激活aint的惰性发生µ当它被简化为ge（ae）时。我们还注意到以下显而易见的事实。命题4.16设R=（F，R）是左线性TRS，μ∈MF，t，tJ∈RT（FL，XL）. 如果t → tJ，则erase（t）→ erase（tJ）。4.3懒惰术语重写在[FKW00]的定义3.2.3中给出的懒惰图重写对应于to关系n→LR=→A在标记项LR上，→ µ。Remark4.17实际上，→LR允许不完全通过的缩减步骤定义3.2. 3的[FKW 00]（但所有的m可以是模拟的das→LR-步骤）。 µ卢卡斯247特别地，在原始公式中，重写项t的有效位置p（即，a→Rμ-阶跃在t|p）只有在整个过程结束后，卢卡斯248一→µRRR一LRLRµµµµµt的子项激活|p（即， 在得到t的→-正规形式后，|p）。这一事实与本文的主要结果无关，我们在这里不再进一步考虑它们。当LR用于计算未标号项s∈ T（F，X）时，我们实际上对从标签µ（s）发出的µ-减少感兴趣如在[NO01，OF00]对于OBJ（类似）语言（并且在[FKW00]中是隐式的），我们可以定义一个求值语义，即，映射LR-evalμ：T（F，X）→ P（T（F，X）），通过使用LR获得给定项的求值：LRL R-e valμ（s）={e rase（t）∈T（F，X）|la belµ（s）−→！t}对于CSR，我们可以做同样的事情：CSR-eval µ（s）={sJ∈ T（F，X）|s <$→！ sJ}。现在我们可以比较两种评估机制。例4.18考虑例3.1中的和μ，s = 2nd（从（0））。我们有以下LR-评估序列：labelµ（s）=2nde（frome（0e））→µ2nde（0e：efroml（se（0e）→2nde（0e：efrome（se（0e）→R2nde（0e：ese（0e）：efroml（se（se（0e）→µse（0e）因此，我们认为，s（0）∈LR-evalµ （2nd（from（0）如所期望的（这遵循实施例1.3中的讨论）。 与此相反，s（0）/∈ CSR-eval µ（2nd（from（0）={2nd（0：from（s（0）}。根据这一点，给定R=（F，R）和μ∈MF，我们说，R是LR（μ）-终止的，如果对于所有s∈ T（F，X），没有从标号μ（s）开始的无限重写序列。→µ-5惰性重写和上下文敏感重写n→R和CSR之间的以下联系是有趣的。命题5.1设R=（F，R）是左线性TRS，μ∈MF，s∈ T（F，X）R且t∈ T（FL，XL）.然后，标号为μ（s）→t当且仅当μsJ∈ T（F，X），s <$→μsJ而t = label μ（sJ）。下面的定理表示，CSR总是可以被看作是LR的限制，只考虑定理5.2设R=（F，R）是左线性TRS，μ∈MF，s，SJ∈LRT（F，X）。 当且仅当label µ（s）→ label µ（sJ）时，s <$→ µ s j。卢卡斯249RR/∈∈µ下面的定理表明，当-everyμ∈CMR时，LR可以由CSR模拟。定理5.3设R=（F，R）是左线性TRS，μ∈CMR，s∈ T（F，X），LR且t∈ T（FL，XL）.然后，标号为μ（s）→t当且仅当μsJ∈ T（F，X），s <$→μsJ而t = label μ（sJ）。通过这种方式，CSR提供了一种替代（更简单）的评估机制。我们拥有：推论5.4设R是左线性TRS且μ ∈ CMR.然后，LR-eval µ= CSR-eval µ。例4.18表明，如果μ CMR.关于LR（μ）-终止，定理5.3也有以下结果。推论5.5设R是左线性TRS且μ∈CMR.故R是μ终止的，当且仅当R是LR（μ）终止的。例5.6考虑例3.2中的和µ。Fokkink等人使用这个TRS和替换映射μ（更准确地说，对应的惰性预测ΛL）来激励惰性重写（希望）能够避免无限重复ductions 自µCMR（见例3.3），推论5.5、LR（µ）-终止和µ-终止重合。 以来是µ-终止的(see例3.2），推论5.5证明了Fokkink等人的观点。s索赔。6懒惰重写的终止性证明推论5.5对于LR（μ）-终止的证明是相当有限的然而，它为证明LR（μ）-终止作为转换的TRS（和替换映射μJ）的CSR终止在[Ngu01]中，给出了TRS和替换映射对的变换提出强制R中规则的所有左手边的不可变子项被μ-替换，即，以实现µcan±µ。转换如下（请参见[Ngu01]的第6.1节）：令RR=（F，R）beaTRS和μ∈MF.设l→r∈R，p∈ PosF（l），root（l|p）= f，且i/∈ μ（f）使得p.i ∈ PosF（l）. 然后我们得到RJ=（FJ，RJ）和μJ∈MFJ如下：FJ=F<${FJ}，其中FJ是元数ar（FJ）=ar（f）的一个新符号，使得μJ（ FJ）=μ（f）<${i}和μJ（g）=μ（g），对所有g∈ F.另一方面，在一项研究中，RJ=R−{l→r} <${lJ→r，l[x]p.i→lJ[x]p. i}其中lJ= l [fJ（l|p. 一，L|p.k）] p如果ar（f）= k且x是新变量。例6.1考虑例4.8中的R，且μ=μπ ι。 那么，RJ是：f1（c（d，a））→ab→f（c（b，d））f（x）→f1（x）且μJ（f）=μJ（c）= μ，μJ（f1）={ 1}。卢卡斯250RR一RRRµ#R11313µ#13#转换过程如下（从RJ和µJ开始），直到R#和µ#是这样得到的，即µ可以±µ#。特别是，如果µ可以±µ，R#=R，µ#=µ。RR实例6.2继续实例6.1，R#为：f1（c2（d，a））→a f1（c（x，y））→f1（c3（x，y））f1（c1（d，x））→f1（c2（d，x））f（x）→ f1（x）f1（c3（x，a））→f1（c1（x，a））b → f（c（b，d））和µ#isgivenbyyµ#（f）=µ#（c） =，µ#（f1）=µ#（c1）={1}，µ#（c2）={1，2}，且μ#（c）={2}。不可能有µcan±µ#。3R#注6.3由于在每一步中f和p的选择，变换具有一些例如，例6.1第一步的不同可能性（以及其他）如下：f（c'（d，a））→ ab→f（c（b，d））f（c（x，a））→f（且μJJ（f）= μJJ（c）= μ，μJJ（c'）= { 1 }。推论5.5建议用这样一种变换来证明R的LR（μ）-终止也是R的μ#-终止，前提是这种变换保持R的LR（μ）-终止。不幸的是，这不是真的。实施例6. 4考虑例4.8中的R，μ=μπι，并且#和µ#在例6.2中。注意，它不是LR（μ）终止的：对于t= f（c（b，d）），我们有：labelμ（t）=fe（cl（bl，dl））→fe（ce（bl，dl））→fe（ce（be，dl））→Rµfe（ce（fe（cl（bl，dl）），dl））−A→+ fe（ce（fe（ce（be，dl）），dl））→μ·· ·如何证明，#是L R（µ#）-终止的8。问题是有些惰性子项的激活fe（cl（bl，dl））→fe（ce（bl，dl））→fe（ce（bl，de））惰性子项bl不能被激活;fe（ce（bl，de））是a→-正规form. 此外，由于fe（ce（b1，de））=labelμ（f1（c3（b，d））且μ#∈CMR#，由命题4.11是a→A-正规形，因此a→LR-正规形。对Nguyen变换的一个简单修改诀窍是为每个考虑的符号包含所有可能的惰性（有问题的）参数的8这可以正式提供：根据Corollary5.5，我们只需要提供µ# -#的终止。使用[GM 99，GM 02]最后一节中描述的Giesl和Middeldorphttp://cime.lri.fr变换（可在mu - term1.0中获得）;如果先前已激活“依赖对标准”（参见[AG 00]），则可使用C i ME 2.0系统（可在www.example.com上获得）自动证明变换TRS的终止。一RRµ#µ#卢卡斯251F{}≤ ≤ ∈FF{|联系我们RRRµqRR+R›→R114µq141414l→r∈R且p∈Pos（l），设I（l，p）={i∈{1， . ，ar（root（l|p））} −µ（rroot（l|（p））|p. i∈PosF（l）}设I（l，p）={i1， . ，in}，对于某些n>0（即，，I（l，p）/=f（l，p）和letf= root（l，p）|p）。然后，Ro=（Fo，Ro）和μo∈MFo如下：Fo=f j1jn，其中每个f j是元数ar（f j）= ar（f）的新符号。我们令μo（fj）=μ（f）Ij持续1J（1）凡所有相，皆是虚妄;凡所有相， 皆 是 虚 妄 。另一方面，在一项研究中，Ro= R − {l → r}<${ljJ→ r，l [x] p.ij → ljJ[x] p.ij |1 ≤ j ≤ n}其中ljJ=l [f j（l|p. 一，L|p.k）] p如果ar（f）= k，并且x是新变量。例6.5考虑例4.8中的情形，且μ = μ πι。通过新的变换，我们可以得到与第一次一样，J获得在示例6.1中。另一方面，如果考虑lhsf（c（d，a））→a的符号c（而不是f），我们现在得到：f（f（f（c（x，a））→f（（1）（2）（3）（4）（5）（6）（7）（8）（9）（10同样，变换像这样进行（现在从Ro开始，（1）当Rq=（Fq，Rq）时，得到μq，使得μ可以± μq。 如果μ∈CM，则Rq=R且μq=μ。RqR例6.6假设R与例4.8相同，且μ=μπι。那么，Rq是f1（cj2（d，a））→af1（c（x，y））→f1（c3（x，y））f1（c2（x，a））→f1（cJ2（x，a））f1（c4（d，y））→f1（c2（d，y））f1（cj1（d，a））→af1（c（x，y））→f1（c4（x，y））f1（c1（d，x））→f1（cj1（d，x））f（x）→f1（x）f1（c3（x，a））→f1（c1（x，a））b → f（c（b，d））和μqisgivenbyyμq（f）=μq（c）=μ q，μq（f1）=μq（c1）=μq（c4）={1}，μq（cJ1）=μq（cJ2）={ 1， 2}，且μq（c）=μq（c）={ 2}。请注意，µcan±µq。2 3Rq现在，我们能够适当地模拟每个ery→LRinRasa→LR -约化序列。µ-归约序列例6 - 7考虑例6 - 4中的t项现在我们有以下内容（无限）→LR -Rq中的还原序列 ：labelμ（t）=fe（cl（bl，dl））→fe（ce（bl，dl））→fe（ce（be，dl））→fe（ce（fe（cl（bl，dl）），dl））−→fe（ce（fe（ce（be，dl）），dl））→···我们说从对（TRS，替换映射）到同类对的变换Θ：（，μ）（J，RRRµqµqµqµqµq卢卡斯252μJ）是正确的（关于LR（μ）-卢卡斯253RRRRRRRR关于我们R如果LR（μJ）-终止J意味着LR（μ）-终止。 我们说Θ是完全的，如果LR（μ）-终止于的蕴涵LR（μJ）-终止于J。根据我们的讨论（由于µq-终止和LR（q）-终止是一致的，见推论5.