Soft Linear Logic and Implicit Complexity

Prerequisites. Direct starred prerequisites: none. No later core chapter depends on this route.

In ordinary linear logic, contraction duplicates a reusable proof. Nested boxes may therefore duplicate boxes that duplicate boxes. A local statement such as “this variable is used twice” does not by itself bound the length of normalization. Soft Linear Logic controls the shape of exponential boxes so that a proof net of fixed depth has a polynomial normalization bound. The control is structural, not an input-dependent cost annotation [Laf04].

The SLL2 proof system

Lafont works with second-order intuitionistic linear logic. Formulas are The multiplicative, additive, quantifier, identity, cut, and exchange rules are those of ${\mathsf{ILL}}_2$. Soft Linear Logic, written ${\mathsf{SLL}}_2$, replaces the ordinary exponential rules by exactly two rules:

$A_1,\dots ,A_m⊢B$

$!A_1,\dots ,!A_m⊢!B$

$\mathrm{\Gamma },\underset{n}{{\displaystyle \underbrace{A,\dots ,A}}}⊢C$

$\mathrm{\Gamma },!A⊢C$

There is no digging rule. Soft promotion boxes a proof and puts a bang on every assumption at the same boundary. Multiplexing consumes one banged assumption and exposes a fixed finite number $n$ of linear copies. The case $n=0$ is weakening; $n=1$ is dereliction.

Proof nets, degree, rank, and weight

Proof nets quotient sequent derivations by inessential rule permutations. Atomic cells represent logical rules; a cut plugs the output of one net into an input of another. A soft-promotion rule gives an exponential box, and Multiplexing gives a cell labeled by its rank.

For a proof net $u$, define:

• the degree $d(u)$ as the greatest nesting depth of exponential boxes;

• the rank $r(u)$ as the maximum label of a multiplexor, with a generic net viewed homogeneously at any chosen rank;

• the weight $W_u(X)$ as the polynomial obtained by summing cell weights.

An atomic right-logical cell and a constant have weight $1$; a left-logical cell and a multiplexor have weight $0$. The three box equations are The coefficient variable $X$ is later instantiated by the rank of the whole net. Multiplexors contribute no weight because their duplication potential is already charged by the factor $X$ at each surrounding exponential box.

For example, if $W_u(X)=2X+3$, then $$W_{!u}(X)=2X^2+3X+1.$$ At rank $4$, the weights are $11$ and $45$. The added box increases the degree by one and exposes exactly one more multiplication by the rank.

Proof of Lemma 56.2 — External reduction decreases weight

Proof. Inspect the external interaction rules. A logical cut removes its principal right cell and matching left cell, so the positive unit contribution disappears. A quantifier interaction removes the outer quantifier box and therefore its added $1$. In the exponential interaction, a multiplexor of rank $q\le n$ opens a box and creates at most $q$ copies of its contents. The redex was charged $n{W}_w(n)+1$ by that box, while the reduct contains at most $q{W}_w(n)$ from the copies and the multiplexor itself has weight $0$. Hence Commutative variants have the same local weights. These are all external interactions, so every step decreases the natural number $W_u(n)$. ◻

Proof of Theorem 56.3 — Normalization invariant, Lafont Theorem 2

Proof. By lemma 56.2, every step strictly decreases a natural number, so a sequence has length at most its initial weight. External proof net reduction is an interaction system: cells interact only through their principal ports. Its local diamonds give confluence, hence all terminating sequences have the same normal form up to commutation of independent reductions. ◻

Proof of Corollary 56.4 — Fixed-net polynomial

Proof. Induct on the net. Atomic and quantifier clauses preserve the bound after increasing $k$. Additive pairing adds the two bounds. Each exponential box multiplies the polynomial by $n$ and raises the degree by one. Since all coefficients are nonnegative, their sum is bounded by the value at $1$ times $n^p$. ◻

The qualification “fixed net” is load-bearing. If $u$ is part of the input, its degree $p$ may grow with its representation. Lafont explicitly notes that the resulting normalization procedure is exponential in total net size. Corollary 56.4 is a polynomial bound in the rank for a fixed program/proof and fixed depth, not one uniform polynomial in the combined encoding of arbitrary nets.

From typed nets to polynomial predicates

The boolean type and string type used in the representation construction are A homogeneous net of type $\mathsf{S}$, whose multiplexors all have rank $n$, encodes a Boolean string of length $n$. A generic net contains no multiplexors; iterators, conditionals, tape encodings, and a generic transition net assemble a fixed program for a fixed Turing machine. In the following sequent, ${\mathsf{S}}^{(m)}$ means $m$ separate copies of $\mathsf{S}$ in the antecedent; it is not $m$-fold boxing.

Proof of Theorem 56.5 — Polynomial predicate representation, Lafont Theorem 9

Proof. Encode a string of length $n$ by a homogeneous net of rank $n$. The generic length map yields the iterator controlling the time polynomial $P$, while the finite-tape encoding reserves the space polynomial $Q$. A fixed generic net implements one transition of the machine; composition with the iterator performs $P(n)$ transitions. The output net maps accepting states to the first Boolean projection and rejecting states to the second. Because strings are not freely duplicable in SLL2, the polynomial constructions consume $\mathrm{deg}P+\mathrm{deg}Q+1$ antecedent copies. The length net $\mathsf{S}⊢\mathsf{N}$ is the unnumbered generic net on page 11; Lemma 8 constructs the transition net, and their composition is Theorem 9 [Laf04]. ◻

The two directions now have matching interfaces. A fixed typed net has a fixed degree, so the weight invariant yields a polynomial in input rank. Conversely, theorem 56.5 builds a fixed generic net from a polynomial-time, polynomial-space machine. This is a complexity-class characterization at the representation boundary. It is not a symbolic cost formula for each source expression.

A term shadow and its limits

Soft lambda calculus provides a term presentation whose sharing construct corresponds to multiplexing [BM04]. A well-formed term makes each duplicable value cross an explicit soft boundary; its rank is the greatest number of copies demanded by a sharing site. The term system is useful for programming examples, but the normalization proof above is the SLL2 proof-net invariant. A term translation must preserve degree, rank, and the simulated reduction before it may inherit that bound.

This condition blocks a tempting transfer to graded typing. A semiring grade may express exact use, an upper bound, sensitivity, or security. Nothing in the laws of an arbitrary semiring constructs exponential boxes, bounds their nesting, or supplies the decreasing polynomial $W_u$. In particular:

• there is no AARA judgment or potential function in this chapter;

• $W_u(n)$ is indexed by proof-net rank, not by the numeric size of an ordinary program input;

• theorem 56.3 does not transfer to semiring-graded calculi without an explicit invariant-preserving translation.

A complete weight calculation

Let $a$ and $b$ be atomic right cells and form . Put $v$ in two nested exponential boxes and cut the outer box against a rank-$3$ multiplexor. Then Opening the outer box creates at most three copies of $!v$, of combined weight $3(3\cdot 3+1)=30$. Therefore the external step decreases the weight from $31$ to at most $30$. Continuing external reductions cannot take more than $31$ steps. The calculation says nothing about a different family whose box depth grows with its input encoding.

Sources and theorem boundary

The exact exponential rules are on page 3, the degree/rank/weight invariant and Theorem 2 are on pages 5–6, and the representation theorem is Theorem 9 on page 11 of Lafont [Laf04]. The programming-facing term comparison is bounded by Baillot and Mogbil’s soft lambda calculus [BM04]. No public proof assistant artifact is claimed. The chapter characterizes polynomial-time representation through fixed typed proof nets; it does not infer input-dependent costs for arbitrary graded programs.