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. A ⊸ B ≡ A ⊗ ⊤ ⊸ B in affine (can discard).

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

Categorical semantics: Symmetric monoidal closed categories. With terminal object ⊤. ! 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	Unit for weakening
1	—	One	Multiplicative unit

Metatheory. Affine logic decidable (PSPACE-complete for propositional). Cut elimination holds. Weakening doesn't break resource sensitivity. Embedding: affine embeds in linear via !. Categorical: affine categories are SMCCs with terminal object. 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.