理论计算机科学电子笔记57（2001）网址：http://www.elsevier.nl/locate/entcs/volume57.html22页通过惰性重写的紧凑规范化跟踪阮光辉洛丽亚·因里亚BP 101，54602 Villers-l es-Nancy Cedex，France摘要在编译术语重写系统（TRS）时，通常使用最内部的策略，因为它们允许以自底向上的方式高效地构建结果术语。然而，最内层策略并不总是给出最短的规范化推导。在许多情况下，在函数符号的参数上使用适当的惰性注释，我们只在必要时才评估惰性参数，因此，获得更短的范式推导，同时避免无终止的约简。在这项工作中，我们我们应用我们的结果，以提高效率的方程推理Coq证明助理使用ELAN作为外部重写引擎。1引言像PVS[4]、KIV[17]或Coq[13]这样的证明助手提倡使用等式推理来提高效率并减少用户交互。在Coq中，证明对象存储在每个演绎步骤中。证明的正确性通过对这些对象进行类型检查来确定。这种机制提高了可靠性，并允许从证明中提取出经过认证的程序。其规格。然而，等式证明需要大量的用户交互，并且生成的证明对象是巨大的，因为它包含重写步骤的上下文。在[1]中，我们提出了一种使用ELAN[19]作为快速预言机来处理这些问题的方法：Coq将术语规范化过程委托给ELAN，然后重放ELAN提供的规范化轨迹，这些轨迹是h规则标签对的列表;收缩redex i的位置以获得规范形式（NF）。轨迹重放包括Redex与规则左侧（LHS）的句法模式匹配和Redex1电子邮件：Quang-Huy. loria.frc 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。Nguyen2右手边（RHS）。由于ELAN已经给出了规则和redex，因此在最坏情况下，Coq中的语法模式匹配与redex的大小是线性的。与此同时，发出redex的成本取决于条款的大小，这可能非常巨大。因此，ELAN执行证明搜索，Coq稍后检查此证明。Coq和ELAN必须在相同的规范（并发和终止）TRS上工作。在这种情况下，ELAN应向Coq返回尽可能紧凑的轨迹，以最大限度地减少重放所需的时间。这个时间不仅取决于重写步骤的数量，而且还取决于收缩的redices的位置，因为收缩内部redices创建更大的证明对象。Fokkink、Kamperman和Walters在[8]中提出了带惰性注释的惰性重写：函数符号的每个参数都被注释为lazy或eager。只有热切的争论才被热切地减少。一个懒惰的参数是减少只有当这个减少创建新的redexes之间的活动subterms包含它。我们将给出一个正式的定义活动subterms在第3节，但可以看到他们作为子项，允许积极减少，根始终是积极的默认情况下。总之，在本文的后续部分中，我们将带有惰性注释的惰性重写称为惰性在许多情况下，惰性重写可能比最内层重写提供更短的NF派生，因为惰性参数是根据需要计算的此外，延迟重写允许通过避免非终止分支上的减少来处理nite结构。在使用非终止TRS时，此属性非常重要。由于惰性注释，术语的某些子术语在惰性重写期间不会被重写。这些子项称为lazy。惰性重写将项归一化为惰性范式，其中所有活动子项都处于头范式（HNF）。一些惰性子项可能是可约的，但是如果TRS不是终止的，则它们的约化可能不是nite的。否则，所有的惰性子项都可以递归地被规范化，直到HNF。在这种情况下，惰性重写提供了一种获取NF的方法。同样在[8]中，作者展示了如何通过关于（w.r.t.）一个新的TRS通过转换- ING原始TRS获得。这个转化过程被称为转化。一个模拟是正确的，如果它是完整的，健全的和终止保持[12][7]。换句话说，正确性保证原始TRS中的NF上的信息不会丢失。此外，我们强烈关注的关系之间的规范化推导，以保持懒惰的规范化痕迹仍然有用的证明助手。在本文中，我们展示了在原始和转换TRS的归一化迹之间的对应关系如果TRS是终止的，则该过程产生输入项的NF，并且因此，如果TRS是规范的，则它们的唯一NF。另一方面，该过程中的所有归一化任务都使用最左-最内策略，可以在ELAN中高效地执行。我们的标准化程序被用来Nguyen3在使用相关惰性注释的情况下，我们可以得到更短的规范化推导，以替换最左最内的规范化。此外，由于子项是以自上而下的方式依次约简为HNF的，因此在此过程中，外部redice通常首先收缩。Thunki cation只适用于TRS，其中在重写规则的左侧，没有非变量项放在函数符号的惰性参数上。在[8]中，作者通过将原始TRS转换为最小TRS（即每个LHS包含不超过两个函数符号）来处理这个问题[7]。因此，这种转换产生了相当多的新的但简单的规则和新的功能符号。由它们的变换给出的最小TRS对于抽象重写机（ARM）[7]是最优的，但对于ELAN不是最优的，ELAN的编译器使用了[10]中提出的多对一模式匹配算法的改进版本。此外，这种转变通过引入新的函数符号和新的性质来关注LHS。这事实改变了redices的位置，因此，使得规范化推导之间的对应关系更难以建立。因此，我们在本文中提出了另一种变换（初步变换），以克服左线性构造器为基础的TRS的thunki阳离子的限制，同时保持良好的对应关系规范化的推导。由于在这项工作中允许TRS重叠，因此需要明确显示重写规则之间的顺序。像大多数函数式语言一样，ELAN使用文本排序，我们决定保留它，而不是使用特定的[8]城市规划[8]另一方面，我们只考虑减少（重写，懒惰重写）在没有变量的条款（地面条款）。此外，所有重写规则都必须是左线性的。如果TRS不是左线性的，则Thunki阳离子的完全性不成立。例如，通过检查实例化相同变量的项的原始形式（在原始签名中）之间的相等性，可以设想一些扩展。但是，如果转换变得过于复杂，那么性能的提高就不那么明显了。本文的组织结构如下。在第二节中，我们简要回顾了术语重写的标准定义第三节给出了一个基于规则的懒惰重写的定义在第4节中描述了Thunki阳离子，其中我们显示了归一化迹线之间的对应关系。在第5节中，我们提出了基于惰性重写的规范化过程第6节描述了初步转换。 在第7节中，给出了一个完整的例子，以说明两个变换的组合。最后，我们讨论了一些相关的工作。 所有缺席的证明可以在www.example.com上找到完整的版本http://www.loria.fr/~nguyenqh/publication。2项重写我们主要使用[5]中介绍的符号。特别地，签名由变量的集合V和函数符号的集合F组成。Arity ofNguyen4`;pRF中的函数符号f由ar（f）表示上的项集用T表示，而在写作G。以项t为标题的函数符号由Head（t）表示一个项是线性的，如果没有变量可以出现一次以上。项中的位置由描述从项的根到该位置处的子项的头的路径的自然数序列表示。词根的位置是一个空序列，用表示。项t中的不可变位置的集合由FPos（t）表示以项t的位置p为根的子项用tjp表示。我们 用t [s] p表示t项，它在p位置的子项由y项s代替。子项tjp1 是子项t j p2上下文 如果p1是p2的前x。替换是从V的变量到项的映射如果是一替换，则t表示在t上应用的结果。我们写tfx7！sg项t，其中变量x的每次出现都被项s替换。如果存在一个不变子项tjp和一个替换项，则项s与项t重叠 使得s=t jp。注意s和t的变量是如有必要，请在之前重命名，以便它们不相交。 根据这一定义，项t总是在根位置重叠。然而，这种情况是微不足道的，不被认为是重叠。如果s与t重叠，则两项s和t重叠，反之亦然。T上的重写规则是项的有序对h l; r i，并且由l！ R.我们把l和r分别称为规则的左手边和右手边。重写规则通常受到两个条件的限制：LHS不是变量，RHS中发生的所有变量必须包含在LHS中。如果重写规则的LHS/RHS是线性的，则重写规则被称为左线性/右线性一组重写规则R在T上被称为术语重写系统（TRS）。为了识别TRS中的重写规则，在本文中，重写规则通常用[`] l！r，其中`是规则的标签。一个TRSR被称为左线性的，如果它的所有规则都是。如果两个（不一定是不同的）规则的LHS重叠，则TRS是重叠的如果F中的一个符号是R中某个规则的LHS的头符号，则称它为TRSR的定义符号。不是定义符号的函数符号称为R的构造器符号如果没有指定的符号可以出现在LHS中，则R称为基于构造器的在基于构造器的TRS中，仅允许在LHS的根处重叠设R为TRS。T中的项s在一个重写步骤中重写为T中的项t，如果存在某些规则[`] l！R中的r，s中的位置p，以及替换假设：s [r] p=l且t=s[r]p。我们用y来表示这个重写步骤！Rt或s！t和reive-transitive关闭关系！R by！ . R中的一个导子是一个ny（nite或in nite）重写步骤的顺序。从操作的观点来看，重写步骤包括两个阶段：给出替换的sjp和l之间的模式匹配，以及用r替换s中的redexsjp。由于句法模式匹配只产生一个解，所以位置p和标签“successful”用于记住给定项s上的重写步骤。对h`; p i被称为Nguyen5！！nR我我这个重写步骤的踪迹。子项sjp也被称为redex，因为它是R中某个规则的LHS 一个项被称为标准形式w.r.t. R，如果它不包含Redex。从项到其NF之一的推导被称为该项的归一化推导。定义2.1（归一化迹线）如果t=t1`1;p1 t2`2;p2* *不！;pnt是一项t的归一化推导R，然后列表TR= fh` ;pi;：;h` ;pigt1 1n n是t的相应归一化迹。项t是头范式（HNF），如果没有redexs使得t！S.如果一个术语在HNF中，那么它的头部符号不能在任何衍生自它。因此，如果一个项t和它的所有子项都在HNF中，那么t也在NF中。在这篇文章中，我们使用了符号！七！ 描述了新算子定义中的评价规则。3懒惰术语重写签名首先被赋予一个laziness注释，该注释标记了其函数符号的每个参数的lazy或eager。定义3.1（懒惰注释）设=（V; F）为签名。的惰性注释L是从F到fe; lg的映射，使得：8 f 2F;L（f）是一个ar（f）-tuple = hx 1;：; x ar（f）i其中x i=l表示f的第i个参数是惰性的; x i=e表示这个参数是渴望的。用f表示L（f）的第i个元素。在续集中，当谈到懒惰重写时，签名总是包括其懒惰注释。这个惰性注释将术语中的位置集分为两个子集：活动位置和惰性位置，这就是我们现在定义的。定义3.2（主动位置和惰性位置）设t是G中的一项。 我们拥有：- 根出现总是一个活跃的位置。- 对于t的任何位置p，使得Head（t j p）=f且8i = 1：ar（f）：p：i是有效的当且仅当p是且f= e;否则，p：i被称为惰性位置。项t中的活动位置的集合由APos（t）表示根在主动位置的子项称为主动的。这个术语的其他子术语因此，t的子项是活动的，当且仅当从其头符号到t的根的路径不包含将函数符号连接到其惰性参数之一的边。Nguyen6惰性重写是（正常）重写的一种受限情况。惰性重写仅适用于活动子项，惰性重写的一个关键行为是，Nguyen7psymbol标题为t的活动子项：（s;p;e）！七！sa和（s;p;l）！七！斯湖它可以将子项的惰性属性从惰性更改为活动（子项激活）。为了在项t上应用惰性重写，我们首先装饰它。也就是说，我们用u x注释t的每个子项u，其中p是u在t中的位置，x= a表示u是活动的，而x= l表示u是惰性的。一个lazy子项的所有子项也是lazy。下面的运算符修饰子项s，它以位置p为根，并作为p p设t是G中的一项。 我们将t与修饰项tDC = DC（t a）相关联其中DC由图1中的规则定义。符号对于任何f2F：DC（fa（t1;：;t））！七！fa（DC （（t1;p：1;fn;p：n;fn）））Nguyen8））;：;DC （（tpnp1DC（fl（t1;：：：;tn））！七！fl（DC（t1l）;：;DC（tnl）的情况）ppp：1p：nNguyen9对于任何常数c：DC（ca）！七！ca和DC（cl）！七！clppppFig.1.名词修饰设G_D_init是对项应用D_C生成的修饰项的集合以G ：GDinit=ftj9s2G：t= DC（sa）g. 另一方面，让我们表示由GDterm修饰生成的所有可能修饰项的集合术语G（GD初始化GD终端）。 映射UD：GDte rm！G删除所有装饰和返回初始条件。在规则l的修饰项t的根处进行的懒惰重写！ r表示为[l！ r]（t），并由图2中的规则描述。 这些规则变换一个4元组：第 一个分量是要约简的项;第二个分量是基本子项（ES）的位置集合，即t的惰性子项，其对应于l的不可变子项;第三个分量的形式为（l 1;：;ln！其中l 1;：;l n是l的子项;第四分量是要与l 1;：; l n对应匹配的修饰项的列表。这些规则的目的是在[3]中为术语重写所做的相同过程中对模式匹配和惰性重写进行建模。规则SymbolClash返回初始项，以防在模式Nguyen10匹配阶段由t的活动子项引起的冲突。懒惰的子项永远不会引起冲突。这一事实将延迟重写中的模式匹配与（正常）模式匹配区分开来，延迟重写被称为模式匹配模惰性如果t的一个子项是惰性的，而l的相应子项不是变量，则这个惰性子项在-Nguyen11RRsa al将其位置插入ES。如果作为t的有效子项的根的符号与l中的对应符号匹配，则应用分解。Instan-itiation实例化RHS的变量，其中子项没有t的装饰。如果ES为空，则替换项由（修饰的）实例化的RHS替换。在这种情况下，没有必要的子项被揭示，模式匹配模懒惰与模式匹配相同。此外，是模式匹配模惰性返回的替换。如果ES不为空，则应用激活来激活t的一个基本子项s，并且因此激活s的所有有效子项。可以使用不同的策略（最左，最右，.）.然而，本文中提出的结果是独立的所使用的策略。如果应用激活或替换，则执行惰性重写步骤，并且t被称为（惰性）redex，因为它将模惰性与l匹配。形式上，（修饰的）项t与线性模式l匹配模惰性，当且仅当作为t的活动子项的根的符号与l的对应符号匹配：8p2 AP os（UD（ t））\FP os（ l）：H ead（UD（ t）jp）= H ead（ ljp）图3描述了在被修饰的项t内执行惰性重写的算子LR：LR通过对子项应用惰性重写的结果来替换该子项。此外，该结果的修饰需要通过移位算子SH：GDte rmN来适应其在t中的位置！GDtermsuchSH（s; p）在s和所有的装饰中的位置上添加了一个pre xp其子项。我们分别表示懒惰重写关系w.r.t.R和它的环exive-transitiveclosure由y;R和; . 一个懒惰的重写步骤由一个规则`;p术语的p表示为yi。定义3.3（惰性范式）修饰项t被称为是惰性范式（LNF）w.r.t. R如果不存在修饰项t0使得t;t0.例3.4（[15]）考虑下面的TRS（在nite列表中）：[r1]第二次（cons（x; cons（y; z）！ yR =：[r2]inf（x）！ cons（x; inf（s（x）））其中L（2nd）= h e i; L（inf）= h e i; L（cons）= h e; l i。项t= 2nda（ infa（0a））被导出到其LNF如下：r2;1a不1a al1：1的比例sllr1;01 - 02 01-01：2：1（01：2：1：1）;第二个a（consa（0a;infa（sa（0ar2;1：2）;十一比一一比二一比二比一1：2：1：12nda（consa（0a;缺点a（sa（0a）;infl（sl（sl（0升））））））十一比一一比二一比二比一1：2：1：1一比二比二1：2：2：11：2：2：1：11：2：2：1：1：1r1;（0）. 在第二步中，基本子项inf（sl（0升））十一比二一比二比一Nguyen121：2：1：1激活Nguyen13ppp初始化[l！ r]（t）！七！ [t][;]（l！（t）分解对于任意f2F[t][ES]（： ; f（t1; ：;tn）; ：！ r）（：; fa（s1; ：;sn）; ：）！七！[t][ES]（：; t 1;：; t n;：！r）（：; s1;：; sn;：）SymbolClashF或anyf;g2F且f6=g[t][ES]（： ; f（t1; ：;tn）; ：！ r）（： ： ：;ga（s1; ： ： ：;sm）; ： ：：）！七！不对于任意f 2 F，任意子项s用l：[t][ES]（： ; f（t1; ：;tn）; ：！ r）（： ;s; ：）！七！[t]（ES[fpg]（： ;： ：！r）（： ;： ：）实例化对于任何x 2 V，任何修饰的子项s：[t][ES]（： ;x; ：！ r）（： ;s; ：）！七！[t][ES]（：;：：！r f x 7！U D（s）g）（：：：：：：）更换激活[t][;]（！ r）（）！七！DC（ra）[t][ES[fpg]（！ r）（）！七！t[DC（UD（tjp）a）]p图二、惰性重写的求值规则Nguyen14;Lr;！UD图3.第三章。项内惰性重写的求值规则如果tjp用 L修饰LR（t; p;l！r）！七！不LR（t; p;l！ r）！七！ t[SH（[l！r]（tjp）;p）]p如果tjp用a对于任意修饰项t，UD（ t）中的任意位置 p和任意规则l！r 2 R：注3.5设t和t为两个修饰项. 如果我！通过应用！替换规则，然后UD（t）（t0）。否则，如果我！rt0byapplyNguyen15R激活规则，则UD（t）=UD（t0）。接下来的命题说明了懒惰重写和在同一个TRS中重写之间的关系。命题3.6如果t在LNF w.r.t. R，则UD（t）在HNF w.r.t.中。R.证据通过归纳得出t的大小。如果t的大小为1，则t是常量或变量：t是活动的，并且t具有没有懒惰的子项。由于LNF的定义，UD（t）在HNF中。现在假设这个命题对所有大小严格小于n的项都是正确的。t的子项的大小小于或等于n1。假设UD（t）不在HNF中。也就是说，存在一个项s2g和一个规则l！r2 R使得UD（t）！ s和s与l（*）匹配。注意到从UD（t）到s的推导仅收缩根以下的redices因为t在LNF中，所以它的所有有效子项也在LNF中通过归纳假设，这些子项（去掉修饰后）是HNF，它们的中心符号不能被UD（t）（**）的任何推导所改变（*）（**）意味着作为t的有效子项的根的符号与l的对应符号匹配。换句话说，t与l匹配模惰性，并且t不在LNF中，这与假设相矛盾并使证明失败。2由于LNF的活动子项也在LNF中，因此LNF的所有活动子项（不带装饰）都在HNF中。命题3.7如果re存在无穷导子t0;Rt1;R： ：：，则re存在k2N使得UD（t0）！RUD（tk）.证据通过应用Activation终止的延迟重写步骤严格减少了延迟子项的数量。因此，在推导中不存在这些延迟重写步骤的也就是说，存在一个最小的k1通过应用Replaceme n t，可以使tk1;Rtk保持不变。 由于注释3.5，我们有：UD（t0）=：=UD（tk1）！RUD（tk）.2这个命题的一个直接推论是，如果重写w.r.t.R是终止的，那么懒惰重写w.r.t.也是R不管懒惰注释。4通基阳离子Thunki阳离子已经在[8]中描述了懒惰图重写。我们考虑惰性项重写，并且不要求原始TRS的LHS最小[7]。这一事实需要在证明中做一个小的概括。我们的thunki阳离子工作在左线性，但可能重叠的TRS，所有懒惰的LHS子项必须是一个变量。在这种情况下，在惰性重写步骤中不可能激活子项，因为惰性子项总是对应于模式的变量换句话说，延迟重写步骤总是以Nguyen16D初始化我0应用替换规则，并且因此，惰性重写推导仅包括GDini t中的项。4.1Thunki cation描述Thunki cation扩展签名并生成新的TRS，通过该TRS，最内重写模拟原始TRS中的惰性重写新的签名0是从原始签名=（V; F）通过添加在挖掘期间引入的新的函数symb来构建的：;f;vecf;vec t; t; inst，用于每个f 2 F和用于原始TRS中的重写规则的RHS的一些子项t。新函数符号的引入允许屏蔽惰性子项。一个懒惰的f-根子项s被一个形式为（f;vecf（： ））的子项屏蔽（或thunked），因此，不能急于重写。s的结构存储在这个-root子项中，以便以后可以恢复它。术语的thunki cation是一个映射：G！的g0 这是德-根据图4中的规则。我们现在描述由thunki阳离子产生的新的TRS。定义4.1（惰性论元位置和子项）设t是G中的项.若存在p2 FPos（t）和i2N，使得Head（tjp）=f，且f=l，则p：i被称为t中的惰性参数位置，而tjp：我被称为t的惰性参数子项。定义4.2（迁移变量[8]）出现在重写规则的LHS中的惰性参数位置和RHS的子项t中的活动位置的变量称为t中的迁移。在惰性重写步骤之后，实例化迁移变量的子项的惰性属性从惰性变为活跃。因此，我们需要稍后激活这些子项的延迟重写。定义4.3（规则集）设R是一个TRS。通过在R上应用化归生成的重写规则集S是四个子集S0、S1、S2和S3的并集，其定义如下：(i) S包含规则l！r0当且仅当l！r2 R和r0由 r构建如下：以自底向上的方式，用y（t;vect（x1; ： ： ：;xnt））替换RHS r的任何惰性参数子项t，其中x1; ： ： ：;xnt 都是t的变量。将RHS r的任何迁移变量x替换为inst（x）。(ii) S1=finst（（f;vecf（x1; ：;xa r（f ）！f（t1; ：;tar（f ））jf2Fg，其中如果f = e，则t =inst（x）;否则t = x。我我(iii) S = finst（;vec（ x;：;x））！t0jt已在（i）中被替换，2t t1ntt 0=t f x i7！inst（x i）g8 i使得x i是t g的迁移变量。Nguyen17(iv) S 3= f inst（x）！x g.事实上，S0包含了R中所有RHS被改变（或thunked）的重写规则：每个惰性参数子项t都被一个形式为（t; vect（：））的子项thunked，因此t不能被急切地重写。然后将相应的规则插入到S2中，以便稍后恢复t插入符号inst允许之后重写具有实例化迁移变量的子项S3的唯一性规则允许处理符号inst中未被thunked的直接子项。这条规则具有最低的优先级，因此是S的最后一条规则，因为我们使用文本排序。在[8]中，只有RHS的不可变惰性参数子项被thunked。由于S将使用最内层策略进行重写，因此在应用任何规则之前，实例化RHS变量的子项总是在NF中。换句话说，作为变量的惰性参数子项的thunki是不必要的。然而，在这项工作中，我们也thunk这些子项，以确保在第5节引理5.1的正确性。（i） '（fa（t1; ：;tn））！七！p（ii）'（fl（t1; ：;tn））！七！p（iii）“（ca）！七！p（i v）' （cl）！七！p图四、f（'（（t1;p：1;f））;：;'（（t;p：n;1N（f;vecf（'（t1l）;：;'（tnl）））fn）））Nguyen18D初始化p：1p：n如果c是常数。（c;vecc）如果c是常数。评估规则'项B的集合定义如下：B=fg2G0 j 9g02G：'（g0）！SGGB的这个定义与[8]略有不同，在[8]中，g 0不被thunked（by '）。 对g0的量化有助于得到NFw.r.t. 更快。这一事实在第5节的标准化过程中得到了应用。地图：B！ GDinit将B中的项和GDinit中的项关联起来，由图5中的规则定义。实际上，恢复懒惰的子项使用的信息存储在其相应的根的子项。4.2Thunki阳离子在GDinit中对项进行延迟重写w.r.t. R可以正确地模拟为最内层重写的条款在子集B的G0 w.r.t. S经由 符合标准[12]。也就是说，它是满射的、完整的、保终止的。这个映射是满射的，因为对于Nguyen19SRR中一[中（i）（g）！七！（g;e）（ii）（inst（t）;p;e）！七！（t;p;e）㈣（（;vec（t; ： ：; t））;p;e）！七！ fa（（t;p：f f1np11nn（v）（（f;vecf（t1; ： ：;tn））;p;l）！七！fl（（t1;p：1;l）; ： ：;（tn;p：n;l））p㈥（（c;vecc）;p;e）！七！ 如果c是一个常数。pp（viii）（（t;vect（t1; ： ：;tnt））;p;e）！七！ （tfx17！ t1g：fxnt7！tntg;p;e）（ix）（（t;vect（t1; ： ：;tnt））;p;l）！七！ （tfx17！ t1g：fxnt7！tntg;p;l）㈦（（c;vecc）;p;l）！七！ 如果 c是一个常数。（x）（f（t; ： ;t）;p;e）！七！ f（（t;p：1;）; ： ：;（t;p：n;））1n一FFp11nn（Xi）（f（t; ：;t）;p;l）！七！ f（（t;p：1;l）; ： ：;（t;p：n;l））1nLp1n（xii）（c;p;e）！七！ Ca 如果c是常数，则为t。p（xiii）（c;p;l）！七！ Cl如果c是常数，则为t。p图五. 评估规则D初始化：（'（g））=g. 在下面的翅膀，！S表示最内层的重写相对关系S.定理4.4（合理性[8]）Letg e是B中的一项。 如果g！g0，则（g）; （g0）. 更准确地说：如果g！g0，则（g）; （0）如果g！g0，则（g）=（g0）.引理4.5（[8]）如果g2 B不包含符号inst，则（g）的每个有效子项从g的对应子项继承头符号.定理4.6（完备性[8]）若g2 B在NF w.r.t. S，则（g）在LNF w.r.t.中。R定理4.7（终止保持[8]）若存在无穷导子g0！Sg1！S： ，则re存在k2N使得（g0）;R（gk）.推论4.8如果懒惰重写w.r.t. R是终止的，那么最里面的重写w.r.t.也是终止的。S.4.3迹线对应在本节中，我们证明了（g）w.r.t.的（惰性）归一化迹。R可以从gw.r.t.的归一化迹线中提取。S.假设S0中的每个规则都继承了R中相应规则的标签，我们有：GS0Nguyen20G定理4.9（迹的对应）设TS是正规的-g2 B项w.r.t.S在最内层约简策略中。
我的内容管理
展开
