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.