线性逻辑（一）
线性逻辑是对经典逻辑和直觉逻辑的改进。它不像经典逻辑那样强调真，也不像直觉逻辑那样强调证明，而是强调公式作为资源的作用。为了实现这一目标，线性逻辑不允许将通常的收缩和弱化结构规则应用于所有公式，而只允许那些标有特定模态的公式。线性逻辑包含完全对合的否定，同时保持了强构造性解释。线性逻辑还为经典逻辑和直觉逻辑中证明的本质提供了新的见解。由于线性逻辑注重资源，它在计算机科学中得到了广泛的应用。
1. 引言
1.1 历史回顾
1.2 线性逻辑与计算机科学
2. 证明系统
2.1 后继演算
2.2 聚焦证明搜索
2.3 证明网
3. 语义学
3.1 可证性语义学
3.2 证明语义学
4. 复杂性
5. 计算机科学的影响
5.1 证明规范化
5.2 证明搜索
6. 变体
6.1 模态的不同处理
6.2 非交换线性逻辑
6.3 无界行为的处理
参考文献
学术工具
其他网络资源
相关文章
1. 引言
1.1 历史回顾
线性逻辑由 Jean-Yves Girard 在其开创性著作 (Girard 1987) 中提出。虽然这种新逻辑的发现源于对系统 F（或多态 λ 演算）模型的语义分析，我们可以把整个线性逻辑体系看作是一种大胆的尝试，旨在调和德·摩根对偶性所提供的经典逻辑的美感和对称性，以及对导致直觉主义逻辑的构造性证明的追求。
事实上，我们可以将线性逻辑的一个片段，称为乘法加法线性逻辑（MALL），作为两个简单观察的结果。
在经典逻辑的后序演算表示中，连接词“与”和“或”的规则，以及Cut规则和蕴涵规则，可以等价地以加法形式（前提上下文相同）或乘法形式（前提上下文不同）表示。在经典逻辑中，这两种表示是等价的，因为存在一些所谓的“结构化”规则，即收缩和弱化。
根岑运用相继式演算来概括古典逻辑和直觉逻辑的证明，表明非构造性证明在相继式的结论（后件）中会运用其中一种结构规则。
因此，如果我们想消除非构造性证明，同时又不破坏相继式演算的对称性（就像直觉逻辑中所做的那样），我们可以尝试消除收缩规则和弱化规则。这样做，我们会得到每个连接词的两个不同版本：与运算和析取运算的加法版本和乘法版本。同一连接词的这些不同版本现在不再等价。这些新的连接词是 &（“与”，加法与）、⊕（“加”，加法或）、⊗（“张量”，乘法与）和⅋（“平分”，乘法或）。这种联结词的重复实际上使我们对经典逻辑和直觉逻辑之间的冲突有了更清晰的理解。例如，排中律（A或非A）在经典逻辑中被认为是有效的，而在直觉逻辑中则被认为是荒谬的。但在线性逻辑中，这条律有两种解读：加法版本（A⊕¬A）是不可证明的，对应于直觉主义对析取的解读；乘法版本（A⅋¬A）很容易证明，并且仅仅对应于在直觉主义逻辑中也完全可以接受的重言式（A蕴含A）。
此外，建构主义中必不可少的析取性质，在加法析取中很容易建立。
因此，我们在这种更丰富的逻辑中找到了一种方法，既能表示直觉主义的需求，又能表示经典逻辑的优雅：否定是对合的，后项是对称的，联结词是可相互定义的。将这些性质与直觉逻辑的性质进行对比，直觉逻辑的否定不具有对合性，后项不具有对称性，并且连接词¬、∧、∨、⇒均不可相互定义。
请注意，一旦消除了收缩规则和弱化规则，公式就不再具有真值性质。事实上，如果我们在不使用这些结构规则的情况下组合 A⇒B 的证明和 A 的证明，我们会消耗它们来得到 B 的证明：也就是说，组合之后 A⇒B 和 A 不再可用。线性逻辑公式的行为更像是只能以受限方式使用的资源。
为了恢复直觉逻辑和经典逻辑的全部表达能力，需要在 MALL 片段中添加两个对偶模态，它们在线性逻辑文献中通常被称为指数函数。具体而言，“当然”指数 ! 允许在左侧序列上下文中对公式 !B 进行收缩和弱化，而“为什么不”指数 ? 允许在右侧序列上下文中对公式 ?B 进行收缩和弱化。这引出了完整的命题线性逻辑，并与计算机科学建立了非常紧密的联系。
请注意，除了 MALL 之外，还有另外两种广泛使用的线性逻辑片段：乘法线性逻辑 (MLL)，它是没有加法连接词的 MALL；乘法指数线性逻辑 (MELL)，它是没有加法连接词的线性逻辑。
Gentzen 的直觉逻辑的序列演算证明系统是对其用于经典逻辑的序列演算进行限制的结果，使得所有序列在序列的右侧最多包含一个公式 (Gentzen 1935)。这种单一结论限制也可以在线性逻辑的背景下进行探索。许多研究人员已经考虑了MLL、MALL和MELL的直觉主义变体：例如，IMLL（Lamarche，1996）、IMALL（Lincoln等人，1993）和IMELL（Dal Lago和Laurent，2008）。Schellinx（1991）提供了一些经典线性逻辑相对于相应直觉主义变体的普遍保守性结果：另见（Troelstra，1992）。
在1987年线性逻辑被引入之前，许多研究人员一直在研究各种子结构逻辑，其中并非所有Gentzen的结构规则（收缩、弱化和交换）都被接受。Lambek研究了一个序贯演算证明系统，其中这些结构规则均不被接受（Lambek，1958）。此类逻辑的其他例子是相关逻辑（其中不接受弱化）（Anderson & Belnap 1975，Anderson 等。1992，Avron 1988，Read 1988）。以及仿射逻辑（其中不接受收缩）（Grishin 1981）。
1.2 线性逻辑与计算机科学
直觉逻辑和构造性逻辑在计算机科学中的应用始于人们发现将 A⇒B 理解为“如果你给我一个 A，我会给你一个 B”的可能性，这与经典的“A 为假或 B 为真”的理解截然不同。
线性逻辑对蕴涵“A⇒B”的解释进行了进一步的扭曲：现在它可以理解为“给我尽可能多的 A，我会给你一个 B”。计算理念中至关重要的“复制”概念现在被嵌入到逻辑中。这种新观点开辟了新的可能性，包括：
表达精细运算性质的新公式，例如“给我一次 A，我会给你 B”。这里的应用范围很广，从利用线性逻辑表示状态能力的精细逻辑编程（Hodas & Miller，1994），到经典逻辑及其计算解释的分析（Abramsky，1993），再到编程语言中异常机制的规范（Miller，1996），以及线性分析（Wadler，1991）。
表达对副本使用约束的新规则，从而产生用于多项式时间计算的线性逻辑片段，这仅仅是最引人注目的应用（Baillot & Terui，2004，Baillot，2015）。
表示证明的新方法（Abramsky & Jagadeesan，1994，Girard，1987）。
2. 证明系统
线性逻辑的核心命题连接词分为加法连接词和乘法连接词。经典的合取及其恒等式 ∧ 和 ⊤ 可以分解为加法运算符 &（与）和 ⊤（上）以及乘法运算符 ⊗（张量）和 1（一）。类似地，经典析取及其恒等式 ∨ 和 ⊥ 分解为加法 ⊕ (oplus) 和 0（零）以及乘法 ⅋ (par) 和 ⊥（底部）。在线性逻辑的表示中，否定通常以两种方式之一处理。否定可以被视为原始命题联结词，其在公式中的出现不受限制。由于否定与所有命题联结词、指数和量词之间存在德摩根对偶，因此也可以将否定视为仅在原子公式中出现的特殊符号。蕴涵也通常通过定义引入线性逻辑：线性蕴涵 B−∘C 可以定义为 B⊥⅋C，而直觉蕴涵 B⇒C 可以定义为 !B−∘C。算符 ! 和 ? 被称为模态函数或指数函数。 “指数”一词尤为贴切，因为遵循指数、加法和乘法之间的通常关系，线性逻辑支持等价关系 !(B&C)≡(!B⊗!C) 和 ?(B⊕C)≡(?B⅋?C)，以及这些等价关系的零元版本，即 (!⊤≡1) 和 (?0≡⊥)。这里，我们使用二元等价关系 B≡C 来表示公式 (B−∘C)&(C−∘B) 在线性逻辑中是可导的。
2.1 序贯演算
下图展示了线性逻辑的双边序贯演算。注意，这里将否定视为任何其他逻辑连接词：也就是说，它在公式中的出现不受限制，并且否定的左右两侧都有引入规则。后项的左侧和右侧是公式的多集：因此，在这些上下文中公式的顺序无关紧要，但它们的多重性很重要。
恒等式规则
B⊢B
init
Δ1⊢B,Γ1Δ2,B⊢Γ2
Δ1,Δ2⊢Γ1,Γ2
cut
否定规则
Δ⊢B,Γ
Δ,B⊥⊢Т
(·)⊥L
Δ,B⊢γ
Δ⊢B⊥,Γ
(·)⊥R
乘法规则
Δ⊢γ
Δ,1⊢γ
1升
⊢1
1R
⊥⊢
⊥L
Δ⊢γ
Δ⊢⊥,γ
⊥R
Δ,B1,B2⊢γ
Δ,B1⊗B2⊢Γ
⊗L
Δ1⊢B1,Т1Δ2⊢B2,Т2
Δ1,Δ2⊢B1⊗B2,伽马1,伽马2
⊗R
Δ1,B1⊢γ1Δ2,B2⊢γ2
Δ1,Δ2,B1⅋B2⊢Г1,Г2
⅋L
Δ⊢B1,B2,伽马
Δ⊢B1⅋B2,Γ
⅋R
加法规则
Δ,0⊢γ
0升
Δ⊢⊤,γ
⊤R
Δ,Bi⊢Γ
Δ,B1&B2⊢Γ
&L (i=1,2)
Δ⊢B1,ТΔ⊢B2,Т
Δ⊢B1&B2,Γ
与研究
Δ,B1⊢ТΔ,B2⊢Т
Δ,B1⊕B2⊢Γ
⊕L
Δ⊢Bi,Γ
Δ⊢B1⊕B2,Γ
⊕R (i=1,2)
量词规则
Δ,B[t/x]⊢Γ
Δ,∀x.B⊢Γ
∀L
Δ⊢B[y/x],Γ
Δ⊢∀x.B,Γ
∀R
Δ⊢B[t/x],Γ
Δ⊢∃x.B,Γ
∃R
Δ,B[y/x]⊢Γ
Δ,∃x.B⊢Γ
∃L,
指数规则
Δ⊢γ
Δ,!B⊢Γ
！W
Δ,!B,!B⊢Γ
Δ,!B⊢Γ
!C
Δ,B⊢γ
Δ,!B⊢Γ
!D
!Δ⊢B,?Γ
!Δ⊢!B,?Γ
!R
Δ⊢γ
Δ⊢?B,Γ
?W
Δ⊢?B,?B,Γ
Δ⊢?B,Γ
?C
Δ⊢B,Γ
Δ⊢?B,Γ
?D
!Δ,B⊢?Γ
!Δ,?B⊢?Γ
?L
请注意，弱化规则和收缩规则仅适用于在后项左侧标有指数!或在右侧标有?的公式。?R 和 !L 规则通常被称为“遗弃”规则。?L 和 !R 规则通常被称为“提升”规则，类似于处理 S4 模态逻辑 (Ono 1998) 中使用的后项演算规则。∀-右和∃-左引入规则的通常条件是：特别是，变量 y 在这些推理规则的较低后项公式中不能是自由的。此处的量化假设为一阶的。Girard 在其 1987 年的论文中提出了一种高阶版本的线性逻辑。
可以省略切割规则，同时仍然保持完备性。对偶地，除了涉及原子公式的 init 规则外，也可以省略 init 规则。
2.2 焦点证明
Andreoli (1992) 提出了一个关于无切割证明结构的重要范式定理。如果非原子公式的顶层逻辑连接词为 ⊤, &, ⊥,⅋, ?，他将非原子公式归类为异步公式。或∀，或同步，如果其顶层逻辑联结词为0、⊕、1、⊗、!或∃。
当将证明搜索视为计算模型时，我们考虑推理规则如何将后继项作为其结论转化为前提。因此，我们可以将后继项中的公式视为“代理”，它们可以独立行动，也可以与其环境中的其他代理协同行动。在这里，这些代理的行为是通过自下而上地读取它们的引入规则来确定的。如果异步公式出现在后继项的右侧，它可以在不影响可证明性且不与其上下文交互的情况下演化，即相应的引入规则是可逆的。例如，代理 (B⅋C)（通过应用⅋-右引入规则）变成两个代理 B 和 C（现在并行工作）。类似地，代理（B&C）通过应用 &-右引入规则，生成两个不同的相同世界（后继项），只不过 B 位于其中一个世界，而 C 位于另一个世界。
另一方面，如果我们将同步公式视为一个代理，其演化取决于自下而上地解读相应的右引入规则，那么可证明的后继项就有可能演化为不可证明的后继项（例如，通过应用 ⊕ 右引入规则）。此外，此类推理规则的实例取决于公式上下文的细节。例如，1-右引入规则的成功要求周围上下文为空，而 ⊗-右引入规则的成功取决于代理的周围上下文如何划分为两个上下文。因此，此类代理的演化依赖于与上下文其他部分的“同步”。现在考虑一个线性逻辑的单侧序贯演算表示，其中唯一的引入规则是右引入规则。鉴于上述连接词的分类，可以证明证明搜索可以构建为以下几个阶段而不失完整性。如果序贯演算中存在异步公式，则进入异步阶段。在此阶段，右引入规则以任意顺序应用（自下而上），直到不再有异步公式。在同步阶段，选择某个同步公式并成为此阶段的“焦点”：也就是说，右引入规则将（自下而上）应用于该公式以及它可能生成的任何同步子公式。
下图展示了线性逻辑的聚焦证明系统。注意，这两个阶段用不同的箭头表示：向上箭头表示异步阶段，向下箭头表示同步阶段。此外，序贯演算被分为三个区域（每个区域由分号或向上或向下箭头分隔）。具体来说，上下箭头左侧是两个区域。记为 Ψ 的区域表示一组公式，这些公式可以在该后序的证明中使用任意次数。记为 Δ 的区域表示公式的多重集。向上箭头右侧的区域也是一个公式多重集，而向下箭头右侧的区域则是一个公式。由于异步公式的引入可以按任意顺序进行，因此可以对向上箭头右侧的公式施加任意顺序。原子被赋予极性，在下图中，A 代表正原子，A 的负号代表负原子。由这些推理规则构建的证明称为焦点证明。Andreoli (1992) 证明了线性逻辑焦点证明的完备性。
异步阶段
Ψ;Δ⇑L
Ψ;Δ⇑⊥,L
[⊥]
Ψ,F;Δ⇑L
Ψ;Δ⇑?F,L
[?]
Ψ;Δ⇑⊤,L
[⊤]
Ψ;Δ⇑F[y/x],L
Ψ;Δ⇑∀x.F,L
[∀]
Ψ;Δ⇑F1,F2,L
Ψ;Δ⇑F1⅋F2,L
[⅋]
Ψ;Δ⇑F1,LΨ;Δ⇑F2,L
Ψ;Δ⇑F1&F2,L
[&]
Ψ;Δ,F⇑L
Ψ;Δ⇑F,L
[R⇑] 假设 F 不是异步的
同步阶段
Ψ;⋅⇓1
[1]
Ψ;Δ1⇓F1Ψ;Δ2⇓F2
Ψ;Δ1,Δ2⇓F1⊗F2
[⊗]
Ψ;⋅⇑F
Ψ;⋅⇓!F
[!]
Ψ;Δ⇓Fi
Ψ;Δ⇓F1⊕F2
[⊕i]
Ψ;Δ⇓F[t/x]
Ψ;Δ⇓∃x.F
[∃]
Ψ;Δ⇑F
Ψ;Δ⇓F
[R⇓] 假设 F 要么是异步的，要么是原子的
身份与判决规则
Ψ;A⇓A⊥
[I1]
Ψ,A;⋅⇓A⊥
[I2] 其中 A 为原子
Ψ;Δ⇓F
Ψ;Δ,F⇑⋅
[D1]
Ψ;Δ⇓F
Ψ,F;Δ⇑⋅
[D2] 其中 F 为正公式
经典逻辑和直觉逻辑也设计了聚焦证明系统 (Danos et al. 1997; Laurent et al. 2005; Liang & Miller 2009)。
