Affine Logic

Affine logic is a substructural logic that occupies the conceptual space between classical logic and linear logic. Like linear logic, it rejects the structural rule of contraction — the assumption that a premise can be used multiple times — but unlike linear logic, it permits weakening: the assumption that a premise can be ignored without being used. The result is a logic of resources that can be wasted but not cloned, a formal framework that captures the behavior of physical and computational systems where duplication is costly or forbidden but discarding is free.

Affine logic was introduced by Jean-Yves Girard as a natural variant of linear logic, and it appears throughout the proof-theoretic literature under various names. Its sequent calculus is identical to linear logic's except that the weakening rule is admissible for all formulas, not merely for formulas marked with the exponential modality ?.

The Logic of Disposable Resources

The characteristic axiom of affine logic is the implication A → (A ⊗ ⊤), which states that any resource A can be paired with a trivial resource without cost. In linear logic, this would require A to be prefixed with the ? modality, marking it as infinitely available. In affine logic, the implication holds for all resources. This makes affine logic a logic of disposable resources: anything can be thrown away, but nothing can be duplicated.

This resource discipline has direct applications in type theory and programming language design. Affine type systems track the linearity of values: a value of affine type must be used at most once. If it is used zero times, the compiler inserts a drop operation. If the programmer attempts to use it twice, the compiler rejects the program. This discipline eliminates a large class of memory-management errors without requiring the full bookkeeping burden of linear types. The Rust programming language draws heavily on affine and linear type discipline for its ownership system.

Proof Theory and Computational Interpretation

The Curry-Howard correspondence for affine logic maps affine proofs to programs in which variables are used at most once. This is the computational interpretation of affine logic: a function that receives an affine argument can either consume it or ignore it, but it cannot copy it. In the terminology of process calculi, affine channels are channels that can be read once or not at all — they cannot be broadcast.

The connection to structural proof theory is equally direct. Affine logic is the proof system obtained by removing only contraction from the structural rules of classical logic. The result preserves the cut-elimination property, has a clear phase semantics, and admits a notion of proof net simpler than linear logic's because the exponential modalities can be partially eliminated. The proof-theoretic study of affine logic has produced results on the complexity of cut-elimination that illuminate why structural rules matter for computational complexity.

Variants and Extensions

Several variants of affine logic have been developed to capture more specific resource disciplines. Light linear logic, introduced by Girard, restricts the exponential modality to control the complexity of normalization, ensuring that every typable term is polynomial-time computable. This makes light linear logic a logical foundation for implicit computational complexity — the study of complexity classes through type discipline rather than explicit resource bounds.

Bounded linear logic, developed by Martin Hofmann and others, extends affine logic with explicit resource bounds, tracking not merely whether a resource can be duplicated but how many times. This yields a type system in which memory allocation and deallocation are statically tracked, with direct applications to certified compilation and resource-sensitive computation in embedded systems.

The relationship between affine logic and quantum mechanics is particularly suggestive. The no-cloning theorem of quantum information theory forbids the duplication of arbitrary quantum states — precisely the contraction rule. But quantum states can be discarded (measured and forgotten) without contradiction. This makes affine logic, rather than linear logic, the natural logical framework for reasoning about quantum resources. The quantum lambda calculus and related type systems are explicitly affine in their treatment of quantum data.

Affine logic is not a weakened version of linear logic. It is a different logic for a different domain. Linear logic captures the discipline of perfect resource accounting; affine logic captures the discipline of systems where waste is free but replication is impossible. The error is to assume that the stronger logic is always the better tool. In quantum computing, in garbage-collected programming languages, in any system where discarding is trivial and copying is forbidden, affine logic is the natural framework. The synthesizer who ignores it because it is 'just linear logic with weakening' has mistaken a boundary condition for a degenerate case.