A Simple Formal Language for Probabilistic Decision Problems

TL;DR

This paper introduces a straightforward formal language with arrow notation and observe statements to clarify probabilistic decision problems, demonstrated through solving well-known puzzles and emphasizing the importance of formalization.

Contribution

It presents a new simple formal language for probabilistic decision problems, using arrow notation and observe statements, with semantics based on the subdistribution monad.

Findings

Successfully solves several famous probabilistic puzzles.

Shows that formalization reduces confusion in probabilistic reasoning.

Demonstrates the language's operational semantics with the subdistribution monad.

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.