范畴文法中的k值范畴文法和Lambek文法的交的空性问题

理论计算机科学电子笔记53（2002）网址：http://www.elsevier.nl/locate/entcs/volume53.html13页k值范畴文法（古典文法和Lambek文法）语言的交的空性问题安妮·福莱特1IRISA-University of Rennes 1法国雷恩摘要本文讨论在范畴文法学习领域中出现的几类范畴文法的判定性问题。 本文证明了两种语言的交的空性对于以下类是一个不可判定的问题：k-值经典范畴文法和k-值Lambek范畴文法，对于每个正的k.1引言范畴文法在自然语言处理领域已经得到了研究，本文主要讨论[1]中介绍的经典（或基本）范畴文法和与Girard [3]介绍的线性逻辑密切相关 这些文法是词汇化的文法，它们为词汇分配类型（或类别）;当词汇中的每个符号最多分配k种类型时，它们被称为k值文法;当1值文法时，它们也被称为刚性文法。这种k值文法在最近的可学习性研究中特别有趣[6][11]。在这种情况下，重要的是要获得一个很好的理解的性质的类的语法的问题本文考虑交的空性问题，即给定两个k值范畴文法G1和G2，L（G1）和L（G2）的交是否为空？ 这个关于文法的常见问题对于范畴文法也是不可判定的，因为它们对应于上下文无关文法。我们发现这个问题仍然存在1电子邮件地址：mailto:foret@irisa.frc2002年由Elsevier Science B出版诉 在CC BY-NC-ND许可下开放访问。2不可判定的k值文法，对于任何k 1，特别是当限制到刚性文法时，即对于k= 1。这个结果特别表明这些子类不是平凡的（宽的）。我们的证明包括对Post的对应问题的2 背景2.1范畴文法在本节中，我们介绍基本定义。感兴趣的读者也可以参考[2，10，13，12]以了解更多细节。设为固定字母表。类型 类型是由Pr（原始类型集）和两个二元连接词=和n构造的。Tp表示类型的集合。Pr包含一个可区分的类型，写作t，也称为主类型。经典范畴语法。上的经典范畴文法是和T p之间的有限关系G。如果2G，我们说G把A赋给c，我们写G：c 7！ A. 我们写SubTp（G）是由G赋给中某个符号的类型的子公式的集合。记法。T p中的一系列类型可以用逗号、连接或简单的并置来写（这不应该混淆，因为我们考虑的是没有乘积类型的语法）。我的天啊。Therelation`AB 这是一个错误的关系n`betwee n Tp+和Tp，因此，对于所有A;2Tp+和所有A;B2Tp：A` A如果`A和`A n B那么;`B（反向应用）如果`B = A和`A那么;`B（正向应用）我们认为Lambek演算限制在两个二元连接词上n和=。我们给出了一个公式，该公式包含了在一个子空间的左边和右边的引入规则LambekDerivation`L. 这种关系是两个人之间的关系Tp+和Tp，对于所有2Tp+;0 2Tp和所有A;B2T p（非空）：A` A如果A;`B那么`A n B（n右）如果;A`B那么`B = A（=右）31n我如果`A和; B;0 C然后; A n B;0 `C（nlef t）if`Aand;B;0`C then;B=A;;0`C（=lef t）我们认为，切割规则由AB和L组成。语言 设G是上的经典范畴文法。G生成a串c* c2+if有类型A;：;A2Tp使得：G：c 7！Ai（1in）和A1; ：;An`ABt。G的语言是由G生成的字符串的集合，记为L（G）.在L（G）的定义中，我们用L代替AB来定义LL（G）。严格k值文法。 范畴语法最多分配字母表中每个符号的k种类型称为k值文法;1-有值文法也称为刚性文法。例2.1设1= fJohn; Mary; likesg，设Pr =ft;ng，分别表示句子和名词。设G1 约翰七号！第7章玛丽！n;喜欢7！n n（t= n）gW e get（JohnlikesMary2L（G1））since（n;nn（t =n）;n`ABt）G1是刚性（或1值）文法.2.2Post波斯特对应问题（Post设X是一个字母表（有两个或更多个字母）。Post是固定字母表上PCP的一个实例X=fa;bg. LetX0 =P r=X[f1; ：;ng [ft;#g（n个成员和#are作为特殊标志）。我们将两个语法G1D和G2D在字母表D上如下：D=fca;cb;c#g[fci;j：i2f1; ：;ng;j2f1; ：;ng [ftgg[fdi;j：i2f1; ： ：;ng;j2f1; ： ：;ng [ftgg定义3.6我们将G1D定义为以下赋值，（其中ui2fa; bg）：cacbC#七！七！七！aB#ci;jdi;j七！七！C（ iuij） C（# uij）：：ff或或我我22f1; ：f1; ：;;ng;ng;JJ22f1; ：f1; ：;;ng[ng[ftgftg我们以类似的方式定义G 2D，交换所有u i和v i的角色。命题3.7G 1D和G 2D都是刚性内射PCP-文法。实施例3.8LetD1=（ab;abbb）;（bb;b）>wegetPrD1 =fa;b;1;2;t;#gG1D1 如下：c1;1 七！C（1ab1）d1;1 七！C（#ab1）6cacbc#七！七！七！ab编号c1;2c1;tc2;1c2;2七！七！七！七！C（1ab2）C（1abt）C（2bb1）C（2bb2）d1;2d1;td2;1d2;2七！七！七！七！C（#ab2）C（#abt） C（#bb1）C（#bb2）c2;t 七！C（2bbt）d2;t 七！C（#bbt）我们观察到abbbbb允许两个分解（ab.bb.bb =abbb.b.b）71111DD0p年q1根据指数：1，2，2.该解与L（G1D1）之间的对应关系通过下面的推导来说明：w= cb cb cb cb cb cac#d1;2c2;2c2;t2 L（ G1D1）G1D （w）=bbbbba #C（#a b2）C（2b b2）C（2bb t）G1D （w） `bb bb2C（2b b2）C（2bb t）G1D （w） `bb 2C（2bb t）G1D （w）`t下面的技术命题对于描述上述文法的语言是有用的。命题3.9（类型描述）设G1D与D相关联，类型赋值为1D：(5) 如果A 21D（D）（即A是一个分配类型），则对于w 2+：1D（w）`ABA意味着1D（w）= A(6) 如果A621D（D）（即A不是赋值类型）则对于w2+：21D（w）`AB A意味着9k>09i1; ：ik2f1; ：;ng9u（可能为空）：0 01D（w）=u~u~ik1 * ：u~i1 #C（#ui1i2）：C（ik1uiK1 ik） C（ yk u A）|{z } |{z8< u=u0t}： tA= C（ tp：tq1 tq）其中y1=#，如果k >1： yk= ik证明在附录中给出;（5）是（4）的推论;（6）更技术性（使用（3）（4）（5））。3.3的对应关系我们现在描述3G1D和G2D语言（具有类型赋值图1D和2D）中所示的方法，其与PCP实例D=（ u1; v1）;：;（ un;vn）>相关联。命题3.10（语言描述）语言L（ G1D）=fw：与G1D相关的1D（ w）`AB tg可以描述如下（ L（ G2D）可以类似地描述）：4L（G1D）=fw：1D（w）=u~iku~ik1： u~i1#C（#ui1i2）：C（ik1uik1ik）C（ykuikt）;|{z}|{z}|{z}|{z}和i 1;：;i k2 f 1;：; n g;y 1=#且 如果k >1：yk=ikg2当k=1时，在一般情况下，（w）如下： （w）=u~0#C：使得9 t p：t q2 P r D（1pq）：Ik81D1DI1I1（#u0A）3证明是（2）和（6）的推论：见1996年。4 在k=1的退化情况下，（w）如下：（w）=u~ #C（#ut）1个D1个D9注意，1D（w）由两个主要的不同部分组成，它们被一个#分隔开，其左边部分没有n运算符，而其右边部分由代码类型组成预 期 的含义如下：对于PCP实例，左部分编码完整单词的书写，而右部分编码索引的序列和相应的分解。P=3.11（Simulatio）L（G1D）\L（G2D）6=;如果D是PCP 的 一个psitiveinstance.推论3.12（主要）k值范畴文法的交的空性问题对于任何k 1都是不可判定的（特别是对于刚性内射PCP-文法）。4k值Lambek文法我们对k值Lambek文法给出了类似的结果这依赖于以下属性：命题4.1设G表示PCP-文法，8t02Pr（本原）：G（w）`ABt0 iffG（w）`Lt0Corollay4.2对于PCP-grammar，L（G），相对于“AB”和LL（G）关于“Lcoincide.”推论4.3（主要）k-值Lambek范畴文法的交的空性问题对任何k都是不可判定的 1、特别是 对于刚性内射Lambek-PCP-范畴文法）。注. 这个结果似乎类似地延伸到非结合版本，但不是交换版本。这个结果显然适用于具有乘积的Lambek演算[7]（通过子公式性质和Cut消去，PCP-文法的语言对于具有或的L是相同的）。一个类似的例子也适用于L[9，5]，由一对剩余模态扩展的Lambek演算（L也享有子公式性质和割消去）。5结论本文回答了每类k值经典范畴文法和每类k值Lambek文法的一个判定性问题：两种语言交集的空性是每类的一个判定性问题 证明依赖于一个特殊的类引入这里作为PCP-文法，一个子类的单向文法，我们建立了几个属性。特别是，我们关注的问题对于这个子类是不可判定的（因此不是微不足道的）。10对于未来的工作，我们保持兴趣的封闭性，可判定性和复杂性问题的k-值范畴文法。特别是，我们离开开放的可判定性问题的包容性问题。引用[1] Y. 巴希勒语法描述的一种准算术符号Language，29：47[2] W. Buszkowski 数 学 语 言 学 和 证 明 理 论 。 在 van Benthem 和ter Meulen[14]，第12章，第683-736页。[3] 让-伊夫·吉拉德线性逻辑：它的语法和语义。 在Jean-Yves Girard，Yves Lafont和Laurent Regnier编辑的Advances in Linear Logic中，伦敦数学学会讲义第222卷，第1-42页。剑桥大学出版社，1995年。[4] John E. Hopcroft和Jeffrey Ullman。自动机理论、语言和计算导论。艾迪森·韦斯利1979年[5] 杰哈德·耶格尔论多模态范畴语法的生成能力。发表在Journal of Language andComputation，2001。[6] 金泽诚类别语法的可学类。逻辑、语言与信息研究FOLLI CSLI，1998年。由剑桥大学出版社出版[7] 约阿希姆·兰贝克句子结构的数学。美国数学月刊，65：154[8] 哈里河刘易斯和克里斯汀。帕帕迪米特里乌计算理论的基础。普伦蒂斯·霍尔1981年[9] 迈 克 尔 · 莫 特 加 特 多 模 态 语 言 推 理 。 Journal of Logic ， Language andInformation，vol.5，第3/4期，第349-385页，1996年。[10] 迈克尔·莫特加特范畴类型逻辑。在van Benthem和ter Meulen [14]，第2章，第93[11] 雅克尼古拉斯。文法推断 作为统一。 Rapport deRechercheRR-3632，INRIA，1999年。相关网站http://www.inria.fr/RRRT/publications-eng.html。[12] Mati Pentus Lambek 文 法 是 上 下 文 无 关 的 。 计 算 机 科 学 中 的 IEEEComputer Society Press，1993.[13] 这 是 我 的 生 日 。Calculdelambeketlogiquelineire.TraitementAutomatique des Schools，37（2）：39[14] J. van Benthem和A.编辑们。逻辑与语言手册北荷兰爱思唯尔，阿姆斯特丹，1997年。11AB010000A附录关于序列长度j_0的归纳证明（1）casejj=0是C（0）`C（0），这是一个公理情况j j>0，令=1;A1，其中A1是Tp的类型：~;C（;0）=A;~;C（; A;）1 1 1 1当j0j>0时，通过应用jj上的感应：~;C（;A ;）`C（A ;） 的方式1 1 1AB1|{z}=A1nC（0）由此，通过与公理（A1`ABA1）一起向后应用，：A;~;C（;A;）`C（）1 1 1 1这是我们想要的结果|{z}`ABA1nC（0）2通过对序列j的个数k的归纳证明（2）。为了便于介绍，让我们这样写：k=~k;~k1;：;~1; A1;C（A1;1; A2）;：;C（A k 1个;K1; Ak）;C（Ak;k; Ak+1）则（2）也重写到k`ABAk+1。情形k= 1是（1）的子情形，其中A2=C（A2）：~1; A1; C（A1;1; A2）`A2在k> 1的情况下，通过对k 1的归纳：k1 `ABA k，即：~K1;：;~1; A1; C（ A1;1; A2）;：;C（Ak1;k1;Ak）`ABAk|{z}|{z}用公理Ak`ABAk：5向后应用k1;C（Ak;k;Ak+1）`ABC（k;Ak+1）| {z}`ABAk|{z}=AknC（k;Ak+1）其中C（Ak+1）=Ak+1：~k; C（k; Ak+1）`AB Ak+1|{z}然后通过CUT onC（k; Ak+1）：~k;K1; C（Ak;k; Ak+1）`AB Ak+1|{z}`ABC（k;Ak+1）这是所需结果k`ABAk+16的写入25 其中C（Ak;k;Ak+1）=AknC（k;Ak+1）6 当k为空时，C（k;Ak+1）是C（Ak+1）12通过对D的一个分支的长度jDj的简单归纳证明了（3）（G记作）在（w）`ABA中的在jDj = 0的情况下，这是一个公理，其中（w）= A，因此显然w 2A 2 SubTp（G）当jDj> 0时，如果最后一个规则是前向应用：则归纳假设将导致在SubTp（G）中有=的类型，这对于PCP-文法是不可能的。case jDj> 0，如果最后一个规则是向后应用：的形式，其中（w）=;9W;W2+ ：（w）=;（w2）=：1 2 1A1和A1nA通过归纳假设，A1nA2SubTp（G）蕴涵A2SubTp（G）根据SubTp的定义2关于D的一个导子在（w）`ABA中的长度jDj的归纳法证明了（4）（G记作）在jDj = 0的情况下，这是一个公理，显然（w）= A在jDj> 0的情况下，D的最后一个规则是向后应用（如在（3）中，向前应用是不可能的），D的前因具有以下形式：A1和A1nA其中和为非空，并且;= (w);但在这种情况下，9 w1：（w1）=and by（3）：A1nA2SubTp（G）因此A是SubTp（G）中的严格右子公式，这是不可能的2（5）的证明是（4）特殊化为G1D的特殊情况，使得通过构造：如果A 21D（D）（fa;b;#g，如果是本原的），则A对于SubTp（G1D）2中的多个不是严格的t-s通过1D（w）`A的导子D的长度jDj的归纳法证明（6）;假设A621D（D）在jDj = 0的情况下，这是一个公理：1D（w）= A，这意味着w 2 D，但这是不可能的，因为A不是一个赋值类型。在jDj > 0的情况下，D的最后一个规则是向后应用，（如在（3）中，向前应用是不可能的）D的前件具有以下形式：“A1”和“A1 n Awith; =1D（w）由（3）A1nA2SubTp（G1D）和由G1D：A1的构造得到 2（PrDftg）=fa;bg [f1; ：;ng [f#g.我们现在根据A121D（D）是否成立来讨论A1亚型 21D（D）（也是本原），则A1 2 X[f#g=130：01个p我年q1K 11K 1>0fa;b;#g，通过（4）我们得到（since=1D（w1） for some prefixw1ofw）=A1- 另一方面，如果A1=#，则通过归纳假设（6）应用于“A1nA我们得到：9k>09i1; ：ik2f1; ：;ng 9u1 （可能为空）：0 0=u~1u~ik1：u~i1 y1C（y1ui1y2）： C（yk1uik1yk）C（yku1A1n A）|{z} | 8> u=u0{tz： t}ik1p年q1当9tp： tq2PrD ： 1pqy1=#;和（8i2f2; ： ：kg：yj=ij）为了便于介绍，让我们这样写：k=u~ik1 * ：u~i1 y1C（y1ui1y2）： C（yk1uik1yk）（其中1=y1）我们的|nre{wzrite}：|{z}0 0=u ~ 1k C（y k u 1 A 1n A）我们首先观察到A1=tp，且A=C（ tp+1：tq1tq），其中1p+1 q;nb yadjoiningg=A，ifeletu0 =u0A=u0t我们得到了想要的1结果如下：111个p1D（w）=;=u~kC（ yk u A）|={Az1}|A{zu~}01| {z}=C（yu0AA）=C（yu0AnA）8> uik =u0t p+1 * *t 年q1=u0t* *t 年q1哪里： 1p+ 1q- 如果A1=#，通过构造#nA2SubT p（ G1D）是一个赋值类型，并且通过（5）我们有=A1nA，因此：; =#;#nA这是一个特定的（边缘）案例，其中 A=ut（通过构造）用于D实例中的某些单元和某些初始化q。子情形A1621D（D），我们已经有A12（PrDftg）和A1nA2SubTp（ G1D）则A1是一个数，通过构造A1nA21D（D）对于形状C（ iui j），其中i2f1：：：ng;j2f1：：：ng[ftgandui fromthe given PCP-instanceD; by（4）我们得到（since=1D（w2）1114for some suff fixw2 ofw）：=A1n A另一方面，应用于A1的归纳假设给出，其中我们像前面的情况一样使用k150=u t110：1Dik1名女1名2名女0009k>09i1; ：ik2f1; ：;ng 9u1 （可能为空）：0 0=u~1k C（ yk u1A1）8>> uik001p00q01其中9t* *t2Pr：<0 0 0p0q0DA1=C（tp0 * tq01tq0）>： 1p0 q0y1=#;和（8i2f2; ： ：kg：yj=ij）A1是一个数，我们首先观察到A1=t，p= q= 1，0 0 0uik =u0;通过调整=AnA，让我们写ik+1 =yk+1 =A1，u0 =（empty），anddlett * tq2PrD 使得A=C（ t1* tq）（通过结构可获得）和（通过结构可获得）+1 =ui=t1： tq1，然后我们得到所需的结果（涉及k +1而不是k）如下：;=u~u~ikkC（ykuikyk+1）C（yk+1uA）|{=z}|=C(y{zu0A1)}|=C{（Az1A）}K 18>> uik+1 =u0t* tq1当9tp; ：tq2PrD：A=C（t1： tq1tq）> 1=pqy1=#;和（8i2f2; ： k; k+1g：yj=ij）2命题3.10的证明。 一方面，所有这样的弦w都在L（G 1D）中(ie1D（w）`AB t）：通过上述性质（2），其中Ak+1=t;A1=#;A2=i2;：;Ak=ik且j=uij，对于1jk。相反，假设w是L（G 1D）中的一个字符串，也就是说我们有1D（w）`t的演绎。通过上述性质（6）获得结果，其中A = t 62（）（且p=q，其中hu =u0）2命题3.11的证明。为了便于表示，对于索引s= i1;：ip的任何有限序列，我们写c= di1;i2 ci2;i3：：： cil;il+1：：： ci（p 1）;ip cip;t我们可以把这些语言等价地描述如下：L（G1D）=fw~0c#c< i;：i>：i1;：：if2f1： ngwith1D（w0）=uiui：：ui 2X+g* *t111160约0 0 0+L（G2D）=fw0c#c：i1;：if 0 2f1： ng;2D（w0）=vi01vi02：：vi00 2Xg1f0f如果w2 L（G）\L（G），则nreexistsi;：i;i0;：i02 f1：ngsuch1D2D的1f1f0~0w=w~0c#c= w0c#c>哪里f1f0（w）=uu：：u 和（w0）=v v：：v0 01个D0I1 i2if2D0i1i2if0这给出sc=c，这是两个顺序的决定f1f0170000000是相等的，并且w0 = w，其中：01D（w0）=ui1ui2：：uif =2D（w0）=vi1vi2：：vif因此D是PCP阳性通常，我们可以支持存在如下内容：i1;：if2f1：n g，即uiui：：ui=1 2 fvi1vi2：viifthenletw0bethewdonalp habetfca;cbghthat1D（w0）=ui1ui2：：uif那么显然1D（w 0）=2D（w 0），因此：w~0c#c2L（G1D）\L（G2D）2用归纳法证明命题4.1显然，如果（w）`ABt0，则（w）`Lt0。我们证明了以下广义逆：如果0`Lt0，其中0只包含SubTp（G）的类型，则0`ABt0。我们通过归纳法很容易地进行演绎的长度公理的情况是：0=t0，这对A B 来说都是一个很好的例子。规则nright是不可能的，因为t 02 Pr规则=lef t和=right在这里是不可能的，这是由于Lambek演算的子公式性质，并且因为=不出现在PCP-文法的SubTp（G）中。带结论的规则及经历; A n B;0|{z}=零A和; B;0在哪里; A n B;0 =.显然，A2Pr，因为假设SubTp（G），特别是A n B 2 SubTp（G）.然后，我们可以将归纳假设应用于两个前因，其中A和t0是原始的：“ABA和; B;`ABt0由此我们得到了nlef t的结果，2