Abstract
We give an adequate denotational semantics for languages with recursive higherorder types, continuous probability distributions, and soft constraints. These are expressive languages for building Bayesian models of the kinds used in computational statistics and machine learning. Among them are untyped languages, similar to Church and WebPPL, because our semantics allows recursive mixedvariance datatypes. Our semantics justifies important program equivalences including commutativity.
Our new semantic model is based on `quasiBorel predomains'. These are a mixture of chaincomplete partial orders (cpos) and quasiBorel spaces. QuasiBorel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasiBorel predomains do support both a commutative probabilistic powerdomain and higherorder functions. As we show, quasiBorel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
Our new semantic model is based on `quasiBorel predomains'. These are a mixture of chaincomplete partial orders (cpos) and quasiBorel spaces. QuasiBorel spaces are a recent model of probability theory that focuses on sets of admissible random elements. Probability is traditionally treated in cpo models using probabilistic powerdomains, but these are not known to be commutative on any class of cpos with higher order functions. By contrast, quasiBorel predomains do support both a commutative probabilistic powerdomain and higherorder functions. As we show, quasiBorel predomains form both a model of Fiore's axiomatic domain theory and a model of Kock's synthetic measure theory.
Original language  English 

Article number  36 
Number of pages  29 
Journal  Proceedings of the ACM on Programming Languages 
Volume  3 
Issue number  POPL 
DOIs  
Publication status  Published  2 Jan 2019 
Keywords
 adequacy
 denotational semantics
 domain theory
 probability
 recursion
 machine learning
 domain specific languages
 interpreters
 functional languages
Fingerprint Dive into the research topics of 'A Domain Theory for Statistical Probabilistic Programming'. Together they form a unique fingerprint.
Profiles

Ohad Kammar
 School of Informatics  Senior Research Fellow
 Laboratory for Foundations of Computer Science
 Foundations of Computation
Person: Academic: Research Active