We present Lilac, a separation logic for reasoning about probabilistic programs where separating conjunction captures probabilistic independence. 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. This combining operation forms the basis for our model of separation, and produces a logic with many pleasant properties. In particular, Lilac has a frame rule identical to the ordinary one, and naturally accommodates advanced features like continuous random variables and reasoning about quantitative properties of programs. Then we propose a new modality based on disintegration theory for reasoning about conditional probability. We show how the resulting modal logic validates examples from prior work, and give a formal verification of an intricate weighted sampling algorithm whose correctness depends crucially on conditional independence structure.

翻译：摘要：本文提出Lilac，一种用于推理概率程序的分离逻辑，其中分离合取捕捉概率独立性。受采样对应于动态分配的可变状态类比启发，我们证明固定环境样本空间上的概率空间自然类似于堆片段，并在此空间上提出一种新的组合操作，使得概率空间的行为类似堆，随机变量的可测性行为类似所有权。该组合操作构成了我们分离模型的基础，并产生具有诸多优良性质的逻辑。具体而言，Lilac具有与普通框架规则相同的框架规则，并天然支持连续随机变量及程序定量性质推理等高级特性。随后，我们基于分解理论提出一种用于推理条件概率的新模态，展示由此产生的模态逻辑如何验证先前工作中的案例，并给出一个复杂加权采样算法的形式化验证——该算法的正确性关键依赖于条件独立结构。