Soft Linear Logic

Origin. Lafont (2004). Polynomial time. Controlled contraction. Light logic variant. Foundation of implicit complexity.

Models. Bounded duplication. Polynomial normalization. Soft exponential. Stratified copying.

Formalism.

Exponential (soft): !A: duplicable, but only in one shot. SLL has no contraction rule and no dereliction; the two exponential rules below replace them. Polynomial bound.

Soft promotion: Γ ⊢ A ───────── !Γ ⊢ !A

The context is banged in the conclusion, not required to be banged in the premise — this is what distinguishes soft from ordinary promotion.

Multiplexing (mux): Γ, A, ..., A ⊢ B (n copies, n ≥ 0) ──────────────────────────────────── Γ, !A ⊢ B

One rule doing the work of contraction, weakening (n = 0) and dereliction (n = 1) at once. The number of copies is fixed when the rule is applied, so duplication cannot cascade.

Key property: Proof normalization in polynomial time. Cut-elimination polynomial. No exponential blowup.

Relation to light linear: Light linear logic: paragraph modality §. Soft: different control. Both polynomial. Different restrictions.

Polynomial soundness: Representable functions = PTIME. Proofs = polynomial algorithms. Implicit complexity. No explicit bounds.

MALL fragment: Multiplicative-additive. Plus soft !. Full connectives available.

Typing: Soft affine lambda calculus. Polynomial normalization. Type-based complexity.

Symbols.

Symbol	Unicode	Name	Meaning
!	U+0021	Exclamation mark / Soft bang	The single exponential of SLL
⊢	U+22A2	Turnstile	Derivability
Γ	U+0393	Gamma	A context; !Γ is the context with every formula banged
⊸	U+22B8	Multimap / Lollipop	Linear implication
⊗	U+2297	Circled times / Tensor	Multiplicative conjunction
§	U+00A7	Section sign / Paragraph	Light linear logic's second modality; absent from SLL
n	—	Multiplicity	Number of copies fixed at a multiplexing step
mux	—	Multiplexing	The rule replacing contraction, weakening and dereliction
SLL	—	Soft linear logic	Lafont's system
MALL	—	Multiplicative-additive linear logic	The exponential-free base SLL extends
PTIME	—	Polynomial time	The class SLL characterizes

Metatheory. Lafont (2004) proved that cut elimination in soft linear logic terminates in a number of steps bounded by a polynomial in the size of the proof, with the degree given by the depth of the proof, and that the functions representable on binary strings are exactly the polynomial-time computable ones, so SLL is sound and complete for PTIME. The mechanism is multiplexing: the rule that fixes the number of copies of A at the moment !A is used, replacing contraction, weakening and dereliction with a single rule whose multiplicity is chosen once and cannot cascade. Soft promotion bangs the context in the conclusion rather than requiring it banged in the premise, which is what keeps boxes from nesting during reduction. SLL needs no second modality and no two-zone context discipline, so it reaches the same characterization as light linear logic with one exponential rather than two. Soft affine logic, obtained by adding unrestricted weakening, retains the bound.

Applies to. Implicit computational complexity. Characterizations of PTIME by typing. Light typed lambda calculi. Resource-bounded functional languages. Soft lambda calculus and soft type assignment. Certifying polynomial-time bounds without an external cost analysis.

Limitations. Completeness for PTIME is extensional: every polynomial-time function has some representation, but the natural program for it usually does not type, because the number of copies must be committed at each multiplexing step and cannot depend on data. Dereliction as a separate principle is unavailable — !A ⊸ A is only the n = 1 instance of multiplexing, so a value cannot be extracted from a box while leaving the box available — and digging is absent, so iterations cannot be nested. The degree of the polynomial is a function of the depth of the proof and is not uniformly bounded, so membership in PTIME is certified without any particular degree being certified. The characterization is of time only: nothing is said about space, and no soft system captures a class below polynomial time.