# ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs

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

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 60 references that are in the map.
- First posted on arXiv 21 Feb 2023.

## Builds on (most cited first, 23 of 23)

- [On the Global Convergence of Gradient Descent for Over-parameterized Models using Optimal Transport](https://mlsanity.com/paper/1805.09545/) (2018)
- [A mathematical model for automatic differentiation in machine learning](https://mlsanity.com/paper/2006.02080/) (2020)
- [Disintegration and Bayesian Inversion via String Diagrams](https://mlsanity.com/paper/1709.00322/) (2017)
- [On Correctness of Automatic Differentiation for Non-Differentiable Functions](https://mlsanity.com/paper/2006.06903/) (2020)
- [A Convenient Category for Higher-Order Probability Theory](https://mlsanity.com/paper/1701.02547/) (2017)
- [Reverse derivative categories](https://mlsanity.com/paper/1910.07065/) (2019)
- [Correctness of Automatic Differentiation via Diffeologies and Categorical Gluing](https://mlsanity.com/paper/2001.02209/) (2020)
- [ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs](https://mlsanity.com/paper/2212.06386/) (2022)
- [Reparameterization Gradient for Non-differentiable Models](https://mlsanity.com/paper/1806.00176/) (2018)
- [You Only Linearize Once: Tangents Transpose to Gradients](https://mlsanity.com/paper/2204.10923/) (2022)
- [Denotational validation of higher-order Bayesian inference](https://mlsanity.com/paper/1711.03219/) (2017)
- [A Domain Theory for Statistical Probabilistic Programming](https://mlsanity.com/paper/1811.04196/) (2018)
- [Densities of Almost Surely Terminating Probabilistic Programs are Differentiable Almost Everywhere](https://mlsanity.com/paper/2004.03924/) (2020)
- [Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference](https://mlsanity.com/paper/2208.10530/) (2022)
- [Backpropagation in the Simply Typed Lambda-calculus with Linear Negation](https://mlsanity.com/paper/1909.13768/) (2019)
- [Automatic Differentiation in PCF](https://mlsanity.com/paper/2011.03335/) (2020)
- [CHAD: Combinatory Homomorphic Automatic Differentiation](https://mlsanity.com/paper/2103.15776/) (2021)
- [Measurable Cones and Stable, Measurable Functions](https://mlsanity.com/paper/1711.09640/) (2017)
- [Denotational Correctness of Forward-Mode Automatic Differentiation for Iteration and Recursion](https://mlsanity.com/paper/2007.05282/) (2020)
- [The Base Measure Problem and its Solution](https://mlsanity.com/paper/2010.09647/) (2020)
- [Concrete categories and higher-order recursion (With applications including probability, differentiability, and full abstraction)](https://mlsanity.com/paper/2205.15917/) (2022)
- [Denotationally Correct, Purely Functional, Efficient Reverse-mode Automatic Differentiation](https://mlsanity.com/paper/2212.09801/) (2022)
- [Factorisation systems for logical relations and monadic lifting in type-and-effect system semantics](https://mlsanity.com/paper/1804.03460/) (2018)

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

- [Compile Once, Differentiate Everywhere: A Differentiable Meta-Circular Interpreter](https://mlsanity.com/paper/2606.09930/) (2026)
- [Differentiate the Evaluator, Not the Program: An Efficient Runtime Representation for Neuro-Symbolic Learning](https://mlsanity.com/paper/2607.03574/) (2026)
- [Sample-Smooth Spaces: A Convenient Category for Differentiable Probabilistic Programming](https://mlsanity.com/paper/2609.26270/) (2026)

## Abstract (arXiv)

We introduce a new setting, the category of ωPAP spaces, for reasoning denotationally about expressive differentiable and probabilistic programming languages. Our semantics is general enough to assign meanings to most practical probabilistic and differentiable programs, including those that use general recursion, higher-order functions, discontinuous primitives, and both discrete and continuous sampling. But crucially, it is also specific enough to exclude many pathological denotations, enabling us to establish new results about both deterministic differentiable programs and probabilistic programs. In the deterministic setting, we prove very general correctness theorems for automatic differentiation and its use within gradient descent. In the probabilistic setting, we establish the almost-everywhere differentiability of probabilistic programs' trace density functions, and the existence of convenient base measures for density computation in Monte Carlo inference. In some cases these results were previously known, but required detailed proofs with an operational flavor; by contrast, all our proofs work directly with programs' denotations.