论文标题
名称生成的概率编程语义
Probabilistic Programming Semantics for Name Generation
论文作者
论文摘要
我们在随机抽样和新名称产生之间做一个形式的类比。我们表明，概率编程模型的准空间可以很好地解释Stark的$ν$ -Calculus，这是一种用于生成名称的计算。此外，我们证明这种语义是完全抽象的一阶类型。对于“现成”模型来说，这是令人惊讶的，并且需要对功能空间上的概率分布进行新的分析。我们的工具是多种多样的，包括$ν$ -calculus的描述性集理论和正常形式。
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 Stark's $ν$-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.
