Lilac: A Modal Separation Logic for Conditional Probability
Lilac: A Modal Separation Logic for Conditional Probability
复制标题
Lilac：条件概率的模态分离逻辑
DOI：
10.1145/3591226
复制
发表时间：
2023
影响因子：
--
通讯作者：
Holtzen, Steven
中科院分区：
文献类型：
--
作者：
Li, John M.;Ahmed, Amal;Holtzen, Steven
我们提出了丁香，分离逻辑推理的概率程序分离结合捕获概率独立性。启发与可变状态的采样对应于动态分配的类比，我们展示了如何在一个固定的概率空间，周围的样本空间似乎是堆碎片的自然模拟，并提出了一个新的组合操作，使概率空间的行为像堆和随机变量的可测量性的行为像所有权。这种组合操作形成了我们分离模型的基础，并产生了具有许多令人愉快的特性的逻辑。特别是，Lilac有一个与普通规则相同的框架规则，并且自然地适应了连续随机变量和程序定量属性推理等高级功能。然后，我们提出了一个新的模态基于解体理论的推理条件概率。我们将展示如何得到模态逻辑验证以前的工作的例子，并给出了一个复杂的加权采样算法的正确性关键取决于条件独立结构的正式验证。
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.
登录
查看更多内容
影响因子：
1.5
作者：
Chang, JT;Pollard, D
通讯作者：
Pollard, D
DOI：
10.1145/964001.964024
发表时间：
2004-01
期刊：
Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on Principles of programming languages
影响因子：
--
作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
通讯作者：
P. O'Hearn;Hongseok Yang;J. C. Reynolds
影响因子：
0.5
作者：
Galmiche, D;Méry, D;Pym, D
通讯作者：
Pym, D
DOI：
10.1109/lics.2017.8005137
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Heunen C
通讯作者：
Heunen C
DOI：
10.1109/lics52264.2021.9470673
发表时间：
2021-01
期刊：
2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
影响因子：
--
作者：
Li Zhou;G. Barthe;Justin Hsu;M. Ying;Nengkun Yu
通讯作者：
Li Zhou;G. Barthe;Justin Hsu;M. Ying;Nengkun Yu