Reverse AD at Higher Types: Pure, Principled and Denotationally Correct

07/10/2020
by   Matthijs Vákár, et al.
0

We show how to define source-code transformations for forward- and reverse-mode Automatic Differentiation 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.

READ FULL TEXT

Please sign up or login with your details

Forgot password? Click here to reset