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具有与普通框架规则相同的框架规则，并自然地容纳连续随机变量等高级特性以及对程序定量性质的推理。随后，我们基于离散化理论提出了一种新的模态，用于推理条件概率。我们展示了由此产生的模态逻辑如何验证先前工作范例，并给出了一个复杂加权采样算法的形式化验证，该算法的正确性关键依赖于条件独立结构。