一句话：扩展 BI 逻辑以非交换合取刻画条件独立，并基于 Markov 核与幂集单子给出模型和概率程序验证逻辑。
独立性与条件独立性是概率程序推理中的核心概念，但现有验证方法尚不成熟，且无法处理条件独立。本文扩展束蕴含逻辑（BI），加入非交换合取，并给出基于 Markov 核的模型；在该模型中，条件独立可直接表示为逻辑公式。作者观察到 Markov 核是分布单子的 Kleisli 箭头，进而提出基于幂集单子的第二个模型，用于刻画数据库理论中条件独立的非概率类比——join dependency。最后，文章发展了一个程序逻辑，用于验证概率程序中的条件独立。
Independence and conditional independence are fundamental concepts for reasoning about groups of random variables in probabilistic programs. Verification methods for independence are still nascent, and existing methods cannot handle conditional independence. We extend the logic of bunched implications (BI) with a non-commutative conjunction and provide a model based on Markov kernels; conditional independence can be directly captured as a logical formula in this model. Noting that Markov kernels are Kleisli arrows for the distribution monad, we then introduce a second model based on the powerset monad and show how it can capture join dependency, a non-probabilistic analogue of conditional independence from database theory. Finally, we develop a program logic for verifying conditional independence in probabilistic programs.
DOI 原文 ·
@inproceedings{paperbot6227,
title = {A Bunched Logic for Conditional Independence},
author = {Jialu Bao and Simon Docherty and Justin Hsu and Alexandra Silva},
booktitle = {LICS},
year = {2021},
doi = {10.1109/lics52264.2021.9470712}
}