TRS的可达性、规范化和需要性的不可判定逼近

RS表示的传递自反闭包理论计算机科学电子笔记124（2005）51-63www.elsevier.com/locate/entcsTRS的一些不可判定逼近耶罗恩·凯特马计算机科学系阿姆斯特丹自由大学理学院De Boelelaan 1081a，1081 HV Amsterdam，荷兰摘要在本文中，我们研究的可达性，规范化，和needededness在n-浅和n-增长的TRS的判定。在n增长的TRS中，在重写规则的左侧和右侧都出现的变量必须在左侧的深度n处，并且在右侧的深度大于n。在n-浅TRS中，在重写规则的左侧和右侧都出现的变量必须在两侧的深度n处n-生长和n-浅TRS是Jacquemard和Comon介绍的生长和浅TRS的推广对于浅的和不断增长的TRS的可达性，规范化，和（在正交的情况下）needededness是可判定的。然而，正如我们所展示的，这些结果并不能推广到n-增长和n-浅TRS。因此，在n-增长或n-浅TRS中，不存在执行所需约简策略的算法.关键词：近似，不可判定性，可达性，规范化，需要性。1介绍众所周知，给定任意项重写系统（TRS），以下问题是不可判定的[10]。• 可达性：一个术语可以从另一个术语到达吗？• 规范化：一个术语是否有规范形式？• 需要：术语中的redex是否需要？然而，对于某些类别的TRS，这些属性是可判定的。这些类通常用作近似值。 也就是说，设R和S是TRS在相同的签名上，则S是R的近似，如果→R→R，并且NFR=NFS。 在这里，→俄.西然后，1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.02452J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51∈TV不R和S的重写关系，NFR和NFS表示R和S的标准形的集合。对于大多数类，其中可达性，规范化和需要性是可判定的，重写规则的形式受到限制[3，1，4，9]。此外，给定需求的可判定性，对于正交TRS存在执行所需约简策略的算法[3，2，1，4]。为了探索边界的可达性，规范化，和needededness的可判定性，我们在本文中介绍了n-增长和n-浅TRS。这些TRS是Jacquemard [4]和Comon[1]分别介绍的生长型TRS和浅层TRS的概括。虽然可达性，规范化，和（在正交的情况下）的需要是可决定的增长和浅TRS，我们表明，这并不适用于我们的概括。n-增长和n-浅TRS与其他四类TRS密切相关，已知可达性、规范化和需要性是不可判定的[4，5，6]。我们证明了n-增长和n-浅TRS是不同的，除了在一个实例中，从这些类。我们按以下步骤进行。在第二节中，我们给出了一些初步的定义。然后，在第3节中，我们定义了波斯特对应问题（PCP）的两个变体在第4节和第5节中，我们将这些变体编码为TRS，以表明可达性、规范化和需要性对于n-增长和n-浅TRS是不可判定的在第6节中，我们将n-增长和n-浅TRS与其他四类TRS进行了比较，其中可达性，规范化和需要性是不可判定的。最后，在第7节中，我们给出了进一步研究的方向。2预赛在本文中，我们假设N是非负整数的集合。我们将集合U和V的不交并表示为U V。我们用Γ表示任意字母表。这里，Γ和Γ+表示Γ上的有限弦和有限非空弦的集合，表示空弦，并且如果s∈ Γ，则|S|表示s的长度。如果s，t∈Γπ，则s·t表示s和t的级联。空字符串是连接的中性元素。如果a∈Γ且n∈N，则a0=n，an+1=a·an.通过er（x，X）我们表示签名x上的项集合，变量X的集合。如果ter（x，X），则ar（t）表示变量集发生在测试中。 我们称t为线性的，当每个变量最多出现一次，t.此外，我们混淆了只由一元函数符号和字母组成的签名。因此，给定一元函数符号f和n∈N，我们有J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5153R→R∈ Tf0（x）=x和fn+1（x）=f（fn（x））.我们用Pos（t）<$N<$来表示项t∈ Ter（x，X）的位置集。 在p∈Pos（t）处的子项的深度为|p|.如果t是线性的，则每个x∈ Var（t）都有唯一的深度，我们记为dt（x）。我们用=（R，R）表示一个项重写系统（TRS），它的符号性质为R，重写规则集为R.R的元素表示为l→r。在近似的研究中，我们通常只需要l/∈X，而不需要Var（r）<$Var（l）。→的传递自反闭包记为→。规则l→r称为线性的，如果l和r是线性的。让=（R，R）是TRS且s，ter（λ，X）.项t从s可达，如果s不客气。 此外，如果s有正规形式，则s正规化。 % s中的redex当s有一个正规形时，在从s到正规形的每一个约简中，通过收缩重叠的redex来消除redex的后代[10，定义9.2.1]。一个必要的减少策略在每一个术语中消除了一个必要的redex。3Post对应问题的两个变形在这一节中，我们将介绍Post对应问题（PCP）和该问题的两个变体。在定义中，我们使用以下符号。定义3.1设s∈Γ+。给定n∈N，定义s[n]为：•当s=a且a∈Γ时，s[n]=an• s[n]=an·t[n]当s=a·t且a∈Γ且t∈ Γ+.请注意，这不是取幂，取幂定义为s0=1，sn+1=1。s·sn. 假设Γ={a，b}，我们有（ab）[2]=aabb，而（ab）2=abab。接下来，我们定义三种配对，就像PCP及其两种变体的定义一样。定义3.2设u，v∈Γ+，n为自然数。• 对（u，v）称为PCP对。• 对（u[n]，v[n]）称为n-PCP对.• 对（u[n]·e[kn]，v[n]·e[ln]）被称为填充n-PCP对，当·k = max {|u|、|v|} − |u|、·l = max {|u|、|v|} − |v|得双曲正弦值.·e/∈r。填充n-PCP对背后的直觉是，它是一个n-PCP对，其中最短的字符串用e个符号填充这将使两个字符串54J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51--····∈/∈·→··→·两人的长度相同。对于任何填充的n-PCP对（u[n]·e[kn]，v[n]·e[ln]）n（|u|+k）= |u[n]·e[kn]|=的|v[n]·e[ln]|= n（|v|+ l）”[10]“以”“以”“以（u[n]·e[kn]，v[n]·e[ln]）[e：=n] =（u[n]，v[n]），这是一个n-PCP对。因此，我们可以将e视为空字符串的占位符。我们现在定义PCP及其两种变体。问题3.3（PCP）设P是PCP对的有限集合。是否存在一个m≥ 1使得u1·. ·u m= v1·. ·v m，其中（u i，v i）∈ P，对所有1 ≤ i ≤ m？问题3.4（n-PCP）设P是n个PCP对的有限集合.是否存在m≥ 1使得u1·. ·u m=v1·. ·v m，其中（u i，v i）∈P，对所有1 ≤i≤ m？问题3.5（Padded n-PCP）设e/∈ Γ，P是Padded n-PCP对的有限集合.是否存在m≥ 1使得（u1·. ·u m）[e：=m] =（v1·. ·v m）[e：=π]，其中（u i，v i）∈P对所有1 ≤i≤ m？PCP和它的两个变体可以相互转化，因为每种配对都存在一个与其他每种配对“相关”的例如，再次假设r =a，b，对于PCP对（a，ab），（a[n]，（ab）[n]）是“相关的”n-PCP对，并且（（ae）[ n ]，（ab）[ n ]）是“相关的这导致了下面的定理。定理3.6当n ≥ 1时，PCP，n-PCP和填充n-PCP可相互约化.使用前面描述的“相关”对，这直接从PCP，n-PCP和填充n-PCP的定义中Q根据前面的定理和PCP [8]的不可判定性，我们有以下结果。推论3.7n-PCP和填充的 n-PCP问题是不可判定的，n≥ 1。对于填充的n-PCP，注意，如果（u1·.. ·u m）[e：= m]=（v1·. ·vm）[e：= n]，则在u1·.中e出现的次数必须相等。 ·u m和v1·.. ·v m。如果 不 是 ， 则 （ u1. u m ） [e ： = 0]和 （ v1. [2019 - 05 - 19 00 ： 01 ：00][2019 - 01：00][2019 - 01使用前面的事实并假设字符串重写系统（SRS），对于所有a Γ和eΓ，重写规则a e e a和e一 一 e，我们可以换个说法填充的n-PCP.J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5155问题3.8（填充n-PCP）设P = Γ {e}，P是填充n-PCP对的有限集合。 是否存在一个m ≥ 1且一个s ∈ n+使得u1·.. ·u m→s和v1·. ·v m→εs，其中（u i，v i）∈P，对所有的1 ≤i≤ m？4不可判定n增长项重写系统在本节中，我们描述了第一类TRS，对于这些TRS，可达性、规范化和需求性是不可判定的。类的定义如下。定义4.1设l→r为重写规则。 当它是线性的并且对所有x∈Var（l）<$Var（r）成立dl（x）=n和dr（x）> n时，该规则是n增长的. 当一个TRS的重写规则都是n增长的时，它就是n增长的观察到在n增长的TRS中，我们限制重写规则的形式。此外，注意到n增长重写规则和TRS与以下重写规则和TRS密切相关，如Jacquemard[4，定义4]所定义定义4.2设l→r为重写规则。规则正在增长，是线性的，当对所有x∈Var（l）<$Var（r）成立时，dl（x）= 1且dr（x）∈N.当所有重写规则都在增长时，TRS也在增长显然，对于n= 1，n个增长的TRS形成增长的TRS的子类。然而，对于n >1，情况并非如此。例如，我们有n增长重写规则fn（x）→ fn+1（x）.对于n>1，这个重写规则不会增长，因为dfn（x）（x）=n> 1。增长的TRS不形成针对任何目标的n个增长的TRS的子类n.例如，不断增长的重写规则f（x）→ x.这个重写规则不是n增长的，因为dx（x）= 0。使用树自动机技术，Jacquemard [4]证明了可达性和规范化对于不断增长的TRS是可判定的。 杜兰德和米德尔多普[2]证明了正交增长TRS的需要性是可判定的。由于每个1-增长的TRS是增长的，我们也有可达性，规范化，和（在正交的情况下）需要1-增长的TRS的可判定然而，正如我们接下来所展示的，这些结果并不能推广到n>1的n增长TRS定理4.3设n ≥ 1. 对于n +1增长的TRS，可达性是不可判定的。证明我们在n+1增长的TRS中将n-PCP降为可达性假设我们有一个n-PCP对的有限集合P定义签名r = r{c，d，f，g，h}。56J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51≥····具体如下• c和d是常数，• g、h和Γ的元素具有元数1，并且• f具有arity 2。对于所有（u，v）∈P和a∈Γ，定义以下重写规则（一）（二）（三）（四）（五）（六）c→f（gn（u（ d ） ） ， gn （ v （ d ） f （ gn（ x ） ， gn （ y ） ） →f （ gn （ u（ x ） ） ， gn （ v （ y ） f （ gn（ x ） ， gn （ y ） ） →hn+1 （ f（x，y））f （ an （ x ） ， an （ y ） ）→hn+1 （ f （ x ，y））f（d，d）→dhn+1（d）→d很容易看出，我们有有限个n+ 1增长的重写规则。因此，重写规则形成n+1增长的TRS。对于TRS，当且仅当n-PCP有P的解时，d从c可达。为了证明当n-PCP有P的解时d是从c可达的，假设u1. u m= v1. m是一个解。我们现在可以构建约简序列c→（1）f（gn（um（d）），gn（vm（d）））→f（2）f（gn（u1·. . . ·um（d）），gn（v1·. . ·vm（d）n+1个→（3）h（f（u1·... ·u m（d），v1·. ·v m（d）作为u1·. ·u m= v1·. ·v m，对于某个k，我们可以扩展约简序列到c→ n+1（f（u1·... ·u m（d），v1·. ·vm（d）→n（4）hk（n+1）（f（d，d））k（n+1）→（5）hJ. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5157········→β（6）d（d）其他事项因此，d可以从c到达。要看到当d从c可达时n-PCP有P的解，请注意，将c减少到d的唯一方法是首先执行（1）步和若干（2）步，然后执行（3）步和若干（4）步，最后执行（5）步和若干（6）步。还要注意，当（1）-步骤和（ 2 ） - 步 骤 给 我 们 一 个 项f （ g n （ u1. u m （ d ） ） ， g n （ v1.. v m（d））），其中u1... u m=v1. v m。也就是说，当n-PCP对P有解时.因此，在n+ 1增长的TRS中，n-PCP可归结为一个可达性问题.由于n-PCP对n≥1是不可判定的，所以n+1-增长58J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51≥TRS，n≥1。Q在前面的证明中观察到，如果我们假设n= 0，那么重写规则f（an（x），an（y））→hn+1（f（x，y））坍缩为f（x，y）→ h n+1（f（x，y））.因此，d不再是从c可到达的。这样的事情是可以预期的，因为对于1增长的TRS，可达性是可判定的我们现在将上述结果扩展到正常化和需求。定理4.4设n为1.对于n+1增长的TRS，归一化是不可判定的。证明我们减少了n-PCP的正规化，在n+1增长的TRS采用的证据表明，n-PCP是可还原的可注意，添加n+1增长重写规则(7)hn+1（x）→hn+1（hn+1（x））从定理4.3的证明到TRS并没有改变d从c可达当且仅当n-PCP有P的解。然而，通过添加规则，如果d是从c可达的，则d成为c的唯一可能的范式。通过这个事实，以及d从c可达当且仅当n-PCP有P的解，我们得到c有标准形当且仅当n-PCP有P的解。因此，在n+ 1增长的TRS中，n-PCP可归约为归一化.由于n-PCP对于n≥1是不可判定的，因此对于n≥1的n+ 1-增长TRS的归一化也是不可判定的。Q定理4.5设n ≥ 1. 对于n +1增长的TRS，需要性是不可判定的。证明假设我们有一个n+ 1增长的TRS，常数为c1，c2，c3，常数为d1，d2，一些重写规则的左手边为 c1， c2， c3。我们可以将Gustave的TRS [ 10，Example 9.2.35]的n+1增长重写规则添加到这个n +1增长TRS中f（d1，d2，x）→ef（x，d1，d2）→ef（d2，x，d1）→e这里，f是新鲜函数符号，c是新鲜常数。如果我们现在考虑f（c1，c2，c3）项，那么我们不能决定需要当前三个赎回中的哪一个。它要求我们知道对于所有1≤i≤ 3，如果J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5159∈ V <$Vd1和d2是从ci可达的，而n+1-增长的可达性是定理4.3不可判定的.因此，需要是不可判定的。Q作为前面定理的结果，我们有，没有算法存在，执行所需的减少策略，在n+ 1-增长的TRS，其中n≥1。5不可判定n-浅项重写系统在这一节中，我们描述了第二类TRS，其中可达性，规范化和需要性是不可判定的。类的定义如下。定义5.1设l → r为重写规则。 当它是线性的并且对所有xar（l）ar（r）成立dl（x）=dr（x）=n。当一个TRS的重写规则都是n浅的时，它就是n浅的我们可以看到，与n-增长的TRS一样，n-浅TRS的重写规则形式也有限制. n-浅TRS既不形成n-增长TRS的子类，也不形成n-增长TRS的超类例如，考虑n浅重写规则fn（x）→ f n（x）.这个重写规则不是n增长的，因为dfn（x）（x）=dfn（x）（x）。 我们也有n增长重写规则fn（x）→ fn+1（x）.这个重写规则不是n浅的，如dfn（x）（x）1，情况并非如此。例如，再次考虑n浅重写规则fn（x）→ f n（x）.对于n>1，这个重写规则并不肤浅，因为dfn（x）（x）=dfn（x）（x）=n>1。浅TRS不形成针对任何浅TRS的 n个浅TRS的子类n.这遵循相同的示例，该示例示出了对于任何n，增长的TRS不形成n个增长的TRS的子类。利用树自动机技术，Comon [1]证明了浅TRS的可达性和规范化是可判定的杜兰德和米德尔多普[2]60J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51∈|||∈ ∈ |∈∈≥∈··→··→证明了正交浅TRS的需要性是可判定的。由于每个1-浅TRS是浅的，我们也有可达性，规范化，和（在正交的情况下）需要1-浅TRS的判定。然而，正如我们接下来所展示的，这些结果不能推广到n>1的n-浅TRS在下面的证明中，我们用[a，b]表示一元函数符号，a，b∈π = Γ{e}. 我们还使用以下定义。定义5.3设u，v∈ +，其中u=v。 对于a，b∈u，uJ，vJ∈ +，定义[u，v]（x）为：• [u，v]（x）=[a，b]（x），如果u=a且v=b，并且• [u，v]（x）=[a，b]（[uJ，vJ]（x））如果u=a·uJ且v=b·vJ.定理5.4设n ≥ 1. 对于n +1-浅TRS，可达性是不可判定的。证明我们减少填充n+1-PCP的可达性在一个n+1-浅TRS。假设我们有一个填充n+ 1-PCP对的有限集合P和一个e/∈Γ。让n = r{e}。定 义 签名<$={[a，b] |a，b∈n}{c，d}，其中每个[a，b]是一元函数符号和c，d个常数。 还定义了所有（u，v）∈ P和a∈P的重写规则，（一）（二）（三）c→[u，v]（c）[a，a]（c）→d[a，a]（d）→d最后，定义所有u，uJ，v，vJ∈n+，其中u[e：=n]=uJ[e：=n]，v[e：=n]=vJ [e：= n]，以及|u|=的|uJ|=的|v|=的|VJ|= n +1以下重写规则(4)[u，v]（x）→[uJ，vJ]（x）这最后一条重写规则可以看作是对字符串的一系列应用在问题3.8之前给出的重写规则的u和v。很容易看出，我们有有限个n+ 1浅重写规则。因此，重写规则形成n+1浅TRS。通过n1，我们有对于TRS，d是从c可达的当且仅当填充n+ 1-PCP有P的解。为了证明当填充的n +1-PCP有P的解时，d是从c可达的，假设对于某个sn+，我们有u1。. u ms和v1.. . v ms。也就是说，填充n+1-PCP有P的解。我们可以构造如下的约简序列c→（1）[u1，v1]（c）→n（1）[u1·. . . ·um，v1·. . . ·vm]（c）作为u1·. . . ·um→vs和v1·. . . ·vm→vs，我们可以推广r导出序列J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5161到62J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51∈≥≥··→·· →| ||≤|≤c→C[u1·. ·um，v1·.. ·vm]（c）→δ（4）[s，s]（c）→（2）......→β（3）d因此，d可以从c到达。要看到当d从c可达时n-PCP有P的解，请注意，将c减少到d的唯一方法是首先执行多个（1）步骤，然后执行（2）步骤，最后执行多个（3）步骤，并将这些步骤与（4）步骤交织。还要注意的是，如果（1）步和（4）步一起给出了一个term[s，s]（c）for some u1. umdos和v1. VM一群人。即作为paddedn +1-PCP有P的解。因此，填充的n+1-PCP可简化为n+1-浅TRS中的可达性问题由于填充n+1-PCP对n≥1是不可判定的，因此对于n≥1的nQ在前面的证明中观察到，如果我们假设n= 0，那么最后一个重写规则折叠为[a，b]（x）→[a，b]（x）a，b，？ 因此，d不再是从c可到达的。 东西 这是可以预料的，因为对于1-浅TRS，可达性是可判定的注意，通过前面证明中指定的TRS，一个更强的性质成立。定理5.5设n为1. 可达性是不可判定的n +1-浅TRS中，每个重写规则有最多一个变量，出现在左手和右手的重写规则。我们现在将上述结果扩展到正常化和需求。定理5.6设n为1.对于n+1-浅TRS，归一化是不可判定的。证明我们减少填充n+ 1-PCP的归一化在一个n+1-浅TRS采用的证据表明，n+1-PCP是可还原的可注意，对于所有u，v∈n+，其中u=v n+1，（五）[u，v]（d）→[u，v]（d）从定理5.4的证明到TRS并没有改变d是从c可达的当且仅当填充n+1-PCP具有P的解的事实。然而，通过添加这些规则，如果d对于c是可达的，则项d成为唯一的J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5163→ ∈ V <$V ≤C的可能范式 通过这个事实和d从c可达当且仅当填充n+ 1-PCP有P的解的事实，我们得到c有正规形当且仅当填充n+1-PCP有P的解。因此，填充的n+1-PCP可简化为n+1-浅TRS中的归一化由于填充n+1-PCP对于n≥1是不可判定的，因此对于n≥1的n+1-浅TRS的归一化Q定理5.7设n ≥ 1. 对于n +1-浅TRS，需要性是不可判定的.证明这个证明与定理4.5的证明是等价的，但是用n+1-shallow代替了n+1-growing，用定理5.4代替了定理4.5。四点三Q作为前面定理的结果，我们有，没有算法存在，执行所需的减少策略，在n+1-浅TRS，其中n≥1。6相关工作在本节中，我们将n-增长和n-浅TRS与其他四类TRS进行比较，对于这些TRS，可达性，规范化和需要性是不可判定的[4，5，6]。我们在比较中使用以下四个重写规则。（一）（二）（三）（四）f（x，x）→g（x）f（f（x））→xfn（x，g（y））→fn+1（x）fn（x，g（y））→fn（x）注意，（1）和（2）既不是n-增长的，也不是n-浅的，并且（3）和（4）不是n-增长的，也不是n-浅的。(4)分别是n-生长和n-浅。第一个类，由Jacquemard定义[4，定理18]，要求所有Lr和xar（l）ar（r）thatdl（x）1.这个定义等同于增长的定义，只是重写规则不再需要是线性的。 因此，1-增长和1-浅TRS形成子类。对于n >1，n-增长和n-浅TRS不形成（3）和（4）的子类。此外，对于所有n，n-增长和n-浅TRS不形成由（1），这既不是n-增长也不是n-浅左手边的超类不是线性的。第二类也由Jacquemard [4，定理19]定义，要求对所有l→r和x∈ Var64J. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）51（l）<$V ar（r），或者dl（x）≤1或者dr（x）≤1，并且l→r是线性的。同样，这个定义等于增长的定义，除了在这种情况下dr（x）1也是允许的。因此，1-增长和1-浅TRS再次形成子类。对于n>1，n-增长和n-浅TRS不形成（3）和（4）的子类此外，对于所有nJ. Ketema/Electronic Notes in Theoretical Computer Science 124（2005）5165≤≤→→ ∈∪∈ V <$Vn-增长和n-浅TRS不形成（2）的超类，当dx（x）= 0时，它既不是n-增长的也不是n-浅第三类，再次由Jacquemard [5，定义1]定义，要求对所有l r，l和r的形式为f（t1，...，t k）与fX和与ti要么是一个变量或一个地面项的所有1i k。 对于所有n，n-增长和n-浅TRS不形成由（3）和（4）得到的子类此外，对于所有n，n-增长和n-浅TRS不形成由（1）得到的超类，其既不是n-增长的也不是n-浅的，因为左手边不是线性的。第四类由Jacquemard等人[6，Proposition 6.1]定义，但未在本技术报告的会议版本[7]中提出，要求重写规则具有以下形式。f1（f2（x））→g1（g2（x））f3（x）→t1t2→g3（x）t3→t4其中fi和gi是一元函数符号，ti是所有1≤i≤ 4。对于所有n，n-增长和n-浅TRS的类不形成由（3）和（4）得到的子类。此外，对于所有n/=2，n-增长和n-浅TRS不通过f1（f2（x））→g1（g2（x））形成超类. 当n= 2时，n-增长的TRS不再由f1（f2（x））g1（g2（x））构成超类，但2-浅TRS显然构成超类.因此，Jacquemard等人已经证明了可达性、规范化和需要性对于2-浅TRS是不可判定的。然而，作为重写规则的证明，定理5.4表明，甚至可以处理规则f3（x）→t1，t2→g3（x），并且仍然以可达性不可判定的类结束7进一步指示至少还有两个问题。首先，可达性、规范化和需要性对于TRS是不可判定的，其中对于每个重写规则l→r，我们对所有xar（l）ar（r）dl（x）=n且dr（x）

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