一句话：提出 quasi-Borel predomains，为含递归高阶类型与连续概率的统计概率编程语言建立充分指称语义，并证明交换性等价。
论文为含递归高阶类型、连续概率分布和软约束的统计概率编程语言给出充分指称语义。这类语言可表达计算统计与机器学习中的贝叶斯模型，并涵盖类似 Church、WebPPL 的无类型语言，因为语义支持递归混合变号数据类型。作者提出 quasi-Borel predomains，它混合链完备偏序（cpo）与 quasi-Borel spaces；传统 cpo 模型用概率幂域，但在带高阶函数的 cpo 上交换性未知。新模型同时支持交换概率幂域与高阶函数，因而证明包括交换性在内的程序等价。作者进一步表明它是 Fiore 公理化域理论和 Kock 合成测度理论的模型。
We give an adequate denotational semantics for languages with recursive higher-order types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixed-variance datatypes. Our semantics justifies important program equivalences including commutativity. Our new semantic model is based on `quasi-Borel predomains'. These are a mixture of chain-complete partial orders (cpos) and quasi-Borel spaces. Quasi-Borel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasi-Borel predomains do support both a commutative probabilistic powerdomain and higher-order functions. As we show, quasi-Borel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
@article{paperbot652,
title = {A domain theory for statistical probabilistic programming},
author = {Matthijs Vákár and Ohad Kammar and Sam Staton},
journal = {Proceedings of the ACM on Programming Languages},
volume = {3},
number = {POPL},
year = {2019},
doi = {10.1145/3290349}
}