第16章：线性逻辑与资源——每个假设只能用一次

经典逻辑默认资源无限。这是一个谎言，而且是一个代价高昂的谎言。

第15章留下了一个令人不安的结论：只要系统足够强，就一定存在它无法证明的真命题；系统本身也无法担保自己的一致性。这是哥德尔的礼物——或者说，他的诅咒。

但"足够强"是什么意思？强在哪里？

一个形式系统之所以强大，部分原因在于它的假设可以被任意重复使用。你知道 P，就可以用 P 一百次——它不会磨损，不会耗尽，永远在那里等你调取。这个能力对应第14章里悄悄列出的一条结构规则：收缩。收缩说的是：一份假设和两份假设，在推断中是等价的。多余的，可以折叠。

这条规则看起来是常识。但它是可以质疑的。

1987 年，让-伊夫·吉拉尔（Jean-Yves Girard）问了一个简单的问题：如果拿掉收缩规则，会发生什么？

发生的事情远比他最初预期的要多。他得到的不只是一个削弱版的经典逻辑，而是一个全新的逻辑——线性逻辑——它精确地描述了资源被消耗的世界。

16.0 一次性厨房游戏：每份资源只能用一次

经典逻辑像一个奇怪的厨房：你有一枚鸡蛋，却可以同时煎一百个蛋卷。因为在经典逻辑里，假设不会被消耗。你用了一次 A，A 还在；再用一次，还是在。这对“知识”也许合理，对“资源”却荒谬。

所以我们换一个厨房。

桌上有若干张食材卡：鸡蛋 A、面粉 B、黄油 C。每条菜谱是一条线性蕴含，例如

意思是：消耗一份 A 和一份 B，得到一道菜 D。一旦用掉，食材卡就从桌面消失。你不能凭空复制鸡蛋，也不能把已经用掉的黄油再拿回来。除非某张卡前面有一个特殊标记 !A，表示它不是普通资源，而是可以重复调用的知识。

这就是线性逻辑的游戏感：推理不再只是“从真推出真”，而是“在资源守恒下完成转换”。

:::details 这个游戏的形式化骨架

• 状态空间：资源多重集，例如 \Gamma = \{A, A, B, !C\}。重复出现的 A 是两份真实资源，不是一个符号写了两遍。
• 合法动作：按线性规则消耗资源并生成新资源；只有 !A 可以复制或丢弃。
• 转移规则：若有菜谱 A \otimes B \multimap D，则状态 \Gamma, A, B 可转移为 \Gamma, D。
• 胜利条件：用有限资源构造目标资源 G。
• 失败模式：目标看似能推出，但你在中途偷偷复用了已经消耗的假设。
  :::

这个游戏会迫使读者看见经典逻辑藏起来的东西：推理有时是有物理代价的。在程序里，内存不是无限的；在通信协议里，消息发出去就不能同时留在原地；在量子系统里，未知量子态不能任意克隆。

线性逻辑不是经典逻辑的怪异变体。它是在提醒我们：经典逻辑默认了一个富得离谱的世界，在那里资源可以免费复制。现实世界没有这么慷慨。

::: info 兔狲教授评
一次性厨房游戏的规则很简单：用掉就是用掉。很多抽象逻辑一落到现实里都会撞上这句话。你不能用一张五元纸币买两杯咖啡，也不能用一份显存装两个互不释放的模型。经典逻辑忘了这件事，线性逻辑把账单递回来了。
:::

16.1 收缩规则在干什么

回忆收缩规则的形式：

横线上：上下文里有两份 A，能推出 B。横线下：只有一份 A，也能推出 B。

这条规则说的是：你知道 A，可以把它用任意多次，而不需要为每次使用"付出"一份 A。

在经典逻辑里，这完全合理。知识不是物质，你知道"1+1=2"，用它一百次，它还在那里，一点没少。

但世界上不是所有"前提"都是知识。

考虑这个句子："我有一张五元钱，可以买一杯咖啡。"

这是一个完全合法的命题推断：有五元钱 \to 可以买咖啡。

但如果你对这个命题应用收缩，就得到：有一张五元钱，可以买两杯咖啡。这显然错了。那张钱被用掉了。

经典逻辑对这种错误无能为力，因为它根本不区分"可以重复使用的知识"和"使用后消耗的资源"。线性逻辑的出发点正是：这两种东西根本不一样，需要不同的符号和不同的规则。

::: info 兔狲教授评
经典逻辑处理知识，线性逻辑处理资源——这个区分是真实的，不是花哨的哲学。你写程序的时候内存会耗尽，量子态不能克隆，协议里的消息发出去就没了。经典逻辑对这些场景的建模从一开始就是错的。不是近似错误，是根本错误。
:::

::: info 逻辑是在描述世界，还是在规范推断？

这里有一个哲学分歧值得停下来想一想。有人会说：逻辑不是在描述资源消耗，它是在谈论真值，而真值不会被"使用"耗尽。这个观点没有错——经典逻辑确实是关于真值的。

但线性逻辑选择了另一种立场：逻辑是在规范推断的合法性，而推断发生在一个有代价的世界里。不是每个"已知"都可以免费重复使用。如果你想用一个资源，你必须为它付出代价。这不是对经典逻辑的否定，而是它的推广——经典逻辑是线性逻辑加上"资源可以任意复制"这个特殊假设之后的退化版本。
:::

16.2 线性逻辑的符号体系

去掉收缩，逻辑的结构就改变了。最明显的变化是：你不能再随意"合并"两个假设，因为它们的计数开始变得重要。

线性逻辑引入了一套与经典逻辑平行但含义不同的连接词。

乘法连接词 \otimes（张量积）：A \otimes B 表示"同时拥有 A 和 B"，而且这两份资源都是真实存在的，各占一份。如果要从 A \otimes B 推出某个结论，必须同时消耗 A 和 B 两份资源。它对应的是"并行使用"——两件事同时发生。

加法连接词 \&（with）：A \,\&\, B 表示"拥有 A 和 B 两个选项，可以选择使用其中一个"。但只能选一个——资源在被选择的那一刻决定去向。它对应的是"选择"——两件事只发生一件。

乘法析取 ⅋（par）：线性逻辑的对偶连接词，对应乘法合取的否定形式。

加法析取 \oplus（plus）：A \oplus B 表示"拥有 A 或 B 其中之一，但不知道是哪个"——这是信息匮乏的表达，而不是可选择的丰盈。

:::details 线性逻辑的四个连接词：用"点菜"来理解（前人工作：Girard, 1987）
线性逻辑里多出来的连接词，用餐厅点菜来类比最清楚：

为什么要区分 \otimes 和 \&？ 在经典逻辑里，"有 A 和 B"只有一种说法（A \land B），因为资源可以复制，"同时拥有"和"可以选择"没有区别。线性逻辑去掉了复制，这两种"拥有"就必须精确区分。
:::

这四个连接词构成两组对称的配对，背后有一个深刻的对偶结构：乘法连接词是关于资源的并发存在，加法连接词是关于资源的可选择性。

::: info 为什么要有这么多连接词？

经典逻辑里只需要两个基本连接词（比如 \neg 和 \to）就能表达一切。线性逻辑需要四个，感觉冗余。但这四个之所以无法合并，是因为它们在资源意义上真的不同：同时拥有 vs. 可以选择，这两件事在经典逻辑里被"收缩"规则抹平了差异——既然知识可以无限复制，"同时拥有"和"可以选择"就没有区别了。一旦去掉收缩，这个差异就必须被精确区分，否则逻辑就会丢失信息。
:::

16.3 感叹号：可以重复使用的资源

但如果所有假设都只能用一次，我们就无法谈论真正的知识——那些确实可以重复引用的事实。线性逻辑通过一个特殊符号解决这个问题：感叹号 !A（读作"当然 A"，of course A）。

!A 的含义是：A 是一个无限可用的资源。你拥有 !A，就意味着可以随时从中取出 A，取多少次都行，不会耗尽。

形式地，!A 满足一组特殊规则：

• 弱化：!A \vdash \mathbf{1}（!A 可以被丢弃——你不需要用它）
• 收缩：!A \vdash !A \otimes !A（!A 可以被复制——你可以把它用两次）
• 推广：如果 !A \vdash B，那么 !A \vdash !B（从无限资源推出的结论，也是无限可用的）

用了感叹号之后，线性逻辑就能恢复对经典推理的模拟：如果所有假设都带上 !，整个系统退化为经典逻辑。感叹号是线性逻辑和经典逻辑之间的桥梁——它精确地标出了哪些假设在经典意义上可以任意使用，哪些是真正的一次性资源。

::: info 兔狲教授评
很多人到这里会说"好的，! 就是把资源变成知识"。等一下——你有没有意识到：在线性逻辑里，"可以重复使用"是一个需要被明确声明的特权，不是默认的权利？这个颠覆比大多数人意识到的要彻底得多。经典逻辑里每条假设默认带着隐形的 !，而你从来不知道。
:::

16.4 蕴含的含义变了

去掉收缩之后，蕴含 A \to B 也分裂成两种意思，需要精确区分。

线性蕴含 A \multimap B（读作 A 线性蕴含 B，或"A 变换为 B"）表示：消耗恰好一份 A，产生一份 B。

这不是知识的传递，而是资源的转换。五元钱 \multimap 一杯咖啡。这是线性逻辑能正确表达的推断——使用之后，那张五元钱就消失了，换成了咖啡。

相比之下，经典逻辑里的 A \to B 不消耗 A——你知道了 A，推出了 B，但 A 还在那里，可以继续用。要在线性逻辑里表达经典蕴含，需要写 !A \multimap B：从无限可用的 A 中取一份，生产一份 B，而 !A 本身毫发无损。

这个区分揭示了"知识"和"资源"的本质差异：知识是 !A 型的——使用后不减少；资源是裸 A 型的——使用后就消耗。经典逻辑没有这个区分，因为它假设所有前提都是知识。

16.5 三个现实的对应

线性逻辑不是逻辑学家的纯思想实验。它精确地对应了三个重要的现实。

内存管理。 在程序设计里，内存是资源：分配一块内存，用完必须释放，否则就泄漏了。经典逻辑对内存的直觉是错的——它假设你"知道"一块内存，可以无限引用，但内存在被释放之后就不存在了。线性类型系统（如 Rust 的所有权系统）的核心，正是线性逻辑：每个变量恰好拥有一次，传递所有权就是消耗一份假设，借用就是使用 ! 修饰的临时视图。线性逻辑给出了 Rust 所有权机制的形式语义。

量子计算。 量子力学有一条著名的禁令：不可克隆定理。一个未知的量子态不能被完美复制。在逻辑语言里，这正是"不允许收缩"——量子比特是线性资源，不能从 \psi 变出两份 \psi。量子计算的计算模型天然地生活在线性逻辑里，量子电路是线性推断序列。

并发协议。 两个进程之间的通信协议，可以被精确地编码为线性逻辑命题。协议的"一方发送，另一方接收"恰好是线性蕴含：资源从一侧转移到另一侧，不可复制，不可丢弃。会话类型（Session Types）正是这个对应关系的工程实现，它允许编译器在类型检查阶段验证协议的正确性——逻辑保证了协议不会死锁，不会遗漏消息。

::: info Curry-Howard 对应的延伸

第14章提到，证明和程序在结构上是同构的（这个对应关系在第22章会正式展开）。线性逻辑把这个对应关系推进了一步：线性证明对应线性程序——每个变量恰好使用一次的程序。这不是意外的巧合，而是因为线性逻辑在设计上就是为了捕捉"计算是消耗资源的过程"这个直觉。Girard 最初发现线性逻辑，正是在分析 System F（多态 λ-演算）的证明结构时——他在逻辑的深处发现了资源的痕迹。
:::

16.6 两种真值：占有与选择

线性逻辑还引出了一个更基本的哲学转变："真"不再只有一种意思。

在经典逻辑里，A 为真就是 A 为真，就这一种情况。

在线性逻辑里，"拥有 A"可以是两种不同的事情：

• 张量式拥有：A \otimes B——你同时拥有 A 和 B 两个独立资源。
• 加法式拥有：A \,\&\, B——你拥有两个选项，可以决定用哪一个。

这两种"拥有"在资源经济学里有完全不同的价值。我有一个苹果和一个梨，不等于我有"可以选苹果或梨"的能力——前者是两份资源，后者是一份资源加上一个选择权。

经典逻辑把这两种情况混为一谈，因为在真值层面，"A 和 B 都为真"等价于"A 为真，或者 B 为真，而且两者都是真"——说的是同一件事。但一旦资源有计数，这两件事就截然不同了。

这个区分，将在第17章里以一种完全出乎意料的方式重新出现：当真值本身变成一个连续区间 [0,1]，"同时拥有"和"可以选择"的区别就变成了概率的乘法规则和贝叶斯更新的两种不同模式。

16.7 过渡：在真值变成连续之前——三值逻辑作为热身

第17章要做一件激进的事：把真值从 \{0, 1\} 扩张到 [0, 1]。在这之前，先做一个小实验：如果真值有三个值，而不是两个，会发生什么？

波兰逻辑学家 Łukasiewicz 在1920年提出了三值逻辑。真值集合是 \{0, \frac{1}{2}, 1\}，其中 \frac{1}{2} 表示"不确定"。连接词的规则如下：

否定：\neg 0 = 1，\neg \frac{1}{2} = \frac{1}{2}，\neg 1 = 0

合取：a \land b = \min(a, b)

析取：a \lor b = \max(a, b)

蕴含：a \to b = \min(1,\ 1 - a + b)

（蕴含的规则是三值逻辑里最反直觉的部分，多看几眼。当 a = 1, b = 0 时得到 0——和经典逻辑一致；当 a = \frac{1}{2}, b = 0 时得到 \frac{1}{2}——"从不确定推出假，结论也是不确定"。）

练习： 用上面的规则，计算以下命题在所有三种真值赋值组合下的值。设 P = \frac{1}{2}（不确定），Q = 0（假）。

1. P \to Q
2. \neg Q \to \neg P（逆否命题）
3. P \lor \neg P（排中律）

第3个问题最有意思：在经典逻辑里，P \lor \neg P 是重言式，永远为真。在三值逻辑里，当 P = \frac{1}{2} 时，\neg P = \frac{1}{2}，所以 P \lor \neg P = \max(\frac{1}{2}, \frac{1}{2}) = \frac{1}{2}。

排中律，在三值逻辑里，不再是重言式。

这不是一个技术细节。它意味着：当你把"真值"扩张，你就在隐含地修改你愿意接受的推断规则。三值逻辑拒绝排中律；经典逻辑接受它。这不是哪个更"正确"，而是两种不同的选择，对应不同的推断合法性理解。

回到一次性厨房游戏，本章真正改变的不是菜谱名字，而是厨房的物理法则。经典逻辑的厨房默认食材可以无限复制；线性逻辑把食材重新变成会消耗的东西；三值逻辑则进一步暗示，连“熟了/没熟”这种二分判断都可以被第三种状态打断。每一次改变状态空间，都会改变合法动作。

第17章要做的事，是把这个方向推到极致：真值不是三个点，而是 [0, 1] 上的连续区间。届时，推断规则会变成什么？

悬而未决

线性逻辑里的"真"是什么？ 在经典逻辑里，语义很清楚：命题要么真要么假，真值表给出一切。在线性逻辑里，资源的"语义"是什么？如何定义一个模型，使得"A 为真"意味着某种具体的资源占有？这个问题的答案是相位语义（Phase semantics）和相干空间（Coherence spaces），但它们都指向同一个方向：真值不再是 \{0,1\}，而是某种更丰富的结构。

到什么程度，"资源"是一个精确的数学概念？ 线性逻辑给了我们一个形式框架，但"资源"本身仍然是一个直觉词。什么是一份资源？资源的复制何时是合法的？这些问题在不同的应用域里有不同的回答，而线性逻辑提供的是一个可以容纳这些不同回答的框架，不是一个单一的答案。

去掉交换规则会怎样？ 第14章列了三条结构规则：弱化、收缩、交换。线性逻辑去掉了收缩（有时也去掉弱化）。如果再去掉交换规则——让假设的顺序变得重要——就得到有序逻辑（Ordered Logic），它对应着有时间顺序的资源使用，比如消息必须按顺序发送和接收的通信协议。这个方向还在展开中。

如果"真"本身是一个程度，推断规则又该怎么改？ 线性逻辑通过资源计数，把 \{0,1\} 的真值撑开了一个维度——假设有"份数"的区别，但每一份仍然是确定的真或假。但还有另一个方向：真值不是"1份还是2份"，而是"0.3还是0.7"。这个方向不再是资源的问题，而是不确定性的问题。推断规则在不确定性下的推广，正是第17章的主角。

思考题

★ 热身

用线性逻辑的资源直觉，判断以下推断是否成立。不需要写形式证明，只需要用"五元钱买咖啡"那类资源例子说清楚为什么对或错。

1. A \otimes B \vdash A（同时拥有 A 和 B，可以单独推出 A）
2. A \,\&\, B \vdash A（拥有"A 或 B 的选择权"，可以推出 A）
3. !A \vdash A（无限可用的 A，可以取出一份 A）
4. A \vdash !A（一份 A，可以变成无限可用的 A）

第1和第2的对比是这章最重要的区分。第4是收缩规则被拿走后直接失效的推断。

★★ 推导

考虑以下三个推断，判断在线性逻辑中是否成立，并写出理由。

1. A \multimap B,\ A \multimap B \vdash A \multimap B（两份"A 变为 B"的能力，可以合并为一份？）
2. !(A \multimap B),\ !A \vdash !B（无限可用的转换规则，加上无限可用的输入，可以产生无限可用的输出？）
3. A \otimes B \multimap C \vdash A \multimap (B \multimap C)（消耗 A 和 B 产生 C，等价于先消耗 A、再消耗 B 产生 C？）

第1个涉及收缩。第2个涉及感叹号的推广规则。第3个是线性逻辑版本的柯里化——想想它在资源意义上是否真的成立。

★★★ 挑战

Rust语言的所有权系统实现了线性类型：每个值恰好拥有一个所有者，传递所有权就是消耗一份假设，借用（borrow）对应使用 ! 修饰的临时视图。

试着用线性逻辑的符号，为以下Rust操作各写一个对应的线性逻辑推断式：

• 把变量 x 的所有权移动给函数 f（移动语义）
• 把变量 x 的不可变引用传给函数 g（不可变借用）
• 函数返回值（消耗输入，产生输出）

不要求完全精确，但要说清楚：哪些操作对应消耗性推断（线性蕴含 \multimap），哪些操作对应可重复使用的视图（感叹号 !）。这个练习的目的是把语言设计的直觉翻译成逻辑的语言——翻译过程中你会发现哪些地方对应得上，哪些地方对应不上。