The Lambek-Grishin calculus is NP-complete
Jeroen Bransen
Lambek-Grishin演算LG是非结合Lambek演算NL的对称扩展。本文证明了LG的可导性问题是NP-完全的。
The Lambek-Grishin calculus LG is the symmetric extension of the non-associative Lambek calculus NL. In this paper we prove that the derivability problem for LG is NP-complete.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
继续探索
Proof nets for the Lambek-Grishin calculus
Grishin对Lambek句法演算的推广将非交换乘法合取及其残差（乘积、左除和右除）与对偶族：乘法析取、右差和左差结合起来。这两个家庭之间的相互作用采取的形式线性分配原则。我们研究证明网络的Lambek-Grishin演算和这些网络之间的对应关系和非集中和集中的版本，其微积分。
Polarized Montagovian Semantics for the Lambek-Grishin calculus
Grishin提出用乘法析取（PAR）和余残差来丰富Lambek演算。Moortgat讨论了Lambek-Grishin演算（LG）在语言学中的应用。在本文中，我们适应吉拉德的极性敏感的双重否定嵌入经典逻辑提取一个组成的蒙塔哥维语义显示演算集中证明搜索在LG。我们抓住这个机会来说明我们的方法，同时分析提取，提供语言的动力张量的线性分布超过标准杆，从而回答了一个问题的Kurtonina和Moortgat。最后，我们比较我们的建议，继续语义的Bernardi和Moortgat，对应的调用的名称和调用的值评估策略。
The Logic for a Mildly Context-Sensitive Fragment of the Lambek-Grishin Calculus
虽然上下文无关文法的特点是一个简单的证明理论的语法形式主义，即范畴语法和它的逻辑Lambek演算，没有这样的特征是已知的树邻接文法，甚至任何轻度上下文敏感的语言类在过去的四十年，尽管一些努力。本文解决了这一问题。在现有的片段的Lambek-Grishin演算捕获树邻接语言的基础上，我们提出了一个逻辑称为HLG：一个证明理论的表征树邻接语言的Lambek-Grishin演算的基础上限制到超边替换文法与秩二的Moot研究。HLG定义在具有割容许性的显示演算中。一些新的技术，如纯结构连接词，有用性，并证明网络HLG的图论参数的证明。
Tableaux for the Lambek-Grishin calculus
由Lambek开创的范畴类型逻辑，通过用公式识别范畴，用证明识别推导，寻求对自然语言语法的证明论理解。我们通常会观察到一种直觉偏见：假设的结构配置（一个组成部分）得出一个结论（分配给它的类别）。根据Grishin的建议，Moortgat提出了Lambek-Grishin演算（LG），目的是恢复假设和结论之间的对称性。我们开发了一个理论的标记模态tableaux LG，其连接词的解释为二进制模态算子的关系语义的Kurtonina和Moortgat的启发。作为我们的方法的语言应用，我们表明，语法的基础上LG是上下文无关的，通过使用插值引理。这个结果补充了Melissen的结果，Melissen证明了混合结合性和-交换性增强的LG在表达能力上超过了LTAG。
Proof nets for display logic
本文探讨了几个扩展的证明网络的Lambek演算，以处理不同的连接词的显示逻辑在一个自然的方式。新的证明网演算处理一些最近添加到Lambek词汇表，如伽罗瓦连接和Grishin相互作用。它的结论与探索的生成能力的Lambek-Grishin演算，提出了一个嵌入的词汇化树邻接语法到Lambek-Grishin演算。
Symmetric categorial grammar: residuation and Galois connections
Lambek-Grishin演算是Lambek演算的一个对称扩展：除了Lambek演算的剩余积族、左除法运算和右除法运算之外，还考虑了一个余积族、右差分运算和左差分运算，它们通过箭头反转对偶与前者相关。两个家庭之间的沟通是根据线性分配原则来实现的。本文的目的是补充（对偶）剩余类型形成操作与正交反对对比剩余和伽罗瓦连接操作之间的对称性。虽然（对偶）剩余运算是单调的，但伽罗瓦连通运算（及其子运算）是反调的。讨论了（对偶）Galois连通运算的代数性质，并将（上）积分配原理推广到包括负运算。我们给出了新的类型形成操作的连续传递式翻译，并讨论了一些语言应用。
Displacement Calculus
Lambek演算以连接逻辑的形式为范畴语法提供了基础。但是自然语言的特征是依赖性，这种依赖性也可能是不连续的。本文介绍了Lambek演算的推广--位移演算，它在包含不连续性和包含不连续性的同时保持了Lambek演算良好的证明理论性质，并举例说明了它在语言学中的应用，证明了割消、子公式性质和可判定性
Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
Extended Lambek calculi and first-order linear logic
一阶乘法直觉线性逻辑（MILL 1）可以看作是Lambek演算的一个扩展。除了MILL 1的片段对应于Lambek演算（Moot & Piazza 2001），我将展示MILL 1的片段，它们生成多种上下文无关语言，并对应于Morrilll等人的位移演算。
Vector Space Semantics for Lambek Calculus with Soft Subexponentials
本研究为带软亚指数的可判定Lambek演算构建向量空间语义，将其用于寄生gap名词短语等的组合向量构造，经句子相似度任务验证，该语义可将缩约定义为投影，为相关问题提供线性理论支撑。
Undecidability of the Lambek calculus with subexponential and bracket modalities
Lambek演算是一种著名的逻辑形式主义，用于建模自然语言语法。最初的演算涵盖了大量复杂的自然语言现象，但仅限于上下文无关的设置。为了解决更微妙的语言问题，Lambek演算已经以各种方式扩展。特别是，Morrill和Valentin（2015）引入了一种扩展，即所谓的指数和括号模态。他们的扩展是基于一个非标准的收缩规则的指数，相互作用的括号结构在一个复杂的方式。标准的压缩法则在这个演算中是不允许的。本文证明了微积分中可导性问题的不可判定性。我们还调查了限制可判定的片段考虑Morrill和瓦伦丁，我们表明，这些片段属于NP类。
Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
Lambek演算可以被认为是非交换直觉线性逻辑的一个版本。Lambek演算的一个有趣的特性是所谓的“Lambek限制”，也就是说，任何可证明的前件都应该是非空的。本文讨论了在保持Lambek限制的前提下，用线性逻辑指数形式推广Lambek演算的方法。有趣的是，我们表明，任何系统配备了一个合理的指数模态以下成立：如果系统享有削减消除和替代的最大程度上，那么系统必然违反Lambek的限制。然而，我们证明了三个条件中的两个可以实现。即，我们设计了一个具有Lambek限制和割消元的系统和一个具有Lambek限制和替换的系统。对于这两个演算，我们证明，他们是不可判定的，即使我们只采取两个部门提供的Lambek演算之一。具有割消和替换而不受Lambek限制的系统是民间传说，已知是不可判定的。
Comparing and evaluating extended Lambek calculi
Lambek语法演算，通常被称为Lambek演算，在许多方面都是创新的，特别是作为线性逻辑的先驱。但它也表明，我们可以把我们的语法框架视为逻辑（而不是逻辑理论）。然而，尽管它至少成功地对许多语言现象进行了基本的处理，但很明显，在许多其他情况下，还需要一种稍微更具表现力的逻辑演算。因此，自80年代以来，直到今天，已经提出了许多Lambek演算的扩展和变体。因此，现在有一大类微积分，每一类都有自己的经验成功和理论结果，但也有自己的逻辑原语。这就提出了一个问题：我们如何比较和评价这些不同的逻辑形式主义？为了回答这个问题，我提出了两个统一的框架，这些扩展的Lambek演算。两者都是具有图收缩准则的证明网演算。第一个演算是一个非常通用的系统：你指定了你的序列的结构，它给你对应的连接词和缩写词。演算可以用结构规则扩展，这些规则直接转换成图重写规则。第二个演算是一阶（乘法直觉主义）线性逻辑，它有几个其他的，独立提出的扩展兰贝克演算的片段。我将举例说明每种演算在不同框架中提出的分析之间建立桥梁的用途，突出差异并帮助识别问题。
A polynomial time algorithm for the Lambek calculus with brackets of bounded order
Lambek演算是范畴语法的逻辑基础，是语法作为逻辑、句法分析作为演绎的语言学范式。Pentus（2010）给出了一个多项式时间算法，用于确定允许空前件的Lambek演算中有界深度公式的可证明性。Pentus的算法基于证明网的列表化。带括号的Lambek演算是带括号模态的Lambek演算的保守扩展，适用于句法域的建模。本文给出了一个允许空前件的括号型Lambek演算的可证性算法。我们的算法运行在多项式时间的公式深度和括号嵌套深度都有界。它结合了Pentus风格的表格化证明网与自动机理论的括号处理。
Undecidability of the Lambek calculus with a relevant modality
Morrill和Valentin在论文“Computational coverage of TLG：Nonlinearity”中考虑了通过所谓的“指数”模态丰富的Lambek演算的扩展。这一情态表现为“相关”风格，即允许压缩和置换，但不允许弱化。Morrill和Valentin提出了一个开放的问题，即这个系统是否是可判定的。在这里，我们展示了它的不可判定性。如果我们考虑所有除法运算都有一个方向的片段，我们的结果仍然有效。我们还表明，在一个限制的情况下，模态只能应用于变量（原始类型）的可导性问题，是可判定的，属于NP类。
Lambek vs. Lambek: Functorial Vector Space Semantics and String Diagrams for Lambek Calculus
分布组合范畴（Distributional Compositional Categorical，DisCoCat）模型是一个为自然语言句子的意义提供组合语义的数学框架。它包括一个计算过程，用于构建句子的意义，给定它们在组合类型逻辑方面的语法结构，并给定它们的单词的经验推导的意义。对于在分布式向量空间模型中对单词的含义进行建模的特定情况，其实验预测（来自真实的大规模数据）优于其他经验验证的方法，这些方法可以为完整的句子构建向量。这一成功可以归因于概念动机的数学基础，通过整合定性成分类型逻辑和定量建模的意义范畴理论的数学框架。DisCoCat模型中使用的类型逻辑是Lambek的前群文法。预群类型形成一个posetal紧闭范畴，它可以通过函子的方式传递到向量空间、线性映射和张量积的紧闭结构上。紧凑封闭范畴中等式推理的图解形式可以解释为句子中词义的流动。前群简化了Lambek以前的类型逻辑，Lambek演算，它已被广泛用于形式化和推理各种语言现象。DisCoCat对前团体的明显依赖被视为一个缺点。本文针对这一问题，指出，人们也可以实现一个函式通道从原来的类型逻辑的Lambek，monoidal双闭范畴，向量空间，或任何其他模式的意义组织在monoidal双闭范畴。Baez和Stay给出了相应的字符串图演算，描述了词义的流动。
Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality
本文为带相关模态 !L* 的 Lambek 演算构建范畴组合分布式语义，通过量子化函子实例化到有限维向量空间，并在寄生空位短语消歧任务中评估三种余代数模态解释。
On embedding Lambek calculus into commutative categorial grammars
我们考虑张量文法，它是\commutative文法的一个例子，基于经典的（而不是直觉的）线性逻辑。它们可以被看作是抽象范畴文法ACG的表面表示，因为ACG的派生转化为张量文法的派生，并且这种转化在串语言的水平上是同构的。基本成分是张量项，它可以被视为编码和概括证明网。使用张量项使得语法非常简单，直接的几何意义变得透明。然后，我们解决的问题，在我们的设置编码非交换操作。在用新的一元运算符丰富系统后，这是可能的。由此产生的系统允许代表ACG和Lambek文法作为保守的片段，而形式主义仍然是，因为它似乎对我们来说，相当简单和直观。
Parsing for Semidirectional Lambek Grammar is NP-Complete
我们研究了Lambek范畴语法的一个变体{ \em semi-directional}的解析问题的计算复杂性。在半定向Lambek演算$\SDL$中，有一个额外的非定向抽象规则，允许被抽象的公式出现在前提条件的左手边的任何地方，从而允许非外围提取。$\SDL$语法能够生成每一种上下文无关语言，甚至更多。我们证明了半定向Lambek文法的解析问题是NP-完全的3-分区问题的减少。
Higher-Order DisCoCat (Peirce-Lambek-Montague semantics)
本文提出高阶DisCoCat模型，将单词意义定义为图值高阶函数，结合蒙塔古语义与lambda演算，实现从兰贝克演算到皮尔士系统beta的翻译，并给出DisCoPy实现，用于处理副词、介词、否定和量词等非线性语义过程。
Conjunctive categorial grammars and Lambek grammars with additives
本文提出带合取运算的范畴语法，证明其与合取语法等价，可嵌入兰贝克演算，并用于定义NP完全集及处理空字符串问题。
A Typedriven Vector Semantics for Ellipsis with Anaphora using Lambek Calculus with Limited Contraction
基于Jäger（2006）的Lambek有限收缩演算（LCC），我们使用类型驱动的组合分布语义，为带回指的动词短语省略开发了一个向量空间语义。分布语义学对实词的统计搭配意义有很多解释，但对如何处理虚词却没有提供什么指导。另一方面，形式语义学有强大的机制来处理关系代词、协调词等。类型驱动的组合分布语义将这两个模型结合在一起。我们回顾了Coecke等人（2010，2013）的DisCoCat框架中关系代词，协调和省略的限制性解释的先前组成分布模型。我们展示了DisCoCat如何无法处理依赖于信息复制的一般形式的省略，并通过以Muskens & Sadrzadeh（2016）的风格将向量可解释的lambda项分配给LCC的派生，开发了一种将类型语法与分布语义联系起来的新方法。下面是对（动词短语）省略的解释，在省略中，词义可以被复制：句子的意义现在是一个程序，可以非线性地访问单个词嵌入。我们提出的理论设置，工作的例子，并证明我们的结果的玩具分布模型的数据。
Putting a Spin on Language: A Quantum Interpretation of Unary Connectives for Linguistic Applications
目前在计算语言学中使用的Lambek演算的扩展版本依赖于一元模态，以允许影响词序和短语结构的结构规则的受控应用。这些受控的结构操作引起的衍生歧义，错过了原来的Lambek演算或其pregroup简化。已经提出了在FVect和线性映射的紧凑闭范畴中对扩展的Lambek演算进行组合解释的建议，但是在这些建议中，语法语义映射忽略了控制模态，有效地将它们的作用限制在语法中。我们的目标是把模态变成向量解释的一等公民。在方向密度矩阵语义的基础上，我们用一个额外的自旋密度矩阵空间扩展了类型系统的解释。证明的解释，然后在模糊的推导结果与正交自旋状态张紧。我们的方法引入了一种同时表示歧义话语的共存解释的方式，并为词汇和派生歧义的整合提供了一个统一的框架。
扫码添加微信好友，提出您的宝贵建议 👇
💡 备注请填写：网站反馈
发表机构由 AI 从论文文本抽取，如发现错误，欢迎反馈修正建议。