WG211/M15Carette

Starting with a probabilistic program, we want another program that denotes the same measure but runs more efficiently and reads more easily. We approach this longstanding challenge by composing three semantics-preserving program transformations: given a program, we (1) apply the denotational semantics; (2) improve the resulting integral; then (3) invert the denotational semantics. Whereas step 1 is a straightforward transformation from monadic to continuation-passing style, the rest builds on computer algebra: step 2 reorders and performs integrals, and step 3 represents density functions as differential operators.