一句话：为含连续随机变量、scoring 与递归的无类型概率语言给出上下文等价的完整推理原则。
本文研究无类型概率语言中上下文等价的推理问题。该语言包含连续实值随机变量、条件分支和 scoring，并因可表达标准 call-by-value 不动点组合子而支持递归。作者提出一个完整的上下文等价刻画/推理原则，并利用它证明多种等价模式，既涵盖 lambda 演算中的常见事实，也包含概率编程特有的结果。关键应用是证明概率程序中随机抽取的重排保持上下文等价：若 x 不在 e2 中自由出现且 y 不在 e1 中自由出现，则 (let x = e1 in let y = e2 in e0) =ctx (let y = e2 in let x = e1 in e0)，即使 e1 和 e2 带有采样与 scoring 效应。这为概率程序的等价推理提供了实用工具。
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 ) = ctx (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.
@article{paperbot295,
title = {Contextual equivalence for a probabilistic language with continuous random variables and recursion},
author = {Mitchell Wand and Ryan Culpepper and Theophilos Giannakopoulos and Andrew Cobb},
journal = {Proceedings of the ACM on Programming Languages},
volume = {2},
number = {ICFP},
year = {2018},
doi = {10.1145/3236782}
}