The reverse derivative is a fundamental operation in machine learning and automatic differentiation [Martín Abadi et al., 2015; Griewank, 2012]. This paper gives a direct axiomatization of a category with a reverse derivative operation, in a similar style to that given by [Blute et al., 2009] 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.
@InProceedings{cockett_et_al:LIPIcs.CSL.2020.18, author = {Cockett, Robin and Cruttwell, Geoffrey and Gallagher, Jonathan and Lemay, Jean-Simon Pacaud and MacAdam, Benjamin and Plotkin, Gordon and Pronk, Dorette}, title = {{Reverse Derivative Categories}}, booktitle = {28th EACSL Annual Conference on Computer Science Logic (CSL 2020)}, pages = {18:1--18:16}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, ISBN = {978-3-95977-132-0}, ISSN = {1868-8969}, year = {2020}, volume = {152}, editor = {Fern\'{a}ndez, Maribel and Muscholl, Anca}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, URL = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2020.18}, URN = {urn:nbn:de:0030-drops-116611}, doi = {10.4230/LIPIcs.CSL.2020.18}, annote = {Keywords: Reverse Derivatives, Cartesian Reverse Differential Categories, Categorical Semantics, Cartesian Differential Categories, Dagger Categories, Automatic Differentiation} }
Feedback for Dagstuhl Publishing