Conditional Separation as a Binary Relation. A Coq Assisted Proof

TL;DR

This work extends Pearl's $d$-separation beyond acyclic graphs to general, possibly infinite graphs and recasts it as a binary relation between vertices, enabling equational reasoning. By treating graphs as binary relations and introducing extended-oriented paths, active/blocked path concepts, and a Coq-verified formalization, the paper derives a binary-relational characterization of $d$-separation: the conditional directional separation $x ot_d^W y vert W$ is the complement of the conditional active relation ${ extcal A}^W$. The main result, proven via a structured sequence of lemmas and propositions, shows that $d$-separation can be captured entirely by relational constructs, providing a computationally amenable framework for reasoning about conditional independencies. This formalization supports connections to topological conditional separation and complements prior work, with publicly available Coq code underpinning the results.

Abstract

The concept of d-separation holds a pivotal role in causality theory, serving as a fundamental tool for deriving conditional independence properties from causal graphs. Pearl defined the d-separation of two subsets conditionally on a third one. In this study, we present a novel perspective by showing i) how the d-separation can be extended beyond acyclic graphs, possibly infinite, and ii) how it can be expressed and characterized as a binary relation between vertices. Compared to the typical perspectives in causality theory, our equivalence opens the door to more compact and computational proofing techniques, because the language of binary relations is well adapted to equational reasoning. Additionally, and of independent interest, the proofs of the results presented in this paper are checked with the Coq proof assistant.

Figures (6)

• Figure 1: Tail and head endpoints of an edge path projection mappings \ref{['eq:Projection_PATH_EdgePath_all']} for $\varrho \in P({{\cal V},{\cal E}})$
• Figure 2: Projection mappings \ref{['eq:Projection_UPATH_all']} on the tail and the head endpoints of an extended-oriented path $\rho \in U({{\cal V},{\cal E}})$
• Figure 3: Sketch of proof of Theorem \ref{['th:ConditionalDirectionalSeparation_IFF_relation']}, mentioning the corresponding Appendices and lemmata
• Figure 4: Coq-produced dependency graph for Coq Theorem \ref{['th:ConditionalDirectionalSeparation_IFF_relation']} (B_L7 is Lemma \ref{['le:cond-act-equals-cond-act-star']}, D_P15 is Proposition \ref{['th:main_isimplied']} and C_P8 is Proposition \ref{['pr:ConditionalDirectionalSeparation_seilpmi_relation']})
• Figure 5: Projection on the tail (resp. head) subpath of an extended-oriented path

Theorems & Definitions (18)

• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Theorem 5
• Definition 6
• Lemma 7
• Proposition 8
• Lemma 9
• Lemma 10