# Denotationally Correct, Purely Functional, Efficient Reverse-mode Automatic Differentiation

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

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 19 Dec 2022.

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

- [ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs](https://mlsanity.com/paper/2302.10636/) (2023)
- [nablaSD: Differentiable Programming for Sparse Tensors](https://mlsanity.com/paper/2303.07030/) (2023)

## Abstract (arXiv)

Reverse-mode differentiation is used for optimization, but it introduces references, which break the purity of the underlying programs, making them notoriously harder to optimize. We present a reverse-mode differentiation on a purely functional language with array operations. It is the first one to deliver a provably efficient, purely functional, and denotationally correct reverse-mode differentiation. We show that our transformation is semantically correct and verifies the cheap gradient principle. Inspired by PROPs and compilation to categories, we introduce a novel intermediate representation that we call 'unary form'. Our reverse-mode transformation is factored as a compilation scheme through this intermediate representation. We obtain provably efficient gradients by performing general partial evaluation optimizations after our reverse-mode transformation, as opposed to manually derived ones. For simple first-order programs, the obtained output programs resemble static-single-assignment (SSA) code. We emphasize the modularity of our approach and show how our language can easily be enriched with more optimized primitives, as required for some speed-ups in practice.