References & Citations
Computer Science > Programming Languages
Title: Reverse AD at Higher Types: Pure, Principled and Denotationally Correct
(Submitted on 10 Jul 2020 (v1), last revised 22 Jan 2021 (this version, v2))
Abstract: We show how to define forward- and reverse-mode automatic differentiation source-code transformations or on a standard higher-order functional language. The transformations generate purely functional code, and they are principled in the sense that their definition arises from a categorical universal property. We give a semantic proof of correctness of the transformations. In their most elegant formulation, the transformations generate code with linear types. However, we demonstrate how the transformations can be implemented in a standard functional language without sacrificing correctness. To do so, we make use of abstract data types to represent the required linear types, e.g. through the use of a basic module system.
Submission history
From: Matthijs Vákár [view email][v1] Fri, 10 Jul 2020 10:05:46 GMT (3422kb)
[v2] Fri, 22 Jan 2021 10:02:59 GMT (480kb)
Link back to: arXiv, form interface, contact.