ELAN系统中证明重写程序终止性和规范化的方法总结

理论计算机科学电子笔记36（2000）网址：http://www.elsevier.nl/locate/entcs/volume36.html28页ELAN中策略证明下的可终止性和规范化H'el'eneKirchner和IsabelleGnaedigLORIA-CNRS和INRIA-LorraineBP 23954506VandÜuvre-l`es-NancyCedex，FranceEmail：Helene. loria.fr，gnaedig@loria.fr摘要在本文中，我们回顾了几种方法来证明重写程序的终止性或回答有关规范形式的问题。我们集中在方法，已设计的ELAN和这是有用的研究终止和规范形式的ELAN程序。我们解决几个问题：重写程序的一般终止、基项集合上的最内终止、范式集合的计算或近似、重写系统的并集的模块化终止、具有策略的非确定性重写程序的范式数目的估计。对于每一点，我们简要介绍了一种方法，解释其范围，并提供参考其他方法对同一问题，然后描述在ELAN的实现。最后，我们提出一些开放性问题。1介绍这里提出的终止和规范化问题的研究的一般背景是由基于规则的编程语言ELAN[BKK+ 96，BKK+ 98]给出的，它提供了一个环境，用于指定和原型化演绎系统，一种基于重写规则并由策略控制的语言ELAN是一个设计证明工具的框架，支持定理证明器、逻辑程序设计语言、约束求解器和决策过程的设计，并提供了一个研究它们组合的模块化框架因此，本文中提出的用于证明重写程序的终止性或回答有关规范形式的问题的大多数方法都是在ELAN中开发的，这并不奇怪重写逻辑的反射能力[CM96]给出了将它们应用于ELAN程序的潜力然而，这里介绍的方法和技术超越了ELAN，适用于基于规则的语言，如ASF+SDF [Kli 93]，Cafe-OBJ [FN97]或Maude [CELM 96]。ELAN系统在第2节中介绍，该节还介绍了重写系统和终止的初步概念和符号。2000年由ElsevierScienceB出版。 诉 操作访问和C CB Y-NC-ND许可证。2在基于规则的编程语言中，程序是一组规则，查询是一个输入表达式，计算是将表达式归约为它们的范式。结果可能是唯一的，也可能不是唯一的，并且某些计算可能不会终止。在某些情况下，例如对于功能评估，终止是非常重要的，因为至少有一个结果是预期的。终止对于检查计算是否具有唯一结果也很重要，通过局部连续性属性。第三节回顾了如何用句法良据序证明终止。本文描述了一种简化排序的实现。有了这样的排序，它是足够的证明，每个规则的左手边大于右手边，以确保重写程序的终止大多数函数式语言都有隐式求值策略，通常内置于编译器或解释器中。例如，ASF+SDF [Kli93]或ELAN中的无标签规则就是这种情况，其中最内层的策略用于约简。然后，当然，存在这样的程序，它终止于这个最内层的评估策略，但一般不会终止。第4节中讨论了系统的最内部终止，这些系统通常不会终止此外，并不总是需要证明所有条款的终止。在实践中，重写系统通常被设计为重写来自子集E的项，例如析取范式中的逻辑公式、注意列表或良好类型的项。同样，一些重写系统可以仅在这样的子集E上终止。第5节中介绍的基于自动机的技术非常适合这种限制。它们允许研究E中项的后代，即程序在其执行的每一步的所有中间结果，以及E的R-范式的集合，即当程序停止时，通过在可能的给定输入E的集合上执行程序R而获得的所有可能结果。根据左线性假设的规则，这两个集合中的每一个都包含在一个由近似自动机描述的正则树语言一旦建立，这个自动机可用于检查重写程序的属性。例如，可以证明某些表示死锁或错误的值实际上是不可访问的。将终止重写程序放在一起并不能确保它们的联合终止然而，重写程序的层次结构可以提供帮助，一个有趣的问题是研究模块化规范化策略，例如首先用一组规则进行规范化，然后用另一组规则进行规范化，并证明这个过程的终止。这种所谓的顺序归约策略结合了不同的终止性证明方法，可用于证明程序的终止性。第6节研究了重写系统的并集的模块化终止。在ELAN中，一个程序由一组未标记的规则和一组标记的规则组成，其中未标记的规则应用于最内层的归约策略，而标记的规则的应用则由策略定义，这些策略是从规则标签和语言中可用的策略构造器（不关心，不知道，首先，重复，然后）构建的在这些用户定义的策略下终止程序是一个开放的问题。然而，可以对程序执行静态分析，以检测它是否没有结果，只有一个或多个。这种技术对于检测某些非终止情况也很有用。带策略程序的范式分析是3∈ TF XFV V→TF {}XF ›→ X T F X FFR→ ∈ T FX/∈ XRR在第7节中解释最后，开放性问题在第8节中陈述本文中提出的大多数结果是与Protheo集团的其他成员，即Olivier Fissore，Thomas Genet和Pierre-Etienne Moreau合作获得的。2初步概念和符号全面的调查可以在[DJ 90，BN 98，Kir99，KK 99]中找到重写系统。本文中使用的定义和符号在第2.1节中回顾，关于终止的简要调查在第2.2节中介绍然后在第2.3节中介绍ELAN系统，并给出激励本研究的一般背景2.1术语、替换、重写系统设是一个有限的符号集，与一个由ar表示的arity函数相关联：N，是一组可数的变量（、）项的集合，以及（）基项的集合（没有变量的项）。上下文是一个只有一次出现的（，）项，其中是一个不出现在中的特殊常数。对于任何项t （ 、 ），C[t]表示在上下文C[]中用t替换t项中的位置表示为整数序列项t中的位置集合，记为Pos（t），按整数的字典序空的序列表示最顶端的位置。Root（t）表示在t中的位置n处的符号。若p∈Pos（t），则t|p表示t在位置p处的子项，t [s] p表示通过替换子项t而获得的项|p在位置p处由项s表示。对于任意项s∈ T（F，X），记为PosF（s）s中函数位置的集合，即{p∈ Pos（s）|p/= r和Rroot（s|p）∈F}。项t的变量集由Var（t）表示。 一组变量{x1，.，xn}也由x表示。一项是线性的，如果任何变量Var（t）在t中只出现一次.置换是从X到T（F，X）的映射σ，它可以唯一地扩张到T（F，X）的自同态。 它的定义域Dom（σ）是{x∈X| xσi = x}。重写系统是一组重写规则，r，其中l，r（ 、），l和ar（l）ar（r）。重写规则l r是左线性的（相应地， 右线性），如果左手侧（分别（右）规则是线性的。一个规则是线性的，如果它是左线性和右线性的。TRSR是线性的（相应地，左线性，右线性），如果R的每个重写规则l→r是线性的（分别为左线性，右线性）。出现在TRS R中的函数符号F的集合可以被划分成定义符号D={R_oot（l）|l→r∈ R}和构造函数集C= F \D. 构造函数项是没有定义符号的基础项。构造函数项的集合由T（C）表示。由R诱导的关系→R定义如下：对任意s，t∈ T（F，X），s→Rt，如果R中存在规则l→r，位置p∈Pos（s）和置换σ使得lσ = s|p和t = s [rσ] p。 子项s|p称为redex。及物（分别） R的闭包记为→+（或R的自反传递闭包）。 →A）。 一个术语4{∈ T→FX∈TF X→ → ∈ TF XR可被R约，如果存在t使得s →Rt。一个项s是R-正规形式（或R-不可约），如果s不能被R约. 项s有正规形，如果存在R-正规形项t，使得s→t。 项t也用s ↓表示。R-正规的所有基项的集合好吧！形式记为IRR（R），当t∈IRR（R）时s→Rt记为s→Rt.基项集E的R-下降项的成立记为R_y（E）和R∈（E）={t∈T（F）|εs∈Es。t. s→t}。的基R-正规形的成立E表示为R！（E）和R！（E）=R（F）|s∈E s. t. s→！t}。此外，委员会认为，tRR！（E）=R（E）IRR（R）。一般来说，我们考虑形式为l→r的条件重写规则，如果cw，其中c是一个叫做条件的布尔项，写成s→t形式的合取。如果由从l到要归约的项的匹配实例化的条件满足，则该规则适用。条件重写系统的终止属性可以使用以下变换简化为无条件重写系统使用[OCM00]中描述的以下变换U将c中具有n个条件的每个规则lrifc变换为n+1个U（l→rifc）={l→r}ifc is empty{l→u（s，x）} <$U（u（t，x）→rifc′）ifc=s→t<$c′其中u是新函数符号，x=Var（l）<$（Var（t）<$Var（c′）<$Var（r））2.2终止重写系统R是（1）终止的或强正规化的，如果不存在无限导子s1Rs2R... 其中s1，s2，. （ 、），（2）弱正规化（简称WN），如果（，）的每个s都有一个正规形，（3）在E（，）上弱正规化（WN onE），如果每个s E都有一个正规形，（4）（强）最内终止，如果不存在无限的最内导子（即导子，其中所选择的兑换没有正确地包含其他兑换）。现有的重写系统可终止性证明方法基本上都是基于包含重写关系的良基序。在这些方法中，处理自由项代数上的终止，我们找到了语法和语义方法，它们通过分析TRS中的项结构提供了Noether排序，并确保对于所有项s和t，s→t，意味着s t。 [2018 - 07 - 28]《易经》的经典之作词典路径排序（LPO）[KL 80]，递归路径排序（RPO）[Der82]，多项式解释[Lan79][BCL 87]和一般路径排序（GRP）[DH95，GG97]，这是对以前的路径排序的推广。另一种方法是将TRSR到另一个TRSRJ的终止问题，证明与技术的前一个条件y和su c h，对于所有项s和t，s→jRt意味着s→jt。5≥ →≥≥例如转换技术[BL90]或语义标记[Zan95]。另一种证明重写系统终止的强大方法在[AG00]中描述。将重写系统看作程序，其思想是无限减少源于这样一个事实，即定义的符号由规则的右侧引入通过追踪这些定义符号的引入，可以获得关于R终止的信息。这就是依赖对标准如果f（t1，...，tn）→t [g（s1，.，sm）]是R中的规则，其中f和g被定义为符号，并且t是某个上下文项，则对（f（t1，.，tn），g（s1，.，sm））是R的依赖对。在[AG97a，Art97]中提出的技术如下：构建依赖图，其顶点用依赖对标记存在从（s，t）到（u，v）的边，如果存在一个置换σ使得thattσ−→<$Ruσ。由于这最后一个命题通常是不可判定的，图必须用具有相同圈的超图来近似依赖然后使用对来生成一组不等式。如果这些等式可以通过适当的良基序满足，则R是终止的。 更确切地说，如果存在一个拟序，良好基，在上下文和替换下封闭，使得lr对于每个规则lr in R，s对于每个依赖对（s，t），如果依赖图的每个循环上的依赖对（s，t）为s > t，则R终止。该方法也可以证明R的最内终止性。2.3ElanELAN是一个基于策略控制的重写规则的语言演绎系统的指定和原型环境它为计算和演绎范式的结合提供了一个自然而简单的逻辑框架ELAN具有基于重写逻辑[BKKR 01]和重写演算[CK 99]的清晰操作语义 它的实现涉及编译匹配和减少技术集成的关联和交换功能。非确定性计算返回几个结果，其枚举是由几个选择策略的构造函数处理的。策略语言可用于控制重写。策略的评估和策略的应用也是基于重写。该语言接近于代数规范形式主义，但提供了值得强调的附加规范。• 首先，该语言允许规则是非终止和非连续的，但它们的应用必须受到控制。因此，有计算的规则，要求是连续的和终止的，以便给出唯一的结果，还有演绎的规则，既不需要连续也不需要终止• 规则和策略是语言中的第一类对象。提供了一种策略一些策略构造器被设计并有效地实现，以允许用户设计自己的策略。• 在一个词项上应用规则或策略可能会得到0、1或多个结果。6这种与结果集的产生相关的非确定性可通过回溯来操作性地处理。由于这些特性，该语言允许不同的编程风格。函数式程序自然地用连续和终止规则来表达，而用于处理搜索过程的回溯机制则提供了逻辑编程的便利，并允许对非确定性计算进行编程。主要的独创性是策略编程的能力，以声明的方式表达程序的该语言提供了以下策略构造函数。• 标签规则是原始策略。对术语t应用标记为lab的规则的结果返回术语的多集。如果结果项的多集为空，则此原始策略失败。• 两个策略可以用符号“;"连接起来，这意味着第二个策略应用于第一个S1;S2表示两种策略的顺序组合。如果S1失败或S2失败，则它失败。它的结果都是S1的结果，S2应用于S1，并给出了一些结果.• dc（S1，.，Sn）在列表中选择一个不会失败的策略Si，并返回 所有的结果。该策略可以返回多个结果，或者如果所有子策略Si都失败，则该策略失败。• 第一个（S1，...，Sn）在列表中选择第一个不失败的策略Si，并返回其所有结果。同样，该策略可以返回多于一个结果，或者当所有子策略Si失败时失败。• dc一（S1，...， Sn）在列表中选择一个不会失败的策略Si，并返回其第一个结果。此策略最多返回一个结果，如果所有子策略都失败，则返回失败• 第一个（S1，...，Sn）在列表中选择第一个不失败的策略Si，并返回其第一个结果。此策略最多返回一个结果，如果所有子策略都失败，则返回失败。• dk（S1，...，Sn）选择参数列表中给出的所有策略，并为每个策略返回所有结果。这个多结果集可能是空的，在这种情况下策略失败。• 策略id是什么都不做但从不失败的标识。• fail是指总是失败，永远不会有任何结果的策略• repeat（S）反复应用策略S，直到失败，并返回最后一次成功应用的结果该策略可能返回多个结果，但永远不会失败，因为S的零应用是可能的：在这种情况下，返回初始项。• 策略repeat（S）类似于repeat（S），但返回重复应用的所有中间这里介绍的一些策略构造器非常接近于在LCF风格设计的证明系统上使用的其他策略语言[Plo 77，GMW 79]，例如7→例如伊莎贝尔[Pau94]。它们被用来表达主要的控制结构：连接、迭代和搜索。所有这些构造器都是ELAN语言的一部分，并且对于设计ELAN定理证明和约束求解工具非常有用。从现在起，让我们考虑一下，不仅规则，而且战略也可以按条件应用。（S）t表示策略S在项t上的应用，它产生了一个多集结果。ELAN规则的一般形式实际上如下：[l] l→r，其中 p1：=（S1）c1. 哪里 pn：=（Sn）cn• l，r，p1，...，p n，c1，.，Cn∈ T（F，X），• Var（pi）<$（Var（l）<$Var（p1）< $ ··< $Var（pi−1））=<$，• Var（r） <$Var（l） <$Var（p1） <$· ·<$Var（pn），• V ar（c i）<$V ar（l）<$V ar（p1）<$· ·<$V ar（pi−1）。在这样的表达式中，wheretrue：=c通常写为如果c。模式pi经常被简化为变量x。Si可以是恒等式策略，写作（）ci或简称为ci。其中p：=（S）c的表达式也可以被认为是（S）cp，其中p是不可约项。一个额外的构造choose try允许因式分解具有相同左侧的规则的公共部分。例如，两个规则[l]l→r其中y1：=（）u1ifc′2（l，y1）[l]l→r其中y1：=（）u1ifc′2′（l，y1）被分解为一个规则：[l]lr其中y1：=（）u1选择tryifc′2（l，y1）tryifc′2′（l，y1）端在这种因式分解形式中，项u1仅被归一化一次，并且对y1的赋值也仅执行一次。ELAN规则的示例将在下一节中给出。ELAN程序的研究激发了广泛的终止和正常化问题。对于未标记的重写规则，最内层终止是相关的。由于语言是模块化的，终止的模块性也是一个问题。这可能是有趣的模块化评估策略，其终止是相对容易检查模块化的方式与不同的终止方法。对于由策略控制的标记规则，终止问题是广泛开放的。在这个方向上的第一步是帮助程序员检测一些非终结性的8F→FLPO程序.另一个要解决的问题是分析重写程序的策略的确定性。在下面的部分中，我们将考虑这些问题并提出一些答案。由于ELAN也是设计证明工具的框架，因此大多数这些方法都是在ELAN中开发的。由于重写逻辑的反射能力，我们希望在不久的将来将它们应用于ELAN程序。3用句法良基序证明终止性在2.2节中提到的句法排序是证明重写系统终止性的最简单但也是最基本的工具让我们考虑一个简单的语法方法来证明重写系统的终止性，基于简化排序，这是一个在上下文和替换下封闭的关于项的非自洽传递关系>，它包含子项排序。重写系统R是简单终止的，如果存在一个简化排序>，使得对于任何规则l r在R中，l > r。 当运算符符号的集合是有限的，重写系统R是终止的，如果R只是终止[Der82]。简化排序可以从函数符号上的良基排序建立，称为优先级。一个例子是下面的字典路径排序。定义3.1设>F是F上的优先级。字典式路径排序>lpo由s=f（s1，...，sn）>lpot=g（t1，...，tm）如果以下条件中的至少一个成立：（i）f=g且（s1， . ，sn）>lex（t1， . ，t，m），并且m∈{1， . ，m}， s>lpotj(ii) f>Fg，且fj∈{1， . ，m}， s>lpotj(iii) i ∈ {1，.，n}，使得si>lpot或si= t。字典式路径排序是一种简化排序[KL 80]。这种排序可以用来表示定义阿克曼函数的重写系统的终止假设优先级ack >Fsucc，这意味着对于每个规则，左侧大于右侧，即：ack（0，y）>lposucc（y）ack（succ（x），0）>lpoack（x，succ（0））ack（succ（x），succ（y））>lpoack（x，ack（succ（x），y））。为了同时说明ELAN语法，让我们展示一些来自实现排序的程序的规则。//lpolpo（@，@）：（term）bool;@>lex@：（list[term] list[term]）bool;lpo（@，@）：（list[term]term）bool;lpo（@，@）：（termlist[term]）bool;lpo1（@，@）：（term term）bool;lpo2（@，@）：（term term）bool;lpo3（@，@）：（term term）bool;//--------------------------------------------------------------------------------------9//Case：f（s1，...，Sn）>lpo f（t1，.，（tn）//如果s >lpot1，...，tnets1，.，sn>lex t1，...，TN//[] lpo（s，t）=> trueifnot（isvar（s））and not（isvar（t））选择尝试端尝试端ifhead（s）==sighead（t）其中b：=（）lpo 3（s，t）ifb其中b：=（）lp0 2（s，t）如果b[] lpo 3（s，t）=> b选择尝试尝试结束iflist_subterm（s）>lex list_subterm（t）其中b：=（）lpo（s，list_subterm（t））其中b：=（）false端////Case：f（s1，...，Sn）>lpog（t1，.，tn）如果f>sig g和s>lpo t1，.，TN//[] lpo2（s，t）=> lpo（s，list_subterm（t））端////Case：si>lpo t//[] lpo（s，t）=> lpo 1（s，t）端[] lpo1（s，t）=> lpo（list_subterm（s），t）end该程序用于ELAN应用程序，例如完成过程或下一节介绍的证明终止的最复杂程序其他的语法排序（RPO，RPO）在ELAN中也有类似的实现。4证明最内层终止到目前为止，证明最内层终止性的问题，对于可能的非终止系统，只有上面提到的依赖对方法[AG97b]才能解决在[GKF00]中，提出了另一种方法，并使用基于基项的良基排序的显式归纳法，该方法在上下文下是封闭的，并且包含子项排序。在证明过程中，通过添加与必须进行比较的基础项相对应的限制来递增地约束排序关系证明方法如下：假设<证明了t是最内终止的。这一种技术被用来证明终止在地面条件或确定通用模式f（x1，...，xm），其中f是定义的符号，是最内部终止的。该方法基于有限数目的树的发展，其中每一个树分析模式tref= g（x1，.， xn）其中g是定义函数符号10N↓↓∧> TF>>> >TF X N的签名和x1，. n是不同的变量。这些树是通过应用三种不同的机制构建的。• 第一个抽象了当前项f（u1，. m），同时可能设置一些约束。首先，约束tref>ui1，.，uip被放在一组约束C中，其中uij是u i中的那些约束，还没有正常形式的基础术语。通过归纳假设，证明了ui1，.的不可约形式的存在性uip，这些子项由所谓的NF变量Xi1，. Xip，它们是集合中的新变量，并且只能由范式中的基项实例化。这通过陈述约束Xi1= ui1. Xip= uip在集合A中。我们把这个步骤称为抽象步骤。 如果因为约束t > ui1，.，uip不能被证明是令人满意的，该过程因失败而停止。• 第二步缩小所得项f（U1，.在一个步骤中以所有可能的方式在位置V处使用重写系统R的所有可能的重写规则和所有可能的替换来将约束约束条件（例如，约束条件）压缩到项V中，条件是缩小替换与所有约束条件兼容。这是缩小的步骤。如果当前项u是不可窄化的，则它的任何基实例都是正规形式。然后u终止，该过程在该分支中成功停止• 在前面的步骤之前，我们可以测试当前项u和当前排序约束集合C，A和C是否意味着tref> u。在这种情况下，通过归纳假设，u终止，过程在该分支中成功停止。这是停止步骤。这些不同的步骤由变换3元组（T，A，C）的规则执行，其中• T是一组项， （，），包含当前项，其最内层终止必须被证明。这是一个单例或空集。• A是形式为u↓=X，u∈ T（F，X），X∈ N的抽象约束的合取。如果Xθ=（uθ）↓，则基代换θ满足u↓=X。• C是排序约束的合取。一个基替换θ和一个序（）满足t > tj，如果tθTJθ.注意，t >tJ是一种高阶约束，因为关系>是未知的。应用停止和抽象步骤需要证明一些性质。更确切地说，给定t，u∈ T（F，X<$N），我们说（A，C）蕴涵t > u，记为（A，C）→t > u，如果对于任意>1和满足（A，C）的任意基置换集合Θ，存在2使得2和相同的基置换集合Θ满足（A，C t > u）。一般来说，这样的属性是不可判定的，但在实践中，证明开发者通常可以通过检查约束来找到证明。终止证明过程由表1中给出的一组规则描述。这些规则必须与特定的策略一起应用，在ELAN中实现如下：11联系我们公司简介{} T TT} TT停止：{u}，素八你好，A，C参考文献如果（A，C）→tref>u摘要：{f（u1，.，μ m）}，素八{f（U1，...，U m）}，A u i1 ↓=X i1. u ip ↓=X ip，C u ip）其中f（u1，...，μ m）由f（U1，...，Um）在位置i1，.，，ip如果（A，C）→ t ref> u i1，...，u IPStopA：{f（u1，.，μ m）}，素八 你好，素八如果（A，C）→ t ref> u1，...，m无法证明窄：{f（u1，.，μ m）}，素八{v}，σA，C如果f（u1，...，u m）σv，σv和（σA，C）满足R停止编号：{u}，素八A，C如果u不是可窄化的，或者u是可窄化的，σ和（σA，C）不满足表1t引用终止的推理规则重复 *（first（Abstract，StopA）;first（dk（Narrow），StopN）;first one （ dc （ test narrow ） ，StopN ） ; first （ Stop ， id ））其中，test narrow仅检查是否可以在顶部进行缩小，但不应用它。这个过程的行为有三种情况应用于初始状态（tref，，）的策略，其中是约束的空合取，如果存在无限数量的抽象和狭义的应用，则可能不会终止。如果所有的规则都失效，并且过程在形式为（T=，A，C）的状态下停止，则不可能得出任何结论。最好的情况是策略终止，因为规则不再适用，并且所有状态都是（A，A，C）的形式We写入SUCCESS（g，>），如果在（{g（x1，. xm），，），其条件满足，在导出树的任何分支上给出形式为（，A，C）的 状 态 。定理4.1设R是符号集F上的TRS。设>是T（F）上的一个序，在上下文下是封闭的，包含子项序，使得对于任何定义的符号g∈DefR，SUCCESS（g，>）。如果F的常数在最里面终止，则T（F）的任何项都在最里面终止。这种方法的一个改进在于确定一个先验的偏序12f依赖于g（记为f>dg），如果g出现在定义f的规则的右侧（即f是左侧的顶部符号）。然后，首先处理较小的符号，部分结论可以用于检查Abstract或Stop的条件。该方法已在ELAN中实现。当无法自动证明Abstract或Stop的条件时，程序与用户交互。让我们用一个小例子来说明ELAN的输入，它是一个带有重写规则的指定文件，其终止性必须得到证明。请注意，重写系统不是终止的，而是最内部终止的。规格示例变量x yOpsf：3 g：1规则f（g（x），x，y）-> f（y，y，g（y））g（g（x））-> g（x）无规格结束输出被表示为具有所应用的规则的名称的派生树和派生的跟踪f（g（x），x，y）-> f（y，y，g（y））g（g（x））-> g（x）-汉灵符号[g] -* 衍生树 *+-摘要+-窄+-StopN* 推导 *[初始化]t_ref= g（x_1）A =真C =true1 -->[摘要]t=g（var（1））A = x_1| =var（1）C = g（x_1）>x_11.1 -->[窄]t=g（var（2））一 =x_1| =g（var（2））C = g（x_1）>x_11.1.1 -->[StopN]t= vide一 =x_1| =g（var（2））C = g（x_1）>x_1- 处理结束符号[g]--处理符号 [f]-* 衍生树 *+-摘要+-窄+-摘要13TFTFTFTF X TF+-StopN* 推导 *[初始化]t_ref = f（x_1，x_2，x_3）A =trueC =true1 -->[摘要]t=f（var（1），var（2），var（3））A = x_3| =var（3） /\x_2| =var（2） /\x_1|=var（1）C = f（x_1，x_2，x_3）> x_1，x_2，x_31.1 -->[窄]t=f（var（5），var（5），g（var（5）A = x_3| =var（5） /\x_2| =var（4） /\x_1| =g（var（4））C =f（x_1，x_2，x_3）> x_1，x_2，x_31.1.1 -->[摘要]t=f（var（5），var（5），var（6））A = g（var（5））|=var（6） 联系我们|=var（5） /\x_2| =var（4）/\x_1| =g（var（4））C = f（x_1，x_2，x_3）> x_1，x_2，x_31.1.1.1 -->[StopN]t= videA = g（var（5））|=var（6） 联系我们|=var（5） /\x_2| =var（4）/\x_1| =g（var（4））C = f（x_1，x_2，x_3）> x_1，x_2，x_3- 处理结束符号[f]-在这项工作中，ELAN已被用于原型的最内部的终止证明方法的推理规则，运行的例子，并与不同的策略进行实验由于函数库的条款已经在系统中，TEM，这样的规则的发展已经很容易。这也是一个用户交互非常重要的例子，可以通过ELAN的输入输出功能轻松实现。5标准形集的计算或近似上一节研究了在特定策略（最内层策略）下基项的归一化，但另一种限制也值得考虑：实际上并不总是需要证明（，在实践中，TRS通常被设计为重写来自子集E的项（ ）. 此外，一些TRS在严格子集E上弱正规化（），但不是（）。对于这种情况，基于自动机的技术非常方便。一些作者已经提出使用树自动机技术来证明TRS上的各种性质。对于给定的TRSR和一个项集E，这些证明是基于E的R-后代集和E的R-范式集的计算。不幸的是，除了极少数和特殊的情况下，这些计算不会终止，也不是正则集。在[Gen98]中提出的想法是使用一个近似自动机来识别E的R-后代集的超集和一个自动机来识别R-项的范式集由于这种方法，它显示在[Gen98]中如何证明一个14∈F<$程序在一组可能的初始输入上，或者如何在程序上实现可达性测试在更精确地描述如何建立E的R-后代和R-正规形式的近似之前，需要一些定义和符号5.1自动机，正则树语言在[GS 84，CDG+ 97]中可以找到树自动机和树语言理论的全面调查，在[GT 95]中可以找到正则树语言和重写系统之间的联系设Q是一组有限的符号，元数为0，称为状态。T（F Q）称为配置集。转换是重写规则c→q，其中c∈ T（F <$Q）且q∈ Q。标准化转变是转变c→q，其中c = f（q1，...，qn），f ∈ F，ar（f）= n，且q1，.，qn∈ Q。对于每一个转换，都存在一组等价的归一化转换。规范化包括将转换s → q分解为转换f（u1，...，un）→qJ，其中u1，...，n，并且qJ是状态，通过由Q的状态抽象s的子项sJ/∈ Q。一个自底向上的有限树自动机（简称树自动机）是一个四元组A=<$F，Q，Qf，<$F，其中Qf<$Q是最终状态的集合，而<$F是一组归一化的转换。由导出的重写关系表示为→。由y A识别的树语言为L（A）={t∈T（F）|q∈Qfs.t. t→t→q}。对于给定的q∈Q，A和q所识别的树语言是L（A，q）={t∈T（F）|t→t→q}。 一个树语言（或一组项）E是正则的，如果存在一个自下而上的树自动机A使得L（A）= E。正则树语言的类在布尔运算下是封闭的，包含是可判定的。一个Q-置换是一个置换σ使得<$x∈ Dom（σ），xσ∈ Q. 设X（Q，X）是Q-置换的集合.5.2逼近R（E）和R！（E）如果R是左线性的，则R-范式IRR（R）中的所有基项的集合是正则树语言[GB85]，并给出了构造正则树文法的一个过程（分别为：树自动机）产生（或[2019- 08 - 17][2019 - 08 - 17][2019 - 08][2019 - 08 - 17]然而，一组基项E的R-后代的集合，记为R（E），是不一定是正规的树语言，即使E是。语言R（E）是正则的如果E是正则的，如果R是基TRS [DT90]，右线性和一元TRS [Sal88]、线性和半一元TRS [CDGV 91]或另一方面，对于给定的正则语言E，R（E）不一定是正则的，即使R是一个连续的和终止的线性TRS [GT 95]。如果R不是为了研究E的基R-正规形集，记为R！（E）及1“逆生长”意味着每个右边要么是一个变量，要么是一个项f（t1，.， t n）其中f，ar（f）=n，i=1，.，n，t i是一个变量，一个基项，或者是一个变量不在左边的项。15∩→→T ↑L/→→定义为R（E）IRR（R），对于重写程序的合理表达类，其思想是构建R（E）的近似，即左线性TRS和正则集E的R（E）的正则超集。然后，由于正则语言是交封闭的，R的正则超集R（E）和IRR（R）之间的交给出了R的正则超集！（E）。设A是识别项集合E的树自动机。 为了构造识别R的正则超集的近似自动机R（A）！（E），[Gen98]中提出的算法从树自动机A开始，通过计算R的规则和R的规则之间的临界峰，递增地添加到新的转换。这相当于计算置换σ，使得rσR<$lσ→rσq。 Ifrσ则跃迁rσ如果需要，q被加到k上并被归一化。用于归一化rσ的新态的选择q是由一个近似函数γ，给定规则lr、状态q和替换σ计算新状态的序列，r的根下的每个子项一个。下面两个定义是从[Gen98]借来的。定义5.1（近似函数）设Q是一组状态，Qnew是一组新的状态，使得Q <$Qnew=n，Q<$new是Q new中的状态的序列集q1·· ·qk。一个逼近函数是一个映射γ：R×（Q<$Qnew）× <$（Q <$Qnew，X ）<$→Q<$new，使得γ（l→r，q，σ）=q1·· ·qk，其中rek=Card（Pos F（r））.对任意序列S=q1·· ·qk∈Q_（？）_new，且对于所有条件1≤i≤k，πi（S）表示序列S的第i个元素，即.奇岛定义5.2（近似自动机）设A =<$F，Q，Qf，<$F是一个树自动机，R是一个左线性TRS，Qnew是一组新的状态，使得Q <$Qnew=<$，γ是一个近似函数。近似自动机TR↑（A）是树自动机<$F，QJ，Qf，<$J <$，使得(1) QJ=Q <$Qnew，以及(2) ∆⊆ ∆J,and(3)<$l→r∈R，<$q∈QJ，<$σ ∈<$（QJ，X ），lσ→ <$<$Jq蕴涵N j.归一化根据近似函数引入新的状态γ。准确的定义可以在[Gen98]中找到。通过选择特定的逼近函数γ，我们得到不同的逼近。然而，与前面的构造一起使用的每个近似都提供了R（L（A））的正则子集定理5.3给定树自动机A和左线性TRSR，每个逼近自动机满足：对于任何逼近函数γ，L（TR↑（A））R（L（A））为了让一个有限自动机逼近集合R（（A）），直觉是将递归调用折叠成一个唯一的新状态。这是祖先近似的基本思想之一：非正式地，每个状态q∈ QJ=Q<$Qnew都有一个唯一的16→∈ Q→T ↑∈ Q祖先qa. 任何状态q的祖先都是q本身，而每个新状态q的祖先都是J序列γ（l）中出现的新的r，q，σ）（用于规范化新的转换rσq）是q的祖先。很容易看出，在祖先近似中，γ函数不依赖于σ参数，而且对于任意新态QJ∈Qnew，γ（l→r，QJ，σ）=γ（l→r，q，σ），其中q∈ Q是QJ的祖先.这个性质对于使TR↑（A）的构造终止是至关重要的。定理5.4 [Gen98]用祖先逼近构造的逼近自动机是有限自动机。ELAN中提供了树自动机的算法库。实现了树自动机的一些基本算法：并、交、清洗、包含测试，以及构造树自动机R（A）和AIRR（R）的算法，AIRR（R）是识别给定自动机A和给定自动机A的集合IRR（R）的自动机。左线性TRSR.让我们用一个小例子来说明这个库中可用的功能规范文件包含签名（变量和操作符）的描述，定义程序的规则集，以及描述程序的常规输入项集的自动机规格ex_nf_automaton变量x y zOpsa：0 b：0 cons：2 append：2null：0R1append（null，x）-> xappend（cons（x，y），z）-> cons（x，append（y，z））nil自动机//形式为append（l1，l2）的项，其中l1和l2是//任何a和b的平面列表。A（0）状态q的描述|0.q| 1.Q| 2nil最终状态q| 0.niltransitions append（q| 1，q| 1）-> q| 0.cons（q| 2，q| 1）-> q| 1.null -> q| 1.a ->q| 2.b -> q| 2.无结束描述规格结束为了计算A（0）上R1的近似自动机，即的超集R1-L（A（0））的后代，用户在（！A（0））。输入查询词，由关键词“end”完成T_up（R1）on（！A（0））结束[]以term：T_up（R1）on（！A（0））[]结果项：A的描述状态q| 4.Q| 0.q| 1.Q| 2.nil17∪最终状态q| 0.niltransitions cons（q| 1，q| 4）->q| 4.append（q| 1，q| 1）