PaperlayerView exact revision on arXiv

Source-linked AI summary

Coherent differentiation with a monoid of degrees: derivatives, Taylor expansion, finite differences...

Thomas Ehrhard, Aymeric Walch

arXiv:2610.29874v1cs.LOmath.CT

TL;DR

The paper addresses how differentiation can be modeled without requiring total addition of morphisms, which can entail nondeterminism. It generalizes coherent differentiation using a nonnegative commutative partial monoid of degrees, obtaining a framework that includes finite differences and truncated Taylor expansions.

  • Problem

    Existing categorical models of differential lambda-calculus and differential linear logic require addition of morphisms, an assumption that can entail nondeterminism.

    Source: Introduction · p. 2

  • Method

    The paper parameterizes coherent differentiation by a nonnegative partial commutative monoid of degrees and extends the summability functor to nonlinear morphisms.

    Source: Introduction · pp. 3, 6

  • Results

    The theory subsumes coherent differentiation and coherent Taylor expansion, and accommodates finite differences, truncated Taylor expansion, and Taylor expansion with a remainder.

    Source: Conclusion · p. 79

  • Takeaways & Limitations

    Different choices of degree monoid yield distinct differential theories, including finite-difference and Taylor-expansion variants.

    Source: Conclusion · p. 79

    The paper uses the nonnegative SPCM-based theory because general recursion appears hardly compatible with non-positive partial commutative monoids.

    Source: Introduction · p. 7

Abstract

from arXiv · show

Coherent differentiation has been introduced a few years ago as a refinement of the (categorical semantics of the) differential lambda-calculus and of differential linear logic, compatible with the determinism of computation, and hence in categories where addition of morphisms in the hom-sets is only partially defined. In this setting differentiation is implemented by a kind of ''tangent functor'', with the difference that it maps an object to its object of summable tuples rather to a tangent bundle. In our earlier work, these tuples were pairs in the case of simple differentiation, and families indexed by integers when dealing with Taylor expansion and the Fa{\`a} di Bruno formula. We push this idea further, considering now tuples indexed by an arbitrary commutative partial monoid satisfying a nonnegativity condition. The monoid structure on these indices plays a crucial role in the definition of the ''differential'' calculus associated with this ''tangent functor''. In that way, and without changing the general categorical infrastructure of coherent differentiation, this theory accommodates new notions of ''differentiation'' of which we describe several instances. Among many others, such notions include various forms of finite differences as well as Taylor expansion truncated at any fixed degree, and finite Taylor expansion of a fixed finite degree with a remainder.

Introduction

The introduction motivates coherent differentiation as a way to differentiate analytic maps without requiring total addition of morphisms, then generalizes its tangent-like construction to tuples indexed by a nonnegative commutative partial monoid. This framework subsumes coherent differentiation and Taylor expansion and includes finite-difference and truncated-Taylor examples.

Contribution of the paper

  • For D = N with addition, the induced functor computes the Faà di Bruno formula, a functorial generalization of Taylor expansion.The summability functor characterizes when a countable family of morphisms can be summed.Source: Introduction · p. 4
  • The paper generalizes coherent differentiation to degrees in an arbitrary commutative partial monoid satisfying a nonnegativity condition.The degree monoid parameterizes the theory; the earlier binary differentiation and natural-number Taylor expansion arise as instances.Source: Introduction · pp. 4, 6
  • For D = N with maximum, T maps successive input increments to successive output differences, giving a finite-difference instance of the theory.For D = {0,1} with 1 +D 1 = 1, the construction gives T f(x0,x1) = (f(x0), f(x0+x1)−f(x0)).Source: Introduction · pp. 5–6
  • For D = {0, …, N} with truncated addition, T contains a Taylor expansion of order N−1 with a remainder and has a Faà di Bruno form of that order.The general expression of T f is more complicated than the displayed Taylor term.Source: Introduction · p. 5
  • The framework extends a summability functor S to nonlinear morphisms via a distributive law with the resource comonad, yielding a differentiation functor T.In the representable case, a !-coalgebra structure on the degree object induces the distributive law and the associated differential comonoid.Source: Introduction · pp. 3, 4, 6

Comparison with previous articles

  • The theory uses nonnegative partial commutative monoids because the authors focus on models with general recursion, whose semantics appears hardly compatible with non-positive partial commutative monoids.The paper leaves the cartesian theory of coherent Taylor expansion outside its scope.Source: Introduction · pp. 6–7

1 Differences in LL

The section presents a difference-based characterization of stability on coherence spaces and a functor that applies the difference operation to stable functions. This construction is an instance of the paper’s general theory.

1.1 Stability and differences

  • Stability is characterized by conditional multiplicativity: when x ∪ x′ is a clique, f(x) ∩ f(x′) ⊆ f(x ∩ x′).The section presents this as an equivalent condition for Scott-continuous functions.Source: §1.1 · p. 9
  • The authors report that this characterization had not appeared in the available literature on stable functions.They note that the notion of stable functions is more than 40 years old.Source: §1.1 · p. 9
  • The difference operator sends f to the increment f(x ∪ u) \ f(x) on cliques compatible with u, and its functorial version maps (x, u) to (f(x), f(x ∪ u) \ f(x)).The input pairs require x ∩ u = ∅ and x ∪ u to be a clique.Source: §1.1 · p. 10
  • For Scott-continuous stable f, Tf is also Scott-continuous and stable, and T is a functor; its monad and comonad structures satisfy compatibility conditions making it a bimonad.The general theory supplies the bimonad structure used in this example.Source: §1.1 · pp. 10–11

2 Categorical preliminaries

The section collects categorical tools used later, while assuming standard notions such as adjunctions and monads are familiar. It also establishes a basic commuting-diagram lemma.

2 Categorical preliminaries

  • The section gathers the categorical material needed for the paper and directs readers to definitions and results where they are used.The authors say readers may skip this preliminary section and consult it as needed.Source: §2 · p. 11
  • The notation fixes ⊗ as the monoidal product, 1 as its unit, and λ, ρ, α, and γ as the unitors, associator, and braiding.The braiding notation applies when the monoidal category is symmetric.Source: §2 · p. 11
  • For morphisms f : X → 1 and g : 1 → Y in a monoidal category, the diagram in Lemma 2.1 commutes.The proof uses naturality of λ and ρ and λ1 = ρ1.Source: §2 · p. 11

2.1 Notations

The section establishes notation for finite multisets, including their addition, finite sums, tagging by an index, and flattening nested multisets.

2.1 Notations

  • A finite multiset on A is a function A → N with finite support, and [ ] denotes the empty multiset.The support is the set of elements assigned nonzero multiplicity.Source: §2.1 · p. 11
  • The notation m1 + m2 and Σ_i mi denotes pointwise addition of multisets, while [a1, …, ak] records the listed elements with multiplicities.For finite I, i · m tags each element of m with index i.Source: §2.1 · p. 11
  • For a finite multiset M of finite multisets, Σ M denotes the multiset obtained by adding its constituent multisets.The definition writes this as the sum of the listed members of M.Source: §2.1 · p. 11

2.2 Commutative and symmetric (co)monoids

These preliminaries develop monoid-like structures in monoidal categories and explain how they support the paper’s functorial constructions. They also relate monads and comonads to these structures.

2.2.1 Monoids and commutative monoids

  • A monoid in a monoidal category consists of an object, a unit, and a multiplication; in a symmetric monoidal category, commutativity requires multiplication to respect the symmetry.The section also defines the dual comonoid structure.Source: §2.2.1 · p. 12

2.2.2 Symmetric monoids

  • Symmetric monoids add a symmetry operation to a monoid, with compatibility conditions including involution and the Yang–Baxter equation.The framework covers both symmetric monoidal categories and categories of functors with composition as monoidal product.Source: §2.2.2 · pp. 13–14

2.2.3 Lax and oplax monoidal functor

  • Strong monoidal functors preserve symmetric monoids, symmetric comonoids, and symmetric bimonoids.The preservation result is stated in Theorem 2.12.Source: §2.2.3 · pp. 15–16
  • Lax monoidal functors preserve monoids, while oplax monoidal functors preserve comonoids; strong monoidal functors combine the two structures.The section defines strong monoidal functors as lax and oplax structures that are inverse to each other.Source: §2.2.3 · pp. 15–16

2.2.4 Monads and comonads

  • Monads and comonads are monoids and comonoids in the category of endofunctors, respectively, and compatible monoidal structure extends to their Kleisli or Eilenberg–Moore categories.The specific extension depends on whether the monad or comonad structure is lax or oplax.Source: §2.2.4 · pp. 17–18

2.3 Resource categories and coalgebras of the resource modality

The section sets out the categorical structures used to model linear and nonlinear computation, then relates coalgebras to commutative comonoids. For Lafont categories, it proves these structures yield isomorphic categories and that the correspondence preserves products.

2.3 Resource categories and coalgebras of the resource modality

  • A resource category combines symmetric monoidal and cartesian structures with a resource modality whose comonad and Seely isomorphisms connect them.Its Kleisli category models nonlinear morphisms, while the linear category maps into it via Der.Source: §2.3 · p. 18

2.3.1 Coalgebras and comonoids

  • Every coalgebra carries a canonical commutative comonoid structure, and the Eilenberg–Moore category of coalgebras is cartesian.The induced structure extends the comonoid structure on free coalgebras.Source: §2.3.1 · pp. 19–20

2.3.2 The Lafont situation

  • A Lafont SMC is characterized by a right adjoint to the forgetful functor from commutative comonoids, yielding cofree commutative comonoids.When the Lafont SMC is cartesian, its induced comonad makes it a resource category, and its free coalgebra comonoids coincide with the free commutative comonoids.Source: §2.3.2 · p. 20
  • For a Lafont SMC, the category of commutative comonoids is isomorphic to the Eilenberg–Moore category of its induced comonad.The functors implementing the isomorphism are inverse; the comonoid-to-coalgebra functor is strict monoidal and thus transports symmetric monoids, comonoids, and bimonoids.Source: §2.3.2 · pp. 21–22

2.4 Distributive laws between functors and comonads

Distributive laws provide a way to extend functors to Kleisli categories or lift them to Eilenberg–Moore categories. The section shows that monoidal structure lets these constructions transport symmetric (co)monads and bimonoids, including the structure used for coherent differences.

2.4 Distributive laws between functors and comonads

  • The paper generalizes coherent differences from coherence spaces to Kleisli categories of other models of linear logic using a distributive law.The distributive-law framework also serves as the means to define the D-differentiation functor in the Kleisli category of the exponential comonad.Source: §2.4 · pp. 22–23
  • A distributive law between a functor and a comonad corresponds to an extension of the functor to the Kleisli category, while the dual construction provides liftings to the Eilenberg–Moore category.The relevant categories of distributive laws are isomorphic to categories of extensions and liftings.Source: §2.4 · pp. 23–24
  • The extension and lifting constructions are strict monoidal, so symmetric monoids, comonoids, and bimonoids transfer to the Eilenberg–Moore category.A symmetric monad equipped with a distributive law induces a symmetric monad there; the corresponding construction supplies the symmetric bimonad of coherent differences.Source: §2.4 · p. 24

2.5 From monoids to monads

This section builds reader/writer effects from monoids and comonoids, then uses coalgebra structures and distributive laws to make these constructions compatible with the exponential. The resulting functorial framework is strong monoidal and supports the paper’s D-differentiation construction.

2.5 From monoids to monads

  • Commutative bimonoids in the Eilenberg–Moore category, or in commutative comonoids for Lafont categories, yield reader/writer effects compatible with the exponential.The construction composes strong monoidal functors, and the paper notes that many concrete linear-logic models have D-differentiation built this way.Source: §2.5 · p. 25

2.5.1 Reader and writer monads

  • Tensoring by a commutative monoid induces a writer monad, while internal hom from a commutative comonoid induces a reader monad; bimonoids yield bimonads.The tensor and internal-hom assignments are strong monoidal functors, and their structures are related by the mate isomorphism.Source: §2.5.1 · pp. 26–27

2.5.2 The mate isomorphism.

  • The mate isomorphism relates natural transformations involving tensor and internal hom, and its compositionality identifies the induced monad multiplication with the corresponding comonad comultiplication.The paper uses this correspondence to relate the structures on the writer and reader constructions.Source: §2.5.2 · p. 27

2.5.3 From coalgebras to distributive laws

  • Each coalgebra induces distributive laws for the tensor and internal-hom functors, related to each other by the mate isomorphism.These assignments form strong monoidal functors; conversely, the corresponding distributive laws determine a coalgebra structure.Source: §2.5.3 · pp. 28–29

3 Categories enriched over SPCMs

The section develops strong partial commutative monoids (SPCMs) to model partial summability and categories whose hom-sets carry that structure. It then defines enrichment and compatibility conditions for monoidal, closed, and product structures.

3 Categories enriched over SPCMs

  • Differential categories typically use commutative-monoid enrichment, while this framework defines differentiation over categories enriched by partial commutative monoids.The shift allows summability to be partial rather than requiring addition to be defined throughout each hom-set.Source: §3 · p. 29

3.1 SPCMs and infinitary SPCMs

  • An SPCM specifies a partial sum on finite or at most countable indexed families, subject to unary summability and partition associativity.The empty family is summable, and reindexing by bijections preserves summability and its sum.Source: §3.1 · pp. 30–31

3.2 Enrichment over SPCMs

  • An SPCM-enriched category equips each hom-set with an SPCM structure and requires composition to preserve summable families in each argument.The section also specifies compatibility with tensor products, internal homs, and finite products through bilinearity or preservation of summability.Source: §3.2 · pp. 32–34

4 Summability structures

The section develops D-summability structures for categories with partially defined sums, showing how they induce enrichment and canonical monadic structures and characterizing their compatibility with tensor, internal-hom, and cartesian structure. Examples of degree monoids include theories of truncated Taylor expansion and finite differences.

4 Summability structures

  • Degree monoids yield truncated Taylor expansion, Taylor expansion with a remainder, finite differences, and a prospective multivariate Taylor theory.The examples use bounded natural numbers with partial ordinary addition, capped addition, maximum as addition, and finite multisets on N, respectively.Source: §4 · p. 35
  • A D-summability structure represents summable D-indexed morphism families by unique witnesses into SX, with projections πi and sum map σ.The category's homset zeros are zero morphisms; the projections are jointly monic, and summability is preserved under composition on either side.Source: §4 · pp. 35–36

4.1 D-summability structures and D-ary SPCM enrichment

  • A D-summability structure is unique up to natural isomorphism, and it makes the category enriched over D-ary SPCMs.The enrichment proof builds summability structures on iterates Sn indexed by Dn, then reindexes general families into such index sets.Source: §4 · p. 36, §4.1 · pp. 37–38

4.2 The monad (and comonad) structure of the summability functor

  • The summability functor S carries a canonical symmetric monad structure, with multiplication summing projections over degree decompositions i = l + r.The decomposition sets D(i) form a partition of the composable degree pairs; they cover all of D2 exactly when D is total.Source: §4.2 · p. 39
  • In the Kleisli category, morphisms into SY can be viewed as D-indexed formal power series, and composition is a Cauchy product.For D = N this is ordinary power-series multiplication; for D = {0, 1} with 1 + 1 undefined, it gives degree-one polynomials with ε2 = 0.Source: §4.2 · p. 40
  • The same functor S also carries a canonical symmetric comonad structure, with comultiplication given by the natural lift l characterized by πi πj l = δi,j πi.The counit is σ, and the comonad is stated as the triple (S, σ, l, c).Source: §4.2 · pp. 40–41
  • When D is total, (S, σ, l, ι0, τ, c) is a symmetric bimonad.The theorem’s proof uses totality only for its final commutation.Source: §4.2 · p. 42

4.3 Compatibility of the D-summability structure with the tensor product and the internal hom

  • Tensor compatibility is equivalent to zero preservation and summability of (πi ⊗ X2)i∈D with sum σ ⊗ X2; it makes (S, φ1) a commutative strong monad.The analogous compatibility map φ2 is also defined using (X1 ⊗ πi)i∈D.Source: §4.3 · pp. 43–44
  • Closed monoidal enrichment is equivalent to summability of (X ⊸ πi)i∈D and to the canonical map φ⊸: S(X ⊸ Y) → X ⊸ SY being an isomorphism.The paper names this equivalent condition (S-⊸), a property of the summability structure rather than an additional structure.Source: §4.3 · p. 45

4.4 D-summability structure in a cartesian category

  • In a cartesian category, cartesian D-ary SPCM-enrichment is equivalent to summability of the product projections and to the canonical map ⟨S pr_l⟩l∈L being an isomorphism.This condition is called (S-&); under it, the monad S has a strong monoidal structure.Source: §4.4 · p. 46

5 D-summability structures in the representable case

This section studies representable D-summability structures, in which a summability functor is induced by an object whose jointly epic projections encode summability. It develops examples and algebraic properties of that object, including monoid and, when D is total, bicommutative bimonoid structures, and relates them to symmetric monad and comonad structures identified with S.

5 D-summability structures in the representable case

  • A D-summability structure is representable when its functor has the form S = (D ⊸) for a specific object D.The section’s general construction uses a D-summability object to induce this structure.Source: §5 · p. 47

5.1 Joint epicity, joint monicity and currying

  • In an SMCC, jointly epic families are completely jointly epic, linking joint epicity to currying and internal homs.Lemma 5.3 further characterizes joint epicity by joint monicity of the induced family under internal hom.Source: §5.1 · p. 47

5.2 D-summability object

  • A pre-D-summability object induces a pre-D-summability structure, and representable D-summability ensures the (S-&) , (S-⊗), and (S-⊸) properties.The D-summability object is unique up to unique isomorphism; the section also motivates allowing objects beyond D-fold products of 1.Source: §5.2 · pp. 47–49

5.3.1 Coherence spaces

  • For coherence spaces, a family of morphisms is summable when its union is a morphism and distinct family members are disjoint.The representability construction uses DL = &i∈D 1, with underlying set D.Source: §5.3.1 · p. 50

5.3.2 Probabilistic coherence spaces

  • For probabilistic coherence spaces, a family is summable exactly when, for every input in PY, the sum of its output vectors belongs to PX.The witness packages the family’s matrices as a morphism into SX, yielding representable summability.Source: §5.3.2 · p. 52

5.4 The structures of the D-summability functor, in the representable case

  • In the representable case, the structures of S = HDL are made explicit through elementary (co)algebraic structures on DL, including a commutative comonoid.The text also states that π0 is a monoid morphism from 1 to DL.Source: §5.4 · p. 52
  • The representable object DL has a unique multiplication making it a commutative monoid; if D is total, its comonoid and monoid structures form a bicommutative bimonoid.The multiplication satisfies l(π_i ⊗ π_j) = δ_i,jπ_i; the bimonoid property is stated to hold exactly when D is total.Source: §5.4 · pp. 54, 56
  • The induced structures on HDL are a symmetric monad and a symmetric comonad; Theorem 5.27 identifies them with S and states Hγ = c.When D is total, the theorem also identifies the resulting structure HDL with S.Source: §5.4 · p. 55
  • The text notes that it has not proved whether the bimonoid and symmetric bimonad properties imply that D is total.Totality is given as a sufficient condition, but the converse remains unproved.Source: §5.4 · p. 55
  • In the Pcoh example, elements of PDL are represented by coordinates indexed by D, and multiplication sends u ⊗ v to the coordinatewise products u_i v_i.The passage gives the representation PDL ≃ [0,1]^D and characterizes multiplication by l · (u ⊗ v) = Σ_i∈D u_i v_i e_i.Source: §5.4 · p. 56

6 The D-differentiation structure

This section defines the D-differentiation structure by extending the summability functor through a distributive law with the exponential modality and specifying axioms for its monad and comonad structures. It describes the structure in representable settings and illustrates how it supports qualitative and probabilistic differentiation calculi—including finite differences, Faà di Bruno and Taylor formulas, and truncated expansions—with available calculi depending on the degree monoid.

6 The D-differentiation structure

  • D-differentiation extends S to nonlinear morphisms through a distributive law with !, and its axioms ensure structural properties including local behavior and symmetry of second differences.For D=({0,1}, max), the example maps (x0,x1) to (f(x0), f(x0+x1)−f(x0)).Source: §6 · pp. 56, 58, 59
  • Under ∂-Schwarz and ∂-add, T forms a symmetric monad; with ∂-lift, ∂-sum, and ∂-Schwarz it forms a symmetric comonad, and residuation yields a symmetric bimonad.Residuated categories require D to be total and ∂-sum to hold.Source: §6 · pp. 58–59

6.1 The D-differentiation structure, in the representable case

  • Representable D-differentiation is obtained from a coalgebra structure on DL with conditions making DL a commutative bimonoid in L!; in Lafont resource categories it is unique, and residuated when D is total.The coalgebra’s conditions induce ∂-local, ∂-add, and ∂-lift, while ∂-Schwarz and ∂-& always hold.Source: §6.1 · pp. 59–60

6.2 Examples of representable D-differentiation resource categories

  • The examples subsection illustrates representable D-differentiation in coherence spaces and probabilistic coherence spaces for various choices of D.Source: §6.2 · p. 61

6.2.1 Coherence spaces

  • In coherence spaces, e∂ relates a degree i to finite multisets whose entries sum to i; for D=N with max, the induced component at i>0 is a set difference of successive bt values.At i=0 the component is bt(x0).Source: §6.2.1 · pp. 61–62
  • In coherence spaces, the functor T gives a qualitative Faà di Bruno formula without rational coefficients, and the earlier theory is recovered by taking D = {0, 1} with 1 +D 1 = 1.For the original Girard exponential, differentiation is available for D = (N, max), but not for D = (N, +).Source: §6.2.1 · p. 63

6.2.2 Probabilistic coherence spaces

  • For D = (N, max), the probabilistic construction gives finite differences: c Tt(x)i = bt(x0 + ··· + xi) − bt(x0 + ··· + xi−1) for i > 0.Naturality of the counit in this case means that bt is Scott continuous.Source: §6.2.2 · p. 65
  • For D = (N, +), probabilistic coherence spaces yield all k-derivatives, and the induced map computes the Faà di Bruno formula with coefficients that tame possibly oversized terms.The formula uses extended derivatives at 0; its terms need not individually belong to PY, while their combination does.Source: §6.2.2 · pp. 65–66
  • With D = {0, …, N} and partial addition, the probabilistic construction gives the Faà di Bruno formula truncated at rank N; the counit is natural only for polynomials of degree at most N.This partial monoid is not total.Source: §6.2.2 · p. 67
  • Taking D = {0, …, N} with i +D j = inf(i + j, N) yields a Taylor expansion of order N − 1 whose last tuple component is the remainder, and T is a bimonad.Here the monoid is total.Source: §6.2.2 · p. 68
  • The structure D = ({0,1,2}, +), with 1+1=2, 1+2=1, and 2+2=2, is a nonnegative total commutative monoid; the text also specifies the monad structure of T.The counit of the comonad is cσX(x⃗) = x0 + x1 + x2.Source: §6.2.2 · pp. 68–69

7 Products, function spaces and fixpoints

This section develops categorical machinery for D-differentiation in products and function spaces, including conditions for fixpoint operators and their behavior in probabilistic coherence spaces. Under Scottness and closedness, it shows that differentiating a fixpoint is equivalent to taking the fixpoint of the differential.

7.1 Partial derivatives

  • The global derivative is a monad-structure “sum” of coordinate partial derivatives, which the theory defines with their expected properties without further assumptions.The construction uses the strong monoidal and commutative monad structure induced on T.Source: §7.1 · pp. 70–72

7.2 Linear and multilinear morphisms

  • Linearity in an argument implies additivity and D-linearity; Theorem 7.9 proves the latter implication coordinate-wise, while converses need not hold generally.The result is presented for binary morphisms, with an n-ary generalization described as feasible.Source: §7.2 · pp. 72–73

7.3 The closed case: function spaces

  • The Kleisli category of T is cartesian closed, with products given by & and internal hom X ⇒ TY.The result follows from T's strong monoidal structure and an isomorphism for its pointwise structure on function spaces.Source: §7.3 · pp. 74–75
  • Currying then internalizing T agrees with deriving then currying, establishing a form of differential β-reduction for any f ∈ L!(U & X, Y).The comparison uses the internalized action of T and the second partial derivative.Source: §7.3 · p. 75
  • Differentiating application yields T2ap(f, g) = ap(T2,3f, T2g), for f and g in the function spaces specified by Theorem 7.13.T2,3f represents the derivative of f with respect to both its X and Y arguments.Source: §7.3 · p. 76

7.4.1 Reminder about fixpoint operators in a CCC

  • In a λ-category, a morphism Y gives the least fixpoint for each f: Z → X ⇒ X, with Y ◦ f the least g satisfying Ev ◦ ⟨f, g⟩ = g.A λ-category is a cartesian closed category enriched in ω-cpos whose pairing and currying operations are Scott-continuous.Source: §7.4.1 · p. 77

7.4.2 The D-differentiation of fixpoints

  • If L is Scott—its morphism spaces have lubs of monotone sequences, composition is Scott-continuous, and ! is increasing and Scott-continuous—then L! is a λ-category.The theorem follows using continuity of currying; continuity of pairing also holds when L is Scott.Source: §7.4.2 · pp. 77–78
  • In probabilistic coherence spaces, nonnegative matrix coefficients yield an analytic least-fixpoint operator, whereas allowing negative coefficients can produce a discontinuous fixpoint that is not a power series.Pcoh is Scott, and its least fixpoint is sup_n b t^n(0).Source: §7.4.2 · p. 78
  • Under Scottness and closedness, the differential of a fixpoint equals the fixpoint of the corresponding differential, allowing coherent differentiation to combine with general fixpoints.The identity is T2(Fix(f)) = Fix(T2,3f).Source: §7.4.2 · pp. 78–79

Conclusion

The paper develops D-differentiation, a general theory parameterized by nonnegative partial commutative monoids. It encompasses coherent differentiation and coherent Taylor expansion, as well as finite-difference and truncated-Taylor calculi.

Conclusion

  • D-differentiation generalizes coherent differentiation and coherent Taylor expansion through choices of a nonnegative partial commutative monoid D.The respective index structures are D = {0, 1}, with 1 + 1 undefined, and D = (N, +).Source: Conclusion · p. 79
  • Other choices of D yield finite-difference calculi, truncated Taylor expansion, and finite Taylor expansion with a remainder.Source: Conclusion · p. 79
  • A syntactic counterpart in the form of a functional programming language is under development.The authors describe it as having fewer syntactic constructs and reduction rules than [Ehr23a].Source: Conclusion · p. 79

Related papers

Loading 2610.29874v1…