类型逻辑语法（四）

灵活解释。对于这种语法-语义界面的僵化观点，一个颇具吸引力的替代方案是对 Hendriks 1993 的灵活解释。在这种方法中，句法源演算的一种类型与一个无限的 LP 类型集相关联：其中一个是与句法源类型相关联的默认语义类型，其他类型则通过类型转换律从该默认类型推导而来。类似地，一个源演算项被翻译成一个无限的目标语义项集；其中一个是基本翻译（不一定是相关句法类别的默认语义类型），其他类型则通过类型转换律的 Curry-Howard 项像推导而来。所使用的类型转换原则包括 (i) 降低论元 (argument lowering)、(ii) 提升值 (value raising) 和 (iii) 提升论元 (argument raising)。前两个对应于自然语言的有效类型转换；正如我们在§2.2中看到的，论元提升是超越句法源演算表达能力的关键原则。

作为灵活解释的一个例子，比较“John loves Mary”和“Everyone loves someone”。从句法上讲，所有名词短语都被类型化为np，动词则被类型化为(np\s)/np。“John”和“Mary”被解释为类型e的常量，“loves”被解释为类型e → e → t的常量，这是句法源类型的默认语义类型。但“everyone”和“someone”被映射到类型(e → t) → t的常量。解释“Everyone loves someone”的句法推导时，语义类型不再适合简单的函数应用：动词需要两个e类型的参数，而是找到了两个 (e → t) → t 类型的论元。通过论元的提出，有两种方式可以容纳这些高阶论元：根据是先提出宾语论元再提出主语论元，还是反之，对同一个句法推导可以得到两种解读：一种对应于表层顺序的解读，∀ 的作用域覆盖 ∃，另一种是作用域顺序相反的解读。在这种灵活的视角下，句法和语义之间的对应关系变成了一种关系，而不是由§2.2 中的翻译同态在功能上决定。

延续。近年来，越来越明显的是，亨德里克斯关于推导歧义的类型转换解释的核心思想可以用计算机科学中发展起来的延续传递式解释（CPS）以及可用于此类解释的不同求值策略进行深刻的重构。在自然语言语义中使用延续（continuation）的先驱是 de Groote (2001b) 和 Barker (2002)。在编程语言理论中，延续是控制状态（即待执行计算的未来）的表示。通过将控制状态作为显式参数添加到解释中，程序可以操纵其延续，从而表达原本无法实现的控制结构。从技术上讲，延续语义使用指定的响应类型来表示计算的最终结果；对于类型 A 的表达式，延续是一个将 A 值传递给响应类型的函数。在自然语言语义的应用中，响应类型通常与真值 t 的类型相对应，即分配给完整句子的类型。

Barker 2004 展示了如何通过延续传递式翻译来获得“Everyone loves someone”的类型转换范围歧义。其关键思想在于，在将源语言演算映射到语义目标语言演算时，所有类型都通过一个额外的延续参数进行参数化。为此，我们使用了一个新的翻译函数 (·)*，它将句法类型到语义类型的映射与延续参数组合起来。源语言类型 A 现在与目标语言中所谓的计算相关联，即作用于其自身延续的函数：A* = (A′ → t) → t。

在证明层面，给定上述类型的解释，任务是找到下列后序项的 LP 证明，即 A, A\B ⊢ B 和 B/A, A ⊢ B 的 \ 和 / 消去规则的像。在源语言演算中，只有一种方法将 A\B（或 B/A）函数与其 A 参数组合在一起，而在目标语言演算中，可以选择求值顺序：我们是先求参数的平移像，然后再求函数的平移像，还是反过来。我们将第一个选项（按值调用）写为 ·v，将第二个选项（按名称调用）写为 ·n。在目标语言中，m 和 n 分别是 A′ → B′ 和 A′ 类型的变量；k 是由此产生的 B′ → t 延续。

应用的LP翻译：

(A′ → t) → t, ((A′ → B′) → t) → t ⊢ (B′ → t) → t

按值调用解：

(M ⊲ N)v = (N ⊳ M)v = λk.(Nv λn.(Mv λm.(k (m n))))

按名称调用解：

(N ⊳ M)n = (M ⊲ N)n = λk.(Mn λm.(Nn λn.(k (m n))))

延续传递式解释，类似于类型转换方法，可以将句法类型np分配给专有名词和量化名词短语：在目标演算中，np 的翻译具有适当的语义类型 (e → t) → t。但是提升策略现在推广到所有源类型：及物动词 (np\s)/np) 映射到 ((e → e → t) → t) → t，等等。对于 A 类型词汇常量的翻译，默认配方是 λk.(k c)，c 是 A′ 类型的非逻辑常量。默认翻译只是将这些词汇项的语义值传递给延续参数 k。但量化名词短语有效地利用了延续参数：它们将范围扩展到其延续，从而得到针对“每个人”和“某人”的词汇配方 λk.(∀λx.(k x))，λk.(∃λx.(k x))。评估策略之间的选择，结合这些词汇配方，会导致对源演算 M = (everyone⊳(loves⊲someone)) 中的单个推导产生不同的解释，其中 ·v 产生表面作用域构造，而 ·n 产生倒置作用域解读。

Mv = λk.(∀ λx.(∃ λy.(k ((loves y) x)))

Mn = λk.(∃ λy.(∀ λx.(k ((loves y) x)))

上面的例子在句法源演算中只使用了NL的斜线消去。引入延续的一个重要动机是，它们使得对经典（而非直觉主义）逻辑进行建设性解释成为可能；有关讨论请参见Sørensen and Urzyczyn 2006。因此，多结论对称范畴语法LG在延续传递风格中也有自然的解释也就不足为奇了（Bernardi and Moortgat 2010, Moortgat 2009）。在我们上面给出的例子中，源类型A只有一个延续参数。在LG的CPS翻译中类型，句法源类型的延续是递归执行的。我们将目标语言中类型为 A 的值记为 V(A)，将延续函数记为 K(A)，即函数 V(A) → R，将计算函数记为 C(A)，即函数 K(A) → R，其中 R 是响应类型。对于 LG 句法源类型 A，按值调用的 CPS 翻译将生成如下的 LP 值 V(A)。对于原子类型，V(p) = p，

蕴涵：V(A\B) = V(B/A) = K(B) → K(A)

蕴涵（蕴涵的对偶）：V(A ⊘ B) = V(B ⦸ A) = K(A\B)

在证明层面（以及与它们具有 Curry-Howard 对应的项），CPS 翻译将多结论源推导转化为单结论 LP 推导。该翻译遵循以下不变量。主动输出公式 A（下方方框中竖线标出）映射到计算 C(A)，主动输入公式映射到延续 K(A)。因此，一次切割被解释为将 C(A) 应用于 K(A)。

来源：LG/,\,⊘,⦸ →CPS 目标：LP→

X ⊢ A | Y V(X),K(Y) ⊢ C(A)

X | A ⊢ Y V(X),K(Y) ⊢ K(A)

X ⊢ Y V(X),K(Y) ⊢ R

讨论：基于延续的方法现已可用于解决许多难以通过组合方法处理的棘手现象。在句子层面，例如，Shan 和 Barker (2006) 对原位范围构想和 wh 问题的处理，其中交叉和优势性违规可以用人类处理器偏好从左到右的评估策略来解释；驴子首语重复 (Barker 和 Shan (2008))；Bernardi 和 Moortgat (2010) 研究了 LG 的按值调用和按名称调用解释中的量词范围歧义。在话语层面，de Groote (2006) 对动态现象进行了类型论分析，将命题建模为句子左右语境（延续）上的函数。

4.证明网与处理

在前几节中，我们已经了解了如何将不同的范畴演算呈现为具有基于序贯式决策程序的证明系统。然而，从计算的角度来看，在这些系统中进行简单的证明搜索效率低下：通常，会有多种方法构造不同的证明，这些证明仅在推理规则的应用顺序上有所不同，但会生成相同的解释（即在解释同态下与推导相关的LP项）。这种“虚假”歧义问题可以通过引入范式推导（例如Hepple 1990、Hendriks 1993，比较线性逻辑中的聚焦证明搜索机制）并结合使用基于图表的解析方法（例如Hepple 1999、Capelletti 2007）来解决。范畴演绎解析的另一种方法是保留序贯式演算，转而采用证明网方法。证明网最初是在线性逻辑的背景下发展起来的，它使用的推导表示本质上不存在“伪歧义”，也就是说，根本不会出现无关规则排序的问题。关于证明网的一般处理，我们参考了“线性逻辑”条目。下面我们将讨论专门处理范畴语法问题的方面。

兰贝克演算的证明网。结合演算L和交换变体LP的证明网最初是由Roorda (1991, 1992)研究的。为了捕捉这些系统的“直觉主义”本质，人们使用具有极性的公式：公式的先行出现为输入（“给定”）极性，而后行出现为输出（“待证明”）极性。正确性标准将证明网与更广泛的图类区分开来：除了适用于一般线性逻辑的非循环性和连通性标准之外，还增加了平面性以捕捉词序敏感性：在L的证明网中，公理链接不能交叉。关于语法-语义接口，de Groote和Retoré（1996）证明，通过指定一组用于遍历网络的“移动指令”，可以从证明网中读取Curry-Howard对应关系中与语义目标演算中的LP推导相关的lambda项；然后，这些指令与相关lambda项的构造逐步对应。

增量处理。证明网被静态地视为满足某些正确性标准的图，它消除了与序贯演算中规则应用顺序相关的虚假选择：在这方面，它们代表了对范畴演算的纯粹“声明式”观点。 Johnson (1998) 和 Morrill (2000) 指出，另一种关于构建网络实际过程的“程序性”观点也完全合理，并且为理解性能现象提供了一个颇具吸引力的视角。在这种解释下，网络以从左到右的增量方式构建，通过在与实时出现的词汇项相关的部分证明网络的输入/输出文字之间建立可能的链接。这暗示了增量遍历的简单复杂性度量，由文字之间未解决的依赖关系数量给出。该复杂性度量与许多已得到充分证实的处理问题（例如中心嵌入的难度、花园小径效应、附着偏好以及歧义结构中的首选范围构造）密切相关。

一阶量词。平面性条件将 L 的非交换证明网从 LP 网络中单独挑出。为了处理本文讨论的更结构化的范畴演算，必须改进正确性标准。实现此目的的一种策略是将其转换为 MILL1（一阶乘法直觉线性逻辑），其中的证明网带有额外的链接，用于对一阶变量进行存在性和全称量化。然后，人们可以以与逻辑编程中定理子句语法中位置论元的使用方式非常相似的方式使用这些变量。Moot 和 Piazza (2001) 为 L 和 NL 给出了这样的转换。对于 L 的串联运算，人们用二元项替换命题字母（原子公式），标记连续字符串的开始和结束。对于非结合性 NL，人们添加一个额外的变量来跟踪子公式的嵌套深度。对于简单不连续演算DL（允许单个分裂点）中的包装操作，Morrill和Fadda（2008）使用了四元谓词。一般而言，我们发现演算的句法表达能力与编码其结构资源管理所需的变量数量之间存在相关性。

网络与重写。§3.1和§3.3中的多模态对称演算对最初为线性逻辑开发的证明网络方法提出了挑战。在这些系统中，我们通常会发现单向结构规则，例如显位移的提取公设，或LG情况下的Grishin分配律：这些单向规则自然地引出了图重写的概念。一个针对扩展Lambek演算的完全通用的证明网络框架，其正确性标准基于重写，已在 Moot 和 Puite 2002 和 Moot 2007 中得到发展。

Moot-Puite 网络的基本构建块是广义的链接概念，它适用于任意元数的连接词。链接由其类型（张量或余张量）、前提（序列 P1,…,Pn，0 ≤ n）、结论（序列 C1,…,Cm，0 ≤ m）及其主公式（在中性链接的情况下可以为空，或者为 Pi 或 Ci 之一）决定。证明结构是有限公式集上的一组链接，其中每个公式最多一次是链接的前提，最多一次是结论。不是任何链接结论的公式是证明结构的假设，而不是任何链接前提的公式则是结论。公理公式是非任何链接主公式的公式。抽象证明结构是通过擦除内部节点上的所有公式获得的。证明网是一种证明结构，其抽象证明结构转换为张量树——在直觉系统的情况下是一棵有根树，在对称LG的情况下可能是一棵无根树。如此定义的证明网可以证明为与有效推导相对应的图。

将候选抽象证明结构转换为证明网的重写步骤有两种。对于复公式A，逻辑收缩对应于恒等式A ⊢ A；它们将匹配张量和余张量链接的配置简化为一个点。结构转换将具有假设H1,…,Hn和结论C1,…,Cm的证明结构进行内部重连，使其变为以Hi的某些排列作为假设，以Ci的某些排列作为结论的结构。换句话说，复制和删除是被排除的。例如，对应于§3.3中讨论的Grishin交互原理之一的重写，使我们能够从A⊗B⊢C⊕D推断出C⦸A⊢D/B。假设A和B在左边，结论C和D在右边。网络表示以特别清晰的方式表明这些原理是结构保持的：它们保持假设和结论的顺序不变。

ABCD网络

5. 认识容量与复杂性

反思以上内容，可以说，本文回顾的句法演算的扩展是出于在表达能力和计算易处理性之间找到适当平衡的愿望：在表达能力方面，一个合适的类型逻辑框架应该能够识别严格上下文无关之外的模式；理想情况下，人们希望保持这种表达能力与多项式可导性问题兼容。在当代“词汇化”语法形式主义中，满足这些要求的系统呈现出显著的趋同性：即所谓的“轻度上下文敏感”系统（Joshi、Vijay-Shanker 和 Weir，1991）。那么，我们该如何看待这里讨论的类型逻辑系统在识别能力和复杂性方面的表现呢？

类型逻辑层次结构 NL 中的最小系统存在多项式识别问题（参见 de Groote，1999 和 Capelletti，2007 的实际解析算法），但它严格地与上下文无关（Kandulski，1988）。使用全局结构规则的扩展在表达力和复杂性方面都不能令人满意。至于 L，Pentus（1993b，2006）表明它仍然严格地与上下文无关，而全局结合性的加入使可导性问题成为 NP 完全问题。对于 L 的无积片段，NP 完全性已经成立 (Savateev 2009)。对于 LP，也同样成立，即在乘法直觉线性逻辑中，我们具有NP完备性（Kanovich 1994）。关于识别能力，van Benthem（1995）表明LP能够识别上下文无关语言的所有置换闭包：从句法角度来看，这一类别过于宽泛。作为意义组装的逻辑，LP是类型逻辑库的核心组成部分。但正如我们在句法-语义界面的讨论中所看到的，我们可以将注意力集中在LP的子语言上，它构成了句法演算中派生的形象，并对词序和短语结构做出了有趣的断言。

多模态扩展和对称扩展的情况更加复杂。这里的表达力与人们对结构资源管理施加的限制类型直接相关。一方面，没有结构规则的多模态性并不能使我们超越上下文无关识别：Jäger (2003) 表明，n 元类型形成操作族的纯剩余逻辑严格保持上下文无关。如果要求结构规则具有资源敏感性（无复制或删除操作），并且对于一元模态，要求其不扩展，则可以获得上下文相关语法的完整表达能力，以及随之而来的 PSPACE 复杂度 (Moot 2002)。（PSPACE 包含那些可使用多项式级内存空间解决的问题。参见可计算性和复杂性条目。如果不对结构规则施加任何限制（具体来说，如果允许复制和删除操作），不出所料，可以获得不受限制的重写系统的表达能力 (Carpenter 1999)。Jäger 2005 在对指代消解的分析中采用了受控的复制操作。如 Bastenhof (2010) 所示，不包含交互原理的对称演算 LG 是上下文无关的。对于包含§3.3 交互原理的系统，Melissen (2009) 证明，所有作为上下文无关语言与上下文无关语言的置换闭包的交集的语言，在 LG 中都是可识别的。在这类演算中，我们发现了 MIX 的广义形式（该语言由相等数量的符号 a、b、c 组成，顺序任意），其字母符号的重数 k 相等，顺序任意，并且对任意数量的字母符号计数依赖性 an

1

…an

k

。此类模式可被范围连接语法和全局索引语法识别；与这些形式主义进行比较可能有助于确定 LG 识别能力的上限，而该上限目前尚不清楚。

关于计算复杂性，Moot (2008) 建立了词汇化树邻接语法与范畴语法（具有§3.1的多模态提取假设和一组有限的LG语法）之间的对应关系。对于这些语法，他通过将其翻译成超边替换语法获得了多项式可解析性结果。对于LG，该限制要求蕴涵⊘,⦸在词汇类型赋值中以匹配对的形式出现。Melissen (2009) 的广义MIX构造的词汇表，以及Bernardi和Moortgat (2010) 在范围构象分析中用于量词短语的类型赋值，均不遵循此限制。对于具有§3.3交互原理的LG的一般情况，Bransen (2010) 建立了NP完全性。 §3 的不连续演算的位置。必须确定此层次结构中的第二个：它们比上下文无关语言识别范围更广，但尚不清楚它们是否属于轻度上下文相关语言家族。