Distribution Theoretic Semantics for Non-Smooth Differentiable Programming
summary
Defines lambda_δ, a simply-typed core calculus that lifts arbitrary (even discontinuous) functions to distributions and gives a concrete semantics using bump/test functions from distribution theory. Claims this fixes AD unsoundness caused by branching by making all lifted objects infinitely differentiable and replaces jump derivatives with explicit Dirac impulse terms. Formal typing rules restrict differentiation to distributions, and examples (Heaviside → impulse) demonstrate the approach and its improved equational properties over prior semantics.
AI-written summary · about
chapters (8)
- 0:00Intro
- 0:18The Problem
- 1:01The Other Problem
- 2:24Distribution Theory: The Lift Map
- 3:12Distribution Theory: Differentiation
- 4:06Types and Syntax
- 4:43Typing Rules
- 5:17A brief example
related talks
30mλS: Computable Semantics for Diff'ble Programming with HO Functions and Datatypes
23mDistributions for Compositionally Differentiating Parametric Discontinuities
49mSemantic Foundations for Probabilistic Programming
14mNominal Semantics for First-class Automatic Differentiation
18mA Language and Smoothed Semantics for Convergent Stochastic Gradient Descent
13mFormalizing a First-order Differentiable Logic with MathComp
19mTowards Denotational Semantics of AD for Higher-Order, Recursive, Probabilistic
13mSemantic Foundations for Laziness in Discrete Probabilistic Programming