树自动机语言在重写下的封闭性研究

理论计算机科学电子笔记237（2009）23-38www.elsevier.com/locate/entcs树自动机语言在最内层重写下的封闭性Adria`Gasco'na，1，GuillemGodo ya，1andFlorentJacquemardb，1a加泰罗尼亚技术大学，Jordi Girona 1，巴塞罗那，西班牙。2bINRIA Futurs& LSV，UMR CNRS/ENS Cachan，法国。摘要项重写系统（TRS）的正则性保持表明，树自动机（TA）语言（也称为正则项集）也是TA语言。是一项重要而有用的属性，并且已经有许多关于确定TRS类别的工作来确保它;不幸的是，对于像浅TRS这样的TRS的受限类别，规则性不被保留。然而，这一财产还没有研究过重要的重写策略，比如最里面的策略，程序设计语言的按值计算我们证明了由浅TRS从TA语言得到的最内可达项的集合不一定是正则的，但它可以被具有兄弟之间的等式和不等式约束的TA所识别。 作为由此我们得出了TA语言的可达项集的正则性的可判定性。这一结果是在与平原（不一定是最内层）重写，我们证明不可判定性。我们还表明，像纯重写，最内层重写与线性和右浅TRS保持规律性。关键词：术语重写，树自动机，重写策略。介绍无限项集的有限表示在计算机科学的许多领域都很有用。为此目的的形式主义的选择取决于它的表达能力，但也取决于它的计算特性。 状态树自动机（TA）[3]是一个很好的研究形式主义表示长期的语言，由于其良好的计算性和表现力的属性。从理论和实践的角度来看，它们被用于计算机科学的许多领域。例如，对于系统或程序的分析，当配置可以用树来表示时（例如，具有并行和顺序组合运算符的并发进程），TA提供了可能在有限集合中的配置的有限表示1adriagascon@gmail.com，ggodoy@lsi.upc.edu，florent. lsv.ens-cachan.fr2前两名作者由西班牙教育和科学部支持FORMALISM项目（TIN 2007 -66523）和LOGICTOOLS-2项目（TIN 2007 -68093-C 02 -01）1571-0661/© 2009 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2009.03.03324A. Gascón等人/理论计算机科学电子笔记237（2009）23→RRR±R项重写（Term rewriting）是一种通用的形式主义，用于通过用其他模式替换某些模式来对项进行符号求值，遵循定向方程或重写规则，在有限集中给出（项重写系统，或TRS）。简单重写有时过于笼统，在许多情况下，重写是用特定的策略来应用的，从而更好地表示系统行为。 是这种情况最内层的策略，它对应于编程语言的值计算调用，其中参数在应用函数之前被完全求值。在上述系统验证的应用中，无限状态系统中的转换通常可以由重写规则表示关于TA和重写之间的联系已经有很多研究，而这个领域的一个中心属性是规则性的保持。它指出，对于任何给定的正则语言L（这意味着L被TA接受），由TRS从L可达的项的集合，记为（L）也是正则的。正则性的保持已经被广泛研究。这种类型的第一个结果是正则性的保持对每个基TRS都成立，如[17]所示。在[15]中，这个属性被建立用于线性（变量在规则的每个左手边和右手边最多出现一次）和右手边（规则的右手边的高度为0或1）TRS。这一结果有几个扩展，例如。[6，11，14，16，5]和[14]表示突破，因为左线性条件（TRS规则左侧的线性）被丢弃。然而，在所有上述情况下，右线性的条件仍然是必要的，事实上，像g（x）f（x，x）这样的重写规则并不保持正则性。此外，除了在[5]中考虑了自底向上策略之外，在这些作品中只考虑了纯重写;（据我们所知）没有研究最内层策略下的正则性保持这项工作的目的是研究最内层重写的正则性保持，并确定一类TRS，可以找到更好的结果，而不是简单的重写。我们考虑浅（所有变量都发生在深度0或1的规则）TRS类。 尽管浅的情况似乎是限制性的，对于纯重写，浅的TRS不保持规则性。此外，TRS的几个有趣属性，如可达性、可连接性、连续性[13]和终止性[9]，对于浅TRS是不可判定的，而添加某些线性限制允许所有这些问题的可判定性[14，16，10，9]。 因此，从理论的角度来看，浅的情况下，当人们考虑由句法限制定义的TRS类时，可判定性的边界。我们的主要结果（定理4.9，4.2节）是，给定一个正则语言， L和浅TRS 在最内层策略下，L的可达项集R（L）由扩展的树自动机来识别，树自动机在状态转移中加入了兄弟之间的相等和不等约束.这种自动机，我们称之为BTTA，是在[2]中作为TA的扩展而引入的，它也具有良好的封闭性和可判定性，但比标准TA具有最差的复杂性。这与纯重写的情况相反：R（L）（使用纯重写的R从L可达的项的集合）通常既不是A. Gascón等人/理论计算机科学电子笔记237（2009）2325R±RRR在相同的假设下，TA也不是BTTA语言（命题3.2，第3节）。一个经典的技术证明结果的保持规律性包括添加过渡到自动机识别的起始语言L，为了模拟规则的应用程序，并认识到所有的条款也可从L。显然，这种完井技术对标准TA（在迄今为止引用的所有规则性保存结果中）效果良好，但对一般的浅层TRS不起作用。最内部的重写不能通过TA转换来模拟，尽管它几乎以自下而上的方式操作浅TRS [5]。的原因从该文件的其他两个结果如下• 首先，我们证明了在TRS（TRS的所有规则的左手边和右手边的深度最多为1）处使用最小值的最内层重写不保持正则性（命题4.2，第4节）。因此，我们需要考虑BTTA而不是标准TA。• 第二，TRS和线性TRS都不能识别BTTA（提议4.3，第4.1节）。因此，在这种情况下，TA完成无法工作。主要结果分两步得到。首先，我们减少了问题的可达条款从一个正规的集合，可达条款从一个常数。接下来，我们给出了一个直接的BTTA的建设，从一个常数识别可达的条款。它基于[8]中引入的使用约束项的可达项集的表示。作为主要结果的直接结果，我们从[1]中得到，给定正则语言L和浅TRS，，在最内层重写的情况下（L）是否正则是可判定的。相反，我们证明了当考虑纯重写时，正则性的不可判定性。另一个肯定的结果（定理5.2，5.1节）是，像纯重写一样，使用线性和右浅TRS的最内层重写保留了正则语言。这个结果是在[12]中独立得到的。 在我们的案例中，例如[15，11]的TA完成技术的非平凡适应。 的案件简单的和最深处的重写在本质上是不同的，需要介绍一些微妙的区别。我们特别表明，即使TA完成允许建立，右线性和右-在TRS（即当左手边的规则可能不是线性的）保持正则语言下纯重写，我们表明，这一性质不再是真实的下最内层重写（命题5.3，第5.2节）。这篇论文的长版本可作为研究报告[7]。第1章我们使用来自术语重写文献[4]的标准符号签名符号是一组有限的函数符号我们把m元的函数符号的子集写成m元。给定一个无穷多个变量的集合V，在V和V上建立的项的集合记为T（V， V），基项的子集记为T（V）。出现在项t∈T（n， V）中的变量的集合记为vars（t）。一26A. Gascón等人/理论计算机科学电子笔记237（2009）23..|→∈ R|{||∈}| |FVR−R−−→±RR±±RR→∈∈→→⊆一F. q1x1，.，qmxm→.）−→符号NF<$（s）和NF±（s）（其中s∈ T（F， V））分别为R（ {s}）NFR和--置换σ是从V到T（Σ， V）的映射。 一个代换σ的应用记为σ（t），是σ到T（V， V）的同态扩张一个项t像往常一样从它的位置集合（正整数串）Pos（t）到符号和的函数中识别出来。我们注意到空字符串（根位置）。位置p的长度表示为p，也称为深度。项t的高度，记为h（t），是p pPos（t）的最大值。 t在位置p处的子项记为tp，在t中用u替换位置p处的子项记为t[u]p。签名环上的项重写系统（TRS）是重写规则l → r的有限集合，其中l∈ T（n，V）\ V（称为规则的左侧），r ∈ T（n，vars（l））（称为规则的右侧）。如果存在重写规则l r使得sp = σ（l）和t = s [ σ（r）] p，则项s∈ T（V，V）通过在s的位置p处的TRS重写为t，其中替换为σ，记为s，p，σt（在该记法中p和σ可以省略）。在这种情况下，s被称为可约的。不可约项的集合，也称为R-正规形，记为NFR。传递闭包和响应闭包所以，R的值记为−−R→。 Gi venLT（t），我们注意R（L）={t|s∈L，s−−n→t}。的上面的重写步骤R被称为最内层，如果s的所有真子项|p是R-正态的EURRforms. 在这种情况下，我们写s−−→t，并且−−→表示该关系的传递闭包和恢复闭包，并且R（L）表示{t|s∈L，s−−→t}。我们亦会使用R±（{s}）NFR.TRS被称为线性（或右线性，左线性），如果每个变量在每个项中最多出现一次（分别为右手边，左手边）的规则。这是一个很浅的名字（resp）。右浅，左浅），如果变量出现在深度0或1的条款（分别）。在右手边，在左手边）的规则和killat（分别）。右-右，左-右），如果条款（分别）。右手边、左手边）的高度最多为1。如果r是一个变量，则规则lr被称为collapsing。2兄弟约束树自动机签名上的树自动机（TA）是元组（Q，Qf，Δ），其中Q是与签名不相交的零值状态符号的有限集合，QfQ是最终状态的子集，并且Δ是以下形式的基本重写规则的集合：qm）q，或q1q（ε-跃迁），其中f≠ m，且q1，.，qm，qQ（q称为规则的目标状态）。Bogaert-Tison树自动机（BTTA，或兄弟之间具有约束的树自动机）的定义类似于TA，只是它的状态是一元的，并且它的转换是以下形式的约束重写规则（ ）（）qf（x1，.，xm） c，或ε-跃迁q1（x1）q（x1）， 其中x1，.，xm是指 着色变量和约束c是等式xi= xj的布尔组合。等价地，约束c可以被定义为1，...，m具有与如下等式的合取相同的含义：对于索引i，j，等式xi = x j，使得i≠Pj，以及对于索引i，j，等式xi/=xj，使得i/≠Pj。去吧RA. Gascón等人/理论计算机科学电子笔记237（2009）2327∗AAA ∈A{a，f }fA ∈ TqAt t−−→qtLAAΔ.联系我们 →−−−→AAA∈Bf−→.{gx→fx，x}BRBΣ{}R使用[2，3]的符号，a bove转变被写为f（q1， . ，qm）−→cq（或f（q1，.，qm）→ q（当c为真时）和q1→ q，以及每个等式xi= xj（分别为约束c中的不等性xixj）写为i=j（resp.i j）。 注意每个TA都是BTTA的特殊情况，其约束都等于真。语言L（，q）是在状态by中接受的基础项的集合，即使得（）的项 的语言（） 是q QfL（，q），一组基项称为正则（或BT-regular）如果是一种语言的语言（或 BTTA）。例2.1下面的BTTA识别出了一组Bin的完全二叉树，其内部节点标记为，叶子标记为：q，q，aq，f（q，q）1=2q。 众所周知， 不是普通的。QBTTA被称为确定性（deterministic）。 如果对于每个项t，（），thereis at most（resp.至少）一个状态q，使得t L（，q）。如果是决定性的和完备的，则这个唯一的状态表示为 （t）。 A BTTA 如果它不包含非线性转换，则被归一化，转换中的约束使用划分来定义，并且对于具有元数m的每个函数符号f，状态q1，...，qm与分拆{1， . ，m}，A包含形式为f（q1， . ，qm）−P→q. 一规范化的BTTA A是确定性的和完整的，并且任何BTTA都可以被转换成识别相同语言的规范化的BTTA。如果A是正规化的，我们写A（t，P），对于一个t∈ T（Q），来表示唯一的状态q，t-P→q是A的跃迁。BT T A对于表示正常的某些类型的TRS的形式，如TRS的TRS，参见例如 [3]的第11段。引理2.2 [3]设R是一个在TRS上的R。 存在一个标准化的BTTA B =（QB，Qf，Δ B），它识别基R-正规形的集合. 此外|QB\QB|= 1。证据B =（QB，QB\{qreject}， ΔB）的构造如下。它的状态集QB是{qc|c ∈<$0}<${q，qreject}其中除q reject外的所有状态都是接受状态。它的规则集ΔB包含：• 规则c→qc对于每个常数c是R-正规形。• 规则c→q拒绝每个不是R-正规形的常数c• 规则 f（q1，. qm）cq拒绝，使得某个qiq拒绝，c为真，或者每个qi为与q拒绝不同，c是f（l1，.，lm）→r∈R，<$1≤i≤mli∈<$0<$qi=q<$i 1≤−P→ <$S，q<$e是规则在AR（t）的最后一次应用跃迁中发射。然后，它保持i<$Pji <$ti= tj。给出了S={d∈φ0}的两个包含|d−−R±→t}分离。方向 设c∈S. 通过构造AR，存在约束项f（α1，...，αm）|C ∈（rc<$rc），其中上述条件i和ii成立。设σ是定义域变量（f（α1，…，αm）），其中σ（αi）：=ti。替换σ定义得很好：如果对于不同的i和j，我们有αi= αj∈ V，通过条件ii，它意味着i<$Pj，然后ti= tj。它认为每个这样的σ（αi）都是非常数正规形，因为由于条件i，αi∈ V蕴涵qi=B（ti）∈ Q1.此外，σ（αi）是从C（αi）可达的，因为αi∈ V从条件i蕴涵C（αi）<$Si，且Si={d∈<$0|d−−→ti}y归纳hy理论。总之，可以得出σ（f（α1，...，αm））是f（α1，...，αm）C（rcrc）。 我们知道f（α1，. αm）Crc或f（α1，...， αm）Crcrc。一方面，如果f（α1，…，αm）Crc则由条件a，cσ（f（α1，.，αm））。另一方面，在一项研究中， 如果f（α1，...，αm）Crcrc则条件ii意味着（f（q1，.，qm），P）Q1，因此q Q1和t是非常数正规形。而且，αi为每一个人这些常数α i已知αi∈Si，因此也有veαi−−R±→ti。但由于这个αi是一个标准形式，因此αi= ti。 这意味着σ（f（α1，...，αm））= t，因此，t是一个非常数的正规形，它是f（α1， .. ，αm）|C∈rc，by条件b，c−−R±→σ（f（α1， . ，αm））。因此，它表明，σ（f（α1， … ，αm））−−R±→t，以便得出结论。根据σ的定义，项σ（f（α1，…，αm））和t只能在i，则αi为常数。但在这种情况下，我们知道αi∈Si，并使用Si={d∈φ0|d−−R±→ti}则得到αi−−R±→ti。因此，σ（f（α1， … ，αm））−−R±→tfollowows.方向设c是这样的，使得c t。 由于t不是常数，因此可以通过将位置Λ处的最后重写步骤显式地写为（>Λ表示除Λ之外的任何位置c−−R±→−R−−，Λ→ f（s1， . ，sm）−R−−，±>−Λ→ t=f（t1， . 、tm）因此，存在（子）派生siti。项s= f（s1，...，sm）是弱正规形，因此，通过条件c，存在约束项uCrc使得s是uC的实例。在这一点上，要么存在这样一个形式为f（α1，...， αm），或者满足这个条件的每个u都是一个变量。 在第二种情况下，s必然是规范形式，因此，通过条件d，存在约束项f（α1，...，αm）|C在rc中，使得s是f（α1，...，αm）|C.为了证明c∈S，可以证明条件i和ii成立。34A. Gascón等人/理论计算机科学电子笔记237（2009）23±R±RB∈|\±R∈RAR rr±±R联系我们 --∈∗R如果某个αi是一个常数，那么它与si重合，其中R-到达ti。以来Si={d∈N0|d−−→ti}，它必然包含αi。如果某个αi是一个变量，则si与ti重合，并且是从C（α i）可达的非常数正规形。因此，qi=B（ti）在Q1中，并且再次由于Si={d∈φ0|d−−→ti}，它必然包含C（αi）。如果αi=αj∈ V，则si=sj，并且由于两者都是标准形式，我们也有ti=tj，由此得出i<$Pj在f（α1，...，αm）C属于rcrc，f（s1，...，sm）是一个非常数正规形。因此，q=（f（q1，...，qm），P）Q1和所有常数αi也是标准形.Q在TRS上给定一个以及正则集L，BTTA Rc（对应于C相关如引理4.4），仅限于认识到，（L）通过标记为接受状态对S，q使得c S，根据引理4.4和4.8。与TRS上的简化假设一起，这允许结束定理4.9的证明。定理4.9当L是正则的且R是浅的时，R ±（L）是BT-正则的。地面可达性（一个给定的地面项t从另一个给定的地面项s可达吗？）和可连接性（是否存在从两个给定的基项s和t可达的项u？）”[13]“不，不。当他们被应用最内层的策略时，他们变得可判定[8]。我们在这里可以把这个性质表示为定理4.9的推论。推论4.10对于具有浅TRS的最内层重写，基可达性和可连接性是可判定的。证据 当限制为最内层重写时，t可从sit到达（s）。 以来S是正则语言，当s是基时，（s）是BT-正则的定理4.9因此，地面可达性归结为BTTA的成员问题，这是可判定的。类似地，s和t是可连接的i <$R±（{s}）<$R±（{t}）<$。根据定理4.9，通过对BT语言在布尔运算下的闭包的研究[2，3]，我们得到了BTTA的地可连接性到空性问题的一个约化，它也是可判定的。 Q在[1]中，显示了BTTA的规律性的可判定性。将这个结果与定理4.9相结合，我们得到下列推论。推论4.11给定一个正则语言L和一个浅TRS R，R ±（L）是否正则是可判定的。当 我 们 处 理 纯 重 写 时 ， 这 个 结 果 不 成 立 。在 [13] 中 ， 通 过 将 Postcorrespondence问题i n简化为0 − − n → 1，证明了可达性对于可达的TRS是不可判定的。我们应该考虑如何将Rin推广到R0因此，R<$0（0）是正则i<$0−−R→1。A. Gascón等人/理论计算机科学电子笔记237（2009）2335−−R→--RR −−→12RT {} R R R−−→R<$R<$RT<${}12RR±±R±R−−→→定理4.12给定一个正则语言L和一个在TRS R上的子空间，R ∈ R（L）是否正则是不可判定的。证据 在[13]中，通过将PCP实例P约简为签名上的TRSR，证明了对于可达TRS，可达性是不可判定的， 0、 1个 使得P有解i = 0，i = 1。 [13]中的约化也满足了，如果P无解，则0不会正确地到达任何包含1的项或任何包含0的项。这种简化可以通过向当前签名i添加新的符号{f，h，g，a，b，c}来修改，并向R添加两组新的规则：R 1={0 → f（a，b），a → g（a），b → g（b），a → c，b → c，f（x，x）→ h（x，x）}和R 2包含所有必要的规则，以使第2（1）至be（f、h、a、b、c）。 规则确保（）<$（0）是非正则语言，除非0< $1。注意，如果P有解，则0∗ 1，因此（）（0）是（R）f，h，a，b，c），其中ch是正则的。与Re相同，如果P无解，则0doo不包含任何项1，也不包含0正确，因此（R <$R1<$R2）<$（0）<$T（{h，c}）是集合{h（gn（c），gn（c））|n> 0}，这是不规则的。Q5最内层重写和右浅TRS在这一节中，我们研究了正则语言在最内层重写下的闭包，其中TRS规则的右手边是浅的。我们证明了用线性右浅TRS进行最内层重写可以保持正则性（5.1小节），但用右（线性和非左线性）TRS进行最内层重写则不能（5.2小节）。第一个结果也在[12]中得到独立证明5.1TA语言与线性和右浅TRS首先，我们观察到每个右浅TRS R可以在TRSRJ（在扩展签名上）变换为右浅TRSR j，使得对于所有s，t∈T（k），s−−→ti ∈sJ t. 这个想法是添加一个新的常量cr和一个规则crr代表每一个理由的规则的右侧的真子项r ，并在所有的右手边。这种转换保留了原始签名项设A =（Q，Qf，Δ）是树语言L上的确定完备TA，R是TRS上的线性右-TA.对于所有c∈ φ0，我们将Q的唯一状态记为qc，使得c→qc∈ Δ。我们还假设wlog，L（A，qc）