Reverse AD at higher types: pure, principled and denotationally correct

DOI10.1007/978-3-030-72019-3_22MaRDI QIDQ2233481zbMATH OpenOpenAlexFDO

Publication date 18 October 2021

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2007.05283

semantics program correctness automatic differentiation

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Numerical differentiation (65D25) Functional programming and lambda calculus (68N18) Abstract data types; algebraic specification (68Q65)

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.

Recommendations

Cites work

Cited in

(13)

This page was built for publication: Reverse AD at higher types: pure, principled and denotationally correct

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2233481)