Conditioning in Probabilistic Programming
Abstract
We investigate the semantic intricacies of conditioning, a main feature in probabilistic programming. We provide a weakest (liberal) pre-condition (w(l)p) semantics for the elementary probabilistic programming language pGCL extended with conditioning. We prove that quantitative weakest (liberal) pre-conditions coincide with conditional (liberal) expected rewards in Markov chains and show that semantically conditioning is a truly conservative extension. We present two program transformations which entirely eliminate conditioning from any program and prove their correctness using the w(l)p-semantics. Finally, we show how the w(l)p-semantics can be used to determine conditional probabilities in a parametric anonymity protocol and show that an inductive w(l)p-semantics for conditioning in non-deterministic probabilistic programs cannot exist.
Cite
@article{arxiv.1504.00198,
title = {Conditioning in Probabilistic Programming},
author = {Friedrich Gretz and Nils Jansen and Benjamin Lucien Kaminski and Joost-Pieter Katoen and Annabelle McIver and Federico Olmedo},
journal= {arXiv preprint arXiv:1504.00198},
year = {2015}
}