Formal semantics for Bayesian reasoning

We establish a link between Bayesian inference (learning) and predicate and state transformer operations from programming semantics and logic. This setting is used to propose a formal definition of influence, based on the total variation distance for probability distributions. We distinguish between direct and `crossover' influence: the latter pinpoints non-locality phenomena in a probabilistic setting. 

As a proof of concept, we use these definitions to translate the d-separation criteria in a Bayesian network into formal, provable statements.

This is joint work with Bart Jacobs.