Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion

TL;DR

This paper develops a complete reasoning principle for contextual equivalence in a probabilistic language with continuous variables, recursion, and scoring, enabling formal verification of program transformations.

Contribution

It introduces a novel characterization of contextual equivalence for a probabilistic language with continuous variables and recursion, including proofs of equivalence schemas.

Findings

Reordering random draws preserves contextual equivalence.

Proved equivalence of complex probabilistic program transformations.

Demonstrated applicability to lambda calculus and probabilistic programming facts.

Abstract

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 = $e_1$ in let y = $e_2$ in $e_0$) is equivalent to (let y = $e_2$ in let x = $e_1$ in $e_0$) (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.