Probabilistic Programming Semantics for Name Generation

TL;DR

This paper establishes a formal connection between probabilistic programming semantics and name generation, demonstrating that quasi-Borel spaces can interpret the $ u$-calculus with full abstraction, using advanced mathematical tools.

Contribution

It introduces a novel interpretation of name generation in probabilistic semantics using quasi-Borel spaces, achieving full abstraction up to first-order types.

Findings

Quasi-Borel spaces can interpret Stark's $ u$-calculus soundly.

The semantics is fully abstract up to first-order types.

The analysis involves descriptive set theory and normal forms for the $ u$-calculus.

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 $\nu$-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 $\nu$-calculus.