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. Dereliction is !A ⊸ A (use once from !A); codereliction is its dual, A ⊸ !A — inject a single resource into an exponential, so that the result may be consumed exactly once. 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.(∂t/∂x · u), the differential beta rule. ∂t/∂x · u is linear substitution: u replaces exactly one occurrence of x, summing over the possible choices.

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.

Metatheory. Ehrhard and Regnier add codereliction, cocontraction and coweakening as exact duals of the three exponential rules, so the exponential carries a bialgebra structure rather than merely a comonad one. Cut elimination holds, but reduction does not preserve single proofs: a cut between a codereliction and a contraction rewrites to a formal sum of two proofs, so the calculus is confluent only modulo the additive structure, and every model must be enriched over commutative monoids. The untyped differential λ-calculus (Ehrhard and Regnier 2003) is confluent and, containing the ordinary untyped λ-calculus, is not normalizing; the resource calculus obtained by fixing all multiplicities is strongly normalizing. Taylor expansion is the central construction: a term is developed as an infinite formal sum of resource terms, each of them normalizing, and Ehrhard and Regnier related this expansion to the term's Böhm tree. Ehrhard's finiteness spaces (2005) provide a model in which a proof denotes an analytic function given by a power series, and Blute, Cockett and Seely's differential categories (2006) axiomatize the structure a model must carry.

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

Limitations. The object of study is a formal linear combination of proofs, not a proof: reduction introduces sums, so the syntax must carry an additive structure that ordinary linear logic does not have, and there is no notion of the normal form of a derivation. Models are correspondingly constrained — hom-sets must be commutative monoids, and coherence spaces, where the union of two cliques need not be a clique, are therefore not a model of the differential rules even though they model linear logic. The interaction of promotion with the co-rules is delicate, and a large part of the theory is developed in the promotion-free fragment. Taylor expansion is an infinite sum that lives outside the calculus, so it is a metatheoretic device and not a derivation, and the coefficients require the semiring of coefficients to admit division by n!. Differentiation here is formal and algebraic, with no limits, norms or topology, so the connection to analytic differentiation and to automatic differentiation in machine learning is a shared algebraic structure rather than a theorem about numerical derivatives.

© 2026 Lingenic LLC