We discuss semantic intricacies of conditioning, a main feature in probabilistic programming, and propose how to deal with these issues in an operational way and in a weakest pre-condition semantics. This includes the interplay between conditioning and possible non-termination as well as between conditioning and non-determinism.
Furthermore, we propose a program transformation that eliminates conditioning from programs at the expense of introducing loops.
Friedrich Gretz, Nils Jansen, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Federico Olmedo (RWTH Aachen University)
On The Semantic Intricacies of Conditioning (Extended Abstract, PDF)
Conditioning in Probabilistic Programming (Technical Report, PDF)