一句话：为带一阶精确条件化的高斯概率程序建立操作、指称与等式语义，并用范畴构造 Cond 推广精确条件化。
这篇论文研究带一阶精确条件化构造的概率编程语言。精确条件化——尤其对连续随机变量施加等式观测——因观测事件概率可能为零而引发 Borel 悖论，传统条件概率定义难以直接适用。作者以高斯随机变量为具体实例，给出该语言的操作语义、指称语义和等式语义，并证明条件可交换等良好性质。进一步地，他们借助条件概率的范畴表述表明，这些性质并非高斯分布所特有，而可由普遍性质推出，从而推广到更广情形。论文定义 Cond 构造，将条件化内部化为态射，为带精确条件化的概率程序提供通用的组合语义。
We define a probabilistic programming language for Gaussian random variables with a first-class exact conditioning construct. We give operational, denotational and equational semantics for this language, establishing convenient properties like exchangeability of conditions. Conditioning on equality of continuous random variables is nontrivial, as the exact observation may have probability zero; this is Borel's paradox. Using categorical formulations of conditional probability, we show that the good properties of our language are not particular to Gaussians, but can be derived from universal properties, thus generalizing to wider settings. We define the Cond construction, which internalizes conditioning as a morphism, providing general compositional semantics for probabilistic programming with exact conditioning.
DOI 原文 ·
@inproceedings{paperbot6171,
title = {Compositional Semantics for Probabilistic Programs with Exact Conditioning},
author = {Dario Stein and Sam Staton},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470552}
}