条件项重写系统的转换和性质分析：满足额外条件的最小转换

理论计算机科学电子笔记174（2007）75-95www.elsevier.com/locate/entcs条件项重写系统西田直树1水谷智弘2酒井正彦3名古屋大学大学日本名古屋摘要解拆开是条件项重写系统到无条件项重写系统的转换，对于分析条件项重写系统的性质具有重要意义。为了完全模拟重写序列的CTRS，由一个特定的上下文敏感和成员资格条件，这是由额外的功能符号，由于解开引入的限制，必须施加在重写关系解开CTRS。在本文中，为了削弱上下文敏感和成员资格条件，我们提出了一种变换应用于解开的CTRS，减少了额外的符号的数量。在转换中，适当地更新上下文敏感条件，我们删除了满足一定条件的额外符号。如果变换成功地去除了所有额外的符号，则我们获得与原始CTRS在计算上等效的TRS。保留字：解开，上下文敏感约简，隶属约束，程序转换1介绍Unraveling是从条件项重写系统（CTRS，简称）到无条件项重写系统（TRS，简称）的转换[7]。 它们对于分析CTRS的性质是有用的。 例如，操作终止[6]4是CTRS的一个重要属性，它可以通过终止解开的CTRS来保证[6，7，13]。从CTRS 到 TRS 的 第 一 次 转 换 是 由 J.A. Bergstra 和 J.W. Klop [3]. 这 一 概 念 被M.Marchiori等人讨论了它的句法性质、终止性、模块性等[7]。他还提出了一个1电子邮件：nishida@is.nagoya-u.ac.jp2电子邮件：mizutani@sakabe.i.is.nagoya-u.ac.jp3电子邮件：sakai@is.nagoya-u.ac.jp4直觉地，如果由连续部分引起的并且需要用于决定给定项是否可约的所有约化也终止，则终止CTRS在操作上是终止的。文[6]表明，对于CTRS终止，操作终止比“effective termination1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.04876N. Nishida等人理论计算机科学电子笔记174（2007）75K我ρ：l→rs1→t1···sk→tk⎧⇓U⎫l→uρ（s1，−x→），11uρ（t1，−x→）→uρ（s，−x→），⎩11222ρ−→⎭你 （tk，xk）→r图1.一、确定性CTRS的分解概述为加入CTRS而解散E. Ohlebusch提出了一个确定性3-CTRS的解释，以证明逻辑程序的终止性[12]。Ohlebusch的解开的一个变体众所周知，CTRS的约简比TRS的约简复杂得多。原因之一是递归约简对于评估实例化条件部分是必要的。解缠似乎是有吸引力的，为了计算约简序列的CTRS。然而，在一般情况下，他们不保持两个重要的属性，不可约的正规形式的CTRS（正规形式的不变性）或模拟完整性。 请注意，所有CTR的正规形式都没有很好的定义。在这里，如果解开保留了签名上的项的可达性和不可达性，则解开被称为签名上的CTRS的模拟完成[9，10，11]。请注意，本文中的模拟完全性” 直觉，计算等价性可以被认为是“模拟完全性和规范型的不变性”。一般来说，对于任意目标CTRS而言，解开不是模拟完成的，因为解开的CTRS是原始CTRS的过度近似[7，13]。然而，研究表明，特定上下文敏感和成员资格条件对解开的CTRS的重写关系的限制使得确定性CTRS的解开保持了原始CTRS的不可达性，即，关于特定上下文敏感和成员资格约简的解开的模拟完整性[11]。解开通常是通过将每个条件规则分解为一些无条件规则来完成的，这些规则应该以固定的顺序使用（见图11）。①的人。设ρ是CTRSR中的条件重写规则l→rs1→t1···sk→tk，σ一个替代品用一个约简来模拟ρ从lσ到rσ的约简步骤从相应的无条件规则构造的序列如下：lσ−→uρ（s1，−x→）σ−→<$ uρ（t，−x→）σU（R）11U（R）11 1−→uρ（s2，−x→）σ−→σ···−→∗uρ（t，−x→）σ−→rσ。U（R）22U（R）U（R）KKKU（R）序列从lσ开始。在序列中，每个额外的函数符号uρ，称为U符号，顺序地检查从siσ到tiσ的可达性（换句话说，uρ用σ）评估条件si→ti序列最终在rσ处结束我的这是一个非常复杂的问题，它是，siσ−→Rtiσ。我们确信，解开保留在原始签名的条款上的可达性。另一方面，如上所述，解开并不保存N. Nishida等人理论计算机科学电子笔记174（2007）7577JJJ..Σl→uρ（t1δ，.，tmδ），uρ（t1，.、tm）→rΣ单位：μi不=<$（{l→rδ}<$S，μi+1）其中uρ是可移除的（满足第4.2小节中描述的条件R M c），并且context-s i isiv e contionμii supdtooμi+1withr e pettoroot（r）。图二、通过变换T删除U符号的概要。对于所有CTR来说，这是不可达的，因为意外的重写序列有时是由于不遵守规则的应用顺序而导致的，规则的左手边以U符号为根[7，13]。为了避免这种情况，需要对解开的CTRS的重写关系进行限制，这禁止减少以下赎回：• （上下文敏感）严格出现在U符号下方的符号，除了U符号的第一个字符串之外（对于字符串，redexsinx→iσ），或者• （MEMBERSHIP）在其适当的子项中包含U符号的那些。通过这种方式，上述上下文敏感和成员资格条件的限制被施加在解开的CTRS的重写关系上，以保持模拟完整性[11]。在本文中，我们试图构建无条件的TRS（从解开的CTRS）是模拟完成相应的CTRS没有上下文敏感和成员资格条件。首先对确定性CTRS的解包方法进行了改进，使得解包规则的数量少于普通解包方法.这种改进是通过对尽可能多的条件进行分组来完成的然后，我们提出了一个变换，应用于解开的CTRS，以消除尽可能多的U符号从解开的CTRS。虽然这种改进并不新奇，但在某些情况下，它有助于减少U符号的数量（见第4节）。我们提出的转换的每一步都是基于两个规则的2）的情况。我们展示了一个微妙的条件（4.2小节中的RM c），要删除的U符号应该满足该条件，以保持模拟完整性，我们收紧它，以保持与函数式程序的let结构相关联的CTRS的优势（第6节中的RM cJ）。“合成”是一个相当琐碎的通过上下文敏感和成员条件放松限制，因为该条件依赖于U符号的存在。我们还证明了变换的正确性，并证明了分解和变换的组合也是一种分解。我们还表明，变换保存的连续性的CTRS模的减少策略的上下文敏感和成员资格条件，在原始签名的条款在非“操作终止”意味着“非终止或没有操作终止的终止”的所有情况下，转换不保留非该缺点使得不可能通过终止相应的解开的CTRS来证明CTRS的操作终止为了消除这个缺点，我们需要使用一个收紧的RM c，即RM cJJ78N. Nishida等人理论计算机科学电子笔记174（2007）75在第7节。不幸的是，不是所有的U符号都可以被移除，也就是说，转换有时会在移除所有U符号时失败尽管如此，即使不是所有的U符号都被删除，我们也有一些• 上下文敏感的条件有时会被删除。• 转换帮助我们简化条件规则。如果我们成功地删除所有U符号，还有以下进一步的优点。• 上下文相关条件和成员资格条件消失。• 保留了CTRS的连续性。因此，为了证明CTRS的连续性，我们可以使用几种技术来证明TRS的连续性• 保持了CTRS的正规形式的不可约性。这使我们计算等效的TRS与原来的CTRS。因此，我们提出的转换是无害的模拟完整性，操作终止和非CTRS无论何时都是基于RMCJ和RMCJJ。 最大的优势的变换是，我们获得计算等效的TRS与如果我们成功地移除所有U符号，则会生成原始CTR。即使不是所有的U符号都可以被删除，我们也可以获得简化的CTRS，这些CTRS在计算上与原始CTRS等效。在[10，11]中提出的反演编译器编译器将构造器TRS转换为CTRS，CTRS计算TRS中定义的函数的（部分）逆然后编译器将CTRS分解为TRS，TRS的规则可能有额外的变量。由于表示多对一函数的逆计算的项可能有几个范式作为计算的解，因此作为编译器的中间结果的CTRS并不总是连续的。出于这个原因，本文不假设CTRS的连续性。本文中的变换有时对于简化编译器得到的TRS是有用的。我们将在本文的最后给出一个例子。作为模拟完全性的另一种方法，证明了正常CTRS的解开对于所有左线性正常CTRS都是模拟完全的[7]。还表明，如果解开的CTRS是左线性的或右线性和非擦除的，则确定性CTRS的解开对于CTRS是模拟完成的[9]。[9]中的方法不适用于所有确定性CTRS，而[11]中的方法适用于所有确定性CTRS。本文的组织结构如下。在第二节中，我们给出了项重写的符号。在第3节中，我们介绍了一个变种的Ohlebusch我们还稍微改进了解开。在第4节中，我们提出了一种转换，该转换将由于改进的解开而引入的额外功能符号从解开的CTRS中移除。在第5节中，我们讨论了CTRS的一致性和未解决的问题。N. Nishida等人理论计算机科学电子笔记174（2007）7579RRCTRS。在第6节中，我们收紧了删除多余函数符号的条件。第七部分是结束语和相关著作。2预赛本文遵循项重写的基本概念[2，13]。在本节中，我们将概述基本的符号。通过本文，我们使用V作为变量的可数无限集合。签名F和V上的所有项的集合由T（F，V）表示。出现在t1，.，t，n由Var（t1，.，tn）。项s和t的恒等式用st表示。 对于项t和t的位置p，符号t|p表示t在p处的子项。 在t的根位置ε处的函数符号由root（t）表示。符号C [t1，.，tn] p1，...，pn表示通过将n空穴上下文C的位置pi处的Q替换为项ti（1 ≤i≤n）而获得的项。置换σ的定义域和值域分别用Dom（σ）和Ran（σ）表示。σ对t的应用σ（t）简写为tσ。所述组合物置换σ和θ的σθ定义为σθ（x）=θ（σ（x））。签名F上的（定向）条件重写规则是三元组（l，r，c），由l→r→c表示，使得左手侧l是下式中的不可变项：T（F，V），右边r是T（F，V）中的一项，条件部分c的形式为T（F，V）中的项si和ti的s1→t1···sn→tn（n≥0）特别地，如果n= 0，则条件重写规则l→rc被称为（无条件）重写规则，并且我们可以将其简化为l→r。我们说二元关系~和代换σ满足条件部分c，记作c（σ，~），如果siσ ~ tiσ对1≤i≤n。我们用一个唯一的标号ρ来表示l→rc，记作ρ：l→rc。为了简化符号，我们可以写标签而不是相应的规则。对于一个条件重写规则ρ：l→rc，不在l中但在r或c中出现的变量称为ρ的额外变量。ρ的所有额外变量的集合记为EVar（ρ）。设R是签名F上的条件重写规则的有限集合。n级R的rewrel a t i o n−→nRofR的定义如下：−→R=n，nd−→R0n +1={（C[lσ]p， C[rσ]p）|ρ：l→r<$c∈R，c（σ，−→σ）}. Thereriterelation−→nR R如果R被定义为s−→R=n≥0−→nR。为了实现这一点，我们writes−→ptors−→[p，ρ]t. 一种（面向）条件重写系统（CTRS，f（fh）v∈ F是f（f，V），-→R）的一个随机可积系统（T（F，V），-→R）T（F，V）和F上条件重写规则有限集R的重写关系。 我们使用规则的集合R来确定CTRS（T（F，V），−→R）。一个CTRS被称为带有额外变量的项重写系统（简称EV-TRS），如果它包含无条件重写规则。请注意，如果在重写序列中将每个额外变量替换为范式，则可以通过缩小来模拟EV-TRS的重写序列[8]。具体地说，它是一个项重写系统（TRS，简称），如果对于其中的每个规则l→r，Var（l）都等于Var（r）一个CTRSR称为1-CTRS，如果R中的每个规则都没有额外的变量，一个2-CTRS，如果R中的每个规则在其右侧没有额外的变量，3-CTRS，如果对于R中的每个规则，规则的所有额外变量都出现在条件部分，80N. Nishida等人理论计算机科学电子笔记174（2007）75R∈T∈T如果没有施加限制，则为4-CTRS。一个条件重写规则ρ：l→rs1→t1···sk→tk称为确定性的，如果Var（si）<$Var（l，t1，.，ti−1），其中1 ≤i≤k。一个CTRS被称为正常的，如果它的每个规则l → r s1→ t1···sk→ tk满足t1，. ，t，k是Ru={l → r |l → r <$c ∈ R}。我们在[ 5 ]中使用了上下文敏感约简的概念。设F为签名。上下文敏感条件（替换映射）μ是从F到一组自然数的映射，使得μ（f）={1，. ，n}，对于F中的n元符号f. 当μ（f）没有明确定义时，我们假设μ（f）={1，.，n}。一个项t的替换（有效）位置的集合Oμ（t）归纳定义如下：Oμ（x）当x∈V时，满足Oμ（f（t1，.，tn））={ip|f∈F，i∈μ（f），p∈Oμ（ti）}. 的具有h μ的EV-TRSR的文本敏感检索定义为s−→（R，μ）={（s，t）|s−→pt，p∈Oμ（s）}. Anabstractreductionsystem（T（F，V），−→（R，μ）），表示为（R，μ）的约简系统称为上下文敏感约简系统（CS-TRS）。在本文中，我们使用一个简单的变体隶属条件系统[16]。对于EV-TRSR，由一个映射映射映射定义的− →R的二阶递归映射（其中T∈T（F，V））定义为−−→R={（C[lσ]p， C[rσ]p）|l→r∈R，R∈n（σ）<$T}. 对于r−→（R，μ）的所有计算，该公式的定义与s − →（R，μ）类似。3确定性CTRS在本节中，我们首先介绍了Ohlebusch的unaveling [ 12 ]的一个变体UO，然后，我们给出上下文敏感和成员条件[11]来保持模拟-等网站和资源最后，我们稍微改进了解开UO。这种改进是基于正常CTRS的unraveling UN [7]，并且通过我们将在第4节中展示的转换有效地减少了unraveled规则的数量（参见第4.3小节末尾的示例）。3.1Ohlebusch的分解和模拟的一个变体-我们首先定义了Ohlebusch的解开[ 12 ]的一个变体−→[4、9、10、11]。 在这里，给定一个有限项集T，我们表示为T的序列T中的元素（以某种固定的顺序），我们表示t∈TVar（t）乘Var（T）。定 义 3.1 设 R 是 签 名 F 上 的 确 定 性 CTRS 。 对 于 每 个 条 件 重 写 规 则 ρ ：l→rs1→t1···sk→，令|ρ|表示ρ中的条件数（即，|ρ|= k），我们需要k个“新鲜”函数符号uρ，.，uρ，称为U符号。 在这里，“新鲜”这个词的1ρkui∈ F，其中1≤i≤k。我们将ρ转换为k+ 1个无条件重写规则的集合UO（ρ），如下所示：UO（ρ）={l→uρ（s1，−X→），uρ（t，X−→）→uρ（s，−X→），· · ·，uρ（t，−X→）→r}.111 11222KKK其中Xi= Var（l，ti，...，ti−1）Var（ti，si+1，ti+1，.，sk，tk，r）5 对于1≤i≤k。5Xi是在r1，t1， .. . . ，orti−1andalsoinei terti，si+1，ti+1， . . . . ，sk，tkN. Nishida等人理论计算机科学电子笔记174（2007）7581我我UJ系统UO（R）= ρ∈RUO（ρ）是广义签名FU（R）= F {uρ|ρ ∈ R，1 ≤ i ≤ |ρ|}。注意，如果R是3-CTRS，则UO（R）是TRS。从原来的定义修改的点是Xi。其次，我们给出了基于[7]中提出的超性质完备性的模拟完备性定义3.2设U是从CTRS到TRS的变换，R是签名F上的CTRS。• UissaidtobeR-reachability-preserving（−→对于R，如果U∗保持R的可达性，即对于所有项s和t∈ T（F，V），s−→Rtimpliess−→U（R）t。• U是R的模拟声音，如果U保持R的不可达性，即对所有sandt∈T（F，V），s−→tifs−→U（R）t。• 如果Uis−→Ui，则Uisimulation-完全满足Ri6∗R-保留和模拟声音，用于∗R，thatiss，对于所有s和t∈T（F，V），s−→Rtif和nlyifs−→U（R）t.我们类似地定义了解开系统U（R）的这些性质。所有的计划都是∗−→∗ 对于每个目标CTRS保持R，因为−→R-pres erving是一个非常复杂的概念，它将数据存储为一个“不存在”的数据。On另一方面，一般来说，它们不是所有目标CTR的模拟声音，因此不是完全模拟的。其原因是解算的CTRS对原始CTRS过于近似。在[7]中，我们可以找到一个反例，模拟-UN，UO和Ohlebusch的解开的完整性为了避免这种情况，对解开的CTRS的重写关系进行了限制关于U O的非“模拟完全性”的困难在• 定义3.1中ρ的上下文敏感条件μ，使得μ（uρ）={1}，我每个uρ，以及• 隶属条件设R的上下文相关条件μR定义为μR（uρ）=μρ（uρ）。然后，我我用UOμ（R）表示CS-TRS（UO（R），μR我们认为UOμ是从CTRS到CS-TRS的一个解。定理3.3（[11]）对于签名F上的每个确定性CTRR，U0 μ是模拟完全的（关于隶属条件is，对于所有lls和t∈T（F，V），s−→ttifandoifs−→t.∈T（F，V）Oμ（R）−→−−−−→−−−−−→−−−−−−→或r. 在Ohlebusch的原始定义中，Xi是变量序列“V ar（l），V ar（t 1），. .，Var（ti−1）"，因为所有变量都保留在自变量中，所以计算项时存在冗余如果在i+1， . ..... . 你 好 。 斯堪的纳维亚河[6][9，10，11]中“模拟完备性”的定义 更确切地说，[9，10，11]中的“模拟完备性”对应于本文中的模拟可靠性。然而，在那些关于模拟完全性的讨论中，paperessentiallyequivalentbeaceu se−→n-为所有CTRS S提供服务。RORR82N. Nishida等人理论计算机科学电子笔记174（2007）751在本文的其余部分，我们假设隶属条件3.2解缠机的改进有空间改善解开UO。我们首先解释我们改进的直观想法。UnravelingUO将具有k个条件的每个条件重写规则ρ分解为k+ 1个无条件重写规则，这些无条件重写规则用于评估条件按从左到右的顺序，引入U符号（见定义3.1）。例如，条件重写规则ρ1：f（x，y）→zg（x）→wg（y）→zh（w，x）→z被分解为以下四个无条件重写规则，引入U sym-u1，u2和u3：.UO（ρ1）=f（x，y）→u1（g（x），x，y），u1（w，x，y）→u2（g（y），w，x），u（z，w，x）→u（h（w，x），z），u（z，z）→z.2 3 3这些规则在约简序列中的应用顺序正好对应于评估条件的顺序。然而，u1和u2之间的顺序是不必要的，因为第一和第二个条件g（x）→w和g（y）→z可以并行计算。原因是所有用于求值的变量x，y已经出现在条件规则ρ1的左侧f（x，y）中。从这个事实上，我们可以将u1和u2组合成一个符号uj，如下所示f（x，y）→ UJ（g（x），g（y），x）和UJ（w，z，x）→ u3（h（w，x），z）.1 1因此，为了允许同时评估可被评估的条件，同时，我们改进了普通的UnravelingU0，使得一些条件规则被分解为更少的无条件规则。这个想法来自于正常CTRS [7]的 UnderwealingUN如后面定理3.7的证明所示，这种改进是并不新奇。然而，通过我们将在第4节中展示的转换（见4.3小节末尾的一个例子）来减少未解规则的数量有时是有效的。上述改进的思想形式化如下。定义3.4设R是签名F上的确定性CTRS。 我们认为条件重写规则ρ：l→r.Mj=1Σs1，j→t 1，j∧···∧ .Kj=1Σsk，j→t k，j在R中，使得对于所有i和j，Var（si，j）<$Var（{l}<$T1<$··<$Ti−1），其中Ti={ti，1，.，ti，mi}。注意，每个确定性条件重写规则都可以这样表达。 对于上述形式的每个条件重写规则ρ，令|ρ|表示ρ中的条件组数（即，|ρ|= k），我们需要k U符号uρ，.，uρ。 我们将ρ变换为k+ 1个无条件重写的集合U（ρ）1K1MN. Nishida等人理论计算机科学电子笔记174（2007）7583，X1），我规则如下：⎪l→uρ（s1，1， .. . ，s1，m−→⎪−→11 −→⎪⎨uρ(t1,1.. . . ，t1，m，X1）→up（s2，1， . . ，s2，m，X2），U（ρ）=11。22- 是的⎪uρ（tk，1，.，tk，m−→→rK其中Si={Si，1，... ，si，mi}和k，Xk）Xi=Var（{l}<$T1<$··<$Ti−1）<$Var（Ti<$Si+1<$Ti+1<$··<$Sk <$Tk<${r}）对于1≤i≤k。集合U（R）=ρ∈RU（ρ）是扩展签名上的EV-TRSFU（R）=F<${uρ|ρ∈R，1≤i≤|ρ|}。在上述定义中，集合Xi扮演着向后面的条件传递值的角色;这些值通过l、T1、···或Ti−1中的变量获得，并用于r、Si+1、.中。，Sk或Ti，.，Tk.在定义3.4中，人们可以自由地将条件部分划分为满足可变出现条件的条件组。集合U（ρ）等于UO（ρ）直到U符号的一些重命名，如果对于每个i，mi= 1，并且它等于UN（ρ）直到重命名，如果k= 1。 因此，UO和UN是U的特殊情况。 为为了减少无条件规则的数量，本文假设ρ定义3.4满意度Var（si，j）/<$Var（l）<$Var（T1<$··<$Ti−2），其中1

下载后可阅读完整内容，剩余1页未读，立即下载