Conditioning in Probabilistic Programming

Nils Jansen, Benjamin Lucien Kaminski, Joost Pieter Katoen, Federico Olmedo, Friedrich Gretz, Annabelle McIver

Research output: Contribution to journalArticlepeer-review

11 Citations (Scopus)


In this paper, we investigate the semantic intricacies of conditioning in probabilistic programming, a major feature, e.g., in machine learning. We provide a quantitative weakest pre-condition semantics. In contrast to all other approaches, non-termination is taken into account by our semantics. We also present an operational semantics in terms of Markov models and show that expected rewards coincide with quantitative pre-conditions. A program transformation that entirely eliminates conditioning from programs is given; the correctness is shown using our semantics. Finally, we show that an inductive semantics for conditioning in non-deterministic probabilistic programs cannot exist.

Original languageEnglish
Pages (from-to)199-216
Number of pages18
JournalElectronic Notes in Theoretical Computer Science
Publication statusPublished - 21 Dec 2015
EventConference on the Mathematical Foundations of Programming Semantics (31st : 2015) - Nijmegen, Netherlands
Duration: 22 Jun 201525 Jun 2015


  • Probabilistic Programming
  • Semantics
  • Conditional Probabilities
  • Program Transformation


Dive into the research topics of 'Conditioning in Probabilistic Programming'. Together they form a unique fingerprint.

Cite this