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

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

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

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

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

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

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

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

16.1 收缩规则在干什么

回忆收缩规则的形式：

\frac{Γ, A, A ⊢ B}{Γ, A ⊢ B}

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

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

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

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

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

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

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

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

兔狲教授评

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

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

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

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

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$ 其中之一，但不知道是哪个"——这是信息匮乏的表达，而不是可选择的丰盈。

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

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

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

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

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

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

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

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

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

兔狲教授评

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

16.4 蕴含的含义变了

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

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

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

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

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

16.5 三个现实的对应

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

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

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

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

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$ （假）。

$P \to Q$
$\neg Q \to \neg P$ （逆否命题）
$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章的主角。

思考题

★ 热身

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

$A \otimes B ⊢ A$ （同时拥有 $A$ 和 $B$ ，可以单独推出 $A$ ）
$A & B ⊢ A$ （拥有" $A$ 或 $B$ 的选择权"，可以推出 $A$ ）
$! A ⊢ A$ （无限可用的 $A$ ，可以取出一份 $A$ ）
$A ⊢! A$ （一份 $A$ ，可以变成无限可用的 $A$ ）

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

★★ 推导

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

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

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

★★★ 挑战

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

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

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

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

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

16.1 收缩规则在干什么 ​

16.2 线性逻辑的符号体系 ​

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

16.4 蕴含的含义变了 ​

16.5 三个现实的对应 ​

16.6 两种真值：占有与选择 ​

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

悬而未决 ​

思考题 ​