A Nominal Approach to Probabilistic Separation Logic

TL;DR

This paper bridges the gap between probability theory and formal reasoning in probabilistic programs by establishing an equivalence between their decomposition methods, connecting measure-theoretic and categorical perspectives.

Contribution

It introduces a categorical equivalence between probabilistic state decompositions and nominal set models, validating prior work and linking different theoretical frameworks.

Findings

Establishes an equivalence between probability space decompositions and nominal sets.

Validates design choices in existing probabilistic separation logic.

Creates new connections between measure-theoretic and categorical models of probability.

Abstract

Currently, there is a gap between the tools used by probability theorists and those used in formal reasoning about probabilistic programs. On the one hand, a probability theorist decomposes probabilistic state along the simple and natural product of probability spaces. On the other hand, recently developed probabilistic separation logics decompose state via relatively unfamiliar measure-theoretic constructions for computing unions of sigma-algebras and probability measures. We bridge the gap between these two perspectives by showing that these two methods of decomposition are equivalent up to a suitable equivalence of categories. Our main result is a probabilistic analog of the classic equivalence between the category of nominal sets and the Schanuel topos. Through this equivalence, we validate design decisions in prior work on probabilistic separation logic and create new connections to nominal-set-like models of probability.