Automatic Differentiation for ML-family languages: correctness via logical relations

We give a simple, direct and reusable logical relations technique for languages with recursive features and partially defined differentiable functions. We demonstrate it by working out the case of Automatic Differentiation (AD) correctness: namely, we present a proof of the dual numbers style AD macro correctness for realistic functional languages in the ML-family. We also show how this macro provides us with correct forward- and \textit{reverse-mode} AD. The starting point is to interpret a functional programming language in a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD macro and the basic $\omega$-cpo semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations argument. The key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$-cpos.