一句话：用有序 Banach 空间上的线性算子为带条件的高阶概率程序建立指称语义，并验证 Gibbs 采样。
论文针对高阶概率程序（尤其含条件化）缺乏指称语义的问题，提出基于 Banach 空间之间线性算子的指称语义。该语义建立在 Banach 空间及其张量积的经典理论上，并借助有序 Banach 空间与不动点定义，与 Scott 风格的高阶程序语义相似。作者构造了一个对称幺半闭范畴，将随机性视为线性资源，从而成为直觉主义线性逻辑的模型；同时通过指数余单子支持非线性推理。作为应用，他们用该语义验证了经典 Gibbs 采样算法。
We present a denotational semantics for higher-order probabilistic programs in terms of linear operators between Banach spaces. Our semantics is rooted in the classical theory of Banach spaces and their tensor products, but bears similarities with the well-known semantics of higher-order programs a la Scott through the use of ordered Banach spaces which allow definitions in terms of fixed points. Our semantics is a model of intuitionistic linear logic: it is based on a symmetric monoidal closed category of ordered Banach spaces which treats randomness as a linear resource, but by constructing an exponential comonad we can also accommodate non-linear reasoning. We apply our semantics to the verification of the classical Gibbs sampling algorithm.
@article{paperbot563,
title = {Semantics of higher-order probabilistic programs with conditioning},
author = {Fredrik Dahlqvist and Dexter Kozen},
journal = {Proceedings of the ACM on Programming Languages},
volume = {4},
number = {POPL},
year = {2019},
doi = {10.1145/3371125}
}