项重写系统的性质的可判定性与不可判定性

可在www.sciencedirect.com在线获取理论计算机科学电子笔记290（2012）69-85www.elsevier.com/locate/entcs项重写系统性质的新的不可判定性结果Rakesh Verma拉凯什·维尔马1，2美国德克萨斯州休斯顿大学计算机科学摘要本文讨论了术语重写系统的几个基本性质：可达性，可连接性，范式的唯一性，唯一规范化，一致性和范式的存在性，对于重写系统的子类，由变量的语法限制定义。所有这些性质都是不可判定的对于一般类和可判定的地面（无变量）系统。最近，有令人印象深刻的进展，有效的算法或可判定性的结果，许多这些属性。 本文的目的是提出新的结果，并组织现有的，以进一步澄清这些属性的可判定性和不可判定性之间的界限。另一个目标是刺激研究走向一个完整的分类这些属性的子类定义的语法限制的变量。所提出的结果的证明可能是本质上有趣的，以及由于其经济性，这是部分基于改进的减少之间的一些关键词：项重写系统，决策问题，可达性，一致性，规范化性质1介绍编程语言解释器，证明方程，抽象数据类型，程序转换和优化，甚至计算本身都可以通过一组规则来这些规则用于将给定表达式的子表达式替换（重写是定理证明器和符号代数简化算法的核心。重写系统可以是特定语言，甚至是编程语言。近年来，重写系统的可达性、可连接性、一致性、唯一规范化（UN→）、规范唯一性等基本性质的1研究部分由国家科学基金会资助CCF-0306475。2电子邮件：rmverma@cs.uh.edu1571-0661 © 2012 Elsevier B.V. 在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.11.01270R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）69形式（UN=）和重写系统的更广泛子类的范式的存在。所有这些性质都是众所周知的，对于无限制的情况是不可判定的（例如参见[19]），对于基础（无变量）情况是可判定的，[16，2，3，1，18，17]。可达性、可连接性和连续性对于线性浅重写系统类[7]、右基系统[8]和浅右线性系统[6]都是可判定的UN=对于线性浅重写系统是可判定的[20]。UN→被证明是可判定的左线性，右地面系统[17] 并且对于浅右线性系统和线性右浅系统，证明了正规化是可判定的[5]（由此我们在这里也证明了正规形存在的可判定性可达性和可连接性对于左线性增长系统也是可判定的[14]。在终止问题上也取得了进展，但这里不研究。另一方面，就这些问题的不可判定性结果而言，最新进展可概括如下。文[11]证明了可达性、可结合性和连续性对于线性右浅系统是不可判定的，文[5]证明了UN→对于线性右浅系统是不可判定的，文[17]证明了UN →对于右基系统是不可判定的。UN=对于右地面系统也是不可判定的[17]。本文的目标是探讨在何种程度上最近的可判定性的结果可以扩展到更一般的重写系统的子类。事实证明，对于某些属性-例如，可连接性、可达性、范式和规范化的存在以及重写系统的相应子类的扩展空间较小并且对于少数（例如，UN→和UN=）似乎有一定的推广范围。具体地，证明了以下问题都是不可判定的：(i) 可达性，可连接性，范式的存在性和连续，线性，非重叠，非折叠，var保持，基于构造函数和深度2系统的规范化。这些结果改进了文[19]中的相应结果，文[19 ]中的结果是针对线性系统给出(ii) 线性、非折叠、基于构造函数和深度两个系统的一致性。(iii) UN=线性、非塌陷、保变量和深度2系统，以及右接地、右接地系统。(iv) 线性的、左可折叠的、保变的和非折叠的系统的可连接性，其中右侧的深度至多为2。(v) 非UN→对于线性的，右可调的，保var的和非坍缩的系统，其中lhs这改进了[5]的结果(vi) 非UN→，对于左边为右线性的非坍缩系统，其中右边的深度最多为2;对于右边为底的右线性系统，则为右坍缩系统。(vii) 可达性，连续性，正规形的存在性，以及其中右侧深度至多为2的左可达，右线性，非塌陷系统的正规化。(viii) 非线性系统正规形的存在性与正规化。R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）6971i=1这些不可判定性结果是有用的，因为它们限制了对潜在的可判定性结果的搜索，并且可达性结果也产生了对于计算通用的受限的各种在某些问题之间也提出了更严格的约简，其动机是为了更经济地得出新的结果，而不是每次都从零开始。本文件的结构如下。第2节定义了使用的术语，并包括一些有用的新的和现有的结果。第3节专门讨论两计数器机，第4节讨论可达性，第5节讨论可合并性，第6节讨论连续性，第7节讨论UN→，第8节讨论范式和正规化的存在性，第9节讨论UN=。第10章结束了论文。2预赛假设熟悉重写的基本概念[4]。设m为一个集合，称为asignatu re，具有非相关性函数α：N→N。LeVteeacoun table与…不相交的项的集合T（T，V）被定义为包含V的最小集合，并且使得f（t1，...，t n）∈T（n，V）当f∈ n，α（f）= n且t1，.，tn∈T（V，V）.集合V和V的元素分别称为函数符号和变量。注意，对于α（a）= 0，称为常数，包括在集合T（V，V）中。对于项s，Var（s）表示s中的变量集。符号s，t，u，。. ，可能带有下标，用于表示项; f，g，. . ，函数符号;以及a，b，. . ，常数。一个函数符号f∈M使得α（f）=m也记为f（m）。将项f（t1，...，t m）没有括号，ft1. t m，当这样做是明确的时候。 一个项的top（t）是t，如果t ∈ V;是f， 如果t = ft1.. t m。一个术语的大小，如果t ∈ V且t = ft1. t n是1 + nt i。一个项s的深度是0，如果s是一个变量或常数，如果s = fs1. 的作案以下定义来自[5]。如果t不包含变量，则称项t为ground。如果t中的所有变量位置都在深度0或1.如果它的深度最多为1，则它是可扩展的。它被称为线性的，如果每个变量在t中最多出现一次。位置是一个可能为空的正数序列。如果p是位置，t是项，则t|p表示t在位置p处的子项，定义为，t|λ= t（其中λ表示空序列）和（ft1. t n）|i.p= t i|p，如果1 ≤i≤n（如果i> n，则为unfined）。也可以写t[s]p（或者当p从上下文中很清楚时就写t[s]）来表示通过将t中位置p处的子项替换为项s而获得的项。例如，如果t是f（a，g（b，h（c）），d），则t|二、二、1= c，且t [d] 2。2= f（a，g（b，d），d）.一个置换，记作σ，是一个从V到T（V，V）的映射，同态扩张为一个从T（V，V）到T（V，V）的映射。σ的应用使用post fix符号表示。（无向）方程是一对无序的项，写作s=t，满足s和t不能是不同变量的条件（这个条件确保了下面定义的文字问题的非平凡性）。如果s和t是基项，则方程是基的。如果V ar（s）=V ar（t），则它是var保持的有向方程或72R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）693R规则是一个有序的项对，写作s→t，满足条件V ar（t）<$V ar（s），并且s不能是变量。此规则是接地（浅，线性，可调），如果s和t是接地（浅、线性、可调）项。 一个有限的（基本）规则集R 被称为（地面）重写系统。如果t是地（浅的，线性的，直的），则它被称为右地（右浅的，右线性的，右直的）。如果s是浅的（线性的，线性的），则称为左浅的（左线性的，左线性对于被称为浅、左浅或任何其他此类属性的重写系统，每个规则都必须满足该属性。项s和t是unifiable的，当且仅当存在一个基项C，它是s和t的instance。假设s与t重叠，当且仅当两项之一的不可变子项u(To检查重叠，重新标记s和t中的变量，使它们不共享任何变量。 A set S T不重叠当且仅当对所有s，t∈S，不（s重叠t）。（由于S和t可以相等，不重叠的定义不允许像结合性这样的自重叠规则。一个系统R是不重叠的当且仅当lhs的集合定义2.1重写系统，其中左侧和右侧的深度最多为2，将被称为深度2系统。重写系统R的定义符号的集合D（R）是D（R）={root（l）|l→r∈R}。重写系统被称为基于构造器的，如果没有定义的符号出现在任何左手边的非根位置。 重写系统是var保持的，如果对于系统中的每个规则s→t，V ar（s）=V ar（t）。方程s=t或 规 则 s→t 的 大 小 定 义 为 s= t+t= t 。如 果 R 是 一 组 规 则 ， 则 我 们 定 义R−={s→t|t→s∈R}。 我们说s在位置p（由R）一步重写为t，记为s→R，pt，如果s|p= lσ和t = s [rσ] p，对某些l→r∈R和代换σ. 如果p=λ，则重写步骤被称为在nr最高位置（在根处），记为s→Rt;记为s→Rt否则，请执行以下操作。由R在T（V，V）上诱导的重写关系→R定义为s→Rt，如果对于某个位置ps→R，pt。一组R方程或规则的大小是R中各个方程或规则的大小之和。集合R的基数表示为：|R|.如果规则（等式）的右侧（任一侧）是变量，则该规则（等式）是折叠的。 非崩溃重写系统（等式理论）没有崩溃方程式（Equations）如果→是一个二元关系，则←表示它的逆，参与它的对称闭包，→它的过渡闭包和→它的恢复过渡闭包。Thus，←E和→E− 表示相同的关系。（利用R）s→R_t的一个 还原方程是有限序列s=s0→Rs1，s1→Rs2，···，sk−1→Rsk=t（k≥0），通常简写为s=s0→Rs1→R···→Rsk=t（k≥0）。两项s和t可由R连接，或R-可连接（记法：s↓Rt），如果存在存在一项usu c h，使得s→<$Ru和t→<$Ru。s和t等于R，或R-等价nt，如果s参与Rt（也写作s=Rt）。重写系统R是con deduent如果每对R-等价项都是R-可连接的。一个左线性的，不重叠的3请注意，这些条件与[19]中的相同。第一个条件确保这里处理的一些问题不会变得微不足道。+R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）6973系统也称为正交系统，正交系统是连续的[10，15]。如果不存在项t使得s→Rt，则项s是不可约的或R-正规形式（当从上下文清楚时，R将被丢弃）。一个项s的R-正规形是一个R-正规形t，满足s→ <$Rt。 重写系统是UN=（交替地具有UN=属性），如果每当n = RN对于范式n和N意味着n和N在语法上相同。 它是UN →（或者具有UN →性质），如果每个项至多有一个R范式。可达性/可连接性。实例：重写系统、R、项s和t。问：D oess→Rt/s↓Rt？范式可达性。实例：重写系统，R，项s和t，其中t是w.r.t.的正规形式。 R. 问题：D oess→Rt？对于上面的三个问题，也定义了输入重写系统满足某个属性P的版本。为了表明这些版本，短语UN=/UN→/浓度。实例：重写系统R。问题：R是否具有UN=/UN→/Concuruence属性？规范形式的存在。 实例：重写系统R和项s。问：S有R范式吗文字问题（WP）。实例：有限方程组E（或重写系统R），项s，t。问题：s=Et（s=Rt）吗？正常化。实例：重写系统R。问题：每个不变项4s是否都有一个R范式？2.1一些新的和现有的有用结果在这一节中，我们收集了一些现有的结果和观察，以及一些新的结果（特别是推论2.2，定理4，定理5和推论2.7），我们需要为其余的文件。通常，A≤PB表示从A到B的多项式时间约简。定理1（[11]）可达性、可结合性和连续性是不可判定的。定理2（[5]）对于线性右浅系统，非UN →不可判定。我们改进了下面[5]的结果（附录包括它们的构造以帮助读者）。推论2.2 Not UN →对于左边深度至多为2的线性、右可解、var-保持和非坍缩系统是不可判定的。证据首先，观察到在[5]中从Post correspondence problem（PCP）到UN→的约现在证明这个结果有两个障碍：[5]的约简不是var保持的，并且某些左手边是任意深度的。第一个是固定的如下。从签名中删除常量循环，4由于我们的限制，lhs的规则不能是一个变量，每个变量总是一个范式。74R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）69规则循环→循环。接下来，形式为l→loop的每个规则，它不是var保持的，其目的是破坏不需要的范式，被规则l→l取代。对于第二种情况，请按以下步骤操作。令PCP ={（u i，v i）|1 ≤i≤n}是关于{a，b}的后相关问题. 将规则pcp（x，y）→pair r（x，y）in[5]替换为n个新规则pcp（x，y）→ pair i1（x，y）。 现在删除[ 5 ]中的规则对（u i（x），v i（y））→对（x，y），其左侧可以具有任意深度。（1）A = max（|u i|、|vi|）.不失一般性地假设，|u i| ≥ |v i|.那么，u i= u i（1），u i（2），.，u i（m（i））和v i= v i（1），.，v i（k（i）），其中k（i）≤m（i）。当然，ui（j），vi（j）∈{a，b}. 有两个案子。情况1：k（i）0}是一组不在N中的新函数符号. 对于每个f（m）∈f，对应的函数符号hf具有元m+2.令J=H{true，false}。设T ={c→c|c∈{fx1. x n→fx1. X n|f（n）∈N，n> 0}. 所以T（n，J，V）中的所有非变量项都是可约的，除了真和假。让S={c → h（cs，c）|c ∈ {f x1. x n→ h f（c s，x1. x n）|f（n）∈N}。令V ={h f（c t，y1，.，y n）→true|f（n）∈ N}。令RJ=R<$S<$T<$V <${ct→false}。因此，如果RJ不是UN→is→Rt。假设RJ不是UN→。想想看， 一个项A∈T（N，V），并假设A有两个不同的正规-表格B和C。由于对R的非塌陷要求和RJ的非塌陷，RJ也是非塌陷的，因此B和C都不能是变量。因此，我们必须有一个约简序列p：A→R′t rue和q：A→R′false。我们主张p和q意味着s→<$Rt。 注意，由于RJ是重写系统，一个人不能成为一个人。则top（A）∈R，否则A→R′false为不可能现在，由于top（A）∈A，并且没有折叠规则，所以规则top（A）（x1，.，x n）→h f（c s，x1，.，xn）必须已经应用在序列p的根处，并且随后规则hf（Ct，y1，...，y n）→ true必须已应用在p的r ot。 这意味着cs→<$R′ct，而ch意味着s↓R′t。现在，与定理9（[17]）的完整推导类似的一个公式可得到s→Rt。现在假设s→Rt，这意味着s→R′t。显然，RJ不是UN→，因为t→<$R′ct→R′h（cs，ct）→<$R′h（ct，ct）→R′true和t→<$R ′ct→R′false和true和false是不同的范式。QR. Verma/Electronic Notes in Theoretical Computer Science 290（2012）6981注意，上述减少保留了线性和非线性。推论7.1Not UN→不可判定：(i) 左对称、右线性、非坍缩系统，其中右侧的深度最多为2。(ii) 线性、非塌陷和深度2系统。证据（i）定理10和定理5（ii）定理10和定理7。Q在[17]中，证明了对于右基系统UN→我们可以应用[20]的保留UN→属性的保留过程来得到：定理11 UN →对于右基右群重写系统是不可判定的。8正规形的存在性与正规化定理12对于连续的、线性的、非塌陷的、保var的、基于构造函数的和深度为2的系统，规范形的存在性是不可判定的。证据设R（M）的签名表示在上述定理7中构造的R（M我们构造RJ和SJ，这是标准形存在的一个例子，如下所示。设T={c→c|c∈ n} n {hx1，.，x n→hx1，...，X n|h∈ H}，使得T（H，V）中的所有不变项都是可约的。令RJ=R（M）<$T<${h（f，Z，Z）→d}，其中d是一个新常数，令SJ=h（s0，Z， Z）. 然后，显然sJ有一个RJ标准形式（即， d）i∈s→i ∈Rh（f，Z，Z）.注意，RJ是var保持的，非折叠的，线性的，深度为2。这也是一致的，因为所有的临界对都是平凡地平行闭合的。Q定理13可达性≤P规范形的存在性.证据设R，s，t是可达性的一个实例。构造RJ和SJ，规范形式存在的一个实例，如下所示。第一步，使用注意规则[7]。这些规则保持了R项的可达性。让ct成为t的新我们把所有引入的新名字加到R上，把所有的注意规则加到R上。设d是一个新的常数，不等于0。设T ={c→c|c∈ n} n {hx1，.，x n→hx1，...，X n|h∈ H}。设RJ=R<$T<${ct→d}，sJ=s。那么，显然SJ有一个RJ标准形（即d）i ∈s→Rt. 回想一下，s可以假设地面。 我们没有假设一个固定的签名，所以这并不影响s的范式性质，因为新常数是R-不可约的（因为它们是新的）。如果我们不得不引入新的常数来强制s，t的基性，那么我们使它们成为n的一部分，并使它们可约为w.r.t.。RJ.上述简化保留了左线性、右线性、线性、非线性，非折叠属性，并且是var保持的。它也可以被修改以保持接地（见[19]）。推论8.1（a）对于下列系统，规范形的存在性是不可判定的：（i）非线性系统和（ii）左线性、右线性、非坍缩、保var系统，其中右侧深度至多为 2。(b) 归一化是不可判定的：（i）线性，非塌陷，var保持82R. Verma/Electronic Notes in Theoretical Computer Science 290（2012）69J和深度为2的系统，（ii）非线性系统，和（iii）左非线性、右线性、非线性、VAR保持系统，其中右手边的深度至多为2。(c) 规范形的存在性是可判定的：（i）线性，右浅和（ii）浅，右线性系统。证据（1）定理13和定理1。定理13和5。(b) 可达性可以简化为标准化。证明是非常相似的还原到存在的正规形式的问题，所以我们只描述的变化。使用定理13的符号，构造如下的归一化的实例R j j：RJ J= RJ<$S，其中RJ如定理13中所示，并且S={c→cs|c∈}{hx1，.，x n→c s|h（n）∈ n，n > 0}.回想一下，cs是通过对s进行幂次运算得到的。 如果s是常数，我们仍然引入常数c s和辅助规则。然而，我们将展示一些更强大的东西，即，规范形式的存在性和规范化之间的还原的存在性正规形的存在性是正规化问题的一个特例。如果这对读者没有说服力，我们证明存在从规范形式的存在到规范化问题的简化，如下所示。设R，s是正规形问题存在性的一个例子.像[20]中那样展平s，并将结果重写系统也称为R。构造一个图灵机N，它在一个最终状态（比如f）中精确地接受基R范式。现在用一个双计数器机器M来模拟N。接下来，使用重写系统R（M）模拟M，并让（M）表示R（M）的字母表（我们确保f是（M）中的常数现在使用定理13的符号，如下构造RJ的归一化实例 RJ= R<$S<$R（M），其中S ={c→cs|c∈（M）− {f}}{hx1，.，x n→c s|h（n）∈ n，n> 0}. S规则确保f是唯一的基标准形式的R和每一个不可变的条款，除了f，减少到cs，新的名称为s。那么，每一项都有一个RJ标准形式i ∈s都有一个R标准形式。请注意，缩减保留了线性度和深度2。 它可以被修改以保持如下的可扩展性。不是用双计数器机器模拟N，而是构造一个PCP实例，然后通过重写系统模拟PCP实例，如[11]所示。 这一结构的细节将推迟到本文的完整版本。(c) 这两个部分都是从部分（b）归约到规范化，并在[5]中得到规范化的可判定性结果。Q9正规形作为定理8的推论和从同生系统的可合并性到规范形的唯一性的简化[19]，我们有如下结果：定理14 UN =对于线性的、非塌陷的、var保持的和深度为2的重写系统是不可判定的。证据[19]的约简保留了线性，非塌陷和var保持属性，并且可以使用[20]的对（地面）项s和t的衰减过程进行修改以保持深度。QR. Verma/Electronic Notes in Theoretical Computer Science 290（2012）6983在[17]中