所有权与借用

形式陈述 ​

本页先固定一个 Rust-like core calculus，只含 owner、move、共享借用、独占借用和区域生命周期；它用来说明共同静态不变量，不等同于某个 Rust 编译器版本的完整 borrow checker。Rust 的 non-lexical lifetimes、variance、interior mutability 与 two-phase borrows 会在边界处单独说明，不能反向当作所有权系统的一般定理。

在核心演算中，每项资源有一个负责其有效性和最终释放的 owner。移动（move）把这项责任从源绑定转给目标绑定；移动完成后，源绑定处于不可读状态，直到它被重新赋值。这个规则约束的是被移动值的责任，不是说源变量在整段程序里只能出现一次，也不妨碍显式标记为可复制的值按语言规则复制。

借用在不转移所有权的情况下临时授予访问能力。用 ${\mathrm{\&}}^{\rho }T$ 表示生命周期 $\rho$ 内的共享借用，用 ${\mathrm{\&}}^{\rho }\mathsf{mut}T$ 表示独占借用。对每个被借位置 $\ell$，核心不变量是：

1. 可以同时存在多个有效共享借用，但它们只提供读访问；
2. 或者存在一个有效独占借用，它可读写该位置；
3. 两种状态不能重叠，独占借用之间也不能重叠；
4. 每个借用的生命周期都包含在所有者和被借对象仍有效的区间内。

若 $\mathrm{live}(x)$ 是 owner $x$ 保持有效的区域，创建借用要求

$$\rho \subseteq \mathrm{live}(x).$$

在共享借用有效期间，不能移动或可变访问 $x$；在独占借用有效期间，除该借用途径外不能再访问 $x$。借用结束后，这些临时限制解除，所有权本身从未离开 $x$。

在这个核心模型中，生命周期可形成子类型公理库子类型Subtyping允许某类型值在期望其上界类型的位置使用的可替代关系。或区域包含关系。若 ${\rho }_{long}\supseteq {\rho }_{short}$，一个更长寿命的共享引用可安全缩短：

$${\mathrm{\&}}^{{\rho }_{long}}T<:{\mathrm{\&}}^{{\rho }_{short}}T.$$

独占引用通常通过 reborrowing 获得较短的 ${\mathrm{\&}}^{{\rho }_{short}}\mathsf{mut}T$。原独占引用在新借用有效期间被暂停，待短借用结束后恢复；这不是把可变权限复制两份。Rust 对 $T$ 与 lifetime 的 variance 是具体类型构造器和语言规则的一部分，不能从共享引用的协变公式机械照搬到任意所有权演算。

这些约束属于静态语义。借用检查算法可以用词法作用域、数据流或非词法生命周期推断 $\rho$，并保守拒绝无法证明安全的程序。运行语义仍由堆、位置和更新组成的可变状态语义公理库可变状态语义Semantics of mutable state · Store semantics把位置到值的存储纳入配置并随求值更新的语义。给出；类型系统的可靠性要求求值保持 owner/loan 与实际位置的一致性，使安全子语言中的解引用不会悬空，也不会经两个冲突权限同时访问同一位置。

直觉 ​

所有权回答“谁负责让这项资源继续有效并最终收尾”，借用回答“在责任不转手时，谁能暂时看或改它”。move 像交接钥匙和保管责任，旧持有人不能继续开门；shared borrow 像发出若干只读访客证，exclusive borrow 则像暂时把唯一工作证交给维护者。

生命周期不是对象实际存活秒数，而是静态证明中一次引用可能被使用的程序区域。只要编译器能证明借用在最后一次使用后结束，就可以恢复所有者访问；非词法生命周期因此比“必须等到花括号结束”更精确，却不改变核心排他不变量。

例子与边界 ​

设向量 v 拥有一段可能在扩容时迁移的缓冲区，p = &v[0] 创建指向元素的共享借用。只要 p 后续仍会使用，执行 v.push(x) 就需要可变借用整个向量，并可能让缓冲区换址；它既与现有共享借用冲突，也可能使 p 悬空，所以静态规则拒绝这段重叠。p 最后一次使用后，短生命周期结束，push 才可获得独占访问。

对拥有堆字符串的值，let b = move a 把释放责任交给 b，随后读取 a 会被拒绝；若重新给 a 赋一个新字符串，它又成为新值的 owner。整数等 Copy 值可以显式复制而不使源失效，这说明所有权不等于“每个变量只能用一次”。

共享所有权和内部可变性是 Rust 层的重要边界。Rc/Arc 通过引用计数让多个 owner 共同保持分配存活；RefCell 把共享/独占检查推迟到运行时，违规时失败；Mutex 通过加锁在并发访问中动态取得独占权限。这些库类型改变检查发生的位置，却不是核心演算里“共享借用只读”的反例：可变操作必须经过额外的动态协议。unsafe 代码还可绕过静态限制，但必须由程序员或库证明恢复调用方看到的安全不变量。

Two-phase borrow 是另一项 Rust 特定规则。某些方法接收者的可变借用先处于 reservation 阶段，允许在真正调用前完成受限的共享求值，例如计算 v.push(v.len()) 的参数；到 activation 后才取得独占访问。它不允许两个任意写者重叠，也不是对所有 &mut 表达式开放的通则，所以核心模型仍用单阶段独占借用陈述不变量。

线程间可否移动或共享值还需要类似 Send/Sync 的能力约束。所有权与借用能排除一类悬空引用和冲突别名，却不自动证明锁顺序正确、程序无死锁或所有数据访问都无竞争。

推论与应用 ​

所有权系统常借鉴线性与仿射类型公理库线性类型与仿射类型Linear type · Affine type · Linear and affine types分别以恰好一次和至多一次的上下文纪律约束值使用，并显式隔离可复制资源。的不可复制资源观念：move 类似消费旧能力并产生新能力。但所有权还要描述堆位置、共享只读别名、临时独占、生命周期包含与 reborrow；普通线性演算并不自动给出这些规则。因此所有权不是线性类型的语法糖，Rust 变量也不是普遍线性值。

编译器可利用独占借用推断某段时间没有竞争别名，从而安全地原地更新或优化访问。验证这类优化仍需连接静态 loan 事实与运行存储：若 interior mutability、外部函数或 unsafe 边界能绕过别名承诺，优化器必须依赖更精确的语言内存模型和库契约。

参考资料

• The Rust Reference，ownership, references, subtyping, and variance；The Rustonomicon，unsafe abstractions and aliasing。
• Ralf Jung et al., “RustBelt: Securing the Foundations of the Rust Programming Language,” POPL, 2018。
• Nicholas D. Matsakis and Felix S. Klock II, “The Rust Language,” ACM SIGAda Ada Letters 34(3), 2014，ownership and borrowing model。