References & Citations
Computer Science > Programming Languages
Title: Higher Order Automatic Differentiation of Higher Order Functions
(Submitted on 17 Jan 2021 (v1), last revised 21 Mar 2022 (this version, v6))
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.
Submission history
From: Matthijs Vákár [view email] [via LOGICAL proxy][v1] Sun, 17 Jan 2021 19:24:46 GMT (65kb)
[v2] Mon, 11 Oct 2021 11:49:00 GMT (67kb)
[v3] Sun, 30 Jan 2022 16:21:09 GMT (68kb)
[v4] Mon, 7 Mar 2022 12:12:27 GMT (70kb)
[v5] Tue, 8 Mar 2022 16:37:12 GMT (70kb)
[v6] Mon, 21 Mar 2022 10:02:03 GMT (70kb,D)
Link back to: arXiv, form interface, contact.