Probabilistic Programming Semantics for Name Generation

2020/07/16 by Sabok, Marcin, Staton, Sam, Stein, Dario +1
#F.3.2 #FOS: Computer and information sciences #FOS: Mathematics #Logic (math.LO) #Logic in Computer Science (cs.LO) #Programming Languages (cs.PL)

paper · doi:10.48550/arxiv.2007.08638

Abstract

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.

Related

• A program logic for fresh name generation
• Semantics of higher-order probabilistic programs with conditioning
• Lambda Calculus and Probabilistic Computation
• ωPAP Spaces: Reasoning Denotationally About Higher-Order, Recursive Probabilistic and Differentiable Programs
• A Higher-Order Language for Markov Kernels and Linear Operators