Higher Order Automatic Differentiation of Higher Order Functions

TL;DR

This paper provides a semantic framework and correctness proofs for higher-order automatic differentiation in a higher-order language, extending to higher derivatives via Taylor approximations.

Contribution

It introduces a semantic correctness proof for a forward-mode AD method on higher-order functions using diffeological spaces and logical relations.

Findings

Semantic correctness of AD proven using diffeological spaces

Characterization of AD as a unique structure-preserving macro

Extension of analysis to higher derivatives via Taylor approximation

Abstract

We present semantic correctness proofs of automatic differentiation (AD). We consider a forward-mode AD method on a higher-order language with algebraic data types and we characterise it as the unique structure-preserving macro given a choice of derivatives for basic operations. We describe a rich semantics for differentiable programming based on diffeological spaces. We show that it interprets our language and we phrase what it means for the AD method to be correct with respect to this semantics. We show that our characterisation of AD gives rise to an elegant semantic proof of its correctness based on a gluing construction on diffeological spaces. We explain how this is in essence a logical relations argument. Throughout we show how the analysis extends to AD methods for computing higher-order derivatives using a Taylor approximation.