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	Meaning
!	—	soft exponential
PTIME	—	polynomial time
SLL	—	soft linear logic
mux	—	multiplexing

Metatheory. Polynomial normalization. Controlled contraction. Implicit complexity. Light logics.

Applies to. Complexity theory. Type systems. Implicit complexity. Resource control.

Limitations. Expressiveness limited. Programming awkward. Less intuitive than LL. Specific purpose.