Distributions for Compositionally Differentiating Parametric Discontinuities

Computations in computer graphics, robotics, and probabilistic inference often require differentiating integrals with discontinuous integrands. Popular differentiable programming languages do not support the differentiation of these integrals. To address this problem, we extend distribution theory to provide semantic definitions for a broad class of programs in a programming language, Potto. Potto can differentiate parametric discontinuities under integration, and it also supports first-order functions and compositional evaluation. We formalize the meaning of programs using denotational semantics and the evaluation of programs using operational semantics. We prove correctness theorems about the semantics and prove that the operational semantics are compositional, enabling separate compilation of programs and overcoming compile-time bottlenecks. Using Potto, we implement a prototype differentiable renderer with separately compiled shaders.