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	Section sign / Paragraph	Bounded modality; carries stratification
!	U+0021	Exclamation mark / Bang	Of course, with promotion restricted to at most one premise
⊗	U+2297	Circled times / Tensor	Multiplicative conjunction
⊸	U+22B8	Multimap / Lollipop	Linear implication
&	U+0026	Ampersand / With	Additive conjunction
⊕	U+2295	Circled plus / Plus	Additive disjunction
⊢	U+22A2	Turnstile	Derivability
Γ	U+0393	Gamma	A context
;	—	Context separator	Divides the two zones of an LLL sequent
LLL	—	Light linear logic	Girard's PTIME system
LAL	—	Light affine logic	Asperti's variant with unrestricted weakening
ELL	—	Elementary linear logic	Characterizes the Kalmár-elementary functions
SLL	—	Soft linear logic	Lafont's variant using multiplexing

Metatheory. Girard (1998) proved that cut elimination in light linear logic normalizes in a number of steps polynomial in the size of the proof, with the degree fixed by the depth of the proof, and that the functions representable on binary strings are exactly the polynomial-time computable ones: LLL is sound and complete for PTIME. The mechanism is stratification. The paragraph modality and the restricted promotion rule — !-promotion admits at most one premise — prevent the depth of a box from increasing during reduction, so the reduction can be organized level by level with a polynomial number of steps at each level. Asperti and Roversi's intuitionistic light affine logic (2002) admits unrestricted weakening, which removes the need for the two-zone context discipline, and is likewise complete for PTIME. Elementary linear logic, which admits neither dereliction nor digging, characterizes the Kalmár-elementary functions. Lafont's soft linear logic (2004) reaches PTIME by a different route, replacing contraction with multiplexing and dispensing with the second modality altogether.

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

Limitations. Completeness for PTIME is extensional: every polynomial-time function has a representation, but the obvious program for it usually does not type, since duplication is admitted only at controlled depths and iteration cannot be nested. Dereliction is unavailable — !A ⊸ A is not derivable — so a value cannot be moved out of its box, and data at different depths cannot be combined without a §-shift. The degree of the polynomial is a function of the depth of the proof and is not uniformly bounded, so LLL certifies membership in PTIME without certifying any particular degree, and the constants hidden in the encoding can be large. The characterization is of time only; the system says nothing about space, and no light system captures a class below polynomial time. Deciding whether a given ordinary λ-term admits a light typing is a different and harder problem than provability in the logic, which is why the dual light affine systems restrict the syntax before attempting inference.