类型逻辑语法（五）
6. 相关方法
本文讨论的类型逻辑语法与许多相关的形式语法框架具有许多共同特征，这些框架中类型也起着关键作用。我们简要讨论其中一些相关框架，并为想要进一步探索其联系的读者提供参考文献。
组合范畴语法 (CCG)。CCG 框架（详见 Steedman 2000）的名称源自 Curry 和 Feys 的组合逻辑。类型逻辑语法的设计遵循逻辑议程（序贯演算、健全性、完备性等），而 CCG 传统中的语法则被表示为类型变化和类型组合的有限规则集。该规则库通常包括函数应用模式、类型提升和函数组合，它们既可以是在结合L中有效的类型（组合具有相同方向性的蕴涵类型），也可以是混合类型（组合具有不同方向性的函子）。
20世纪80年代，CCG和Lambek类型的类型逻辑语法的发展最初遵循着不同的路径。最近，出现了趋同的迹象。一个重要因素是引入了多模态控制的类型逻辑技术来微调CCG组合模式的适用性（Baldridge 2002，Kruijff and Baldridge 2003）。从这个角度来看，多模态类型逻辑语法扮演着底层通用逻辑的角色，人们用它来建立CCG组合模式的有效性。而原始组合子的特定选择是出于计算效率方面的考虑（Hoyt and Baldridge 2008）。就生成能力而言，CCG 属于轻度上下文敏感的语法形式主义家族。多项式可解析性是通过对函数组合图式施加一个界限来实现的。
预群语法。预群是紧致双线性逻辑（Lambek 1993）的代数版本，通过折叠张量和余张量运算获得。预群语法于 1999 年 Lambek 提出，作为原始句法演算 L 的简化。此后，Lambek 及其同事使用它们为各种语言构建计算片段。预群是一个偏序幺半群，其中每个元素 a 都有一个左伴随和一个右伴随，al，ar，分别满足 ala → 1 → aal 和 aar → 1 → ara。类型分配的形式是将一个词与一个或多个来自自由预群的元素关联，该自由预群由一组偏序基本类型生成。为了与范畴类型公式建立联系，可以使用翻译 a/b = abl 和 b\a = bra。在预群设置下，解析非常简单。Lambek (1999) 证明，只需执行将 ala 和 ala 替换为乘法单位 1 的收缩操作即可。这本质上是对 well-bracketing 的检查——该操作可以委托给下推自动机。需要展开式 1 → aal 和 1 → ara 来证明像 (ab)l = blal 这样的方程。在下面的例子中，我们使用后者获得了高阶关系代词类型 (n\n)/(s/np) 的预群版本。Carroll 所著书籍
L 中的类型赋值：n (n\n)/(s/np) np (np\s)/np
预群类型赋值：n nr n npll sl np npr s npl → n
紧致双线性逻辑并非原始句法演算的保守扩展。L 中每个可导的后继项在相应的预群中都有一个可导的平移，但反之则不然：例如，类型 (a ⊗ b)/c 和 a ⊗ (b/c) 的预群像为 a b cl，但这两个类型在 L 中不可互导。
关于生成能力，Buszkowski (2001) 指出，预群语法等价于上下文无关语法。换句话说，它们共享原始范畴语法的表达限制。为了克服这些局限性，人们尝试了不同的策略，包括词汇规则（元规则）、派生约束、受控形式的交换性以及预群的乘积。《逻辑学研究》特刊（Buszkowski 和 Preller，2007）和专著 Lambek，2008，很好地展现了当前的研究成果。
摘要：范畴语法。ACG 框架（de Groote，2001a）是一个关于组合语法架构的元理论。 ACG 建立在高阶线性签名 Σ = (A,C,τ) 之上，其中 A 和 C 分别是原子类型和常量的有限集，τ 是一个函数，为每个常量分配一个 A 上的线性隐含类型。给定一个源签名 Σ 和一个目标签名 Σ′，一个解释就是 Σ 到 Σ′ 的映射，由一对函数给出：η 将 Σ 的类型原子映射到 Σ′ 的线性隐含类型，θ 将 Σ 的常量映射到 Σ′ 的良类型线性 lambda 项，其映射方式与类型映射兼容。用编译器理论的术语来说，将源签名和目标签名分别称为抽象词汇表和具体词汇表，将解释映射称为词典。然后，通过将 Σ 的原子类型指定为语法的可区分类型，即可获得 ACG。
在 ACG 设置中，可以根据抽象词汇表与对象词汇表的区别来建模语法-语义接口。但也可以通过使用字符串和树的规范 λ 项编码及其操作，通过解释映射获得表面形式。ACG 引发了一个有趣的复杂性层次结构，用于重写编码为 ACG 的语法形式主义：上下文无关语法、树邻接语法等；例如，参见 de Groote 和 Pogodalla 2004。这些形式主义的表达能力以抽象词汇表中常量的最大顺序以及解释原子抽象类型的对象类型的最大顺序来衡量。对类型逻辑系统的 ACG 编码的研究始于 Retoré 和 Salvati (2010) 的论文；这两位作者提出了一种用于（无积）自然语言 (NL) 的 ACG 构造。
从该描述中可以清楚地看出，ACG 的体系结构与本文所讨论的范畴类型逻辑的组合解释密切相关。一个关键的区别在于“抽象语法”的性质，即同态推导出解释的源演算。对于标准 Lambek 系统和上文§3 中讨论的扩展系统，抽象语法是一种方向类型逻辑；对于 ACG，在源端和目标端都存在 LP 和线性 Lambda 演算。关于语言结构属性是否必须在抽象语法层面进行解释的争论由来已久，始于 Curry 1961；相关讨论参见 Muskens 2007。类型逻辑观点在其逻辑常量（即类型形成操作及其支配规律）层面解释词序共性。ACG 的观点在这方面更为自由：表面形式的推导可以逐词指定。抽象语法与表面实现之间这种更为宽松的联系是否可取，尚有争议。ACG 的一个吸引人的特征是其表达能力与源常量和解释映射的顺序限制之间的联系，而这种联系尚未在类型逻辑框架内得到系统研究。
