2014/12/12 by Neil Toronto, Toronto, Neil, Jay McCarthy +3
Computer Science · Decision Sciences · #Advanced Database Systems and Queries #Bayesian Modeling and Causal Inference #FOS: Computer and information sciences #Programming Languages (cs.PL) #Scientific Computing and Data Management #cs.PL
paper · pdf · doi:10.48550/arxiv.1412.4053
26 pages, ESOP 2015 (to appear)
openalex publication_date 2014/12/12 · arxiv created 2015/01/16 · arxiv updated 2015/01/19 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Many probabilistic programming languages allow programs to be run under constraints in order to carry out Bayesian inference. Running programs under constraints could enable other uses such as rare event simulation and probabilistic verification---except that all such probabilistic languages are necessarily limited because they are defined or implemented in terms of an impoverished theory of probability. Measure-theoretic probability provides a more general foundation, but its generality makes finding computational content difficult. We develop a measure-theoretic semantics for a first-order probabilistic language with recursion, which interprets programs as functions that compute preimages. Preimage functions are generally uncomputable, so we derive an abstract semantics. We implement the abstract semantics and use the implementation to carry out Bayesian inference, stochastic ray tracing (a rare event simulation), and probabilistic verification of floating-point error bounds.