具有连续随机变量和递归的概率语言的上下文等价性
Contextual Equivalence for a Probabilistic Language with Continuous Random Variables and Recursion
摘要：
我们提出了一个完整的推理原则，上下文等价的非类型化概率语言。该语言包括连续（实值）随机变量，条件和评分。它还包括递归，因为标准的按值调用定点组合子是可表达的。我们证明了几个等价模式，包括熟悉的事实，从λ演算以及特定的概率编程的结果，我们的表征的可用性。特别是，我们用它来证明，重新排序的随机抽取概率程序保持上下文等价。例如，这使我们能够证明，（let x = $e_1$ in let y = $e_2$ in $e_0$）等价于（let y = $e_2$ in let x = $e_1$ in $e_0$）（假设$x$在$e_2$中不游离，$y$在$e_1$中不游离），尽管$e_1$和$e_2$可能具有采样和评分效应。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
