Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
We present a complete reasoning principle for contextual equivalence in an untyped probabilistic language. The language includes continuous (real-valued) random variables, conditionals, and scoring. It also includes recursion, since the standard call-by-value fixpoint combinator is expressible.
We demonstrate the usability of our characterization by proving several equivalence schemas, including familiar facts from lambda calculus as well as results specific to probabilistic programming. In particular, we use it to prove that reordering the random draws in a probabilistic program preserves contextual equivalence. This allows us to show, for example, that
(let x = e1 in let y = e2 in e3) = (let y = e2 in let x = e1 in e3)
(provided $x$ does not occur free in $e_2$ and $y$ does not occur free in $e_1$) despite the fact that $e_1$ and $e_2$ may have sampling and scoring effects.
Mon 24 Sep
|16:40 - 17:02|
Conal ElliottTarget, USADOI
|17:02 - 17:25|
Adam ŚcibiorUniversity of Cambridge and MPI Tuebingen, Ohad KammarUniversity of Oxford, Zoubin GhahramaniUniversity of CambridgeDOI
|17:25 - 17:47|
Mitchell WandNortheastern University, USA, Ryan CulpepperCzech Technical University, Theophilos GiannakopoulosBAE Systems, Inc., Andrew CobbNortheastern UniversityDOI
|17:47 - 18:10|
José Bacelar AlmeiraUniversity of Minho & INESC TEC, Alcino CunhaUniversity of Minho and INESC TEC, Portugal, Nuno MacedoUniversity of Minho & INESC TEC, Hugo PachecoUniversity of Minho, Portugal, José ProençaHASLab/INESC TEC & University of MinhoDOI