176网址：http://www.elsevier.nl/locate/entcs/volume70.html20页最左策略下的正则后代集Pierre R ety1;2Julie Vuotto1LIFO奥尔兰大学B.P. 6759，45067 Orl eans cedex 2，France关键词：项重写，策略，树自动机.摘要对于一个基于构造器的重写系统R，一个规则的基项集合E，并假设一些附加的限制，我们建立了一个nite树自动机，它根据最左策略识别E的后代，即通过重写从E1引言由于自动演绎和程序验证（可达性，程序测试）的潜在应用，以有限的方式表达一些有限的术语集的问题是必不可少的。利用树自动机表示正则基项集E关于一个方程组的传递闭包，并讨论了表示该集合的有关问题关于重写系统R的E的后代R（E）的问题，已经研究过[1，2，3，4，7，8]3。除[4，8]外，所有这些文献都假设重写规则的右侧（处理方程组时的两侧）是浅4，直到轻微的差异。另一方面，P.Rety的工作[5]并不总是保持可识别性（E不是任意的），但允许重写规则被其他论文禁止。在过去的几年里，重写和编程中的归约策略引起了越来越多的关注，并且从理论上讲都很1 电子邮件：frety，vuottog@lifo.univ-orleans.fr2 http://www.univ-orleans.fr/SCIENCES/LIFO/Members/rety/3 [4]计算可规范化项的集合，这相当于通过将重写规则定向在相反的方向来计算后代的集合。4 浅意味着每个变量最多出现在深度1处。5像f（s（x））！ s（f（x））。2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。177Stp如果计算结果不是唯一的，从实际的角度来看，对于终止和效率。对于一个策略st，用一个nite树自动机表示E的st-后代R（E），可以帮助研究st：ticular它允许决定st-可达性，因为tst！不（）t2R（ftg），1 2 2Stst1和st-可连接性，因为t#t（）R（ftg）\R（ftg）6=;.更一般-12日1st2此外，它可以帮助重写程序的静态分析，并且通过扩展，功能性程序。在本文中，我们计算最左边的后代，而在[6]中，我们计算最里面，最里面-最左边和最外面的后代。研究一个懒惰的求值，比如leftmost-outermost，是很困难的，目前我们分别考虑最左边的情况和最外面的情况。在这里，我们构建了一个nite自动机，它可以表达E的最左边后代的集合，相对于基于构造器的重写系统，假设：(i) E是给定线性项t（即E=ft g）的基础构造器实例（也称为数据实例）的集合。(ii) 每个重写规则都是线性的（两侧）。(iii) 在右边，没有嵌套的定义函数，定义函数的参数要么是变量，要么是基础项。(iv) 禁止置换重写规则(v) 每个重写规则都是变量保留的。通过变换R，约束v可以减弱为约束v'：每个重写规则是左变量保持的。在[5]中表明，如果不满足1，2，3中的任何限制，则后代集合（即使遵守最左策略）不是正则的。与[6]的最内最左的后代相比，rhs可以包含几个指定函数，这要归功于第3节中给出的新结果。 对另一方面，我们假设额外的限制iv，v，因为计算最左边的后代比只计算最左边的后代更困难。本文的结构如下。第3节给出了语言R/（ft g）的计算（即，根据最左边的策略，在重写之后实际上在t的位置p加上可能在从RHS发出的函数位置处获得的项）。最左边的后代在第4节中计算（我们对t的每个p位置应用前面的语言，在p左边出现的子项通过与识别不可约项的自动机相交而被规范化之前进行检查）。现在，让我们看看，在下面的部分中的概念。第2.1小节（通常的概念）可以由读者跳过。缺失的证据在附录中。6 如果x2Var（l）\Var（r）和y2Var（l）V ar（r），则x出现在l中y的左边。178ppRRppR2预赛2.1术语重写与树自动机设C是构造函数的集合，F是定义函数符号的集合。对于c2C[F]，ar（c）是c的元数. 术语用字母s、t表示。数据项是只包含构造函数的基础项（即没有变量）。T C是数据项的集合，T C[F]是包含构造函数和函数的基础项的集合。对于项t，Var（t）是出现在t中的变量的集合，Pos（t）是t的位置的集合，Pos（t）是t的不可变位置的集合，PosF（t）是t的确定函数位置的集合。 PosVar（t）是t的可变位置的集合。 对于p 2 Pos（t），tj p是t在位置p处的子项，t（p）是t j的顶部符号，t[t0]表示子项nt。 F或位置p;p0，pp0意味着p位于p 0之下，即对于某个位置v，p=p 0：v，而pkp0意味着p和p0是不可比较的，即 ：（pp0）^：（p0p）. 项t包含嵌套函数，如果存在p; p 02P osF（t）s. t。p > p 0.一个替换的定义域dom（）是变量xs. t的集合。x6= x。重写规则是一对有方向的项，写为l！R. 重写系统R是重写规则的集合。 lhs代表左手边，rhs代表右手边。 R是基于构造器的，如果R的每个lhsl都是l=f（t1;：;t n）的形式，其中f2F和t1;：;t n不包含任何函数。重写关系！定义如下：t！t0如果存在p2Pos（t），arulel！ r2R和取代s.t. tj=l且t0=t[r]（也表示为byt！[ p;l！r;]t0）。！表示自反传递clo-当然！R.t是不可导的，如果：（9t0jt！t0）。t！[p] t0是最左边的，如果8v严格出现在p的左边; tjv是不可约的。（自下而上）nite树自动机是四元组A =（C [F; Q; Q f;），其中Q fQ是状态集合，并且是形式c（q1;：; q n）的转换集合！q，其中c2 C [F]和q1; q n;q 2 Q，或形式q1！ q（空跃迁）。状态集用字母Q; S; D表示，状态用q;s;d表示。 ！（也表示！A）是由y导出的重写关系。接地项t被A识别为q，如果t！ Q. L（A）是公认A转换为Qf. 一个派生词！其中q2Qf被称为测试成功。Q f的状态称为nal状态。AQ-置换是一个替代s.t. 8 x 2 dom（）;x2 Q.一个基项集E是正则的，如果存在一个nite自动机A s. t。E=L（A）。2.2嵌套自动机与判别直观地说，自动机A将位置p区分为状态q意味着沿着t2L（A）; tjp（并且只有这个子项）的每一次成功运行都被识别为q。此属性允许修改的行为，A低于位置p，而不修改其他位置，由另一个自动机A0替换Ajp。见[5]引理2.2和2.4的证明，和[6]的证明，R179FpfFFFp0p pp将位置p指定为状态q，并令A0 =（C[ F; Q0; Q0;0）s. t。Q\引理2.5.定义2.1自动机A =（C[F; Q;Qf;）将位置p区分为状态q，如果L（A）6=;，8t2L（A）; p2Pos（t），并为每一个成功的衍生品！t[q]p0 ！其中，- q0！q（即，通过空转换）如果p0= p，- q 0 6= q否则。在这种情况下，我们定义自动机Ajp=（C[F;Q;fq g;）。引理2.2则L（Aj p）= ftj p j t 2 L（A）g。定义2.3设A=（C[F; Q;Q f; ）是一个自动机，区分-Q 0= ;. We de neA[A0]=（C[F; Q [Q0; Q;NFL！ r j l！ R 2^r = qg[0[fq0！qj q02 Q0g）引理2.4L（A[A0]）=ft[t0]jt2L（A）;t0 2L（A0）g，且A[A0]仍将p判别为q.此外，如果A判别另一个位置p0S.T. 均p0 6 p，进入状态q0，则A[A0]仍能区分p0 到q0。引理2.5设A; B是自动机，A\B是经典的用于识别交集的自动机，其状态是A和B的状态对。如果A将p判别为qA，B将p判别为qB，且L（A）\L（B）6=;，则A \B将p判别为（qA;qB）。2.3位置和前因给定项t，我们定义ne：定义2.6设p 2 P os（t）. Succ（p）是最近的函数位置低于p：Succ（p）=fp02PosF（t）jp0>p^8q2Pos（t）（pqp0）q2=PosF（t）） g定义2.7设p; p0 2 P os（t）. p p0意味着p严格出现在p0的左边，即p =u：i：v，p0 = u：i0：v0，其中i; i0 2 IN且i i0。定义2.8Lett！[q;l！这是重写步骤。设v0 2 P os（t0）. v是v0在t中的先行项（由ant（v0; t）表示），通过该步骤如果：(i) v 2 P os（t）(ii)- v 0 /q和v = v0，或者，1800 0 000RR左T[0p;rhss]j+1j j jjt = t！t！“……”t！t=tJp1-9p2PosVar（r）withrjp0=xs：t：v=q ：p：w和v=q ：p：wwwheep00 是x在l中的位置。注：由于lhs是线性的，所以前因（如果存在）是唯一的。定义2.9让我们考虑以下推导：t0！[p0;l0！r0]t1！ “ 不！[pn;ln！（1）（1）v 02 P os（t 0）是v n+12 P os（t n+1）的前件，如果9 v 12 pos（t 1）;：;v n2 P os（t n）s. t。8 i 2 f0;：; n g; v i是v i+1到步骤t i的先行项！ ti+1。2.4子项和不可约基项的t0 是t的一个descendant！t0. 的t0 是t的正规形式，如果t！的t0 和的t0 是不可简化的。如果E是基项的集合，则R（E）表示E的元素的后代的集合。IRR（R）表示不可约基的集合届R（E）表示E的后代的集合，根据最左战略定义2.10吨！+的t0 意味着t0 是通过在p0处重写t来获得的。位置P，加上可能来自RHS的位置形式上，存在一些中间项t1;：;tn和一些位置集合P（t）;P（t1）;：;P（tn）s. t。00[p0;l0！r0]1[p1; l1！[pn1;ln1！[1]n[pn; ln！rn] n+1个哪里-p0=p和 P（ t）= fpg，- 8j; pj 2P（tj），- 8j;P（t）=P（t）nfp0j p0pg [fp：wj w2PosF（r）g.注：P（t j）只包含函数位置。因为在rhs中没有嵌套函数，p;p02P（t）意味着pkp0。定义2.11给定一个语言E和一个位置p，我们定义neR/（E）为：如下R/（E）=E[ft0j9t2E;t！+的t0 由左最后重写p[p;rhs0s]例 2.12 R = ff（ x）！ s（ x） ; g（ x; y）！ c（ h（ x） ;f（y））; h（x）！ f（x）gR/（ff（g（a; b））g）= ff（g（a; b））g [ff（c（h（a）;f（b）g [f f（c（f（a）;f（b）g [ff（c（s（a）;f（b）g[ff（c（s（a）; s（b）g.定义2.13令IRRP（R）=fs2TC[Fjp2Pos（s）^sjp不可约181定理2.14设t是一项，且p2Pos（t）. IRRP（R）是一种正则语言，它是由一个自动机识别的，该自动机能识别每一个位置p02Pos（t）s. t. p06>p.182证据 参见[6]。设Airr是一个能识别IRR（R）的自动机。在 下文中，我们将q irr称为Airr的接受状态。22.5重写与左基派生在最左策略中，在重写某个位置p之前，出现在p左边的子项必须重写成正规形式，也是通过最左导子。然而，为了避免在构造自动化子项时出现循环，我们用无策略导子对这些子项进行了规范化，并证明了由最左导子和任意导子得到的规范形是相同的.对于这一点，我们表明，一个任意的导子总是可以转化为一个左基本导子，并且一个左基本导子导致一个范式是最左的。下图展示了引理和定理之间的联系。- orem 4.4对应于最终结果。定理2.23推论2.24定理3.10引理4.3定理4.4通过下面的两个引理，我们看到了如何对易一个推导（分两步，接下来分几步）。引理2.15设R是线性TRS，s; t; u是项。如果s！[p; g！t！[q;l！（1）是两步推导，q在s中有一个先行项，记为p0。然后，（1）可以转化为：s！我！r]t0！[p; g！（2）第一次见面。现在，让我们假设限制V和IV。如果（1）是最左的，（2）是最左的。备注：Rbeingline ear，g！ d是线性的，因此d是线性的，因此u0=u，即，导数的最后一项通过对易保持[9]。此外，在（2）中，p在s中没有先行词。183nn+1个！j+1j j jj引理2.16设R是线性TRS。如果t0！[p0;l0！r0]t1！ ： ：tn1！[p n1;ln1！nnn！[pn;ln！（1）（1）是一个派生S. T。pn在t0中有一个先行项qn1。那么，（1）可以在：t0！[qn1;ln！rn]01[p0;l0！r0]：t0 ！[pn1;ln1！[1]0n+1个（二）t0=tn+1 P0在t0中没有先行项。现在，让我们假设限制V和IV。 如果（1）是最左的，则（2）是最左边的也是。现在，让我们定义左基本导子的概念。定义2.17让我们考虑以下推导：t0！[p0;l0！r0]t1！ “ 不！[pn;ln！（1）（1）这个推导被称为左基本的，如果：它存在对于项t0; t1;：;tns. t的位置B（t0），B（t1）;：，B（- B（ t0）= P osF（ t0）- 8j; pj 2B（tj）- 8j;B（t）=fp0 p0pg [fp：vj v2PosF（r）g [fp0 j p/p0g注意，最左最内意味着左基本。在一般情况下，反之亦然。反例2.18设R = ff（x）！s（f（x））; h（x; y）！c（f（x）; s（g（y）;g（x）！xg和E=h（s（a）;s（a））.考虑以下推导：艾薇！[]c（f（s（a））;s（g（s（a）！[2：1]c（f（s（a））;s（s（a）这个推导是左基本的，但不是最左最内的，因为位置2： 1处的重写步骤，因为位置1没有归一化。引理2.19让我们考虑下面的推导：t0！[p0;l0！r0]t1！ “ 不！[pn;ln！（1）（1）则（1）是左基本的当且仅当8 i2 f1;：; n g;p i在t i 1中没有先行项。引理2.20让我们考虑下面的左基推导：t0！[p0;l0！r0]t1！*tn （1）接着是非左基本步骤：tn！[pn;ln！[rn]tn+1让我们注意到pn在tn1中有一个先行项。设jn是最小整数s. t。p n在t j中有一个先行词。不不184nj jj不不0n +1n +1oF然后，通过换流获得以下推导：t0！[p0;l0！r0]t1 ！*t j！[q;ln！rn]0j+1 ！[pj;lj！rj]0j+2 ！**是左基本的。“ ……”的t0！[pn1;ln1！[1]tn+1（二）定理2.21设R是线性TRS。如果t！ 不（1）然后，t ！ 不（2）由左基派生。现在，让我们假设限制V和IV。如果（1）是最左的，（2）也是最左的。引理2.22设R是给定的基于构造器的TRS，并假设限制v。让我们考虑下面的左基本推导：t0！[p0;l0！r0]t1！ “ 不！[pn;ln！（1）（1）且令j2f0; ： ：;ng. 如果9p02Pos（t）B（t）s.t. t（p0）2F，则8k>j，9p0 2Pos（t）B（t）s.t. tj0 =tj0.kk kk pkjp定理2.23设R是给定的基于构造器的TRS，并假设限制v。考虑以下左基推导：t！ t s：t：t = t #（1）（1）左为右。推论2.24设R是一个给定的基于构造函数的TRS，并假设限制ii和v。用最左重写策略得到的项t的正规形与不用重写策略得到的正规形相同。证据显然，它由定理2.21和定理2.23得出。22.6启动自动机让我们定义初始自动机，即识别给定线性项t的数据实例集的自动机。定义2.25我们定义自动机A数据，它识别数据项T（C）的集合：A data =（C; Q data;Qdataf; data）其中Q data =Qdataf= fq data g且data =fc（qdata;：; qdata）！ q数据jc2Cg.给定一个线性项t，我们定义自动机At，它识别t的数据实例集：At=（C[F;Qt;Qtf;t），其中Q t=fq pjp2P os（t）g[fqdatagQ t=fqg（q数据，如果t是变量）=t（p）（s;：;s）！ q pjp 2P os（t）; s=qdataiftjp：iisa variable=9t1n：[数据问：我，否则，不不我;185p不arg注意，A t将每个位置p2P os（t）区分为q p。另一方面，A t不是确定性的，只要存在p 2 P os（t）s. t。TJP这是一个建筑术语。实际上，对于任何数据实例tj，tj ！q p和T J ！Q.p p[t]p[t]数据3认识到R/（E）本节介绍的概念由例3.11说明可能发生的是，重写步骤中使用的匹配将未被识别为AE状态的语言的变量实例化。也就是说，实例并不总是E的（子）项。让我们看看下面的例子：例3.1设R=fg（x）！R1t=g（a）的数据实例h（x;b）;h（x;y）R2c（ x; y）g和 E是集合qq1A t可以概括为：G （a）（这意味着g（a）！不g（q1）！q）。从E发出的重写步骤是g（a）！[;r1;x=a]h（a;b）！[; r2;x=ay=b]c（a;b）. 不幸的是，Qt=fq;q1 g和语言识别为q（分别）。q1）是g（a）（分别地，因此，我们没有任何状态可以识别fbg。 这是因为fb g是由rhsr1提供的。因此，我们需要通过额外的状态来加密。因此，我们给出以下定义。定义3.2rhs中函数的不可变参数由状态集Qarg和转换集arg编码，定义如下：Q arg= f q i;pj l i！ri2 R; p2 Arg（ ri）ga rg=fri（p）（qi;p：1; ： ：;qi;p：n）！ qi;pjqi;p2Qa rgg其中Arg（r i）是r i中的不可变参数位置，即Arg（ ri）= f p2 P os（ ri）j 9 pfct2 P osF（ ri）; p> pfctg现在，我们定义如何编码每个实例化rhs的版本设A =（C[F; Q;Qf;）是一个自动机，它把位置p判别为状态q，s.t。Q\Qarg=;（在此节）。设Q =Q[Q. 我们使用dp形式哪里是一Q '-替换，因为rhs可能包含变量。定义3.3重写规则的rhs由状态集Qarg和D = f d i;pj l i！ r i2 R; p 2 P os（r i）n Arg（r i）;是一个Q0-置换s.t. dom（）=Var（rijp） g186DDxjjri（ p：j）是任意变量 xDxjri（ p：j）是任意变量 x定义3.4令Dsat和sat得到的状态和转换的集合为符号：sat =坐着，坐着和一组转换= fr（p）（X;：;X）！d i;pjl！R2个R;d i1n1[：[ni我p2 P os（ri）n Arg（ri）;ri（ p）2 C8 j; j是任何Q 0-取代s. t. dom（j）= V ar（ rijp：j）;其中8j;Xjdi;p：jj否则[fri（p）（X1; ： ：;Xn）！ di;pj li！ri2R;p2PosF（ri）;是任意Q 0-置换s.t. dom（ ）= V ar（r ij p）其中8j;Xjqi;p：jG2Qarg否则[fx！ d i;j l i！ ri是任何变量x;是任意Q 0-置换s.t. dom（）= fx gg因此，ri且仅它被识别为状态dii。在定义3.3中，通过将每个状态di;p2 D替换为di;p。sat;rhs的这两个类似编码的目标是识别rhs的实例感谢（D;d），以及它们的后代感谢（Dsat;sat）和由下面定义的饱和过程产生的sat定义3.5（饱和）设sat是以如下方式添加的转换集：只要有l i！R12R1 a（Q[Qarg]）-取代S.T. dom（）=V ar（li）[var（r i）和li！坐 其中q02 fqg [ Dsat，添加过渡di;sat;jVar（ri）！q 0.t[arg[dD d注：记B0=（C[F;Q[Qarg [Dsat;fqg;[arg[sat）.然后，L（B0）=R（L（Ajp）），即与R/（L（Ajp））相同，除了重写步骤不一定是最左边的（参见[5]以获得更多细节和解释，这里仅列出了步骤）。我们创建另一个rhs的编码。因此，它允许我们拥有通过最左策略获得的rhs实例的后代例如，考虑rhs c（f（x）; g（y））。 我们检查f（x）的实例在用最左策略约简g（y）的实例之前，用任何策略约简为它们的标准形式（感谢推论2.24）。定义3.6为此，我们考虑状态集：D规格= D[ Dsat[ Dsat Qirr==G187伊伊sat;[：[n1sat;sat;sat;pFDDDp以及以下转换集合，其中（d：qirr表示对（d：qirr））：pi;p：jxjri（p：j）是任意变量x坐irr是通过在：：：spec=Sl！r2RSp2Pos（r）=（PosF（r）[A rg（r））Sk2f1;：;a r（r（p））g：：：fri（p）（X1;：;Xn）！ di;pj是nyQ0-取代S.T. dom（j）=V ar（rijp：j）;xj; qirr如果jpA判别p0转换成q，然后是A 也区分p0 到q0。证据 见附录B。2定理4.4设R是满足约束1 ~ 5的重写系统，E是给定线性项t的数据实例集左T左t; （E）ift（）2F否则，令Succ（ p）= f p1;：; png，其中p1/：/pnR（E）R（ E）=[R（（R（L）\IRR（R）左T左侧t;p2左侧t;p1p1[： [Rleft;pn（： （Rleft;pl（L）\IRRpl（R）） ：\IRRpnl（R））左T（E）被自动机有效地识别。证据 见附录B。2R我R和RR（E）=R和R191为了记住eat，我们替换了eat（q;q0）形式的每个c h转换！q00byq！ q00。例4.5设R = ff（x）！ s（x）; h（x; y）！ c（f（x）; g（y））; g（x）！ s（x）g和E = fh（g（s（a））;f（s（a）g.为了清楚起见，我们将s（a）表示为。R（ E）= R（E）=R/（R（E））[R/（R（R）（E）\IRR（R））。左T左t;左t;1左侧t;2左;111921左t;1 （E）=R/（E）=E[fh（s（）; f（））g表示为yL1：-右（R）（E）\IRR（R））=R（fh（s（）;f（））g左侧t;2左t;11例左侧;2例=fh（s（）; f（）g [fh（s（）;s（）g表示为yL2最后，我们得到最左边的后代，它们是：[L1][L2][fc（f（g（））;g（f（）g [fc（s（g（））;g（f（）g [fc（s（s（））;g（f（）g[C（s（））; s（f（））; g（f（））; g（f（））; g（f（）; g（f（））; g（f（）; g（）; g（f（））; g（f（）; g（）; g（f（）; g（）; g（f（）; g（）; g（）; g（f（）; g（）; g（）; g（f（）; g（）; g（5结论当计算后代时，考虑最左边的策略是可能的，保持相同的树语言类（常规语言）并假设额外的限制（限制iv和v '）。限制iv（没有置换规则）是最烦人的，但它不能被轻易削弱，因为我们的方法计算左基导子，而不是直接计算最左导子。然而，我们认为没有这个限制，最左后代的集合仍然是正则的。引用[1] H.来吧序贯性、二阶一元逻辑与树自动机。在程序中，第十届IEEE计算机科学逻辑年会，第508- 509页。517. IEEE计算机协会出版社，1995年6月26-29日[2] J. Coquid e，M.多谢河Gilleron和S.瓦格沃吉自底向上树下推自动机和重写系 统 。 In R. V. Book ， editor ， Proceedings 4th Conference on RewritingTechniques and Applications ， Como （ Italy ） ， volume 488 of LNCS ， pages287-298. Springer-Verlag，1991年4月[3] M. Dauchet和S.提森地面重写系统的理论是可判定的。在程序中，第五届IEEE计算机科学逻辑年会，第242-248页，宾夕法尼亚州费城，1990年。IEEE计算机学会出版社.[4] F. 杰 奎 玛 项 重 写 系 统 的 可 判 定 近 似 。 In H. Ganzinger ， 编 辑 ，Proceedings 7th Conference RTA，新不伦瑞克（美国），LNCS第1103卷，第362-376页。Springer-Verlag，1996.[5] P. Rety.基于构造器的重写系统的正则后代集。在第六届编程逻辑和自动推理（LPAR）国际会议的会议记录中，第比利斯（格鲁吉亚共和国），人工智能讲义。Springer-Verlag，1999.[6] P. Rety和J. Vuotto。通过一些重写策略得到正则的后代集。第13届重写技术和应用会议论文集，哥本哈根（丹麦），LNCS。Springer-Verlag，2002.-右193[7] K.萨洛马确定树下推自动机和一元树重写系统。计算机与系统科学杂志，37：367-394，1988。[8] T. Takai，Y. Kaji和H.关右线性有限路径重叠项重写系统有效地保持可识别性 。 在 洛 Bachmair ， editor ， Proceedings 11th Conference RTA ， Norwich（UK），volume 1833 of LNCS，pages 246-260. Springer-Verlag，2000.[9] P. Rety. M ethodes d'union par surreduction.这是南西一大学的博士。194自己变成T！t ！t. p没有一个-n2[nn nn2q;l！[p;l ！n n1n2n 2n 20[q;l！r] 1[p;l！nn00我1我1附录A重写换易与左基导子的证明A.1引理2.15的证明p没有前因，这是很明显的，因为定义2.8。要么p出现在p的右边，要么p出现在p的上面.现在，让我们证明（1）lef tmot）（2）lef tmost。设（1）最左。让我们从左到右对V ar（r）进行分类。如果jV ar（r）j =n，则V ar（r）= fx1;：：：; xn g。由于（1）是最左边的，让我们用xi=x表示第一个变量由一个包含定义函数的项实例化。然后，8j 2 [1：：i [;（xj）不包含函数。让我们假设p0不是s中的最左位置。只有在以下情况下，9一个出现在l中x左边的函数，由包含函数的项实例化现在，由于禁止置换规则（见限制iv）和由于变量保持TRS（见限制v），它是不可能的。然后，如果我们从左到右对Var（l）进行分类，我们得到与Var（r）相同的顺序。因此，（2）是最左边的。A.2引理2.16的证明这个证明由引理2.15推出。设ant（pn;tn1）=q0 ）tn1！[pn1;ln1！nnn！[pn;ln！rn]tn+1个部件0n1[q0;ln！[pn1; ln1！n+1n1在tn1中的tecedent，并且它是最左边的。设ant（q;t）= q ）t！t！的t0通勤0n 2 1n2[pn2; ln2！[rn2]n1[q0;ln！[n] n自己是T！的t0 ！的t0 . 而p还没有发生，在tn2中，它是最左边的。* *通过归纳，令ant（q;t）=q）t！ t！的t0表示“共同”之义n20n10[p0;l0！r0]1[qn2;ln！[n]2把自己变成了T！的t0 ！ 的t0 . 而p没有ntecedant在t0中，它是最左边的。因此，我们得到（2）。A.3引理2.19的证明设（1）为左基本导子。让我们假设9i2 f1：ng s. t。p i在t i 1中有一个先行项。根据定义2.17，p2B（t）其中8j;B（t）=fp0 j p0 pg [fp：vj v 2PosF（r ）g [fp0 JP/p0g。设ant（p; t）=q.I1根据定义2.8， (i) q2P os（ ti1）195I1我I1
我的内容管理
展开
