P L ] 1 A pr 2 01 5 Conditioning in Probabilistic Programming

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.