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.

Symbol	Unicode	Name	Meaning
⊗	U+2297	Tensor	Multiplicative and
⊸	U+22B8	Lollipop	Linear implication
&	—	With	Additive and
⊕	U+2295	Plus	Additive or
!	—	Bang	Reusable
⊤	U+22A4	Top	Additive unit; terminal object
1	—	One	Multiplicative unit

Metatheory. Decidability is where affine and linear part company: full propositional linear logic is undecidable (Lincoln, Mitchell, Scedrov, Shankar 1992), while full propositional affine logic — exponentials included — is decidable (Kopylov 1995). PSPACE-completeness holds only for the exponential-free fragment, affine MALL; no elementary bound is known for the full system. Cut elimination holds. Weakening doesn't break resource sensitivity, since duplication is what the resource reading turns on. Categorical: SMCCs whose monoidal unit is terminal. Type systems: affine types prevent use-after-move.

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. Less common than full linear logic. Resource must be explicitly !'d to reuse. Proof search can be complex. Tool support less than linear logic. Interaction with other features (polymorphism) subtle. Sometimes overkill when full linear suffices.