A Simple Formal Language for Probabilistic Decision Problems
Elena Di Lavore, Bart Jacobs, Mario Román
TL;DR
This paper tackles the ambiguity inherent in probabilistic decision problems by introducing a compact formal language built around arrow notation for sampling and an observe construct for conditioning. Semantics are given by subdistributions, enabling explicit, step-by-step computation and clear updating rules. The authors demonstrate the approach on classic puzzles (e.g., Monty Hall, Newcomb's paradox) to show how a minimal syntax can yield precise, consistent solutions and reduce interpretive disagreement. They formalize the language categorically, proving soundness and completeness with respect to a copy-discard-compare structure and showing that normalisation can be performed without altering final outcomes. The work points toward broader connections to Bayesian networks and Markov-category-inspired semantics, offering a practical yet theoretically grounded toolkit for reasoning about probabilistic decision problems.
Abstract
Probabilistic puzzles can be confusing, partly because they are formulated in natural languages - full of unclarities and ambiguities - and partly because there is no widely accepted and intuitive formal language to express them. We propose a simple formal language with arrow notation ($\gets$) for sampling from a distribution and with observe statements for conditioning (updating, belief revision). We demonstrate the usefulness of this simple language by solving several famous puzzles from probabilistic decision theory. The operational semantics of our language is expressed via the (finite, discrete) subdistribution monad. Our broader message is that proper formalisation dispels confusion.