Lilac is a probabilistic separation logic whose separating conjunction denotes probabilistic independence. In contrast to ordinary separation logic, where propositions denote properties of heaps and separating conjunction splits heaps into disjoint subheaps, Lilac propositions denote properties of probability spaces and separating conjunction splits probability spaces into independent subspaces. Naively, one would expect this splitting of probability spaces to be defined in terms of product spaces, but this is not so. Instead, Lilac’s separating conjunction is defined in terms of independent combination, a partial binary operation on probability spaces that plays the role disjoint union does for heaps in ordinary separation logic. The definition of independent combination does not mention product spaces at all; rather, independent combination is constructed out of low-level measure-theoretic objects. This disconnect between independent combination and the familiar product space construction is puzzling to those well-versed in probability theory: how do we know that independent combination provides the right notion of separation for probabilistic separation logic?

To answer this question, we first construct two categories: one category equipped with a model of core Lilac where separation is defined via independent combination, and one category equipped with a model of core Lilac where separation is defined via product. Our answer then comes in the form of a theorem: these two categories are equivalent, and the notion of separation in one category corresponds to the notion of separation in the other across this equivalence, showing that independent combination and product are two equivalent points of view on the same underlying probability-theoretic concept. In addition to justifying the use of independent combination in Lilac’s semantic model, our equivalence theorem creates connections between probability theory and nominal sets: it is a probabilistic analogue of a classic theorem of topos theory, showing that the category of nominal sets is equivalent to a suitable category of sheaves.