Compositional Taylor expansion in cartesian differential categories

This paper provides a compositional approach to Taylor expansion, in the setting of cartesian differential categories. Taylor expansion is captured here by a functor that generalizes the tangent bundle functor to higher order derivatives. The fundamental properties of Taylor expansion then boils down to naturality equations that turns this functor into a monad. This monad provides a categorical approach to higher order dual numbers and the jet bundle construction used in automated differentiation.

The combination of the theory of the differential calculus with the theory of programming languages has seen a tremendous growth in the last decades, most notably in the fields of automated differentiation (AD) [1] and of the differential λ-calculus [2]. Both AD and the differential λ-calculus aim at computing the derivative of a program in a compositional way, this compositionality is crucial to scale those methods to complex assemblies of programs. Because of this interplay between derivatives and composition, category theory provides a strong mathematical basis for both of those fields. Categorical semantics provides critical proofs methods of correctness of the AD algorithm [3], [4], and the differential lambda calculus is deeply related to the categorical semantics of Linear Logic (LL) from its very inception [2], [5]. Among those categorical approaches, cartesian differential categories [6]

provide a direct axiomatization of derivatives in any cartesian category. As such, they serve as a framework to understand the differential calculus through the lenses of compositionality.

The compositionality of the derivative is expressed by the chain rule:

The issue of the chain rule is that it is not entirely compositional, because the derivative (g • f ) ′ also depends on f , and not only on g ′ and f ′ . For this reason, one often consider the tangent bundle operator T that intuitively maps f : X → Y to the function Tf : (x, u) → (f (x), f ′ (x) • u). This operator exists in any cartesian differential category, and the chain rule boils down to a functoriality equation on T: T(g • f ) = Tg • Tf . Furthermore, the other axioms of the differential calculus (such as the linearity of the derivative or the symmetry of the higher order derivatives) turn out to be equivalent to naturality equations [7], [8] that turn T into a monad [8] whose algebraic structure is similar to that of dual numbers widely used in AD. This suggests that differentiation is an effect in the sense of Moggi [9], further cementing the use of category theory as a strong mathematical foundation for the differential calculus.