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 ≡ A (no reuse) !¹A: exactly once !ω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) 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	n copies max
§	U+00A7	Paragraph	Light storage
⊸	U+22B8	Lollipop	Linear implication
⊗	U+2297	Tensor	Multiplicative and

Metatheory. Soundness for complexity classes. PTIME (LLL, SLL), PSPACE, EXPTIME characterizations. Cut elimination in polynomial steps. Implicit complexity correspondence.

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

Limitations. Programming restrictive. Multiple variants. Expressiveness vs complexity tradeoffs. Not mainstream for verification. Theoretical focus.