Coherent differentiation generalizes derivatives and finite differences using monoid indices
Coherent differentiation with a monoid of degrees: derivatives, Taylor expansion, finite differences...
Logic in Computer Science
Summary
Differentiation is a way to understand how things change, but traditional methods assume you can always add changes together. This paper talks about a more flexible way, called coherent differentiation, which works even when addition is only partially defined. The authors extend this idea by using sets of indexes called commutative partial monoids to organize the changes, letting them describe many kinds of differentiations, including finite differences and truncated Taylor series. This generalization keeps the mathematical structure but lets the method apply in more situations.
What this means in practice
- •For mathematical software developers: Implement new differentiation tools that handle varied discrete and continuous derivatives within a unified categorical framework.
- •For scientific computing teams: Design algorithms for numerical differentiation that incorporate finite difference methods and truncated Taylor expansions in consistent ways.
A theory result. No direct application yet.
Authors
Thomas Ehrhard, Aymeric Walch
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.