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: unlimited use (restricted). Contraction only at depth 0. Multiplexing limited. Polynomial bound.

Multiplexing rule: !Γ ⊢ A ───────── !Γ ⊢ !A

No arbitrary contraction on !A. Controlled duplication.

Contraction restriction: !A, !A ⊢ B only at top level. Cannot contract deep. Stratification.

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.

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.