Discrete random variables over domains, revisited

Abstract

We revisit the construction of discrete random variables over domains from [15] and show how Hoare’s “normal termination” symbol ✓ can be used to achieve a more expressive model. The result is a natural model of flips of a coin that supports discrete and continuous (sub)probability measures. This defines a new random variables monad on BCD, the category of bounded complete domains, that can be used to augment semantic models of demonic nondeterminism with probabilistic choice. It is the second such monad, the first being Barker’s monad for randomized choice [3]. Our construction differs from Barker’s monad, because the latter requires the source of randomness to be shared across multiple users. The monad presented here allows each user to access a source of randomness that is independent of the sources of randomness available to other users. This requirement is useful, e.g., in models of crypto-protocols.