AD with Integrals
Computations in computer vision, graphics, robotics, machine learning and probabilistic programming often require differentiating integrals with discontinuous integrands. Popular differentiable programming languages do not support the differentiation of these integrals. We build on recent work from Bangaru et al. [2021] by developing a rigorous theory to underlie it. To do so, we define a calculus for differentiating a broad class of measures. Using our theory, we develop the denotational and operational semantics of a differentiable programming language, Potto, that is the first to differentiate parametric discontinuities under integration while supporting compositional evaluation. We prove the soundness and compositionality of the semantics and the differentiation rules. Potto's compositionality allows us to separately compile and compose programs. We provide an implementation of Potto and use it to build a differentiable renderer with shaders that are separately compiled.