A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness
arXiv:2606.20351
The paper formalises conditional independence, Bayesian conditioning, and Pearl's d‑separation within Cubical Agda, showing that the usual convex‑algebra axiom is insufficient and presenting a minimal generalisation that enables constructive verification of semi‑graphoid axioms, do‑calculus rules, and Markov‑category structure for finite distributions.
Abstract
The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural -witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and the soundness of Pearl's d-separation theorem on arbitrary finite directed acyclic graphs (DAGs) -- in interventional form for multi-element , , , and in Bayesian form for the elementary patterns. The probability monad is also verified as a Markov category; the abstract interface discharges at .