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.

Reasoning about Probability and Nondeterminism, by Faris Abou-Saleh, Kwok-Ho Cheung, and Jeremy Gibbons, University of Oxford

Diagrammatic Reasoning about Probability and Nondeterminism (poster)