New foundations for probabilistic separation logic
Probabilistic reasoning frequently requires decomposing a situation into probabilistically independent pieces. We present a separation logic supporting this decomposition. Inspired by an analogy with mutable state where sampling corresponds to dynamic allocation, we show how probability spaces over a fixed, ambient sample space appear to be the natural analogue of heap fragments, and present a new combining operation on them such that probability spaces behave like heaps and measurability of random variables behaves like ownership. Unlike prior work, the resulting program logic enjoys a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs.
|New foundations for probabilistic separation logic (lafi23-final67.pdf)||247KiB|