线性逻辑

线性逻辑是由法国数学家让-伊夫·吉拉尔于1987年提出的一种子结构逻辑。它通过限制传统逻辑中的结构规则（如收缩和弱化），将逻辑联结词视为对逻辑资源的操作，从而更精细地刻画计算中的资源使用。

1. 基本动机：逻辑作为资源管理

• 在经典逻辑或直觉主义逻辑中，命题可以无限次使用。例如，若拥有命题 \(A \to B\) 和 \(A\)，可多次推导出 \(B\)，这隐含了资源的可复制性（收缩规则）和可丢弃性（弱化规则）。
• 线性逻辑的核心理念是将命题视为不可任意复制或丢弃的"资源"。例如，在物理系统或程序执行中，一条数据或一个计算步骤可能只能使用一次。
• 关键思想：将逻辑联结词分为两类——可乘性（乘性联结词，如 \(\otimes\)、\(\multimap\)）和加性（加性联结词，如 \(\&\)、\(\oplus\)），分别对应资源的不同组合方式。

2. 线性逻辑的联结词及其含义

• 可乘性联结词（关注资源的并行组合）：
  • 张量积（\(\otimes\)）：表示同时拥有两个资源。例如，\(A \otimes B\) 意味同时持有资源 \(A\) 和 \(B\)。
  • 线性蕴含（\(\multimap\)）：\(A \multimap B\) 表示消耗一个资源 \(A\) 可产生一个资源 \(B\)。使用后 \(A\) 被消耗，不可重用。
  • 单位元（\(\mathbf{1}\)）：表示空资源，是 \(\otimes\) 的单位元（即 \(A \otimes \mathbf{1}\) 等价于 \(A\)）。
• 加性联结词（关注资源的选择性使用）：
  • 与（\(\&\)）：表示对同一资源可做两种选择。例如，持有 \(A \& B\) 意味可任意选择使用 \(A\) 或 \(B\)，但只能选其一（资源不复制）。
  • 直和（\(\oplus\)）：表示拥有两种可能性之一。例如，\(A \oplus B\) 表示要么有 \(A\)，要么有 \(B\)，但具体是哪一个需由上下文决定。
  • 顶（\(\top\)）：加性的单位元，表示无信息资源（任何语境下皆可成立）。
• 指数模态（！和？）：用于恢复有限度的结构规则。
  • 模态词 \(!A\)（读作"of course A"）：表示资源 \(A\) 可被任意次复制或丢弃。它允许收缩（复制）和弱化（丢弃）规则仅作用于标记了 \(!\) 的公式。
  • 对偶模态 \(?A\)（读作"why not A"）：在经典线性逻辑中与 \(!\) 通过对偶性关联。

3. 证明规则示例：线性蕴含的演绎

• 线性逻辑的序列演算规则严格反映资源流动：
  • \(\multimap\) 引入规则（右规则）：

\[ \frac{\Gamma, A \vdash B}{\Gamma \vdash A \multimap B} \]

表示若从资源集合 \(\Gamma\) 加上 \(A\) 能推出 \(B\)，则仅从 \(\Gamma\) 可推出 \(A \multimap B\)（注意 \(A\) 在前提中被消耗）。

• \(\multimap\) 消去规则（左规则）：

\[ \frac{\Gamma \vdash A \quad \Delta, B \vdash C}{\Gamma, \Delta, A \multimap B \vdash C} \]

表示若 \(\Gamma\) 提供 \(A\)，且 \(\Delta\) 和 \(B\) 能推出 \(C\)，则合并 \(\Gamma\) 和 \(\Delta\) 并消耗 \(A \multimap B\) 可推出 \(C\)。

4. 与计算的联系：证明-程序对应

• 线性逻辑通过 Curry-Howard 对应与计算模型紧密关联：
  • 线性逻辑的证明可解释为程序，其中公式对应类型，证明简化对应程序执行。
  • 例如，可乘性联结词 \(\otimes\) 对应并行计算中的资源对，而线性蕴含 \(\multimap\) 对应一次性的函数（如线性λ演算中的函数，其参数必须恰好使用一次）。
  • 指数模态 \(!A\) 对应可复制的值（如编程中可多次引用的数据），这允许在线性框架内嵌入直觉主义逻辑。

5. 应用与扩展

• 编程语言：线性逻辑启发了线性类型系统（如 Rust 语言中的所有权机制），确保内存安全而无垃圾回收。
• 并发理论：π-演算等进程演算可通过线性逻辑的证明结构建模通信协议。
• 量子计算：线性逻辑的不可复制性与量子比特的不可克隆定理天然契合，用于形式化量子程序逻辑。

线性逻辑通过将"资源意识"引入逻辑推理，提供了分析计算过程的精细工具，其思想已渗透到程序语言理论、并发验证和量子计算等多个领域。