Substructural Logic

Ordinary constructive logic permits three rules that change the shape of that context without inspecting the propositions inside it. These are called structural rules.

A substructural logic restricts or removes at least one of these permissions. The context then becomes an inventory of resources: a proof must account for how often and in what order each assumption is allowed to be used.

Removing contraction does not mean that duplication can never occur. It means duplication is no longer implicit. A system may provide an explicit operation or modality (linear logic uses $!A$) to mark values that are safe to copy or discard.

A logic without weakening rejects this proof as written: every premise must contribute. The point is not that the conclusion is false, but that this particular premise-to-conclusion argument fails to demonstrate relevance.

Without contraction, one copy of your budget premise cannot be reused to buy more than one coffee.

Wihout exchange, you cannot reorder the premises and you are stuck either figuring out how to take off your socks before your shoes or you just reject that statemnet.

Identity

Ordinary constructive logic can retrieve $A$ from a larger context because weakening permits unused assumptions. In a strictly linear context, the identity rule accounts for exactly one resource:

Multiplicative conjunction: tensor

The contexts $\Delta_1$ and $\Delta_2$ must be disjoint partitions of the available resources. The constructive $\wedge I$ rule reuses the same $\Gamma$ in both branches, which would implicitly duplicate every assumption. Also, note that the linear version doesn't have rules for dropping a premise a conjunction because you can't drop premises without using them.

Additive disjunction: plus

A proof chooses a side. Elimination must handle either choice using the same surrounding resources $\Delta'$.

Linear implication: lollipop

Read $A\multimap B$ as a process that consumes one $A$ to produce one $B$. Its symbol $\multimap$ is commonly pronounced “lollipop.”

Rust’s ownership discipline is usually described as affine: an owned value may be consumed at most once, but it may also be dropped unused. Copying resource-owning values is explicit, often through .clone(). Types implementing Copy, such as i32, opt into inexpensive implicit copying.

fn main() {
    let x = "hello".to_string();
    let y = x;
    println!("{x}");
}

fn eat(_: String) {}

fn main() {
    let y = "hello".to_string();
    eat(y.clone()); // explicit duplication
    eat(y);         // consume the original
}

fn print_int(x: i32) { println!("{x}"); }

fn main() {
    let z = 5;
    print_int(z);
    print_int(z);
}

A borrow lends access without transferring ownership. Rust permits any number of shared references &T, or one live mutable reference &mut T, but not both at the same time.

fn print_ref(s: &str) { println!("{s}"); }

fn main() {
    let s = "world".to_string();
    print_ref(&s);
    print_ref(&s);
}

fn modify(s: &mut String) {
    s.push_str(" oops");
}

fn main() {
    let mut s = "world".to_string();
    modify(&mut s);
    modify(&mut s);
}

fn main() {
    let mut s = "world".to_string();
    let r1 = &mut s;
    let r2 = &mut s;
    println!("{r1}");
}

fn main() {
    let mut foo = 5;
    let read_foo = &foo;
    let write_foo = &mut foo;
    println!("{read_foo}");
}

fn dangle() -> &'static str {
    let s = String::new();
    &s
}

• Parsing and grammar: words and tokens must be consumed in sequence.
• Protocols and state machines: “authenticate, then send” differs from “send, then authenticate.”
• Computation by rewriting: a transition consumes one configuration and produces the next.
• Session-typed communication: channels follow a prescribed order of sends and receives.

Substructural rules are therefore not only philosophical constraints. They are design tools for types that express ownership, protocols, state changes, and other forms of disciplined resource use that can guarantee correctness and memory safety.

1. Frank Pfenning, “Structural Proof Theory”, CMU 15-816 lecture notes. Covers exchange, weakening, contraction, and their relationship to linear logic.
2. Frank Pfenning, “Linear Logic”, CMU 15-814 lecture notes. Develops resource interpretations and identifies affine logic as allowing weakening but not contraction.
3. The Rust Project, The Rust Programming Language: “What Is Ownership?” Explains moves, clones, Copy, scope, and automatic dropping.
4. The Rust Project, The Rust Programming Language: “References and Borrowing” Covers shared and mutable references, dangling references, and borrow-checker rules.
5. The Rust Project, The Rust Programming Language: “Fearless Concurrency” Connects ownership and type checking to compile-time prevention of concurrency mistakes.