没有合适的资源?快使用搜索试试~ 我知道了~
正交项重写系统中的恶性循环与弱正规化和强正规化的关系分析
理论计算机科学电子笔记124(2005)65-77www.elsevier.com/locate/entcs恶性循环正交项重写系统Jeroen Ketema1Vrije Universiteit,De Boelelaan 1081a,1081 HV Amsterdam,The NetherlandsJan Willem Klop2Vrije Universiteit,De Boelelaan 1081a,1081 HV Amsterdam,TheNetherlands; CWI,P.O. Box 94079,1090 GB Amsterdam,TheNetherlands; Department of Computer Science,RadboudUniversiteit Nijmegen,Toernooiveld 1,6525 ED Nijmegen,TheNetherlandsVincent van Oostrom3荷兰乌得勒支大学哲学系,Heidelberglaan 8,3584CS Utrecht,The Netherlands摘要本文首先在一阶正交重写系统的框架下研究了弱正规化(WN)和强正规化(SN)之间的区别。在擦除引理的帮助下,我们建立了一个泵引理,产生关于例外项的信息,定义为WN但不是SN的项。一个推论是,如果一个正交TRS是WN,则在有限约简图中不存在循环约简。 这是通往洞察力的垫脚石 具有WN性质的正交TRS根本不允许循环归约。保留字:术语重写系统,循环约简,规范化,函数式编程。1电子邮件地址:jketema@cs.vu.nl2电子邮件:jwk@cs.vu.nl3电子邮件:oostrom@phil.uu.nl1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi:10.1016/j.entcs.2004.11.02066J. Ketema等人理论计算机科学电子笔记124(2005)651介绍本文主要关注的是减少周期的概念。直觉上,循环项(即,位于归约循环上的项)是“坏的”,而正规形式是“好的”;循环归约是正规化的失败尝试。这幅图是复杂的,因为一个术语可能是循环的,但仍然有一个标准形式,例如,CL-术语KI(SII(SII))具有标准形式I,但也是环状。我们要证明的是,一个循环项t后者意味着s项甚至在深度为零时也拒绝归一化。(在λ-演算中,这样的项也被称为“不可解”。这反过来又意味着这个词毫无意义。在一个口号:周期这些术语证实了我们的直觉,即周期是“邪恶的”。相反,当“一切都被定义”时,就没有循环了。正交项重写的精确陈述是蕴涵WN_WN-AC,弱归一化意味着非周期性。这实际上是我们的主要定理,现在的纸。事实上,我们也有“头部正常化”的含义AC.当然,我们有平凡的SN规范化,强规范化意味着无环性。在非擦除还原的上下文中,SN和WN是等价的,这将是本故事的结束这些含义的想法来自于建立一个较弱的事实,即WN可约化,其中后一个性质意味着至少有限个约化图不允许循环。我们将把这种性质称为这是一个属性,值得注意的是,CL也是基于I,K,或者只是K,S喜欢(即使CL绝不是WN!)。(参见Klop)[7])我们将首先建立这个含义WN_ nac_finn,因为证明产生了一些有趣的信息:它是由一个“泵送性质”完成的是擦除引理的结果,擦除引理是正交项重写中的一个有用引理。图1显示了λ演算中最简单的循环,右边是组合逻辑(CL)。如前所述,不可能在CL中有一个圈并保持约简图是有限的,实际上SII(SII)的约简图是无限的。2预赛我们假设熟悉项重写的基本概念,如CR(一致性或Church-Rosser性质),UN(唯一范式性质),J. Ketema等人理论计算机科学电子笔记124(2005)6567(200.xx)(200.xx)SII(SII)图1. 在λ-演算和组合逻辑(CL)中的SN(强归一化),WN(弱归一化)。[4]我们特别需要正交TRS的概念。[5]一般参考资料见Terese [9]。在这里,我们挑选出一个子TRS的概念,这将在以后发挥重要作用。2.1子TRS在本文中,我们将只使用一(i) 签名是原始TRS的子签名(ii) 所述约简规则是所述原始规则集的子集,并且(iii) 该项集合是原始项集合的子集特别地,t的约简图G(t)是子TRS。这里的项集由t和它的所有约简组成。我们将在下面使用的另一个子TRS是t的族F(t),其中项的集合由t和约简的所有子项组成,即,宇宙包含t,并且不仅在约化而且还在取子项下。 重要的是,子TRS,包括F(t)和G(t),被认为是TRS本身,通常的概念和定理适用于它们,例如,正交TRS是连续的。4 参见,例如,Terese [9],Ch. 1,p. 13岁5见,例如,第4章,非理性,载于Terese [9]。68J. Ketema等人理论计算机科学电子笔记124(2005)65备注2.1(i) 项F(t)的族的概念源于Barendregt [1]。(ii) 注意,归约图G(t)是t的族F(t)的子TRS。例如,考虑具有规则{A→B(C),C→D}的TRS。 则TRSG(A)具有项的论域{A,B(C),B(D)},而F(t)具有论域{A,B(C),B(D),C,D}。(iii) 定义d=→,其中是真子项关系的逆。然后:→isSNidisSN。[6]利用柯尼希引理[7] ,我 们由此得到G( t)是 有限的,如果 F( t)是 有限的。例2.2(组合逻辑中的S项集)符号由常数S和二进制应用A组成.唯一的规则是A(A(A(S,x),y),z)→A(A(x,z),A(y,z)),或者用CL的常用符号表示,Sxyz→xz(yz)。这种正交TRS的显著特征是:<$SN,WHN(头部归一化,定义如下),AC(无环性,定义如下)。一个带有<$SN的项的例子是SSS(SSS)(SSS )。头归一化性质由Waldmann建立[12]。性质AC由Bergstra证明,Klop [2].例2.3(CL中的J项集)(见D. Probst和T. Studer [8])这个正交TRS是SN。单一归约规则采用应用符号:Jxyzw→xy(xwz)。2.2基本概念我们需要正交一阶TRS的以下基本性质,如图2所示。有些是标准的,我们不会重复它们的定义:SN(强归一化),WN(弱归一化),WIN(弱最内层归一化),NE(非擦除)。此外,AC意味着TRS没有还原循环t→+t或非循环。性质ACfinn(finite acyclic)意味着有限约简图G(t)不包含圈。换句话说:如果t→+t,那么t有无穷多个不同的约简。性质LF(局部有限)是所有约简图G(t),因此也是族F(t),是有限的。这个属性的重要性很小,提到它只是为了使图2中的图表更加完整。6 这是练习2.3.11,第41页,Terese [9]。7 引理A.1.25,p.798 in Terese [9].J. Ketema等人理论计算机科学电子笔记124(2005)6569?O'DonnellWIN SNNEAC WN LF交流散热片图2.2.3头正规形定义2.4(i) 一个项t是头范式,如果它不是一个redex已经,也不能减少到一个redex。换句话说,没有还原“激活”根。(We使用(ii) 此外,如果t简化为1,则它有一个头范式。(iii) 一个TRS具有WHN(弱头规范化)性质,如果TRS中的每个项t都如果项t有首范式,我们也写作t∈WHN,或WHN(t)。(The限定词定理2.5(Head正规化定理)设R是一个正交TRS,t是R中的一个项,其约化t→TJ→TJJ→. 包含了无数的头部台阶。(i) 则t没有头标准形。(ii) 更不用说,t没有正规形式。证明我们采用最外层公平的减少(见定义。4.9.15(ii),特别是Terese[9]中的Def. 9.3.1)和最外公平约简是正规化的定理(见Terese [9]中的定理9.3.10从这一点出发,定理立即得出,因为具有无穷多个头步的无穷约化是70J. Ketema等人理论计算机科学电子笔记124(2005)65很明显最外层是公平的所以初始项不可能有一个正规形式--如果它有,这个最外层的公平约化就能达到它。Q备注2.6对于CL,应发出警告。刚才定义的头减少的概念属于该术语的根。与λ-演算的类比提出了另一个头归约的概念,即收缩其前导符号S、K或I是手头项的最左边符号的redex的概念。因此,给定CL项SKSIK,在这种意义上的头部redex将是SKSI。 然而,这个术语在根处没有redex,所以它承认没有上述意义上的压头减小步骤。对于S-项,这些归约的概念实际上是不同的:如上所述的头归约Barendregt(个人通信)给出了一个例子:考虑BB一词,其中B=SAA,A=SSS。 这个项在λ-演算的意义上有一个无穷的头步的减少。3擦除引理擦除引理(EL)是由Klop [5,6]在没有证明的情况下提出的,并且似乎是在Bergstra等人[3]中首次证明的。[8] EL有几个重要的推论,包括Church定理、O'Donnell定理[9]我们现在回顾EL的相关概念和声明定义3.1(i) 记法:∞(t)意味着t有无限约化。所以<$∞(t)意味着t是强正规化的,或者t∈ SN。(ii) 如果∞(t)但<$∞(tJ),则称约化步骤t→tJ为临界的因此,关键的一步是失去执行无限还原的可能性。命题3.2(消去引理)设t→tJ是正交TRS中的一个关键步骤,其中s是收缩的Redex。 然后这个步骤用∞(p)擦除子项p。参见Terese [9],p. 126,Proposition 4.8.4.Q注3.3擦除引理也适用于弱正交TRS。这是Terese [9],练习9.3.28的结果。[8]证明也在Terese [9],p.126,命题4.8.4或p.514,引理9.3.27和练习9.3.28(i)中。9 Theorem 5.9.5,p. 175 in Terese [9].J. Ketema等人理论计算机科学电子笔记124(2005)657111t0C1[A]C1 [A]tB1图3. 第一个放大步骤4泵引理我们现在将使用擦除引理来获得关于弱正规化但仍然允许无限约化的项的一些信息。为了便于参考,我们定义:定义4.1设t是弱正规化的,但不是强正规化的。换句话说:t∈WN− SN。那么t是一个例外项。注4.2文献中出现的一个相关定义如下:如果WN(t)≠SN(t),则项t是一致归一化的。所以t是一致正规化的,它并不例外。参见,例如,Khaashvili等人[4]的文件。现在考虑图3中的例外项t0。设t是它的标准形式。考虑将t0→t化为标准形式。现在t0有一个无穷约化,∞(t0),但t∞没有,<$∞(t∞)。所以约化t0→t必须有收缩redexs(用{s}表示)的关键步骤,它是垂直约简t0→t中的重绘步骤。 此关键步骤{s}的开始时间为形式C1[A∞]对于某个非空上下文C1[],项A∞具有1 1无限还原(它是非空的,因为redexs包含A∞将被删除。)反过来,我们将A∞归一化为A∞(它仍然包含在残差1 1在某个可擦除的位置处还原s的sJ我们以步骤{sJ}结束其中正规形式A被擦除。结果是B1。(不一定)一个标准形式,但可通过连续性还原为第一个标准形式t,即图3中左下角的还原。)包含在非空空间中的垂直正规化约化A∞→A∞1 1上下文C1[],现在又有了一个关键步骤,第二个垂直中的重步骤图3中的简化,这是通过相同的推理,非空上下文C2[]中的擦除步骤。放大这一步会产生图4中的第三个垂直缩减。我们无限多次重复放大构造,72J. Ketema等人理论计算机科学电子笔记124(2005)6512312J:t0C1[AC1[C2[A]C1[C2[C3[A]C1 [A]C1 [C2 [A2]C1[C2[C3[A3]]:tC1[B2] C1[C2[B3]]图4. 重复放大构造如图5所示。由于上下文Ci[]是非空的,因此图4中上部水平缩减中的项在长度上是无界的,并且图4中下部扩展中的项也是如此。这里的“扩展”是一种向后的缩减。所以我们可以选择上约简t→t1→t2→. 在“阶梯”中t0←tJ←tJ←. 我们有两两 相 异 项。所以,上层减少以及较低的扩展是免费的重复(非循环),因此无限的。定义4.3缩减阶梯是图5所示的缩减图。这里ti和tJ是两两不同的,所以一个梯子由无限个许多不同的术语。tt1无限非循环约化t2t3范式t0t'1t'2无限非循环展开图5. 无限递减定理4.4(泵引理)设t是弱正规化正交TRS中的例外项。然后又道:(i) 这是一个无限阶梯的起点J. Ketema等人理论计算机科学电子笔记124(2005)6573一BCD(ii) t具有无限非循环约化,其标准形式具有无限非循环展开。直接从梯子的定义和上面描述的迭代放大构造中证明Q我们现在将得出结论,对于正交TRS:WN_n。定理4.5设R是弱正规化正交TRS。(i) 设G(t)是R中的有限约化图。t是SN。(ii) 更不用说,G(t)不包含约化圈。也就是说,R具有ACfinn属性。假设t不是SN。则t是例外项,定理4.4适用。所以t是一个阶梯的开始,根据定义,它是无限的。但这并不适合于有限的G(t)。Q图6.图6中著名的TRS在其签名中有四个常量符号 它似乎反驳了定理,因为它是归一化的,而项B的有限约简图确实有一个约简循环。然而,该TRS不是正交的;规则B→C和B→A重叠。例4.6考虑具有两个规则{A→B(A),B(x)→C}的TRS。这是定理4.4最简单的例子:A是一个例外项,并且确实是一个阶梯的起点,见图7。注意,该TRS还满足WN。它不是SN,而是头部归一化(WHN)。它也是AC。请注意,它是擦除(<$NE),这是必然的情况,因为WN成立,但<$SN。注4.7一个与上面使用的放大结构相当类似的结构也出现在Van Oostrom[10]中。AB(A)B(B(A))B(B(B(A)C B(C)B(B(C))图7.74J. Ketema等人理论计算机科学电子笔记124(2005)65图8.定理4.8设R是正交TRS,不一定是WN。如果G(t)是有限的并且包含一个圈,那么t在它的族中有一项没有正规形。证明如果不是,则TRSG(t)是WN。根据定理4.5,有限图G(t)中不可能有圈。矛盾Q定理4.8由Klop [6]在没有证明的情况下提出以下情况也是如此定理4.9设R是正交TRS,t是R中的一项.如果G(t)包含无限约化,但不包含无限非循环展开式,则t在它的族中包含一个没有正规形的项。证明假设R是一个正交TRS,t是R中的一项,G(t)有一个无限约化但不是无限展开。现在假设为了证明通过矛盾,该t在其族中不换句话说,子TRSF(t)具有特性WN。F(t)是一个正交TRS,其中t是例外项,因为t有无穷大减少和WN保持。因此,定理4.4(ii)t是无限梯子的起点。 请注意,阶梯中的所有点实际上都是t,因此阶梯完全存在于G(t)中。但是G(t)确实包含无限非循环展开,矛盾。Q例4.10设t为图8中正交TRSR的一项,t0为图的顶部。 (SuchR和t0确实存在,J. Ketema等人理论计算机科学电子笔记124(2005)6575?NE很容易给出一个例子)。所以我们有t0→t1→t2→. t n→.. . 对所有i≥0:ti→tω,tω→tω+1,ti→tω+1. 然后,由于图包含无限约化但不包含无限非循环展开,所以t0在其族中必须有一个不具有正规形的项。因此,一个正交的TRSR是WN,不能有这样一个约简图的项5循环和弱正规化现在让我们来看看图9中的情况。WIN SNAC WN LF交流散热片图9.上面的定理4.5提出了一个例子的问题,弱正规化,正交TRS的减少循环存在。我们知道它不可能发生在有限约简图中;但也许在无限约简图中呢?有些令人惊讶的是,这样的例子并不容易找到,因此产生了这样的例子不存在的猜想。换句话说,猜想出现弱正规化正交TRS不允许任何约简循环,或者简称为非循环(AC)。这就是标记为在图9中,我们现在将证明作为证明的一个重要部分,我们使用头部规范化定理。定理5.1对于正交TRS:我们将证明命题<$AC_WN。假设是AC。所以有一个循环。现在取一个最小的循环项t,关于t的大小最小。所以有一个循环还原C:t→. →t,并且所有小于t的项都不是循环的。76J. Ketema等人理论计算机科学电子笔记124(2005)655.2 C的步骤之一是根步骤。证明的索赔让t有形式F(t1,.,t n)对于一些n。 假设这个说法不正确。因此,根符号F是“冻结”的,即,不活跃,并且C中的所有步骤都发生在子项t1,.,t n.必须在C中完成一个步骤,比如在ti中。现在我们从C中取出Ti中的所有步骤。它们不受C中其他步骤的影响。但是很明显,C中的这些步骤a cycle t i→. →ti,与t的极小性矛盾。Q现在我们将这个循环展开为无限约简C; C; C;...... C;.. . ,即,C无限次重复,记作Cω。根据权利要求5.2,约化Cω有无穷多个根阶。因此,根据头部正规化定理,起始项t没有头部正规形,更不用说没有正规形了。form.也就是说,我们已经证明了WN。Q推论5.3设R是正交TRS,不一定是WN。如果t是一个循环项,则t在它的族中有一项没有正规形。证明设t是R中的循环项。假设t在其族中不存在无正规形的项。也就是说,F(t)是具有WN性质的正交TRS。则由定理5.1,F(t)是非循环的,矛盾的。Q注5.4将定理5.1与Van Oostrom [11]的以下相关观察进行比较:允许平凡头阶的项在弱正交TRS中不是正规化的。这里一个步骤是与本定理5.1相比,该观察更一般,因为它适用于弱正交TRS(左线性和只有平凡的临界对)。另一方面,它不太一般,因为只考虑一步循环。然而,在我们计划的本论文的续集(见第6节),一个完整的推广弱正交的情况下获得。注5.5定理5.1在Terese [9],p. 469中也有陈述,在那里它被以一种非常不同的方式证明,产生了一个更一般的定理。这里使用的技术将在我们计划的续集中使用,在第6节中描述。6结论和问题本文的主要定理,即定理5.1,指出对于正交TRS,WN_(?)AC实际上延伸到三个不同的方向:(i) 涉及完全扩展的高阶模式重写系统,其中项可以包含约束变量,J. Ketema等人理论计算机科学电子笔记124(2005)6577(ii) 弱正交的情况下,其中规则可能有(平凡)冲突,和(iii) 弱头部标准化(WHN),其中假设存在头部标准形的减少。在本文的续篇中,我们将首先分别讨论这些扩张,然后讨论它们的组合。通过替代技术,我们发现,对于三个扩张的每一对组合,我们现有定理的推广。这些扩展的部分相关性在于,我们的定理被证明对λβη-演算的子演算,特别是类型化子演算成立。然后我们的结果适用于λ型结石的范围。然而,所有三个扩展的组合仍然是开放的引用[1] 巴伦德雷格特H。P.,“The Lambda Calculus: Its Syntax and Semantics,” Studies in Logicand the Foundations of Mathematics[2] Bergstra , J. 和 J. W. Klop , Church-Rosser strategies in the lambda calculus , TheoreticalComputer Science9(1979),pp. 27比38[3] Bergstra,J.一、J.W.Klop和A.Middeldorp,“Termherschrijfsystemen,”Programmatuurkunde,Kluwer Bedrijfswetenschappen,Deventer,1989,in Dutch.[4] Khaashvili,Z.,M. Ogawa和V.van Oostrom,Perpetuality and uniform normalization inorthogonal rewrite systems,Information and Computation164(2001),pp.118-151.[5] Klop,J.,未出版的笔记,为研讨会上的减少机器。[6] Klop,J.,术语重写系统,在:S。Abramsky,D.Gabbay和T.S. E. Maibaum,编辑,《计算机科学中的逻辑手册》,2,牛津大学出版社,1995页。1-116[7] Klop,J.W.,组合逻辑中的归约循环。作者声明:To H. B. Curry:Essays on CombinatoryLogic,Lambda Calculus and Formalism,Academic Press,1980 pp. 193-214.[8] Probst , D. 和 T.Studer , How to normalize the Jay , Theoretical Computer Science254(2001),pp.677-681[9] Terese,[10] van Oostrom,V.,最终增加(1998年4月),工国委和乌得勒支大学,草案,http://www.phil.uu.nl/~oostrom/publication/ps/ei.ps网站。[11] van Oostrom,V.,Trivial(1998年8月),乌得勒支大学,草稿,http://www.phil.uu.nl/~oostrom/publication/ps/trivial.ps网站。[12] Waldmann,J.,The combinator S,Information and Computation159(2000),pp.2-21
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- OptiX传输试题与SDH基础知识
- C++Builder函数详解与应用
- Linux shell (bash) 文件与字符串比较运算符详解
- Adam Gawne-Cain解读英文版WKT格式与常见投影标准
- dos命令详解:基础操作与网络测试必备
- Windows 蓝屏代码解析与处理指南
- PSoC CY8C24533在电动自行车控制器设计中的应用
- PHP整合FCKeditor网页编辑器教程
- Java Swing计算器源码示例:初学者入门教程
- Eclipse平台上的可视化开发:使用VEP与SWT
- 软件工程CASE工具实践指南
- AIX LVM详解:网络存储架构与管理
- 递归算法解析:文件系统、XML与树图
- 使用Struts2与MySQL构建Web登录验证教程
- PHP5 CLI模式:用PHP编写Shell脚本教程
- MyBatis与Spring完美整合:1.0.0-RC3详解
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功