类型逻辑语法（二）_数学联邦政治世界观

如果 x ∈ Var，则 x ∈ Λ(Lin)；

如果 x ∈ Var，M ∈ Λ(Lin)，则 λx.M ∈ Λ(Lin)且 x 在 M 中恰好有一个自由变量出现；

若 M ∈ Λ(Lin)，N ∈ Λ(Lin)，且 M 和 N 的自由变量集不相交，则 (M N) ∈ Λ(Lin)。

从 Λ(Lin) 得到 Λ(LP)，即 Curry-Howard 对应的 LP 推导式中的项，通过添加一个额外限制，反映了后继先行项必须非空的要求：每个子项至少包含一个自由变量。LP 的推导现在可理解为 Λ(LP) 的类型推理系统的判断。推导以自然演绎风格给出，并带有线性蕴涵 → 的消去规则和引入规则。判断则是形式为 Γ ⊢ M : B 的后继项。Γ 是类型声明 x1 : A1, …, xn : An 的非空多集； Ai 和 B 是线性蕴涵类型，M 是由 Ai 类型的 xi 构建的 B 型 Λ(LP) 项。公理后序的形式为 x : A ⊢ x : A。线性蕴涵的消除规则和引入规则如下。在引入规则中，x ∉ dom(Γ)；在消除规则中，dom(Γ) ∩ dom(Δ) = ∅。

Γ,x : A ⊢ M : B

Γ ⊢ λx.M : A → B

→I

Γ ⊢ M : A → B Δ ⊢ N : A

Γ,Δ ⊢ (M N) : B

→E

类似地，句法演算 (N)L 与方向线性λ项存在柯里-霍华德对应关系 (Wansing 1992)。没有标准符号。在下面的方向类型规则中，我们使用λr vs λl 来表示斜线和反斜线引入规则的图像；在消除规则中，我们有左右函数应用，三角形指向函数。先行词现在是一串（带括号的）类型声明 xi : Ai。

(Γ,x : A) ⊢ M : B

Γ ⊢ λrx.M : B/A

(x : A,Γ) ⊢ M : B

Γ ⊢ λlx.M : A\B

Γ ⊢ M : B/A Δ ⊢ N : A

(Γ,Δ) ⊢ (M ⊲ N) : B

Γ ⊢ N : A Δ ⊢ M : A\B

(Γ,Δ) ⊢ (N ⊳ M) : B

源演算和目标演算各自拥有一组基本类型，分别基于句法和语义的考虑。在句法方面，例如，可以区分句子s、名词短语np和普通名词n。在语义方面，为了进行简单的外延解释，可以引入两种基本类型e和t。然后，语义类型的集合论解释可以用非空个体/实体集合E和真值{0,1}来给出。语义类型A的指称域Dom(A)被设置为：Dom(e) = E，Dom(t) = {0,1}，并且Dom(A\B) = Dom(B/A)是从Dom(A)到Dom(B)的函数集。

接下来考虑从句法源演算到语义目标演算的同态映射。映射在类型级别和证明（项）级别指定。在原子类型级别设置映射如下：句子表示真值；（专有）名词短语表示个体；普通名词函数从个体到真值。对于复杂的句法类型，解释函数将两个方向蕴涵发送给目标演算的线性蕴涵。同样，在证明（项）级别，句法源演算的方向构造在解释中被识别。（我们使用带撇号的版本来表示与源变量对应的目标变量，以提醒我们这些表达式的类型是不同的。）

类型：(np)′ = e，(s)′ = t，(n)′ = e → t，(A\B)′ = (B/A)′ = A′ → B′

项：(x)′ = x′，(λrx.M)′ = (λlx.M)′ = λx′.(M)′，(N ⊳ M)′ = (M ⊲ N)′ = ((M)′ (N)′)

在前面几节中，我们已经看到 NL、L 和 LP 定理构成了一个真包含层次。语义上的对应是，在转向更具区分性的句法演算时，越来越多的LP项在翻译中丢失：理想的意义组装方案通常无法以(N)L证明的像的形式获得。下表给出了这三种演算的特征类型转换。第二行包含与(N)L类型转换相关的方向证明项；第三行给出了相应的LP项，在(N)L情况下，通过平移同态获得；在LP情况下，则直接获得。

NL：论证降低 L：组合 LP：论证提升

(B/(A\B))\C ⊢ A\C A\B ⊢ (A\C)/(B\C) A → (B → C) ⊢

((A → C) → C) → (B → C)

z ⊢ λlx.((λry.(x ⊳ y)) ⊳ z) y ⊢ λrzλlx.((x ⊳ y) ⊳ z)

z′ ⊢ λx′.(z′ λy′.(y′ x′)) y′ ⊢ λz′λx′.(z′ (y′ x′)) x ⊢ λwλz.(w λy.((x y) z))

论证降低在NL中有效，因此在L中也有效。 LP。函数组合依赖于结合律；它在自然语言（NL）中无效，但在语言逻辑（L(P)）中有效。函数组合已用于构建部分语义表示，与字符串的增量（从左到右）处理并行运行。最后，论证的提出仅在LP中有效，也就是说，这种形式的意义组装不能在任何(N)L句法演算中以推导的形式获得。但是，正如我们将在下文中看到的，这种转变在自然语言范围歧义的分析中发挥着重要作用。

推导语义与词汇语义。资源敏感性施加的约束严重限制了推导语义的表达能力。在某种程度上，这些限制可以在词汇语义的层面上得到克服。与推导相关的Curry-Howard术语，被视为意义组装的程序，它抽象了特定词汇项的贡献。A 类词汇项的语义规范采用相应语义类型 A′ 的 lambda 项的形式，但该 lambda 项不再要求是线性的。以下是一些非线性词汇意义配方的示例。反身代词“himself”的规范是一个纯组合子（封闭项）：它标识二元关系的第一个和第二个参数。关系代词“that”或限定词“a, some”的术语具有一个抽象，该抽象绑定了同一个变量的两次出现，以便计算它们的两个 (e → t) 参数（名词和动词短语）的交集，并在“some”的情况下测试交集是否为空。

NL 类型 LP 类型词汇配方

自身 ((np\s)/np)\(np\s) (e→e→t)→e→t λRλx.((R x) x)

a, 一些 (s/(np\s))/n (e→t)→(e→t)→t λPλQ.(∃ λx.((P x)∧(Q x)))

即 (n\n)/(np\s) (e→t)→(e→t)→e→t λPλQλx.((P x)∧(Q x)))

意义组装中词汇方面和派生方面之间的相互作用可通过以下示例说明。请注意，线性证明项反映了派生历史（模方向性）；在替换词汇配方并进行 β 转换后，这种透明性就消失了。对词汇语义的完整封装是范畴方法的一大吸引力。

字符串：‘a boy hurt herself’

自然语言推导：(x : (s/np\s)/n,y : n),(z : ((np\s)/np,w : ((np\s)/np)\(np\s)) ⊢ M : s

对应的线性规划证明项：(M)′ = ((x′ y′) (w′ z′))

词汇插入：x′ ↦ λPλQ.(∃ λx.((P x)∧(Q x))),y′ ↦ boy,z′ ↦ harm,w′ ↦ λRλx.((R x) x)

β 转换后的最终结果：(∃ λx.((boy x) ∧ (hurt x x)))

3.扩展类型逻辑语法

将派生语义层面的资源敏感性与非线性词汇意义赋值相结合的策略，并非解决兰贝克最初构想的句法演算表达局限性的通用方案。一类需要扩展派生机制本身的问题，与（自然）母语无法以令人满意的方式在语法资源之间建立不连续的依赖关系有关。这种依赖关系表现在两种情况下。

提取。生成语法将这些现象称为“显性置换”，就像我们在 wh“移位”结构中发现的那样。比较 wh 短语“什么——惹恼了玛丽”和“玛丽放了——什么”这两个词，因为它们会出现在“我知道什么惹恼了玛丽”或“我知道玛丽放了什么”的语境中。破折号标记了名词短语在正常陈述句中的位置：“这条记录惹恼了玛丽”，“玛丽把记录放在那里”。将类型 wh/(np\s) 分配给“什么”，我们可以为第一个例子推导出 wh，其中 np 假设位于左边缘主语位置。如果这个假设（“间隙”）发生在内部，就像第二个例子一样，那么它对于 (N)L 来说是无法到达的：我们无法为“玛丽——放在那里”推导出 np\s（同样也无法推导出 s/np，因为它需要右边缘间隙）。

中缀。典型的例子是非局部语义建构的情况，例如“爱丽丝知道某人在作弊”，其中“某人”的解读范围很广：“存在一个特定的人 x，使得爱丽丝认为 x 在作弊”。量词短语‘某人’占据了实际上需要np类型假设的结构位置，并在更高的句子层面上实现其语义效果。对于“某人”的类型赋值 s/(np\s)，不存在产生非局部解读的推导。在生成语法中，人们会将非局部构念称为“隐蔽”运动的一个例子。

下文将讨论基本演算的扩展，代表了人们为寻找这些不连续依赖关系问题的原则性解决方案而采取的策略。

3.1 多模态系统，结构控制

20 世纪 90 年代提出的多模态范畴语法的核心思想很简单：它不考虑单一的剩余类型形成操作家族，而是考虑多个家族，它们共存于一个逻辑中。为了区分这些家族，类型形成操作用模式索引 /i, ⊗i, \i 修饰；解释合并关系 Ri 也是如此。每个家族都有相同的逻辑规则（剩余律）。但它们的结构属性可能有所不同。具体来说，它们可以通过混合不同模式的结构规则相互作用。在解释层面，此类相互作用原则引入了框架约束，类似于从自然语境到语言和逻辑短语的转变所带来的约束。

例如，让我们回到非边缘提取“（什么）玛丽把——放在那里”的例子。假设我们有两种组合模式：⊗c 和 ⊗d。常规配价要求用 ⊗c 乘积的斜线来表示。不连续依赖关系由混合结合律和交换律的结构公设以及表达 ⊗c 和 ⊗d 相对“强度”的包含公设来处理。对代词“什么”的类型分配提供了对这些公设的访问，以便它可以与非主语名词假设建立联系，该假设也位于句子内部。混合结合律：(A⊗c B)⊗d C⊢ A⊗c(B⊗d C)

混合交换律：(A⊗c B)⊗d C⊢ (A⊗d C)⊗c B

包含律：A⊗d B⊢ A⊗c B

“what”与非主语np假设相关的类型：wh/c(s/d np)

现在我们可以成功证明短语“Mary put — there”属于s/dnp类型，如下方推导示意图所示。通过混合相互作用公设，np假设找到了通往非边缘位置的路径，在那里它被动词“put”所要求。一旦它到达其起始位置，包含步骤就从结构允许模式d切换到表达常规子范畴化的c模式。

⋮

包容性

混合社区

混合协会

np ⊗c (((((np\cs) /c pp) /c np) ⊗c np) ⊗c pp) ⊢ s

np ⊗c (((((np\cs) /c pp) /c np) ⊗d np) ⊗c pp) ⊢ s

np ⊗c (((((np\cs) /c pp) /c np) ⊗c np) ⊗d np) ⊢ s

(np ⊗c ((((np \c s) /c pp) /c np) ⊗c pp)) ⊗d np) ⊢ s

NP ⊗c (((np \c s) /c pp) /c np) ⊗c pp) ⊢ s /d np

Mary put there

通过多模态交互原则，可以避免单个组合运算⊗的全局结合律和/或交换律选项导致的过度生成。然而，不规范地使用多模态很容易导致引入特定于构造的模态区别，从而损害类型逻辑方法的主要吸引力之一。下文将讨论的结构控制算子理论为多模态方法所解决的问题类型提供了更具原则性的解决方案。

控制算子。线性逻辑通过放弃收缩和弱化的结构规则，将经典逻辑中的连接词“&”拆分为乘法连接词和加法连接词。这种向资源敏感逻辑的转变可以在不牺牲表达能力的情况下实现：一元模态“！”“?”允许以受控形式重新引入收缩/弱化，从而在线性环境中恢复经典逻辑。

在类型逻辑语法中可以遵循类似的策略（Moortgat 1996，Kurtonina 1995）。类型语言扩展了一对一元运算符，我们将其写为◊,□；现在，公式由包含一元和二元类型形成操作的原子公式p构建而成。与二元词汇表一样，我们从◊,□的最小逻辑开始；然后可以以额外公设的形式添加结构控制功能。下面的真值条件将控制运算符◊和□表征为关于二元可及性关系R◊的逆对偶。这种解释将它们转换为剩余对，就像组合以及左右除法运算一样。

公式：A,B ::= p | ◊A | □A | A\B | A ⊗ B | A/B

解释：

x ⊩◊A 当且仅当 ∃y(R◊xy 且 y ⊩ A)

x ⊩□A 当且仅当 ∀y(R◊yx 蕴含 y ⊩ A)

剩余律：◊A ⊢ B 当且仅当 A ⊢ □B

我们已经看到，在最小逻辑中，关于组合及其剩余的框架语义的自然语言完备性并不会对合并关系 R⊗ 的解释施加限制。在纯剩余逻辑 ◊,□ 中，R◊ 也是如此。根据剩余律，可以很容易地推导出控制算子的单调性（A ⊢ B 蕴含 ◊A ⊢ ◊B 且 □A ⊢ □B）；它们的组合满足◊□A⊢A和A⊢□◊A。这些性质可用于改进词汇类型赋值，以便将选择依赖关系纳入考量。比较赋值A/B和A/◊□B的效果。前者在组合中会生成一个A类型的表达式，该表达式既包含B类型的表达式，也包含◊□B类型的表达式；而后者只会生成一个更具体的◊□B类型的表达式。类型为 □◊B 的表达式将无法与 A/B 或 A/◊□B 进行组合。Bernardi 和 Szabolcsi (2008) 提出了基于（推广的）该模态化策略的极性敏感表达式的许可和范围构造的说明。

对于◊,□ 的后续呈现，现在可以通过一元和二元树构建操作 (–) 和 (–,–)，从公式构建先行树结构。剩余模式由此衍生出以下左右引入规则。截断消除直接延续到扩展系统，并随之延续可判定性和子公式性质。

Γ[(A)] ⇒ B

Γ[◊A] ⇒ B

◊L

Γ ⇒ A

(Γ) ⇒ ◊A

◊R

Γ[A] ⇒ B

Γ[(□A)] ⇒ B

□L

(Γ) ⇒ A

Γ ⇒ □A

□R

控制结构资源管理。接下来，让我们讨论◊,□作为控制手段的使用。控制可以采取两种形式：一是授权访问一个如果全局可用就会过度生成的结构选项；二是偶尔阻止语法的结构能力。对于授权类型的控制，请将多模态提取处理（区分⊗c和⊗d）与下面的◊控制版本进行比较，后者依赖于单个二元组合操作，并将“移动”潜力完全缩小到◊标记的资源。

◊ 控制混合结合律：(A ⊗ B) ⊗ ◊C ⊢ A ⊗ (B ⊗ ◊C)

◊ 控制混合交换律：(A ⊗ B) ⊗ ◊C ⊢ (A ⊗ ◊C) ⊗ B

与非主语 np 假设相关的“什么”类型：wh/(s/◊□np)

下方的推导简图展示了逻辑推理和结构推理之间的相互作用。只要间隙子公式 ◊□np 满足许可条件 ◊，结构规则就适用；只要它找到了合适的结构位置，并被及物动词选中，它可以用作常规 np，因为类型转换 ◊□np ⊢ np 消除了先前解释中的包含假设。基于线性逻辑“！”模态的提取相关分析可以在 (Barry et al. 1991) 中找到，其中省略规则 !A ⊢ A 代替 ◊□A ⊢ A 来引入间隙。

⋮

因为 ◊□A ⊢ A

◊ 混合通信

◊ 混合关联

np ⊗ (((((np\s)/pp)/np) ⊗ np) ⊗ pp) ⊢ s

np ⊗ (((((np\s)/pp)/np) ⊗ ◊□np) ⊗ pp) ⊢ s

np ⊗ (((((np\s)/pp)/np) ⊗ pp) ⊗ ◊□np) ⊢ s

(np ⊗ ((((np\s)/pp)/np) ⊗pp)) ⊗ ◊□np ⊢ s

np ⊗ ((((np \ s) / pp) / np) ⊗ pp) ⊢ s / ◊□np

玛丽·普特对于必须阻止结构转换的控制类型，我们可以转向提取岛：不允许出现间隙的短语，例如修饰语。比较“玛丽在音乐会期间睡着了”与类型为 s\s 的修饰语短语“音乐会期间”以及格式错误的“我知道玛丽在——期间睡着了什么”。为了使修饰语无法访问，可以将“期间”指定为 (□(s\s))/np 类型：要消除 □，整个修饰语短语必须被结构◊ 包围，这便充当了提取的障碍。如果没有这样的障碍，如上所述的提取假设将导致格式错误的句子被导出。这种从词汇类型分配中投射岛状障碍的策略是由 Morrill 提出的；参见 Morrill 1994 年关于“结构抑制”的讨论。

本文阐述的控制算子的两种用法，引出了一个关于子结构沟通的普遍理论，该理论与范畴景观中不同类型的逻辑相关。假设源逻辑和目标逻辑是相邻的逻辑，它们在某些结构选项上有所不同，例如 NL 与 L，或 L 与 LP。Kurtonina 和 Moortgat (1997) 建立了一组嵌入定理，其形式如下：

翻译：μ : 源(/,⊗,\) → 目标(◊,□,/,⊗,\)，且

A ⊢ B 在源逻辑中可导当且仅当 μ(A) ⊢ μ(B) 在目标逻辑中可导

当目标逻辑比源逻辑更具判别力时，翻译会实现对许可类型的控制。当目标逻辑的判别力低于源逻辑时，则会实现另一个方向的通信。在这种情况下，翻译产生的模态修饰会阻碍结构规则的适用性。

框架约束，术语分配。纯剩余逻辑的框架语义不会对 R◊ 和 R⊗ 关系的解释施加限制。对于具有模态控制结构公设的扩展版本，每个结构公设都有一个框架约束，并且对于适当限制的框架，其完备性成立。

x y z

\ / |

s t

\ /

y t′

\ /

x s′