Conditioning in Probabilistic Programming

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

doi:10.1016/j.entcs.2015.12.013

Conditioning in Probabilistic Programming

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

School of Computing

Research output: Contribution to journal › Article › peer-review

14 Citations (Scopus)

Abstract

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 language	English
Pages (from-to)	199-216
Number of pages	18
Journal	Electronic Notes in Theoretical Computer Science
Volume	319
DOIs	https://doi.org/10.1016/j.entcs.2015.12.013
Publication status	Published - 21 Dec 2015
Event	Conference on the Mathematical Foundations of Programming Semantics (31st : 2015) - Nijmegen, Netherlands Duration: 22 Jun 2015 → 25 Jun 2015

Keywords

Probabilistic Programming
Semantics
Conditional Probabilities
Program Transformation

Access to Document

10.1016/j.entcs.2015.12.013

Cite this

@article{67b6ae38f3f84b6985e3ca45b39673fe,

title = "Conditioning in Probabilistic Programming",

abstract = "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.",

keywords = "Probabilistic Programming, Semantics, Conditional Probabilities, Program Transformation",

author = "Nils Jansen and Kaminski, {Benjamin Lucien} and Katoen, {Joost Pieter} and Federico Olmedo and Friedrich Gretz and Annabelle McIver",

year = "2015",

month = dec,

day = "21",

doi = "10.1016/j.entcs.2015.12.013",

language = "English",

volume = "319",

pages = "199--216",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

note = "Conference on the Mathematical Foundations of Programming Semantics (31st : 2015) ; Conference date: 22-06-2015 Through 25-06-2015",

}

TY - JOUR

T1 - Conditioning in Probabilistic Programming

AU - Jansen, Nils

AU - Kaminski, Benjamin Lucien

AU - Katoen, Joost Pieter

AU - Olmedo, Federico

AU - Gretz, Friedrich

AU - McIver, Annabelle

PY - 2015/12/21

Y1 - 2015/12/21

N2 - 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.

AB - 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.

KW - Probabilistic Programming

KW - Semantics

KW - Conditional Probabilities

KW - Program Transformation

UR - http://www.scopus.com/inward/record.url?scp=84951776671&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2015.12.013

DO - 10.1016/j.entcs.2015.12.013

M3 - Article

AN - SCOPUS:84951776671

SN - 1571-0661

VL - 319

SP - 199

EP - 216

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

T2 - Conference on the Mathematical Foundations of Programming Semantics (31st : 2015)

Y2 - 22 June 2015 through 25 June 2015

ER -

Conditioning in Probabilistic Programming

Abstract

Keywords

Access to Document

Other files and links

Fingerprint

Cite this