# Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic Languages

arXiv: https://arxiv.org/abs/2111.15456 · HTML: https://mlsanity.com/paper/2111.15456/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Nov 2021.

## Built on by (most cited first, 1 of 1)

- [On the Correctness of Automatic Differentiation for Neural Networks with Machine-Representable Parameters](https://mlsanity.com/paper/2301.13370/) (2023)

## Abstract (arXiv)

Automatic differentiation (AD) aims to compute derivatives of user-defined functions, but in Turing-complete languages, this simple specification does not fully capture AD's behavior: AD sometimes disagrees with the true derivative of a differentiable program, and when AD is applied to non-differentiable or effectful programs, it is unclear what guarantees (if any) hold of the resulting code. We study an expressive differentiable programming language, with piecewise-analytic primitives, higher-order functions, and general recursion. Our main result is that even in this general setting, a version of Lee et al. [2020]'s correctness theorem (originally proven for a first-order language without partiality or recursion) holds: all programs denote so-called ωPAP functions, and AD computes correct intensional derivatives of them. Mazza and Pagani [2021]'s recent theorem, that AD disagrees with the true derivative of a differentiable recursive program at a measure-zero set of inputs, can be derived as a straightforward corollary of this fact. We also apply the framework to study probabilistic programs, and recover a recent result from Mak et al. [2021] via a novel denotational argument.