Markov equivalence and Bayesian network scores

AbbreviationJoint configurations of a set of variables#✓fully proved

The joint values of the variables in S.

abbrev Config (σ : V → Type*) (S : Finset V) := (u : S) → σ u

Used by 12

Used byBayesian–Dirichlet family score · BDe family score as a ratio of marginal likelihoods · Bayesian–Dirichlet network score · BDe hyperparameters · Covered-edge reversal preserves the BDe score · Count of cases matching a configuration · BDe marginal likelihood of a variable set · Sequential Pólya–Dirichlet prediction factor · Sequential Pólya–Dirichlet product of the data · Sequential Pólya–Dirichlet product after prior cases · The BD score is the sequential prediction product · Parent configuration counts sum over family configurations

DefinitionRising factorial#✓fully proved

The rising factorial a (a + 1) ⋯ (a + n - 1), equal to Γ(a + n) / Γ(a) for a > 0.

noncomputable def rising (a : ℝ) (n : ℕ) : ℝ := (ascPochhammer ℝ n).eval a

Used by 5

Used byBayesian–Dirichlet family score · BDe family score as a ratio of marginal likelihoods · Covered-edge reversal preserves the BDe score · BDe marginal likelihood of a variable set · The BD score is the sequential prediction product

DefinitionCount of cases matching a configuration#✓fully proved

The number of cases in D that take the values c on the variables S.

def count (D : List ((v : V) → σ v)) (S : Finset V) (c : Config σ S) : ℕ :=
  D.countP fun x => S.restrict x = c

Uses 1 · Used by 7

Statement usesJoint configurations of a set of variables

Used byBayesian–Dirichlet family score · BDe family score as a ratio of marginal likelihoods · Covered-edge reversal preserves the BDe score · BDe marginal likelihood of a variable set · Sequential Pólya–Dirichlet prediction factor · The BD score is the sequential prediction product · Parent configuration counts sum over family configurations

DefinitionBayesian–Dirichlet family score#✓fully proved

The Bayesian–Dirichlet score of a family F with parent set P ⊆ F and hyperparameters α on the configurations of F.

noncomputable def bdFamily (D : List ((v : V) → σ v)) {P F : Finset V} (hPF : P ⊆ F)
    (α : Config σ F → ℝ) : ℝ :=
  (∏ c : Config σ F, rising (α c) (count D F c)) /
    ∏ j : Config σ P, rising (∑ c with Finset.restrict₂ hPF c = j, α c) (count D P j)

Uses 3 · Used by 4

Statement usesJoint configurations of a set of variables · Count of cases matching a configuration · Rising factorial

Used byBDe family score as a ratio of marginal likelihoods · Bayesian–Dirichlet network score · Covered-edge reversal preserves the BDe score · The BD score is the sequential prediction product

DefinitionBayesian–Dirichlet network score#✓fully proved

The BD score of the structure Pa with family hyperparameters α: the product of the family scores.

noncomputable def bdScore [Fintype V] (D : List ((v : V) → σ v)) (Pa : V → Finset V)
    (α : (v : V) → Config σ (insert v (Pa v)) → ℝ) : ℝ :=
  ∏ v, bdFamily D (subset_insert v (Pa v)) (α v)

Uses 2 · Used by 2

Statement usesJoint configurations of a set of variables · Bayesian–Dirichlet family score

Used byBDe network score · The BD score is the sequential prediction product

DefinitionSequential Pólya–Dirichlet prediction factor#✓fully proved

The sequential Pólya–Dirichlet prediction factor for the case x after the cases D: ∏_v (α_{v,c} + n_{v,c}) / (α_{v,j} + n_{v,j}), with c, j the family and parent values of x and n the counts in D. This is a genuine conditional probability only when Pa is a DAG; for arbitrary parent maps (e.g. cycles or self-parents) the factors over all cases need not sum to one.

noncomputable def predictive [Fintype V] (Pa : V → Finset V)
    (α : (v : V) → Config σ (insert v (Pa v)) → ℝ) (D : List ((v : V) → σ v))
    (x : (v : V) → σ v) : ℝ :=
  ∏ v, (α v ((insert v (Pa v)).restrict x) + count D _ ((insert v (Pa v)).restrict x)) /
    ((∑ c with Finset.restrict₂ (subset_insert v (Pa v)) c = (Pa v).restrict x, α v c) +
      count D (Pa v) ((Pa v).restrict x))

Uses 2 · Used by 2

Statement usesJoint configurations of a set of variables · Count of cases matching a configuration

Used bySequential Pólya–Dirichlet product after prior cases · The BD score is the sequential prediction product

DefinitionSequential Pólya–Dirichlet product after prior cases#✓fully proved

The sequential Pólya–Dirichlet product for the cases D, in order, after the cases E: each case contributes its predictive factor given all cases before it. A genuine probability of the data only when Pa is a DAG (see predictive).

noncomputable def seqProbAfter [Fintype V] (Pa : V → Finset V)
    (α : (v : V) → Config σ (insert v (Pa v)) → ℝ) :
    List ((v : V) → σ v) → List ((v : V) → σ v) → ℝ
  | _, [] => 1
  | E, x :: D => predictive Pa α E x * seqProbAfter Pa α (E ++ [x]) D

Uses 2 · Used by 2

Statement usesJoint configurations of a set of variables · Sequential Pólya–Dirichlet prediction factor

Used bySequential Pólya–Dirichlet product of the data · The BD score is the sequential prediction product

DefinitionSequential Pólya–Dirichlet product of the data#✓fully proved

The sequential Pólya–Dirichlet product for the cases of D, in order. A genuine probability of the data only when Pa is a DAG (see predictive).

noncomputable def seqProb [Fintype V] (Pa : V → Finset V)
    (α : (v : V) → Config σ (insert v (Pa v)) → ℝ) (D : List ((v : V) → σ v)) : ℝ :=
  seqProbAfter Pa α [] D

Uses 2 · Used by 1

Statement usesJoint configurations of a set of variables · Sequential Pólya–Dirichlet product after prior cases

Used byThe BD score is the sequential prediction product

TheoremParent configuration counts sum over family configurations#✓fully proved

The number of cases matching a parent configuration is the sum over the family configurations extending it (N_j = ∑_k N_jk).

theorem sum_count_restrict₂ (D : List ((v : V) → σ v)) {P F : Finset V} (hPF : P ⊆ F)
    (j : Config σ P) :
    ∑ c with Finset.restrict₂ hPF c = j, count D F c = count D P j

Uses 2

Statement usesJoint configurations of a set of variables · Count of cases matching a configuration

TheoremThe BD score is the sequential prediction product#✓fully proved

The BD score is the sequential prediction product of the data (hence it does not depend on the order of the cases). This is an identity for all real hyperparameters. Positivity of the hyperparameters only makes every predictive denominator positive; it does not make this product a probability. The product is a genuine probability of the data only when Pa is a DAG with no self-parents: for cyclic parent maps the predictive factors over all cases need not sum to one.

theorem seqProb_eq_bdScore [Fintype V] (Pa : V → Finset V)
    (α : (v : V) → Config σ (insert v (Pa v)) → ℝ) (D : List ((v : V) → σ v)) :
    seqProb Pa α D = bdScore D Pa α

Uses 8

Statement usesJoint configurations of a set of variables · Bayesian–Dirichlet network score · Sequential Pólya–Dirichlet product of the data

Proof usesBayesian–Dirichlet family score · Count of cases matching a configuration · Sequential Pólya–Dirichlet prediction factor · Rising factorial · Sequential Pólya–Dirichlet product after prior cases

DefinitionBDe hyperparameters#✓fully proved

BDe hyperparameters (Heckerman, Geiger and Chickering): ess times the weight ∑_{x ↦ c} p x of the configuration c of S. When ∑ x, p x = 1, p is a prior joint distribution and this is the prior probability of c.

noncomputable def bdeHyper [Fintype V] (p : ((v : V) → σ v) → ℝ) (ess : ℝ) (S : Finset V)
    (c : Config σ S) : ℝ :=
  ess * ∑ x with S.restrict x = c, p x

Uses 1 · Used by 4

Statement usesJoint configurations of a set of variables

Used byBDe family score as a ratio of marginal likelihoods · BDe network score · Covered-edge reversal preserves the BDe score · BDe marginal likelihood of a variable set

DefinitionBDe marginal likelihood of a variable set#✓fully proved

The (unnormalized) marginal likelihood of the data restricted to the variables S under the BDe Dirichlet prior on the joint values of S. p is treated as generalized weights here: the total Dirichlet mass over configurations is ess * ∑ x, p x, so the omitted normalizing factor is 1 / rising (ess * ∑ x, p x) D.length, the same for every S. When p is normalized (∑ x, p x = 1) this is 1 / rising ess D.length, and p is a prior joint distribution.

noncomputable def margLik [Fintype V] (p : ((v : V) → σ v) → ℝ) (ess : ℝ)
    (D : List ((v : V) → σ v)) (S : Finset V) : ℝ :=
  ∏ c : Config σ S, rising (bdeHyper p ess S c) (count D S c)

Uses 4 · Used by 2

Statement usesJoint configurations of a set of variables · BDe hyperparameters · Count of cases matching a configuration · Rising factorial

Used byBDe family score as a ratio of marginal likelihoods · Covered-edge reversal preserves the BDe score

TheoremBDe family score as a ratio of marginal likelihoods#✓fully proved

With BDe hyperparameters, a family score is a ratio of set marginal likelihoods.

theorem bdFamily_bdeHyper [Fintype V] (p : ((v : V) → σ v) → ℝ) (ess : ℝ)
    (D : List ((v : V) → σ v)) {P F : Finset V} (hPF : P ⊆ F) :
    bdFamily D hPF (bdeHyper p ess F) = margLik p ess D F / margLik p ess D P

Uses 6 · Used by 1

Statement usesBayesian–Dirichlet family score · BDe hyperparameters · BDe marginal likelihood of a variable set

Proof usesJoint configurations of a set of variables · Count of cases matching a configuration · Rising factorial

Used byCovered-edge reversal preserves the BDe score

DefinitionBDe network score#✓fully proved

The BDe score of the structure Pa.

noncomputable def bdeScore [Fintype V] (p : ((v : V) → σ v) → ℝ) (ess : ℝ)
    (D : List ((v : V) → σ v)) (Pa : V → Finset V) : ℝ :=
  bdScore D Pa fun v => bdeHyper p ess (insert v (Pa v))

Uses 2 · Used by 2

Statement usesBayesian–Dirichlet network score · BDe hyperparameters

Used byCovered-edge reversal preserves the BDe score · Covered-edge reversals preserve the BDe score

DefinitionCovered-edge reversal#✓fully proved

Pa' is obtained from Pa by reversing a covered edge x → y (Chickering 1995): x is a parent of y and y's other parents are exactly x's parents (Pa y = insert x (Pa x)); after the reversal y has parents Pa x and x has parents insert y (Pa x). Acyclicity is not required: the score identity holds for any parent-set maps (on a DAG, x ∉ Pa x and y ∉ Pa x hold automatically).

def CoveredReversal (Pa Pa' : V → Finset V) : Prop :=
  ∃ x y, x ≠ y ∧ Pa y = insert x (Pa x) ∧
    Pa' = Function.update (Function.update Pa y (Pa x)) x (insert y (Pa x))

Used by 3

Used byCovered-edge reversal preserves the BDe score · Covered-edge reversals preserve the BDe score · Chickering's transformational characterization

TheoremCovered-edge reversal preserves the BDe score#✓fully proved

Covered-edge reversal preserves the BDe score (for a positive weight function p — a prior when ∑ x, p x = 1 — and positive equivalent sample size).

theorem bdeScore_coveredReversal [Fintype V] [∀ v, Nonempty (σ v)]
    (p : ((v : V) → σ v) → ℝ) (hp : ∀ x, 0 < p x) {ess : ℝ} (hess : 0 < ess)
    (D : List ((v : V) → σ v)) {Pa Pa' : V → Finset V} (h : CoveredReversal Pa Pa') :
    bdeScore p ess D Pa' = bdeScore p ess D Pa

Uses 9 · Used by 1

Statement usesCovered-edge reversal · BDe network score

Proof usesJoint configurations of a set of variables · Bayesian–Dirichlet family score · BDe family score as a ratio of marginal likelihoods · BDe hyperparameters · Count of cases matching a configuration · BDe marginal likelihood of a variable set · Rising factorial

Used byCovered-edge reversals preserve the BDe score

TheoremCovered-edge reversals preserve the BDe score#✓fully proved

Structures connected by a sequence of covered-edge reversals have the same BDe score.

theorem bdeScore_eq_of_reflTransGen [Fintype V] [∀ v, Nonempty (σ v)]
    (p : ((v : V) → σ v) → ℝ) (hp : ∀ x, 0 < p x) {ess : ℝ} (hess : 0 < ess)
    (D : List ((v : V) → σ v)) {Pa Pa' : V → Finset V}
    (h : Relation.ReflTransGen CoveredReversal Pa Pa') :
    bdeScore p ess D Pa' = bdeScore p ess D Pa

Uses 3

Statement usesCovered-edge reversal · BDe network score

Proof usesCovered-edge reversal preserves the BDe score

DefinitionAcyclic network structure#✓fully proved

The structure has no directed cycle.

def IsAcyclic {V : Type*} (Pa : V → Finset V) : Prop :=
  ∀ v, ¬Relation.TransGen (fun u w => u ∈ Pa w) v v

Used by 1

Used byChickering's transformational characterization

DefinitionAdjacent vertices in a network structure#✓fully proved

u and w are adjacent (joined by an edge in either direction).

def Adjacent {V : Type*} (Pa : V → Finset V) (u w : V) : Prop := u ∈ Pa w ∨ w ∈ Pa u

Used by 2

Used byV-structure in a directed graph · Chickering's transformational characterization

DefinitionV-structure in a directed graph#✓fully proved

u → w ← z is a v-structure: two non-adjacent distinct parents of a common child.

def IsVStructure {V : Type*} (Pa : V → Finset V) (u w z : V) : Prop :=
  u ≠ z ∧ u ∈ Pa w ∧ z ∈ Pa w ∧ ¬Adjacent Pa u z

Uses 1 · Used by 1

Statement usesAdjacent vertices in a network structure

Used byChickering's transformational characterization

TheoremChickering's transformational characterization#✓fully proved

Chickering's transformational characterization (1995): two acyclic structures with the same skeleton and the same v-structures (Markov equivalent by Verma and Pearl) are connected by a sequence of covered-edge reversals.

theorem reflTransGen_coveredReversal_of_markovEquivalent {V : Type*} [DecidableEq V]
    [Finite V]
    {Pa Pa' : V → Finset V} (h : IsAcyclic Pa) (h' : IsAcyclic Pa')
    (hskel : ∀ u w, Adjacent Pa u w ↔ Adjacent Pa' u w)
    (hv : ∀ u w z, IsVStructure Pa u w z ↔ IsVStructure Pa' u w z) :
    Relation.ReflTransGen CoveredReversal Pa Pa'

Uses 4

Statement usesAdjacent vertices in a network structure · Covered-edge reversal · Acyclic network structure · V-structure in a directed graph

21 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.