Formalized Lambek Calculus in Higher Order Logic (HOL4)
在这个项目中，一个相当完整的证明理论形式化的Lambek演算（非关联的任意扩展）已经从Coq证明辅助移植到HOL4定理证明器，并进行了一些改进和新的定理。定义了Lambek演算的三个演绎系统（句法演算、自然演绎和序列演算），并证明了许多相关定理。形式上证明了这些系统之间的等价性。最后，在HOL4中设计并实现了序列微积分证明的形式化（其中Coq具有内置支持）。一些基本结果，包括所谓的“割自由”证明的子公式的性质进行了形式证明。这项工作可以被认为是对语言解析器的基础上的类别语法，这是不是多模态的，但仍然有能力支持上下文敏感的语言，通过自定义的扩展的初步工作。
2017-05-20 cs.CL cs.LO
Extended Lambek calculi and first-order linear logic
CNRS（法国国家科学研究中心）；LaBRI（波尔多计算机科学实验室）
一阶乘法直觉线性逻辑（MILL 1）可以看作是Lambek演算的一个扩展。除了MILL 1的片段对应于Lambek演算（Moot & Piazza 2001），我将展示MILL 1的片段，它们生成多种上下文无关语言，并对应于Morrilll等人的位移演算。
2013-05-27 cs.CL cs.LO
Vector Space Semantics for Lambek Calculus with Soft Subexponentials
University College London（伦敦大学学院）
本研究为带软亚指数的可判定Lambek演算构建向量空间语义，将其用于寄生gap名词短语等的组合向量构造，经句子相似度任务验证，该语义可将缩约定义为投影，为相关问题提供线性理论支撑。
2023-10-06 cs.CL cs.LO
Undecidability of the Lambek calculus with subexponential and bracket modalities
University College London（伦敦大学学院）；National Research University Higher School of Economics（俄罗斯国家研究型高等经济大学）；Steklov Mathematical Institute, RAS（俄罗斯科学院斯捷克洛夫数学研究所）；University of Pennsylvania（宾夕法尼亚大学）
Lambek演算是一种著名的逻辑形式主义，用于建模自然语言语法。最初的演算涵盖了大量复杂的自然语言现象，但仅限于上下文无关的设置。为了解决更微妙的语言问题，Lambek演算已经以各种方式扩展。特别是，Morrill和Valentin（2015）引入了一种扩展，即所谓的指数和括号模态。他们的扩展是基于一个非标准的收缩规则的指数，相互作用的括号结构在一个复杂的方式。标准的压缩法则在这个演算中是不允许的。本文证明了微积分中可导性问题的不可判定性。我们还调查了限制可判定的片段考虑Morrill和瓦伦丁，我们表明，这些片段属于NP类。
2017-05-04 cs.CL math.LO
A polynomial time algorithm for the Lambek calculus with brackets of bounded order
National Research University Higher School of Economics（国立研究型大学高等经济学院）；Steklov Mathematical Institute of RAS（俄罗斯科学院斯捷克洛夫数学研究所）；Universitat Politècnica de Catalunya（加泰罗尼亚理工大学）；University of Pennsylvania（宾夕法尼亚大学）
Lambek演算是范畴语法的逻辑基础，是语法作为逻辑、句法分析作为演绎的语言学范式。Pentus（2010）给出了一个多项式时间算法，用于确定允许空前件的Lambek演算中有界深度公式的可证明性。Pentus的算法基于证明网的列表化。带括号的Lambek演算是带括号模态的Lambek演算的保守扩展，适用于句法域的建模。本文给出了一个允许空前件的括号型Lambek演算的可证性算法。我们的算法运行在多项式时间的公式深度和括号嵌套深度都有界。它结合了Pentus风格的表格化证明网与自动机理论的括号处理。
2017-12-18 cs.CL cs.DS cs.FL
Reconciling Lambek's restriction, cut-elimination, and substitution in the presence of exponential modalities
University College London（伦敦大学学院）；National Research University Higher School of Economics（国立研究型高等经济学院）；Steklov Mathematical Institute（斯捷克洛夫数学研究所）；University of Pennsylvania（宾夕法尼亚大学）
Lambek演算可以被认为是非交换直觉线性逻辑的一个版本。Lambek演算的一个有趣的特性是所谓的“Lambek限制”，也就是说，任何可证明的前件都应该是非空的。本文讨论了在保持Lambek限制的前提下，用线性逻辑指数形式推广Lambek演算的方法。有趣的是，我们表明，任何系统配备了一个合理的指数模态以下成立：如果系统享有削减消除和替代的最大程度上，那么系统必然违反Lambek的限制。然而，我们证明了三个条件中的两个可以实现。即，我们设计了一个具有Lambek限制和割消元的系统和一个具有Lambek限制和替换的系统。对于这两个演算，我们证明，他们是不可判定的，即使我们只采取两个部门提供的Lambek演算之一。具有割消和替换而不受Lambek限制的系统是民间传说，已知是不可判定的。
2019-05-09 cs.CL math.LO
Comparing and evaluating extended Lambek calculi
CNRS (LaBRI)（法国国家科学研究中心（拉布里实验室））；University of Bordeaux（波尔多大学）
Lambek语法演算，通常被称为Lambek演算，在许多方面都是创新的，特别是作为线性逻辑的先驱。但它也表明，我们可以把我们的语法框架视为逻辑（而不是逻辑理论）。然而，尽管它至少成功地对许多语言现象进行了基本的处理，但很明显，在许多其他情况下，还需要一种稍微更具表现力的逻辑演算。因此，自80年代以来，直到今天，已经提出了许多Lambek演算的扩展和变体。因此，现在有一大类微积分，每一类都有自己的经验成功和理论结果，但也有自己的逻辑原语。这就提出了一个问题：我们如何比较和评价这些不同的逻辑形式主义？为了回答这个问题，我提出了两个统一的框架，这些扩展的Lambek演算。两者都是具有图收缩准则的证明网演算。第一个演算是一个非常通用的系统：你指定了你的序列的结构，它给你对应的连接词和缩写词。演算可以用结构规则扩展，这些规则直接转换成图重写规则。第二个演算是一阶（乘法直觉主义）线性逻辑，它有几个其他的，独立提出的扩展兰贝克演算的片段。我将举例说明每种演算在不同框架中提出的分析之间建立桥梁的用途，突出差异并帮助识别问题。
2015-06-18 cs.CL cs.LO
Lambek vs. Lambek: Functorial Vector Space Semantics and String Diagrams for Lambek Calculus
University of Oxford（牛津大学）
分布组合范畴（Distributional Compositional Categorical，DisCoCat）模型是一个为自然语言句子的意义提供组合语义的数学框架。它包括一个计算过程，用于构建句子的意义，给定它们在组合类型逻辑方面的语法结构，并给定它们的单词的经验推导的意义。对于在分布式向量空间模型中对单词的含义进行建模的特定情况，其实验预测（来自真实的大规模数据）优于其他经验验证的方法，这些方法可以为完整的句子构建向量。这一成功可以归因于概念动机的数学基础，通过整合定性成分类型逻辑和定量建模的意义范畴理论的数学框架。DisCoCat模型中使用的类型逻辑是Lambek的前群文法。预群类型形成一个posetal紧闭范畴，它可以通过函子的方式传递到向量空间、线性映射和张量积的紧闭结构上。紧凑封闭范畴中等式推理的图解形式可以解释为句子中词义的流动。前群简化了Lambek以前的类型逻辑，Lambek演算，它已被广泛用于形式化和推理各种语言现象。DisCoCat对前团体的明显依赖被视为一个缺点。本文针对这一问题，指出，人们也可以实现一个函式通道从原来的类型逻辑的Lambek，monoidal双闭范畴，向量空间，或任何其他模式的意义组织在monoidal双闭范畴。Baez和Stay给出了相应的字符串图演算，描述了词义的流动。
2013-02-02 cs.CL math.CT math.LO
Undecidability of the Lambek calculus with a relevant modality
University College London（伦敦大学学院）；National Research University Higher School of Economics（国立研究大学高等经济学院）；Steklov Mathematical Institute（斯捷克洛夫数学研究所）；University of Pennsylvania（宾夕法尼亚大学）
Morrill和Valentin在论文“Computational coverage of TLG：Nonlinearity”中考虑了通过所谓的“指数”模态丰富的Lambek演算的扩展。这一情态表现为“相关”风格，即允许压缩和置换，但不允许弱化。Morrill和Valentin提出了一个开放的问题，即这个系统是否是可判定的。在这里，我们展示了它的不可判定性。如果我们考虑所有除法运算都有一个方向的片段，我们的结果仍然有效。我们还表明，在一个限制的情况下，模态只能应用于变量（原始类型）的可导性问题，是可判定的，属于NP类。
2016-08-07 cs.CL math.LO
Categorical Vector Space Semantics for Lambek Calculus with a Relevant Modality
University College London（伦敦大学学院）；Utrecht University（乌得勒支大学）
本文为带相关模态 !L* 的 Lambek 演算构建范畴组合分布式语义，通过量子化函子实例化到有限维向量空间，并在寄生空位短语消歧任务中评估三种余代数模态解释。
2023-05-11 cs.CL cs.LO
Symmetric categorial grammar: residuation and Galois connections
Utrecht Institute of Linguistics OTS（乌得勒支语言学研究所OTS）
Lambek-Grishin演算是Lambek演算的一个对称扩展：除了Lambek演算的剩余积族、左除法运算和右除法运算之外，还考虑了一个余积族、右差分运算和左差分运算，它们通过箭头反转对偶与前者相关。两个家庭之间的沟通是根据线性分配原则来实现的。本文的目的是补充（对偶）剩余类型形成操作与正交反对对比剩余和伽罗瓦连接操作之间的对称性。虽然（对偶）剩余运算是单调的，但伽罗瓦连通运算（及其子运算）是反调的。讨论了（对偶）Galois连通运算的代数性质，并将（上）积分配原理推广到包括负运算。我们给出了新的类型形成操作的连续传递式翻译，并讨论了一些语言应用。
2010-08-01 cs.CL
On embedding Lambek calculus into commutative categorial grammars
National Research University Higher School of Economics（俄罗斯国家研究型高等经济大学）
我们考虑张量文法，它是\commutative文法的一个例子，基于经典的（而不是直觉的）线性逻辑。它们可以被看作是抽象范畴文法ACG的表面表示，因为ACG的派生转化为张量文法的派生，并且这种转化在串语言的水平上是同构的。基本成分是张量项，它可以被视为编码和概括证明网。使用张量项使得语法非常简单，直接的几何意义变得透明。然后，我们解决的问题，在我们的设置编码非交换操作。在用新的一元运算符丰富系统后，这是可能的。由此产生的系统允许代表ACG和Lambek文法作为保守的片段，而形式主义仍然是，因为它似乎对我们来说，相当简单和直观。
2021-11-19 cs.CL cs.LO math.LO
Parsing for Semidirectional Lambek Grammar is NP-Complete
我们研究了Lambek范畴语法的一个变体{ \em semi-directional}的解析问题的计算复杂性。在半定向Lambek演算$\SDL$中，有一个额外的非定向抽象规则，允许被抽象的公式出现在前提条件的左手边的任何地方，从而允许非外围提取。$\SDL$语法能够生成每一种上下文无关语言，甚至更多。我们证明了半定向Lambek文法的解析问题是NP-完全的3-分区问题的减少。
1996-05-10 cmp-lg cs.CL
Higher-Order DisCoCat (Peirce-Lambek-Montague semantics)
Quantinuum（Quantinuum 公司）
本文提出高阶DisCoCat模型，将单词意义定义为图值高阶函数，结合蒙塔古语义与lambda演算，实现从兰贝克演算到皮尔士系统beta的翻译，并给出DisCoPy实现，用于处理副词、介词、否定和量词等非线性语义过程。
2025-09-25 cs.CL math.CT
Conjunctive categorial grammars and Lambek grammars with additives
Steklov Mathematical Institute of RAS（俄罗斯科学院斯捷克洛夫数学研究所）；HSE University（高等经济大学）；St. Petersburg State University（圣彼得堡国立大学）
本文提出带合取运算的范畴语法，证明其与合取语法等价，可嵌入兰贝克演算，并用于定义NP完全集及处理空字符串问题。
2024-05-26 cs.CL cs.LO math.LO
A Typedriven Vector Semantics for Ellipsis with Anaphora using Lambek Calculus with Limited Contraction
Queen Mary University of London（伦敦玛丽女王大学）
基于Jäger（2006）的Lambek有限收缩演算（LCC），我们使用类型驱动的组合分布语义，为带回指的动词短语省略开发了一个向量空间语义。分布语义学对实词的统计搭配意义有很多解释，但对如何处理虚词却没有提供什么指导。另一方面，形式语义学有强大的机制来处理关系代词、协调词等。类型驱动的组合分布语义将这两个模型结合在一起。我们回顾了Coecke等人（2010，2013）的DisCoCat框架中关系代词，协调和省略的限制性解释的先前组成分布模型。我们展示了DisCoCat如何无法处理依赖于信息复制的一般形式的省略，并通过以Muskens & Sadrzadeh（2016）的风格将向量可解释的lambda项分配给LCC的派生，开发了一种将类型语法与分布语义联系起来的新方法。下面是对（动词短语）省略的解释，在省略中，词义可以被复制：句子的意义现在是一个程序，可以非线性地访问单个词嵌入。我们提出的理论设置，工作的例子，并证明我们的结果的玩具分布模型的数据。
2019-05-05 cs.AI cs.CL cs.LO
Traduction des Grammaires Catégorielles de Lambek dans les Grammaires Catégorielles Abstraites
Loria（洛里亚研究所）
Lambek文法（LG）是一种基于非交换组合类型的自然语言计算模型。它已经被广泛研究，特别是对于语法起主要作用的语言（如英语）。这份实习报告的目的是证明每一个Lambek语法都可以用抽象范畴语法（ACG）来表达，虽然不完全，但很有效。后者是一种新的建模的基础上高阶签名同态（使用$λ$ -演算），旨在统一目前使用的模型。其主要思想是通过擦除引入和消除规则并生成足够的公理以满足切割规则的要求，将LG的类型重写系统转换为上下文无关文法（CFG）的类型重写系统。这种迭代方法保留了推导，并使我们能够在任何步骤停止可能的无限生成过程。虽然底层的算法没有完全实现，这个证明提供了另一个论据，有利于ACG在自然语言处理的相关性。
2020-01-23 cs.CL cs.LO
Putting a Spin on Language: A Quantum Interpretation of Unary Connectives for Linguistic Applications
Institute for Theoretical Physics（理论物理研究所）；Center for Complex Systems Studies（复杂系统研究中心）；Utrecht University（乌得勒支大学）；Utrecht Institute of Linguistics OTS（乌得勒支语言学研究所OTS）
目前在计算语言学中使用的Lambek演算的扩展版本依赖于一元模态，以允许影响词序和短语结构的结构规则的受控应用。这些受控的结构操作引起的衍生歧义，错过了原来的Lambek演算或其pregroup简化。已经提出了在FVect和线性映射的紧凑闭范畴中对扩展的Lambek演算进行组合解释的建议，但是在这些建议中，语法语义映射忽略了控制模态，有效地将它们的作用限制在语法中。我们的目标是把模态变成向量解释的一等公民。在方向密度矩阵语义的基础上，我们用一个额外的自旋密度矩阵空间扩展了类型系统的解释。证明的解释，然后在模糊的推导结果与正交自旋状态张紧。我们的方法引入了一种同时表示歧义话语的共存解释的方式，并为词汇和派生歧义的整合提供了一个统一的框架。
2021-09-06 cs.CL cs.LO quant-ph
Minimalist Grammars and Minimalist Categorial Grammars, definitions toward inclusion of generated languages
Nancy Université（南锡大学）；INRIA Nancy-Grand Est（法国国家信息与自动化研究所南锡-大东部分部）
Stabler提出了Chomskyan Minimalist Program，Chomsky 95 with Minimalist Grammars（MG，Stabler 97）的一个实现。这一框架继承了悠久的语言传统。但是如果使用Curry-Howard同构，语义演算就更容易添加。最简范畴语法（MCG）是基于Lambek演算的扩展，混合逻辑，被引入来提供一个理论上有动机的语法-语义接口，Amblard 07。在这篇文章中，我们给出了完整的定义MG与代数树描述和MCG，并采取第一步向证明其生成的语言。
2011-08-25 cs.CL
Proof nets for the Displacement calculus
CNRS（法国国家科学研究中心）
我们提出了一个证明网演算的位移演算，并证明其正确性。这是第一个直接对位移演算进行建模的证明网演算，而不是通过某种形式转换成另一种形式。证明网演算为使用置换演算进行解析和证明搜索开辟了新的可能性。
2016-06-06 cs.CL cs.LO
Logical foundations for hybrid type-logical grammars
LIRMM（蒙彼利埃大学与法国国家科学研究中心联合计算机科学、机器人与微电子实验室）；Université de Montpellier（蒙彼利埃大学）；CNRS（法国国家科学研究中心）；The Ohio State University（俄亥俄州立大学）
本文探讨了证明理论方面的混合类型逻辑文法，逻辑相结合的Lambek文法与lambda文法。我们证明了一些基本性质的演算，如规范化和子公式的属性，也提出了一个混合类型逻辑文法的证明网演算。除了澄清混合类型逻辑语法的逻辑基础之外，目前的研究还开辟了原始系统的变体和扩展的道路，包括但不限于非联想版本和多模态版本，其中包含结构规则和一元模式。
2020-09-22 cs.CL math.LO
Abstract categorial grammars with island constraints and effective decidability
一个众所周知的方法来处理语法岛的限制，在设置的Lambek语法包括在添加特定的括号模态的逻辑。我们适应这种方法抽象范畴语法（ACG）。因此，我们定义了括号（蕴涵）线性逻辑，括号内的代数演算，并最终，括号内ACG的基础上括号内的$λ$演算。这使得我们至少可以在相对化的背景下对最简单的岛屿约束进行建模。接下来，我们确定特定的安全括号ACG，就像普通的（无括号）二阶ACG生成有效的可判定的语言，但足够灵活的模型一些高阶现象，如相对化和正确处理语法岛，至少在简单的玩具的例子。
2020-05-20 cs.CL math.LO
Incremental Interpretation of Categorial Grammar
本文描述了一个范畴语法分析器，它提供了充分的逐词增量解释。解析器不需要句子的片段来形成成分，从而避免了虚假歧义的问题。本文简要讨论了基本范畴语法与其他形式主义，如HPSG，依存语法和Lambek演算之间的关系。它还包括一些问题的讨论时出现的语法分析词汇化，并使用统计技术调整到特定的语言的可能性。
1995-03-14 cmp-lg cs.CL
Mathematical Foundations for a Compositional Distributional Model of Meaning
Oxford University Computing Laboratory（牛津大学计算实验室）；University of Cambridge Computer Laboratory（剑桥大学计算机实验室）
我们提出了一个数学框架，用于统一向量空间模型中的意义分布理论，以及语法类型的合成理论，其中我们依赖于Lambek引入的预群代数。这个数学框架使我们能够从句子成分的含义中计算出一个好类型句子的含义。具体地说，预群的类型约简被“提升”为范畴中的态射，这是一个将成分的意义转化为（良好类型的）整体的意义的过程。重要的是，整个句子的意义存在于一个空间中，独立于句子的语法结构。因此，内积可以用来比较任意句子的意义，就像它是用来比较分布模型中单词的意义一样。我们采用的数学结构允许一个纯粹的图解演算，它揭示了信息如何在句子中的单词之间流动，以构成整个句子的意义。我们的“分类模型”的一个变化，其中涉及约束标量的向量空间的布尔半环的结果在蒙塔格风格的布尔值语义。
2010-03-23 cs.CL cs.LO math.CT
