Substructural Logics

Rust guarantees memory safety without a garbage collector, through linear types baked directly into the type system. This is not just a practical trick: it is Girard's 1987 theorem, instantiated in a production language.

• **Rust ownership:** the ownership system = affine types; the borrow checker = proof checker in separation logic
• **Facebook Infer:** a static analyzer based on separation logic, finding null dereferences and memory leaks in production code at Meta/Amazon
• **Quantum computing:** linear logic models quantum circuits (quantum states cannot be cloned, the no-cloning theorem)

Предварительные знания

• Natural Deduction
• Intuitionistic logic

Structural Rules and Their Absence

Rust's borrow checker enforces linear logic: each value is consumed exactly once (no weakening, no contraction) , 250,000 lines of implementation. Classical and intuitionistic logic silently use three **structural rules** of the sequent calculus: weakening, contraction, and exchange. Substructural logics drop some of these, producing logics with fundamentally different properties.

Without weakening: hypotheses cannot be 'ignored', each must be used. Without contraction: hypotheses cannot be 'copied', each is used exactly once. This models resources: money, time, physical objects.

Girard's Linear Logic

Linear logic (Girard, 1987) is the logic of **resources**: each formula is a resource that is consumed upon use. '$1 → cookie' can be used only once. Girard also showed that classical logic embeds into linear logic via modalities!

Linear logic has two kinds of conjunction: A ⊗ B (tensor, both resources simultaneously) and A & B (with, a choice of one). Analogously two kinds of disjunction: A ⅋ B (par) and A ⊕ B (plus). This reflects different ways of 'splitting' resources.

Separation Logic

Separation Logic (Reynolds, O'Hearn, 2000) extends Hoare logic for reasoning about **heap memory**. The key operator, the separating conjunction P * Q, means 'P and Q hold for disjoint portions of the heap'.

The main power of separation logic is the Frame Rule: {P} C {Q} ⟹ {P*R} C {Q*R}. If a program C is correct under precondition P, adding unrelated state R does not affect it. This allows local reasoning about parts of the heap.

Linear Types in Rust

Rust's ownership system is **affine types** in action. Every value has exactly one owner. A move consumes the value. Borrowing (&, &mut) is limited temporary access. This is linear logic compiled to machine code, without a garbage collector.

Rust's borrow checker is formally equivalent to checking proofs in an affine type system. Lifetimes ('a) are regions in separation logic. RustBelt (2018) is the formal verification of Rust's type system in Coq/Iris.

Key Ideas

• **Structural rules**, W (weakening), C (contraction), E (exchange); substructural logics drop some of them
• **Linear logic**: no W and no C; each resource used exactly once; two kinds of ∧ (tensor ⊗, with &) and two kinds of ∨
• **Separation Logic**: separating conjunction P*Q: P and Q on disjoint heaps; Frame Rule; foundation of Infer
• **Rust = affine types**: move semantics consumes a value; borrow checker is formally equivalent to separation logic

Related Topics

Substructural logics connect theoretical logic with systems programming:

• Natural Deduction — Structural rules appear in Gentzen's sequent calculus; their absence defines substructurality
• Type Theory (CHI) — Linear types = CHI for linear logic; programs = proofs, resources = formulas
• Logic in Verification and AI — Separation logic is applied to verification of neural network code and safety-critical systems

Вопросы для размышления

• In Haskell, functions are pure and data references can be freely copied, what 'logic' does Haskell's type system implement? Does it need linearity?
• Quantum mechanics forbids copying quantum states (no-cloning theorem), how does linear logic model quantum computation?
• Rust solved memory safety through types. What other problems can be solved by embedding logic into the type system?

Связанные уроки

• plt-10-linear-types