Differential Linear Logic

Origin. Ehrhard and Regnier introduced differential linear logic (2003, 2006). Adds differentiation to linear logic. Derivative of proofs: ∂/∂x. Models smooth functions in denotational semantics. Foundation for differential λ-calculus and resource calculi.

Models. Differentiation in proofs. Linear logic: resources used exactly once. Differential: can "differentiate" resource usage. Co-dereliction: !A → A (use once from !A). Codereliction dual: produce !-output incrementally. Models Taylor expansion of proofs.

Formalism.

New rules: Standard linear logic + differential rules.

Codereliction (d): Γ ⊢ A ──────── Γ ⊢ !A

(Differs from standard !-introduction.)

Cocontraction (c̄): Γ ⊢ !A ⊗ !A ───────────── Γ ⊢ !A

Coweakening (w̄): Γ ⊢ 1 ─────── Γ ⊢ !A

Differential λ-calculus: D(t) · u: derivative of t applied to u. D(λx.t) · u = λx.(D(t) · u) + ∂t/∂x · u

Taylor expansion: t = Σₙ (1/n!) Dⁿ(t)|₀ Proof as sum of its "derivatives."

Resource λ-calculus: Variables have multiplicity. x[t₁,...,tₙ]: x used with resources t₁,...,tₙ.

Semantics: Models: differential categories. Smooth functions, power series. Finiteness spaces (Ehrhard).

Symbols.

Symbol	Unicode	Name	Meaning
d	—	Codereliction	Differential promotion
c̄	—	Cocontraction	Differential contraction
w̄	—	Coweakening	Differential weakening
D	—	Derivative	Differentiation
∂	U+2202	Partial	Partial derivative
!	—	Bang	Exponential
Σ	U+03A3	Sum	Taylor sum

Metatheory. Extends linear logic conservatively. Taylor expansion: proof = sum of differential proofs. Cut-elimination: differential cut-elimination. Models: smooth analysis, power series. Normalization results. Coherent with resource interpretations.

Applies to. Denotational semantics. Quantitative semantics. Probabilistic programming. Automatic differentiation. Machine learning theory. λ-calculus with resources.

Limitations. Abstract and technical. Tool support minimal. Learning curve from linear logic. Practical applications emerging. Small research community. Connection to ML differentiation indirect.