Reasoning about Probability and Nondeterminism
Faris Abou−Saleh‚ Kwok−Ho Cheung and Jeremy Gibbons
Abstract
Probabilistic and nondeterministic choice are two standard examples of computational effect, and it is important for some problems to be able to use them in combination — for example, to model probabilistic systems that depend on nondeterministic inputs. However, the algebraic properties that characterise their interaction are tricky to get right (and we have ourselves got them wrong in the past). We outline the problem, and present a technique for diagrammatic reasoning about the properties of probability and nondeterminism combined. It turns out to be a matter of linear algebra. We are curious to know whether others find the diagrammatic notation helpful, and whether there are other applications of it.