Bounded Linear Logic

Origin. Girard, Scedrov, Scott (1992). Polynomial-time complexity via bounded exponentials. !ⁿA: at most n copies of A. Implicit computational complexity. Light and soft linear logic variants.

Models. Resource usage bounded by polynomials. Exponentials with depth/level restrictions. Stratified modalities. Proofs as polynomial-time computations.

Formalism.

Bounded modalities: !ⁿA: at most n copies of A available !⁰A ≡ 1 (no copies at all — the multiplicative unit, not A) !¹A ≡ A (exactly one copy) !ωA: unbounded (standard exponential)

Depth restrictions: Level assignment to formulas. !ᵢA: exponential at level i. Contraction only at lower levels.

Light Linear Logic (LLL): §A (paragraph): limited storage !A (of course): unlimited but restricted Captures PTIME.

Soft Linear Logic (SLL): Multiplexing instead of contraction. mux: !A ⊸ (A ⊗ ... ⊗ A), n times — no bang on the right; as a rule, from Γ, Aⁿ ⊢ B infer Γ, !A ⊢ B Captures PTIME without stratification.

Elementary Linear Logic (ELL): Captures elementary time (tower of exponentials). !A ⊸ !!A not derivable.

Typing complexity: Proofs in BLL → polynomial-time normalization. No unbounded duplication chains.

Symbols.

Symbol	Unicode	Name	Meaning
!ⁿ	—	Bounded bang	At most n copies available
§	U+00A7	Section sign / Paragraph modality	Light storage; stratifies the exponential
⊸	U+22B8	Multimap / Lollipop	Linear implication
⊗	U+2297	Circled times / Tensor	Multiplicative conjunction
⊢	U+22A2	Turnstile	Derivability
Γ	U+0393	Gamma	A context
≡	U+2261	Identical to	Provable equivalence of formulas
!	U+0021	Exclamation mark / Bang	Unbounded exponential
mux	—	Multiplexing	Soft linear logic's single exponential rule
BLL	—	Bounded linear logic	Girard–Scedrov–Scott, resource-polynomial exponentials
LLL	—	Light linear logic	Girard's stratified system
SLL	—	Soft linear logic	Lafont's multiplexing system
ELL	—	Elementary linear logic	No dereliction, no digging
PTIME	—	Polynomial time	The class these systems characterize

Metatheory. Girard, Scedrov and Scott (1992) proved that cut elimination in bounded linear logic terminates in a number of steps bounded by a polynomial in the size of the proof, once the resource polynomials in the types are fixed, and that the functions representable in BLL over binary strings are exactly the polynomial-time computable ones. That is soundness and completeness for PTIME, so the system is an implicit characterization of the class rather than a calculus with an external clock: the bound is a theorem about normalization, not a side condition on execution. Girard's light linear logic (1998) obtains the same characterization without writing resource polynomials into the types, by stratifying the exponential with the paragraph modality §; Asperti's light affine logic adds unrestricted weakening and keeps the bound; Lafont's soft linear logic (2004) replaces contraction by multiplexing, which fixes the number of copies at the point of use, and again captures exactly PTIME. Elementary linear logic, which admits neither dereliction nor digging, characterizes the Kalmár-elementary functions.

Applies to. Complexity theory. Implicit computational complexity. Resource-bounded computation. Certified complexity. Polynomial-time λ-calculi.

Limitations. Completeness for PTIME is extensional: every polynomial-time function has some representation, but the natural algorithm for it usually does not type, since duplication is admitted only at controlled depths and iteration cannot be nested freely. BLL is not implicit in the way its successors are — the resource polynomials are part of the syntax, so a proof carries its own bound and the system certifies nothing that was not annotated. Dereliction is unavailable in the stratified systems: !A ⊸ A is not derivable, so a value cannot be taken out of its box and data at different depths cannot be combined. The degree of the polynomial is governed by the depth of the proof and is not bounded uniformly, so membership in PTIME is certified without any particular degree being certified, and nothing at all is said about space. No system in this family characterizes a class below polynomial time, and the characterizations are of function classes, not of decision problems relative to an input encoding.