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

Abstract

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{à} 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.