一句话：将准Borel空间语义用于ν演算，证明其可靠且在一阶类型上完全抽象，建立随机采样与新鲜名字生成的类比。
本文研究概率编程中的随机采样与新鲜名字生成之间的形式对应。作者以准Borel空间（quasi-Borel spaces）这一概率编程语义模型为ν演算（一种名字生成演算）提供解释，证明该语义是可靠的；并进一步证明其在一阶类型上完全抽象。此结果对现成语义模型而言颇为意外，关键在于对函数空间上的概率分布进行了新分析。证明手段包括描述集合论和ν演算的正规形式，从而把名字生成与概率抽样纳入统一语义框架。
We make a formal analogy between random sampling and fresh name generation. We show that quasi-Borel spaces, a model for probabilistic programming, can soundly interpret the ν-calculus, a calculus for name generation. Moreover, we prove that this semantics is fully abstract up to first-order types. This is surprising for an ‘off-the-shelf’ model, and requires a novel analysis of probability distributions on function spaces. Our tools are diverse and include descriptive set theory and normal forms for the ν-calculus.
@article{paperbot1150,
title = {Probabilistic programming semantics for name generation},
author = {Marcin Sabok and Sam Staton and Dario Stein and Michael Wolman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {5},
number = {POPL},
year = {2021},
doi = {10.1145/3434292}
}