Reverse derivative categories — Robin Cockett, Geoffrey Cruttwell, Jonathan Gallagher, Jean-Simon Pacaud Lemay, Benjamin MacAdam, Gordon Plotkin & Dorette Pronk (2019). arXiv:1910.07065 (v1, PDF).
Axiomatises reverse-mode differentiation directly, in the style of Cartesian differential categories. Every reverse derivative category is a Cartesian differential category, and a Cartesian differential category has reverse derivatives exactly when its linear maps carry a contextual linear dagger; the linear maps form an additively enriched category with dagger biproducts.
Sources: the paper, arXiv:1910.07065v1, checked against the arXiv listing. Index: Papers.
Key definitions and results
- Definitions 1, 4: Cartesian left additive and Cartesian differential categories
- Definition 13: reverse differential combinator, axioms [RD.1–7]
- Theorem 16: every CRDC is a CDC
- Proposition 31: the functor into lenses
- Theorems 41–42: reverse = forward + contextual linear dagger
Concept notes
Reverse Derivative Category, Cartesian Differential Category, Dagger Category, Lens