Reverse derivative categories
Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin, Dorette Pronk
The reverse derivative is a fundamental operation in machine learning and
automatic differentiation. This paper gives a direct axiomatization of a
category with a reverse derivative operation, in a similar style to that given
by Cartesian differential categories for a forward derivative. Intriguingly, a
category with a reverse derivative also has a forward derivative, but the
converse is not true. In fact, we show explicitly what a forward derivative is
missing: a reverse derivative is equivalent to a forward derivative with a
dagger structure on its subcategory of linear maps. Furthermore, we show that
these linear maps form an additively enriched category with dagger biproducts.