类型逻辑语法（一）

类型逻辑语法是一种子结构逻辑，旨在推理自然语言中形式和意义的构成。这些语法的核心是剩余的类型形成操作族；类型逻辑语法的层次结构源于人们对类型形成操作的结构属性所做的选择，以及为控制语法资源管理而引入的方法。计算语义源于范畴推导的 Curry-Howard 解释。解析和自然语言处理则基于线性逻辑证明网的适当精炼版本进行建模。

1. 历史回顾

2. Lambek 系统

2.1 语法组合建模

2.2 语法-语义接口

3. 扩展类型逻辑语法

3.1 多模态系统，结构控制

3.2 非连续性逻辑

3.3 对称范畴语法

3.4 灵活解释，连续语义

4. 证明网络及其处理

5. 识别容量和复杂性

6. 相关方法

参考文献

学术工具

其他网络资源

相关条目

1. 历史回顾

类型逻辑语法源于 Jim Lambek 半个世纪前发表的两篇开创性论文（Lambek 1958, 1961）。在这两篇论文中，作者设定的目标是“获得一种有效的规则（或算法）来区分句子和非句子，该规则（或算法）不仅适用于数理逻辑学家感兴趣的形式语言，也适用于自然语言[...]”。为了实现这一目标，熟悉的词类（名词、动词、……）被转化为一种逻辑公式——一种旨在推理语法构成的逻辑。根据这种观点，判断一个短语是否格式良好是演绎过程的结果。这种判断的决策程序是通过将语法逻辑转化为根岑式的后继演算形式而获得的。后继演算的呈现方式极其简单：语法逻辑是一种没有结构规则的逻辑。收缩和弱化被删除；它们的存在意味着格式良好性不受任意复制或删除语法材料的影响。为了同时考虑词序和短语结构信息，兰贝克进一步删除了交换和（在1961年的论文中）结合性的结构规则。

在发表这些思想时，它们并没有引起共鸣；它们对计算语言学领域的影响始于20世纪80年代。有两个因素在这种迟来的认识中发挥了重要作用。第一个因素是增加了用于范畴推导的计算语义，类似于范·本瑟姆（van Benthem）1983年提出的柯里-霍华德（Curry-Howard）的“证明即程序”解释（该解释重印于1988年的Buszkowski等人的著作中）。由此看来，兰贝克的类型逻辑语法可以毫不妥协地实现蒙塔古的组合性程序，而lambda演算和类型理论为研究推导语义和词汇语义提供了强大的工具。第二个因素是线性逻辑的引入（Girard 1987），以及随之而来的对子结构逻辑兴趣的激增。线性逻辑中引入类型逻辑语法的一个关键洞见是，结构规则可以通过所谓的模态以受控形式重新引入：在转向更具判别力的类型逻辑时，表达力不会丢失。从计算的角度来看，线性逻辑证明网的变体为类型逻辑自然语言处理提供了基础。

类型逻辑语法在其当前版本中保留了兰贝克原始演算的总体架构，但将其扩展为更清晰的类型形成运算词汇。其中最重要的是乘法运算，用于建模语法组合；这些运算构成了本文的重点。除了乘法运算之外，还可以考虑加法运算或布尔运算以及一阶或二阶量化，以处理词汇歧义、类型多态性和特征信息管理等现象。Morrill 1994 是此类扩展的一个很好的例子来源。

本文概述：我们从标准的兰贝克系统入手。我们研究它们的模型论和证明论方面（框架语义、后继演算），以及两者之间的关系（健全性、完备性）。我们将组合解释刻画为一个同态映射，它将句法源演算与用于意义组装的目标演算关联起来。该映射将句法推导与语义解读关联起来，后者以简单类型线性 Lambda 演算的术语表示。在§3中，我们将探讨标准 Lambek 系统在句法和语义方面的表达局限性，并研究如何通过以模块化的方式系统地扩展范畴论架构来解决这些局限性。概括涉及类型形成操作的元数（二元组合操作与一元控制运算符）；多模态扩展，其中多个类型形成操作家族共存并通过结构交互原理进行通信；单排序逻辑与多排序逻辑（非连续演算）；单结论系统与多结论系统（对称演算）；以及语法-语义接口的更结构化视图（连续语义）。为了结束全景之旅，我们为§3中研究的各种类型逻辑系统提供证明网，并比较这些系统的表达能力和计算易处理性。

2. Lambek系统

2.1 语法组合建模

本节将讨论的类型语言由一小部分原子类型组成，并且在二元运算乘法、左除法和右除法下闭合。一些符号约定：在下面的规范中，小写的p表示原子类型的范围，大写的A、B表示任意类型的范围。我们将 A\B 读作“A 下 B”，将 B/A 读作“B 上 A”，以此来明确“分数”中哪部分是分母 (A)，哪部分是分子 (B)。

类型：A,B ::= p | A ⊗ B | A\B | B/A

在对语言表达式进行分类时，原子类型代表那些在语法上可以被认为是“完整”的短语。例如，在英语中，s 可以表示陈述句（“Mary dreams”等），np 可以表示名词短语（“Mary”、“the girl”等），n 可以表示普通名词（“girl”、“smart girl”等）。除法表达不完整性：一个类型为 A\B (B/A) 的表达式与其左侧（右侧）的 A 类型短语组合在一起，将产生一个类型为 B 的短语。乘积类型 A ⊗ B 明确地表达了由类型 A 和 B 的组成部分按顺序构成一个复杂短语。因此，如果“Mary”的类型为 np，动词“dreams”的类型为 np\s，那么我们通过将这些类型相乘，得到组合“Mary dreams”的 s：np ⊗ (np\s)。对于组合“the girl dreams”，同样，限定词的类型为 np/n，而“girl”的类型为 n：((np/n) ⊗ n) ⊗ (np\s)。

为了使这种对类型语言解释的非正式描述更加精确，我们求助于模态逻辑。在范畴论中，框架 F = (W,R) 由一组语言资源（表达式，“符号”）W 组成，并以三元关系 R 的形式构建。这种三元关系代表语法组合，或生成传统中所说的“合并”：将 Rxyz 理解为“表达式 x 由子表达式 y 和 z 组合而成”。相比之下：在 Routley-Meyer 关联逻辑的语义中，R 是解释融合操作的可及性关系。

模型 M 是一对 (F,V)，其中 V 是将原子类型发送给 W 子集的解释（赋值）。对于复杂类型，赋值遵循以下子句。我们将 x ∈ V(A) 记为 M,x ⊩ A，或者，为了避免混淆，记为 x ⊩ A。

x ⊩ A ⊗ B 当且仅当 ∃yz 满足 Rxyz 且 y ⊩ A 且 z ⊩ B

y ⊩ C/B 当且仅当 ∀xz，如果 Rxyz 且 z ⊩ B，则 x ⊩ C

z ⊩ A\C 当且仅当 ∀xy，如果 Rxyz 且 y ⊩ A，则 x ⊩ C

范畴类型语言的句法演算是一个演绎系统，它能生成形式为 A ⊢ B（“B 可从 A 推导出来”）的语句。如果 V(A) ⊆ V(B)，则语句 A ⊢ B 在模型（“M ⊨ A ⊢ B”）中成立；如果它在所有模型中都成立，则它是有效的（“⊨ A ⊢ B”）。对于最小语法逻辑，句法演算中的推导集可从下面的公理和推理规则自由生成。由于历史原因，这个最小系统被称为NL（“非结合兰贝克演算”）。第一行指出，可导性是一种自反传递关系，即预序关系。第二行的双向（“当且仅当”）推理规则将乘法和除法运算描述为剩余理论中所谓的剩余三元组。（Galatos et al. 2007 提供了很好的背景阅读材料。）如此定义的句法演算，就下文的可靠性和完备性结果而言，恰好符合类型语言的预期解释。

预序律：

A ⊢ A（自反性）

从 A ⊢​​ B 和 B ⊢ C 推断 A ⊢ C（传递性）

剩余律：A ⊢ C/B 当且仅当 A ⊗ B ⊢ C 当且仅当 B ⊢ A\C

可靠性和完备性：A ⊢ B 在语法基础逻辑 NL 中可证明，当且仅当 ⊨ A ⊢ B，即，当且仅当 V(A) ⊆ V(B) 对每个框架 F 上的每个赋值 V 成立 (Došen 1992)。

NL 的完备性结果不会对合并关系 R 的解释施加任何限制。这意味着最小语法逻辑的定理和推理规则具有语法不变量的地位：无论各个语言的结构特性如何，组合类型的属性都成立。以下是一些此类普遍有效原则的示例。由于斜线和反斜线左右对称，它们成对出现。

应用：

(A/B) ⊗ B ⊢ A

B ⊗ (B\A) ⊢ A

共同应用：

A ⊢ (A ⊗ B)/B

A ⊢ B\(B ⊗ A)

提升：

A ⊢ B/(A\B)

A ⊢ (B/A)\B

单调性：从 A ⊢​​ B 和 C ⊢ D 推断出以下任意结果：

A ⊗ C ⊢ B ⊗ D

A/D ⊢ B/C

D\A ⊢ C\B

鉴于上面讨论的通用自由生成的句法演算，为特定语言提供范畴语法的任务简化为指定其词汇：从这个意义上讲，类型逻辑框架代表了语法形式主义“词汇化”的顶峰。范畴词典是一种将每个词与有限数量的类型相关联的关系。给定一个词典Lex，范畴语法将类型B分配给一个词串w1···wn，当且仅当1≤i≤n时，(wi,Ai)∈Lex，并且X⊢B在句法演算中是可证的，其中X是一个乘积公式，其结果为A1···An。如果字符串 w1 ··· wn 确实被判定为类型 B 的良构短语，则该语法可视为充分的。

词汇类型分配无需手工设计：Buszkowski 和 Penn (1990) 将词汇习得建模为求解类型方程的过程。他们基于合一的算法以函数论元结构作为输入（具有可区分中心子节点的二叉树）；根据解决方案是否应为每个词汇项分配唯一的类型（所谓的刚性语法），或者是否接受多个分配（k 值语法，其中 k 为最大词汇歧义因子），算法会获得不同的变体。Kanazawa (1998) 从这个角度研究了可学习的语法类别，其意义类似于 Gold 的“极限”可识别性概念。迄今为止，这一研究方向已得到充分确立，不仅适用于类型逻辑语法本身，也适用于§6 中讨论的相关前群形式主义。

类型逻辑语法的激进词汇主义意味着不存在构造特定规则规定的空间：中心语法概念必须从类型结构中产生，而不是被设定。以下是一些例子。

价。不及物动词（“梦”，例如，不及物动词（“sleeps”）左侧只需一个主语名词短语即可构成一个完整的句子；及物动词（“sees”、“admires”）左侧则需要有一个主语，右侧则需要有一个直接宾语。这种选择要求用方向蕴含来表达：不及物动词为 np\s，及物动词为 (np\s)/np。在上下文无关语法中，这些区别需要假设新的非终结符。

格。能够满足任何名词短语选择要求的短语（例如，专有名词）与坚持扮演主语或直接宾语角色的带格代词之间的区别通过高阶类型赋值来表达：专有名词可以简单地输入为 np，主语代词（“he”、“she”）输入为 s/(np\s)，直接宾语代词（和反身代词）输入为 ((np\s)/np)\(np\s)。在这种类型下，人们能够正确区分语法上的“他看见她”和格式错误的“他喜欢她”。

补语与修饰语。比较外心型（A/B 或 B\A，其中 A ≠ B）与内心型 A/A、A\A。后者表达修饰；修饰短语的可选性如下。比较“那个女孩”、“那个聪明的女孩”、“那个（戏弄比尔的）女孩”，其中“女孩”的类型为 n，“聪明”的类型为 n/n，关系从句“戏弄比尔的”的类型为 n\n。

补语-空隙依赖关系。具有嵌套蕴涵的类型 A/(C/B)、A/(B\C) 等，表示在 C 类型域中撤回 B 类型间隙假设。“戏弄比尔的女孩”中的关系代词“who”的类型为 (n\n)/(np\s)：它与一个主语必须保持未表达的句子结合，正如从错误格式的“玛丽戏弄比尔的女孩”中看到的那样。

序贯演算，可判定性。我们如何判断语句 A ⊢ B 是否确实是句法演算的定理？在存在扩展规则（例如提升规则）的情况下，这一点并非显而易见：从 A ⊢​​ B 和 B ⊢ C 到 A ⊢ C 的传递性推理涉及一个“引理”公式 B，该公式在结论中消失，并且有无数个候选引理公式需要考虑。Lambek 原始论文的一个关键点在于将句法演算重新表述为等效的 Gentzen 式后继形式，该形式具有截断消除功能。

语法基础逻辑 NL 的后继形式是语句 X ⇒ A，其中 X（先行词）是一个结构，A（后继词）是一个类型公式。先行词结构必须非空。结构要么是单个公式，要么是叶子节点为公式的二叉树。在下面的后继规则中，先行词的树结构用括号 (–,–) 表示。符号 X[Y] 表示包含特定子结构 Y 的结构 X。对于每个连接词（类型形成运算），都有两条推理规则，分别将连接词引入可导性箭头的左侧或右侧。在本后继规则中，如同在根岑的命题逻辑中一样，Cut 是一条可接受规则：所有使用 Cut 推理的定理证明都可以转化为等价的无截断推导。在无截断系统中，后向链接证明搜索遵循子公式属性，并立即得出决策过程。

A⇒A

Ax

Y⇒A X[A]⇒B

X[Y]⇒B

截断

X⇒A Y⇒B

(X,Y)⇒A⊗B

(⊗R)

X[(A,B)]⇒C

X[A⊗B]⇒C

(⊗L)

Y⇒B X[A]⇒C

X[(Y,B\A)]⇒C

(\L)

(B,X)⇒A

X⇒B\A

(\R)

Y⇒B X[A]⇒C

X[(A/B,Y)]⇒C

(/L)

(X,B)⇒A

X⇒A/B

(/R)

NL：序贯演算

演算的图景。从纯剩余逻辑出发，通过将结合律和/或交换律赋予组合运算⊗，可以得到一系列演算。这些演算反映了人们对语法材料结构的不同看法。下表总结了各种演算。

逻辑结构 结合律 交换律

NL 树 – –

L 字符串 ✓ –

NLP 移动 – ✓

LP (=MILL) 多集 ✓ ✓

由于历史原因，Lambek 1958 年提出的具有结合律组合运算的系统被称为 L；纯剩余逻辑 NL，即 L 的非结合律版本，后来在 Lambek 1961 年被引入。增加交换律后，L 和 NL 分别变成了 LP 和 NLP。LP，即带置换的 Lambek 演算，由 van Benthem 于 1983 年提出；回想起来，这是乘法直觉线性逻辑 (MILL) 的蕴涵/融合片段。NL 的交换变体已被 Kandulski 研究过；但它尚未发现重要的语言学应用。对于层次结构中的四个系统，(非保守)扩展写为 (N)L(P)*，它允许空先行项。

在句法演算的表示中，结构选项采用非逻辑公理（公设）的形式，这些公理会被添加到剩余律中。在后继演算的表示中，有相应的结构规则。L(P) 的后继演算也允许一种糖化表示，其中先行项被视为公式的列表或多集；这样，结构规则的推理步骤就可以保留为隐式的。就框架语义而言，每个结构选项都对合并关系 R⊗ 的解释引入了约束。因此，具有结构选项的演算的完备性是相对于所有遵循相关约束的框架而言的（Došen 1992）。结合演算 L 实际上允许更具体的模型，其中我们将 Rxyz 读作 x = y · z，其中 · 为二元连接运算。Pentus (1995) 提出了一个相当复杂的证明，证明 L 相对于此类自由半群模型（或称语言模型）确实是完备的。

结构公设：

A ⊗ B ⊢ B ⊗ A（交换律）

A ⊗ (B ⊗ C) ≡ (A ⊗ B) ⊗ C（结合律）

后续表达的相应结构规则：

W[(Y,X)]⇒C

W[(X,Y)]⇒C

（交换律）

W[((X,Y),Z)]⇒C

W[(X,(Y,Z))]⇒C

（结合律）

交换律的框架约束：∀xyz(Rxyz 蕴含 Rxzy)

结合律的框架约束（向左重新括号）：∀xyzrs(Rrxs 和 Rsyz 蕴含 ∃t(Rrtz 和 Rtxy)))反之亦然。

LP 的一个特征属性是左右划分之间的区别消失了：A\B 和 B/A 变得可相互导出。从句法角度来看，LP 中结合性和/或交换性的全局可用性意味着，成分结构和/或词序的任意变化都不会影响表达式的合式性——很少有语言学家会认同这一观点。我们在 L 中发现的全局结合性是否是句法上的可行选择，尚有争议。Lambek 在其 1961 年的论文中指出了自由重括号导致的过度生成的情况，但后来又回归了结合性的观点。在下一节中，我们将看到 LP 作为意义合成演算是完全合法的。在§3 中，我们将讨论基于词汇类型分配的受控结构推理形式，作为有问题的“全有或全无”选项的替代方案。

2.2 语法-语义接口

为了兼顾句法和语义的考量，我们可以将范畴语法构建为一对由组合解释链接起来的演算：一个句法源演算、一个语义目标演算，以及一个将源的类型和派生项映射到目标的相应类型和派生项的同态演算。在本节中，我们将为标准 Lambek 演算构建这种架构。在下一节中，我们将看到扩展的范畴类型逻辑如何反映出对语法和语义之间分工的不同看法，从而反映出对实现两者之间组合映射所需工作量的不同看法。

(N)L{n,np,s}

/,\

(·)′

同态映射到LP{e,t}

→

语法同态语义

范畴演绎的语义研究始于1983年的范·本瑟姆（van Benthem）。与柯里-霍华德（Curry-Howard）的“公式即类型，证明即程序”方法一致，各种范畴演算中的推导都与λ演算的适当片段的项相关联。为了简单起见，我们将注意力集中在蕴涵词汇上：(N)L的方向斜线，以及LP的非方向蕴涵。

让我们从LP的柯里-霍华德对应关系开始。选择LP作为自然语言语义的演算，体现了意义合成是一个资源敏感的过程：在解释推导时，任何材料都不能被复制或丢弃。我们将简单类型的线性 lambda 演算中的项称为 Λ(Lin)。在不存在收缩和弱化的情况下，它是最小集合，使得给定一个可数无限的变量集 Var，