Probabilistic Programming Inference via Intensional Semantics
We define a new denotational semantics for a first-order probabilistic programming language in terms of probabilistic event structures. This semantics is intensional, meaning that the interpretation of a program contains information about its behaviour throughout execution, rather than a simple distribution on return values. In particular, occurrences of sampling and conditioning are recorded as explicit events, partially ordered according to the data dependencies between the corresponding statements in the program.
This interpretation is adequate: we show that the usual measure-theoretic semantics of a program can be recovered from its event structure representation. Moreover it can be leveraged for MCMC inference: we prove correct a version of single-site Metropolis-Hastings with incremental recomputation, in which the proposal kernel takes into account the semantic information in order to avoid performing some of the redundant sampling.
Tue 9 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Extended call-by-push-value: reasoning about effectful programs and evaluation orderBest paper nomination ESOP Link to publication | ||
14:30 30mTalk | Effectful Normal-Form Bisimulation ESOP Link to publication | ||
15:00 30mTalk | On the Multi-Language Construction ESOP Link to publication | ||
15:30 30mTalk | Probabilistic Programming Inference via Intensional Semantics ESOP Link to publication |