Light Linear Logic

Origin. Girard introduced Light Linear Logic (LLL, 1998). Captures polynomial time computation. Restricts linear logic's exponentials. Implicit computational complexity (ICC). Proofs normalize in polytime. Extends to Elementary Linear Logic (ELL) for elementary time.

Models. Resource control for complexity bounds. Linear logic: ! allows unlimited copying. Light: restricted !, new modality §. Controls duplication depth. Proof normalization = bounded computation. Type system guarantees complexity class membership.

Formalism.

Modalities:

§ (paragraph): allows limited structural rules
!A: "of course" (further restricted)

Restricted rules: In LLL, ! and § controlled:

§-promotion: Γ; ⊢ A ───────── Γ; ⊢ §A

!-promotion (restricted): §Γ; ⊢ A ───────── ; !Γ ⊢ !A

Stratification: Formulas have depth (levels of §). Contraction only at controlled depths. Prevents exponential blowup in normalization.

Elementary Linear Logic (ELL): Single modality ! but restricted promotion. Captures elementary time (tower of exponentials).

Soft Linear Logic (SLL): Lafont's variant: multiplexing instead of contraction. Also captures polytime.

Light Affine Logic (LAL): Adds weakening (can discard). Still polytime.

Symbols.

Symbol	Unicode	Name	Meaning
§	U+00A7	Paragraph	Bounded modality
!	—	Bang	Of course (restricted)
⊗	U+2297	Tensor	Multiplicative and
⊸	U+22B8	Lollipop	Linear implication
&	—	With	Additive and
⊕	U+2295	Plus	Additive or

Metatheory. LLL proof normalization is polytime. Represents exactly polytime functions. Denotational semantics via stratified coherence spaces. ELL: elementary time (iterated exponential). Soft linear logic equivalent to LLL in expressiveness. Type systems derive from LLL.

Applies to. Implicit computational complexity. Certified complexity bounds. Resource-aware type systems. Safe recursion. Feasible mathematics. Program analysis. Complexity-restricted languages.

Limitations. Programming in LLL is awkward. Restrictive — natural algorithms may not type. Less intuitive than recursion-based complexity. Tool support limited. Active research area. Trade-off between expressiveness and restriction.