In our view, one of the key contributions of the probabilistic programming language Church is a class of constructs, called exchangeable random primitives (or XRPs for short), that can be used to extend the language with stochastic primitives whose implementations use stateful computation.
Surprisingly, XRPs are not mentioned in the paper introducing the language and are buried in the original implementation, dubbed MIT-Church. Despite being reimplemented and generalized in several languages descending from Church, XRPs are poorly documented and, as a result, poorly understood.
XRPs are built from three components: a sampler, an unsampler, and a scorer. We give a rigorous definition for the samplers of XRPs, and give a representation theorem characterizing their essential form and conditional independence structure. A formalization like the one we provide could serve as part of a foundation for deriving a semantics for Church programs with XRPs. A formalization of all three components of XRPs — including the unsampler and scorer — would be necessary to prove the correctness of the MCMC Church algorithm in the presence of XRPs. We highlight some challenges associated with formalizing the scorer. (We also have some ideas for circumventing these obstacles that do not appear in the paper but that we would be happy to discuss.) We are also looking forward to discussing semantic questions surrounding XRPs, especially those involving purity and referential transparency, and would be interested to learn of other possible connections between XRPs and the PL theory literature.
Sat 23 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
16:30 - 18:00
Session 5PPS at Room St Petersburg II
Chair(s): Chung-chieh Shan Indiana University
|eXchangeable Random Primitives|
Nathanael L. Ackerman Harvard University, Cameron Freer Gamalon, Daniel Roy University of TorontoPre-print
|An Application of Computable Distributions to the Semantics of Probabilistic Programs|
Daniel Huang Harvard University, Greg Morrisett Cornell UniversityPre-print
|On The Semantic Intricacies of Conditioning|
Friedrich Gretz RWTH Aachen University, Nils Jansen RWTH Aachen University, Benjamin Lucien Kaminski RWTH Aachen University, Joost-Pieter Katoen RWTH Aachen University, Federico Olmedo RWTH Aachen UniversityPre-print