Uncertainty and Probabilistic UTP

This paper is dedicated to Cliff Jones, whom I have known for nearly 45 years. I describe my personal and professional friendship with him, including our interests in logic, semantics, and formal program development. The second part of the paper describes the relational semantics in UTP for probabilistic programming, inspired by the elegant work of Hehner. With Ye and Foster, we have mechanised this theory elsewhere using the Isabelle/UTP theorem prover. Here, we focus on motivating definitions and giving careful hand-written proofs of critical results. We start by describing Iverson brackets, a correspondence between predicates and arithmetic, which provides a link between conventional and probabilistic programming. We describe our semantic domain in UTP: a relational calculus of mappings from states to discrete state distributions. We give semantics to a simple probabilistic programming language. Following Hehner, we show how to extend the domain to provide the programming language with Bayesian semantics, transforming a priori distributions to a posteriori ones. This Bayesian semantics captures how we learn new facts in an uncertain world. We apply this to a simple robot localisation. Our treatment is characteristic of Hoare and He’s Unifying UTP. We take Hehner’s work and formalise it to unify it with other notations and tools. We conclude by discussing the advantages of doing this.