一句话：证明概率论中的概率空间乘积分解与概率分离逻辑中的测度论分解在范畴等价意义下等价。
概率论研究者通常用概率空间的乘积来分解概率状态，而近期提出的概率分离逻辑则借助测度论中 σ-代数与概率测度的并等构造来分解状态，二者之间存在工具与概念上的鸿沟。本文证明这两种分解方式在适当的范畴等价意义下是等价的。核心结果是经典的名义集范畴与 Schanuel topos 等价的一个概率类比。借助该等价，作者验证了先前概率分离逻辑工作中若干设计决策的合理性，并建立了概率模型与名义集式模型之间的新联系。
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-setlike models of probability.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@inproceedings{LiAJ0H24,
title = {A Nominal Approach to Probabilistic Separation Logic},
author = {John M. Li and Jon Aytac and Philip Johnson-Freyd and Amal Ahmed and Steven Holtzen},
booktitle = {LICS},
year = {2024},
doi = {10.1145/3661814.3662135}
}