线性逻辑（一）

一、简介

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 一些历史

线性逻辑由 Jean-Yves Girard 在他的开创性著作中引入（Girard 1987）。虽然这种新逻辑的发现源于对系统 F（或多态 λ 演算）模型的语义分析，但我们可以将整个线性逻辑系统视为调和经典逻辑的美感和对称性的大胆尝试。德·摩根的二元性所提供的逻辑与对导致直觉逻辑的构造性证据的追求。

事实上，我们可以将线性逻辑的一个片段（称为乘法加性线性逻辑（MALL））作为两个简单观察的结果。

在经典逻辑的顺序演算表示中，连接词“与”和“或”的规则，以及剪切规则和蕴涵规则可以等价地以加法形式表示（前提的上下文相同） ）或乘法形式（前提的上下文不同）。在经典逻辑中，这两种表示是等效的，因为存在一些所谓的“结构”规则，即收缩和弱化。

Gentzen 使用序列微积分来捕获经典逻辑和直觉逻辑的证明，证明非构造性证明在序列的结论（后续）中使用了这些结构规则中的一个或另一个。

因此，如果我们想消除非构造性证明而不破坏后续演算的对称性，就像直觉逻辑中所做的那样，我们可以尝试消除收缩和弱化规则。这样做时，我们留下每个连接词的两个不同版本：合取和析取的加法版本和乘法版本。同一连接的这些不同版本现在不再等效。这些新连接词是 &（“with”，加法和）、⊕（“加”、加法或）、⊗（“张量”、乘法和）和 ⅋（“par”、乘法或）。

连接词的这种重复实际上导致了对经典逻辑和直觉逻辑之间的冲突的更清晰的理解。例如，排中律（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 et al. 1993) 和 IMELL (Dal Lago and Laurent 2008)。 Schellinx (1991) 提供了经典线性逻辑相对于相应的直觉变体的一些一般保守性结果：另见 (Troelstra 1992)。

在 1987 年引入线性逻辑之前，各种研究人员一直在研究各种子结构逻辑，其中并非所有 Gentzen 的结构规则（收缩、弱化和交换）都被接受。 Lambek 研究了一种连续微积分证明系统，其中没有任何结构规则被允许（Lambek 1958）。这种逻辑的其他例子是相关逻辑（其中不接受弱化）（Anderson & Belnap 1975，Anderson et al. 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)eq(!B⊗!C) 和 ?(B⊕C)eq(?B ⅋?C)，以及这些等价式的 0 进制版本，即 (!⊤≡1) 和 (?0≡⊥)。在这里，我们使用二元等价 B^C 来表示公式 (B−∘C)&(C−∘B) 在线性逻辑中是可导的。

2.1 序贯演算

下图展示了线性逻辑的双边序列微积分。请注意，这里否定被视为任何其他逻辑连接词：也就是说，它在公式中的出现不受限制，并且左右都有否定的引入规则。序列的左侧和右侧是公式的多重集：因此，这些上下文中公式的顺序并不重要，但它们的多重性确实很重要。

身份规则

B⊢B

初始化

Δ1⊢B,Γ1Δ2,B⊢Т2

Δ1,Δ2⊢Т1,Т2

切

否定规则

Δ⊢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) 产生（通过应用 &-right 引入规则）两个不同的相同世界（序列），除了 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）。

2.3 证明网

使用顺序微积分提出的证明包含许多有时无趣的细节：例如，考虑有多少种无趣的不同方法可以从⊢Γ,A1,A2,…,An 的导数。这个令人不愉快的事实源于序列微积分中证明的序列性质：如果我们想要将一组 S（包含 n 个规则）应用于序列的不同部分，我们就无法一步应用它们，即使它们不会相互干扰！我们必须对它们进行排序，即在 S 上选择一个线性顺序，并根据这个顺序分 n 步应用规则。

一个自然的问题出现了：“是否存在从这些无趣细节中抽象出来的证明表示？”。在直觉序贯微积分的情况下，通过所谓的自然演绎，可以肯定地回答类似的问题，通过柯里-霍华德对应关系（Howard 1980），自然演绎与称为 λ 演算的计算设备有很强的联系。

对于线性逻辑，证明的这种简洁表示是由证明网给出的，这种类似图形的结构对于逻辑的 MLL 片段具有特别好的属性。实现这种表示的第一步是使用否定的对合性将所有序列微积分系统转换为单侧系统，其中序列的形式为⊢Γ。结果，由于我们没有左引入规则，规则的数量减少了，但我们保持了相同的表达能力，因为可证明性保持不变。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。