Towards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
summary
Extends Lee et al. (2020) to a higher-order, recursive, probabilistic language and proves every program denotes omega-PAP functions and that AD yields correct intentional derivatives (agreeing with true derivatives almost everywhere); derives Mazza & Pagani as a corollary and reproves Mak et al. for probabilistic densities via a denotational monad-of-measures argument. Builds pap spaces and handles partiality and recursion via an omega construction. Shows a concrete change-of-variables example on the unit circle where AD computes an intentional Jacobian that still yields the correct density.
AI-written summary · about
chapters (11)
- 0:00Intro
- 0:33What does
- 2:00Outline
- 3:31Conditionals
- 6:58PAP spaces
- 8:44Higher-order functions
- 9:32Partial functions
- 11:43Applications to Probabilistic
- 12:14Change of variables
- 14:21Differentiating
- 15:19Differentiable
related talks
11mAbstract Interpretation for Automatic Differentiation
49mSemantic Foundations for Probabilistic Programming
26mADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Progra...
24mHigher order programming with probabilistic effects: A model of stochastic memo...
30mAutomatic Differentiation in PCF
14mNominal Semantics for First-class Automatic Differentiation
06mDistribution Theoretic Semantics for Non-Smooth Differentiable Programming
29mPartial Evaluation of Automatic Differentiation for Differential-Algebraic Equati...