We present a complete reasoning principle for contextual equivalence in an untyped probabilistic programming language. The language includes continuous random variables, conditionals, and scoring. The language also includes recursion, since in an untyped language the standard call-by-value fixpoint combinator is expressible. The language is similar to that of [Borgstrom et al 2016].

To demonstrate the usability of our characterization, we use it to prove that reordering the draws in a probabilistic program preserves contextual equivalence (ie, that sampling in our language is a commutative effect). This allows us to show, for example, that

**let x = e1 in let y = e2 in e3** and **let y = e2 in x = e1 in e3**

are contextual equivalent (provided **x** is not among the free variables of **e2**, and **y** is not among the free variables of **e1**), despite the fact that **e1** and **e2** may have the effect of drawing from the source of entropy.