Abstract

The ideals of exact modeling, and of putting off approximations as long as possible, make Bayesian practice both successful and difficult. Languages for modeling probabilistic processes, whose implementations answer questions about them under asserted conditions, promise to ease much of the difficulty. Unfortunately, very few of these languages have mathematical specifications. This makes them difficult to trust: there is no way to distinguish between an implementation error and a feature, and there is no standard by which to prove optimizations correct. Further, because the languages are based on the incomplete theories of probability typically used in Bayesian practice, they place seemingly artificial restrictions on legal programs and questions, such as disallowing unbounded recursion and allowing only simple equality conditions. We prove it is possible to make trustworthy probabilistic languages for Bayesian practice by using functional programming theory to define them mathematically and prove them correct. The specifications interpret programs using measure-theoretic probability, which is a complete enough theory of probability that we do not need to restrict programs or conditions. We demonstrate that these trustworthy languages are useful by implementing them, and using them to model and answer questions about typical probabilistic processes. We also model and answer questions about processes that are either difficult or impossible to reason about precisely using typical Bayesian mathematical tools.

Degree

PhD

College and Department

Physical and Mathematical Sciences; Computer Science

Rights

http://lib.byu.edu/about/copyright/