一句话：在 pGCL 上研究 conditioning 的 wp 与操作语义，证明其对应条件期望奖励，并给出消除 conditioning 的程序变换。
本文研究概率编程中 conditioning（条件化）的语义复杂性。作者将命令式概率守护命令语言 pGCL 扩展以支持 conditioning，给出最弱前置条件（wp）语义与操作语义；为处理可能发散的程序行为，采用 liberal precondition。结果表明发散行为在定义 conditioning 时起关键作用：wp 语义与 Markov 链上的条件期望奖励一致，并保守扩展原 pGCL 语义。将结果扩展到非确定性时出现问题：虽然 Markov 决策过程可给出操作语义，但不存在归纳式 wp 语义。最后提出两种消除 conditioning 的程序变换：一种提升 conditioning 并更新概率选择，另一种类似拒绝采样用循环替换；另给出用 conditioning 替换独立同分布循环的变换。
This article investigates the semantic intricacies of conditioning, a main feature in probabilistic programming. Our study is based on an extension of the imperative probabilistic guarded command language pGCL with conditioning. We provide a weakest precondition (wp) semantics and an operational semantics. To deal with possibly diverging program behavior, we consider liberal preconditions. We show that diverging program behavior plays a key role when defining conditioning. We establish that weakest preconditions coincide with conditional expected rewards in Markov chains—the operational semantics—and that the wp-semantics conservatively extends the existing semantics of pGCL (without conditioning). An extension of these results with nondeterminism turns out to be problematic: although an operational semantics using Markov decision processes is rather straightforward, we show that providing an inductive wp-semantics in this setting is impossible. Finally, we present two program transformations that eliminate conditioning from any program. The first transformation hoists conditioning while updating the probabilistic choices in the program, while the second transformation replaces conditioning—in the same vein as rejection sampling—by a program with loops. In addition, we present a last program transformation that replaces an independent identically distributed loop with conditioning.
@article{paperbot324,
title = {Conditioning in Probabilistic Programming},
author = {Federico Olmedo and Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Annabelle Mciver},
journal = {ACM Transactions on Programming Languages and Systems},
volume = {40},
number = {1},
year = {2018},
doi = {10.1145/3156018}
}