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

arXiv: https://arxiv.org/abs/1807.02809 · HTML: https://mlsanity.com/paper/1807.02809/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 8 Jul 2018.

## Built on by (most cited first, 1 of 1)

- [Nonparametric Involutive Markov Chain Monte Carlo](https://mlsanity.com/paper/2211.01100/) (2022)

## Abstract (arXiv)

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 e0) is equivalent to (let y = e2 in let x = e1 in e0) (provided x does not occur free in e2 and y does not occur free in e1) despite the fact that e1 and e2 may have sampling and scoring effects.