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

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

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

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

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

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

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

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

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

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

所以我们换一个厨房。

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

A \otimes B ⊸ D

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

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

这个游戏的形式化骨架

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

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

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

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

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

线性逻辑的四个连接词：用"点菜"来理解（前人工作：Girard, 1987）

线性逻辑里多出来的连接词，用餐厅点菜来类比最清楚：

符号	读法	类比	意思
$A \otimes B$	张量 / tensor	套餐：汉堡加薯条，两样都给	同时拥有两份资源，都要消耗
$A & B$	with	今日特选：汉堡或沙拉，二选一，随你	拥有选择权，但只能选一个
$A \oplus B$	plus	厨师随机给你汉堡或沙拉，不知道是哪个	拥有其中之一，但不知道是哪个
$A ⊸ B$	线性蕴含	用一份 $A$ 换一份 $B$ ， $A$ 消耗掉	资源转换，不是知识推导

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

16.2.5 实操：在线性逻辑里写一个证明

用 sequent calculus（序贯演算）的格式来写线性逻辑的证明。Sequents 的形式是 $Γ ⊢ Δ$ ，读作：资源集合 $Γ$ 可以转换为资源集合 $Δ$ 。

在线性逻辑的 sequent calculus 里，恒等公理只有一条：

\frac{}{A ⊢ A} (id)

但关键的区别在于上下文管理：每条推断规则都精确地说清楚它消耗了什么、产生了什么。没有弱化（不能凭空丢弃假设），没有收缩（不能复制假设）。

以下是一个完整的证明示例——证明 $A \otimes B ⊸ B \otimes A$ （"同时拥有A和B"可以转换为"同时拥有B和A"——交换律在线性逻辑里不是公理，而是可以被证明的定理）：

证明树：

                ————— (id)             ————— (id)
                A ⊢ A                 B ⊢ B
               ——————————— (⊗R)     ——————————— (⊗R)  
               A, B ⊢ A ⊗ B          B, A ⊢ B ⊗ A
               ————————————— (⊗L, 将A,B打包)  
               A ⊗ B ⊢ A ⊗ B         ——————————————— (交换? 不能!)
               
等等——这里暴露了一个问题。在标准的线性 sequent calculus 里，交换律（context 里的顺序交换）是隐含的结构规则还是显式的？

答案是：**取决于你用的是哪种线性逻辑变体**。在经典线性逻辑（CLL）里，交换律被保留为结构规则——你可以自由重排 context 里的资源顺序。在非交换线性逻辑（NLL）里，交换律被去掉，资源的左右顺序有物理含义（如时间顺序）。

保留交换律的版本里，这个证明很简单：
1. 从 $A \vdash A$ 和 $B \vdash B$ 出发
2. 用 $\otimes R$ 得到 $A, B \vdash A \otimes B$ 和 $B, A \vdash B \otimes A$  
3. 用交换律重排第二个：$A, B \vdash B \otimes A$
4. 用 $\multimap R$ 从 $A \otimes B \vdash A \otimes B$ 和 $A, B \vdash B \otimes A$... 不，更直接的方式是用 $\otimes L$：
5. 要证明 $A \otimes B \vdash B \otimes A$，假设有 $A \otimes B$（即 $A$ 和 $B$ 被捆绑在一起），用 $\otimes L$ 把它们拆开，重新组合。最后用 $\multimap R$。

去掉交换律的版本里，$A \otimes B \vdash B \otimes A$ 是**不可证的**！因为资源的位置信息被纳入了逻辑——你不能"免费"重排 $A$ 和 $B$ 的顺序。

这个练习的意义不在于公理编号，而在于亲身体验：**去掉一条结构规则，整个逻辑的定理集合就变了**。这不是微调，是根本性的改变。

::: info 兔狲教授评
这个证明在保留交换律的版本里只需要两步；去掉交换律，它就变成了不可证。大多数逻辑课不会让你看到这个对比——他们把交换律当空气，你在呼吸却不知道空气的存在。线性逻辑的工作之一，就是让空气变得可见。
:::

::: 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）正是这个对应关系的工程实现，它允许编译器在类型检查阶段验证协议的正确性——逻辑保证了协议不会死锁，不会遗漏消息。

### 16.5.5 实操：Rust 的所有权系统如何对偶于线性逻辑

这不是比喻。Rust 的类型检查器在编译时执行的规则，在线性逻辑里都有精确的对偶。下面用一个具体的Rust程序来说明。

**例1：移动语义 = 线性蕴含**

```rust
let x = String::from("你好");  // x 拥有字符串的所有权
let y = x;                     // 所有权从 x 移动到 y
// println!("{}", x);          // 编译错误！x 已被"消耗"
// error[E0382]: use of moved value: `x`

对应的线性逻辑命题：

String("你好") ⊸ String@y

资源被隐式地从 x 移动到 y，x 不再可用。在线性逻辑里就是：消耗一份资源，产出一份资源，原始的消失。

例2：不可变借用 = $! A$ 的临时视图

rust

let x = String::from("你好");
let r1 = &x;  // 不可变借用——可以读，不能改
let r2 = &x;  // 可以有多个不可变借用同时存在
println!("{} {}", r1, r2);  // ✓
println!("{}", x);          // ✓ x仍然有效

对应的线性逻辑命题：

! A ⊢ A \otimes A \otimes \dots

$! A$ （无限可用的资源）允许从中取出多份只读视图。借用结束后，x 的所有权不受影响。

例3：可变借用 = 线性资源的独占访问

rust

let mut x = String::from("你好");
let r = &mut x;  // 可变借用——独占访问
r.push_str("，世界");
// let r2 = &x;  // 编译错误！不能同时有可变借用和不可变借用
// error[E0502]: cannot borrow `x` as immutable because it is also borrowed as mutable

对应的线性逻辑：可变借用临时"拿走"了资源的独占修改权——和移动不同，借出的资源在借用结束后还会还回来；和不可变借用不同，可变借用是独占的，不能同时存在两份。这是线性逻辑和仿射类型（affine types，资源至少用一次）的交界地带。

例4：函数调用 = 参数消耗

rust

fn consume(s: String) {  // 消耗输入的String
    println!("{}", s);
    // s 在这里被释放（drop）
}

let x = String::from("你好");
consume(x);               // x 被移到函数参数
// println!("{}", x);     // 编译错误！x 已被消耗

对应的线性逻辑命题：

\frac{Γ ⊢ String("你好") ⊸ 1}{Γ, String("你好") ⊢ 1}

函数体消耗资源并产出空（ $1$ ，对应Rust里的 () 类型）；资源在函数调用中被转移，调用者不再拥有它。

四个例子总结：

Rust 操作	线性逻辑	解释
移动 `let y = x`	$A ⊸ B$	资源从一处移动到另一处
不可变借用 `&x`	$! A ⊢ A$	从无限资源中取一份只读视图
可变借用 `&mut x`	独占线性访问	临时转移独占修改权，结束后还回
函数消耗 `f(x)`	$⊸$ 消去	资源被函数体消耗

这个对应不是巧合。Rust 的核心类型系统（所有权、借用、生命周期）建立在线性类型的基础上——类型检查器在编译时执行的逻辑，正是线性逻辑的推断规则。Rust 编译器不是"参考了"线性逻辑，而是实现了线性逻辑。

第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.0 一次性厨房游戏：每份资源只能用一次 ​

16.1 收缩规则在干什么 ​

16.2 线性逻辑的符号体系 ​

16.2.5 实操：在线性逻辑里写一个证明 ​

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

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

悬而未决 ​

思考题 ​

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

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

16.1 收缩规则在干什么

16.2 线性逻辑的符号体系

16.2.5 实操：在线性逻辑里写一个证明

16.6 两种真值：占有与选择

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

悬而未决

思考题