Causal Bayes Net

@cite{grusdt-lassiter-franke-2022}

Two-node causal Bayesian network infrastructure: directed causal structure over two binary variables, noisy-OR parameterization, and probability distributions with conditional probability, independence, and correlation.

• CausalRelation: A→C, C→A, or A⊥C causal structure
• NoisyOR: Noisy-OR parameterization for probabilistic causal links
• WorldState: Joint distribution over two binary variables A and C

inductive Core.Causal.BayesNet.CausalRelation : Type

Causal relations between two binary variables A and C. Used by @cite{grusdt-lassiter-franke-2022} for conditional semantics.

• ACausesC : CausalRelation
• CCausesA : CausalRelation
• Independent : CausalRelation

@[implicit_reducible]

instance Core.Causal.BayesNet.instReprCausalRelation : Repr CausalRelation

Equations

• Core.Causal.BayesNet.instReprCausalRelation = { reprPrec := Core.Causal.BayesNet.instReprCausalRelation.repr }

def Core.Causal.BayesNet.instReprCausalRelation.repr : CausalRelation → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Causal.BayesNet.instDecidableEqCausalRelation : DecidableEq CausalRelation

Equations

• Core.Causal.BayesNet.instDecidableEqCausalRelation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Causal.BayesNet.instInhabitedCausalRelation : Inhabited CausalRelation

Equations

• Core.Causal.BayesNet.instInhabitedCausalRelation = { default := Core.Causal.BayesNet.instInhabitedCausalRelation.default }

def Core.Causal.BayesNet.instInhabitedCausalRelation.default : CausalRelation

Equations

• Core.Causal.BayesNet.instInhabitedCausalRelation.default = Core.Causal.BayesNet.CausalRelation.ACausesC

@[implicit_reducible]

instance Core.Causal.BayesNet.instToStringCausalRelation : ToString CausalRelation

Equations

• One or more equations did not get rendered due to their size.

structure Core.Causal.BayesNet.NoisyOR : Type

Noisy-OR parameterization for a causal link.

• background (b): P(C | ¬A) — background rate
• power (Δ): P(C | A) - P(C | ¬A) — causal power

• background : ℚ

  Background rate: P(C | ¬A)

• power : ℚ

  Causal power: P(C | A) - P(C | ¬A)

@[implicit_reducible]

instance Core.Causal.BayesNet.instReprNoisyOR : Repr NoisyOR

Equations

• Core.Causal.BayesNet.instReprNoisyOR = { reprPrec := Core.Causal.BayesNet.instReprNoisyOR.repr }

def Core.Causal.BayesNet.instReprNoisyOR.repr : NoisyOR → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Causal.BayesNet.instDecidableEqNoisyOR : DecidableEq NoisyOR

Equations

• Core.Causal.BayesNet.instDecidableEqNoisyOR = Core.Causal.BayesNet.instDecidableEqNoisyOR.decEq

def Core.Causal.BayesNet.instDecidableEqNoisyOR.decEq (x✝ x✝¹ : NoisyOR) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

def Core.Causal.BayesNet.NoisyOR.pCGivenA (n : NoisyOR) : ℚ

P(C | A) in the Noisy-OR model.

Equations

• n.pCGivenA = n.background + n.power

def Core.Causal.BayesNet.NoisyOR.pCGivenNotA (n : NoisyOR) : ℚ

P(C | ¬A) in the Noisy-OR model.

Equations

• n.pCGivenNotA = n.background

def Core.Causal.BayesNet.NoisyOR.isValid (n : NoisyOR) : Prop

Check if parameters are valid.

Equations

• n.isValid = (0 ≤ n.background ∧ n.background ≤ 1 ∧ 0 ≤ n.background + n.power ∧ n.background + n.power ≤ 1)

@[implicit_reducible]

instance Core.Causal.BayesNet.NoisyOR.instDecidableIsValid (n : NoisyOR) : Decidable n.isValid

Equations

• n.instDecidableIsValid = Core.Causal.BayesNet.NoisyOR.instDecidableIsValid._aux_1 n

def Core.Causal.BayesNet.NoisyOR.deterministic : NoisyOR

Deterministic cause: P(C|A) = 1, P(C|¬A) = 0.

Equations

• Core.Causal.BayesNet.NoisyOR.deterministic = { background := 0, power := 1 }

def Core.Causal.BayesNet.NoisyOR.noEffect : NoisyOR

No effect: P(C|A) = P(C|¬A) = 0.

Equations

• Core.Causal.BayesNet.NoisyOR.noEffect = { background := 0, power := 0 }

def Core.Causal.BayesNet.NoisyOR.alwaysOn : NoisyOR

Always-on: P(C|A) = P(C|¬A) = 1.

Equations

• Core.Causal.BayesNet.NoisyOR.alwaysOn = { background := 1, power := 0 }

structure Core.Causal.BayesNet.WorldState : Type

A probability distribution over two binary variables A and C.

Used by @cite{grusdt-lassiter-franke-2022}: a "world" is a probability distribution because conditionals make claims about probabilities (P(C|A) > θ).

• pA : ℚ

  Marginal probability P(A)

• pC : ℚ

  Marginal probability P(C)

• pAC : ℚ

  Joint probability P(A ∧ C)

def Core.Causal.BayesNet.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Causal.BayesNet.instReprWorldState : Repr WorldState

Equations

• Core.Causal.BayesNet.instReprWorldState = { reprPrec := Core.Causal.BayesNet.instReprWorldState.repr }

def Core.Causal.BayesNet.instDecidableEqWorldState.decEq (x✝ x✝¹ : WorldState) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Core.Causal.BayesNet.instDecidableEqWorldState : DecidableEq WorldState

Equations

• Core.Causal.BayesNet.instDecidableEqWorldState = Core.Causal.BayesNet.instDecidableEqWorldState.decEq

def Core.Causal.BayesNet.WorldState.isValid (w : WorldState) : Prop

Check if a WorldState represents a valid probability distribution.

Equations

• w.isValid = (0 ≤ w.pA ∧ w.pA ≤ 1 ∧ 0 ≤ w.pC ∧ w.pC ≤ 1 ∧ 0 ≤ w.pAC ∧ w.pAC ≤ min w.pA w.pC ∧ w.pA + w.pC - w.pAC ≤ 1)

@[implicit_reducible]

instance Core.Causal.BayesNet.WorldState.instDecidableIsValid (w : WorldState) : Decidable w.isValid

Equations

• w.instDecidableIsValid = Core.Causal.BayesNet.WorldState.instDecidableIsValid._aux_1 w

def Core.Causal.BayesNet.WorldState.pANotC (w : WorldState) : ℚ

P(A ∧ ¬C)

Equations

• w.pANotC = w.pA - w.pAC

def Core.Causal.BayesNet.WorldState.pNotAC (w : WorldState) : ℚ

P(¬A ∧ C)

Equations

• w.pNotAC = w.pC - w.pAC

def Core.Causal.BayesNet.WorldState.pNotANotC (w : WorldState) : ℚ

P(¬A ∧ ¬C)

Equations

• w.pNotANotC = 1 - w.pA - w.pC + w.pAC

def Core.Causal.BayesNet.WorldState.pNotA (w : WorldState) : ℚ

P(¬A)

Equations

• w.pNotA = 1 - w.pA

def Core.Causal.BayesNet.WorldState.pNotC (w : WorldState) : ℚ

P(¬C)

Equations

• w.pNotC = 1 - w.pC

def Core.Causal.BayesNet.WorldState.pCGivenA (w : WorldState) : ℚ

P(C | A), or 0 if P(A) = 0.

Equations

• w.pCGivenA = if w.pA > 0 then w.pAC / w.pA else 0

def Core.Causal.BayesNet.WorldState.pCGivenNotA (w : WorldState) : ℚ

P(C | ¬A), or 0 if P(¬A) = 0.

Equations

• w.pCGivenNotA = if 1 - w.pA > 0 then w.pNotAC / (1 - w.pA) else 0

def Core.Causal.BayesNet.WorldState.pAGivenC (w : WorldState) : ℚ

P(A | C), or 0 if P(C) = 0.

Equations

• w.pAGivenC = if w.pC > 0 then w.pAC / w.pC else 0

def Core.Causal.BayesNet.WorldState.pAGivenNotC (w : WorldState) : ℚ

P(A | ¬C), or 0 if P(¬C) = 0.

Equations

• w.pAGivenNotC = if 1 - w.pC > 0 then w.pANotC / (1 - w.pC) else 0

def Core.Causal.BayesNet.WorldState.isIndependent (w : WorldState) : Prop

P(A ∧ C) = P(A) · P(C).

Equations

• w.isIndependent = (w.pAC = w.pA * w.pC)

@[implicit_reducible]

instance Core.Causal.BayesNet.WorldState.instDecidableIsIndependent (w : WorldState) : Decidable w.isIndependent

Equations

• w.instDecidableIsIndependent = Core.Causal.BayesNet.WorldState.instDecidableIsIndependent._aux_1 w

def Core.Causal.BayesNet.WorldState.isPositivelyCorrelated (w : WorldState) : Prop

P(A ∧ C) > P(A) · P(C).

Equations

• w.isPositivelyCorrelated = (w.pAC > w.pA * w.pC)

@[implicit_reducible]

instance Core.Causal.BayesNet.WorldState.instDecidableIsPositivelyCorrelated (w : WorldState) : Decidable w.isPositivelyCorrelated

Equations

• w.instDecidableIsPositivelyCorrelated = Core.Causal.BayesNet.WorldState.instDecidableIsPositivelyCorrelated._aux_1 w

def Core.Causal.BayesNet.WorldState.isNegativelyCorrelated (w : WorldState) : Prop

P(A ∧ C) < P(A) · P(C).

Equations

• w.isNegativelyCorrelated = (w.pAC < w.pA * w.pC)

@[implicit_reducible]

instance Core.Causal.BayesNet.WorldState.instDecidableIsNegativelyCorrelated (w : WorldState) : Decidable w.isNegativelyCorrelated

Equations

• w.instDecidableIsNegativelyCorrelated = Core.Causal.BayesNet.WorldState.instDecidableIsNegativelyCorrelated._aux_1 w

def Core.Causal.BayesNet.WorldState.independent (pA pC : ℚ) : WorldState

WorldState from marginals assuming independence.

Equations

• Core.Causal.BayesNet.WorldState.independent pA pC = { pA := pA, pC := pC, pAC := pA * pC }

def Core.Causal.BayesNet.WorldState.perfectCorrelation (p : ℚ) : WorldState

WorldState with perfect correlation (A ↔ C).

Equations

• Core.Causal.BayesNet.WorldState.perfectCorrelation p = { pA := p, pC := p, pAC := p }

def Core.Causal.BayesNet.WorldState.mutuallyExclusive (pA pC : ℚ) : WorldState

WorldState where A ∧ C never happens.

Equations

• Core.Causal.BayesNet.WorldState.mutuallyExclusive pA pC = { pA := pA, pC := pC, pAC := 0 }

theorem Core.Causal.BayesNet.WorldState.valid_implies_pA_bounded (w : WorldState) (h : w.isValid) : 0 ≤ w.pA ∧ w.pA ≤ 1

theorem Core.Causal.BayesNet.WorldState.valid_implies_pC_bounded (w : WorldState) (h : w.isValid) : 0 ≤ w.pC ∧ w.pC ≤ 1

theorem Core.Causal.BayesNet.WorldState.valid_implies_pAC_bounded (w : WorldState) (h : w.isValid) : 0 ≤ w.pAC ∧ w.pAC ≤ min w.pA w.pC

theorem Core.Causal.BayesNet.WorldState.valid_implies_pCGivenA_bounded (w : WorldState) (h : w.isValid) (hA : 0 < w.pA) : 0 ≤ w.pCGivenA ∧ w.pCGivenA ≤ 1

Validity implies 0 ≤ P(C|A) ≤ 1.

theorem Core.Causal.BayesNet.WorldState.valid_implies_pCGivenNotA_bounded (w : WorldState) (h : w.isValid) (hA : w.pA < 1) : 0 ≤ w.pCGivenNotA ∧ w.pCGivenNotA ≤ 1

Validity implies 0 ≤ P(C|¬A) ≤ 1.

theorem Core.Causal.BayesNet.WorldState.law_of_total_probability (w : WorldState) (_h : w.isValid) (hA_pos : 0 < w.pA) (hA_lt_one : w.pA < 1) : w.pC = w.pCGivenA * w.pA + w.pCGivenNotA * (1 - w.pA)

Law of Total Probability: P(C) = P(C|A)·P(A) + P(C|¬A)·P(¬A).

theorem Core.Causal.BayesNet.WorldState.bayes_theorem (w : WorldState) (hA : 0 < w.pA) (hC : 0 < w.pC) : w.pAGivenC = w.pCGivenA * w.pA / w.pC

Bayes' Theorem: P(A|C) = P(C|A)·P(A) / P(C).