Affine Logic

Origin. Affine logic is linear logic plus weakening (1980s-90s). Resources can be discarded but not duplicated. "At most once" rather than "exactly once." Related to affine types in programming languages. Girard's work on linear logic provides foundation.

Models. Resources used at most once. Linear logic: use each resource exactly once. Affine logic: use each resource at most once (can discard). Intuitionistic logic: use each resource any number of times. Affine captures "no duplication" without "must use."

Formalism.

Affine logic: Linear logic + weakening rule.

Weakening: Γ ⊢ B / Γ, A ⊢ B (can drop unused assumptions)

Structural rules:

• Exchange: ✓ (reorder)
• Weakening: ✓ (discard)
• Contraction: ✗ (no duplication)

Connectives (inherited from linear): Multiplicative: ⊗ (tensor), ⅋ (par), ⊸ (linear implication) Additive: & (with), ⊕ (plus) Exponentials: ! (of course), ? (why not)

Key difference: Linear: A ⊸ B needs A exactly once. Affine: A ⊸ B uses A at most once. Concretely: A ⊸ 1 is provable for every A, and hence A ⊗ B ⊸ B. That is weakening, stated in the object language.

Affine types: Variables used ≤ 1 time. Connection to Rust ownership (move semantics). Can drop without explicit destructor.

Categorical semantics: Symmetric monoidal closed categories in which the monoidal unit 1 is terminal — that, not merely the existence of a terminal object, is what encodes weakening. ! is a comonad (but with extra properties for affine).

Symbols.

Metatheory. Affine logic keeps exchange and weakening and drops contraction alone, so a hypothesis may be discarded but never duplicated; weakening is internalized by the provability of A ⊸ 1 for every A. Cut elimination holds for the sequent calculus, and the subformula property follows. Decidability is where affine and linear logic part company: full propositional linear logic is undecidable (Lincoln, Mitchell, Scedrov and Shankar, "Decision problems for propositional linear logic", 1992), whereas full propositional affine logic with exponentials is decidable (Kopylov, "Decidability of linear affine logic", 1995); the exponential-free fragment is decidable in polynomial space. Because weakening makes the multiplicative unit terminal, 1 and ⊤ become isomorphic, a collapse linear logic avoids. The categorical models are symmetric monoidal closed categories whose unit is terminal. In the exponential-free affine λ-calculus every β-step strictly shrinks the term, since substitution replaces at most one occurrence, so reduction terminates even in the untyped setting.

Applies to. Rust ownership (affine types). Session types (channel usage). Memory management (no double-free). Resource-aware programming. Smart contracts (tokens spent once). Linear/affine lambda calculi. Quantum computing (no-cloning).

Limitations. Weakening destroys the "exactly once" reading: affine logic can forbid duplication but cannot compel use, so obligations — a file that must be closed, a session that must run to completion — are outside what it expresses, and affine type systems guarantee absence of double use rather than guaranteed consumption. It is not a relevance logic: A ⊗ B ⊸ B is provable, premises may be idle, and the variable-sharing property fails. The multiplicative and additive units collapse into one another, so the distinction between 1 and ⊤ that linear logic maintains is unavailable. Without the exponential there is no duplication and hence no fixed-point combinator: the affine λ-calculus normalizes and cannot express general recursion, so all computational strength enters through !, and inside the scope of ! contraction returns and the resource discipline lapses.

© 2026 Lingenic LLC