2020/08/20 by Jialu Bao, Simon Docherty, Bao, Jialu +5 · 1 citation
Computer Science · #Bayesian Modeling and Causal Inference #FOS: Computer and information sciences #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Programming Languages (cs.PL) #Semantic Web and Ontologies
paper · pdf · doi:10.48550/arxiv.2008.09231
openalex publication_date 2020/08/20 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
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.