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.CausalBayesNet.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

def Core.CausalBayesNet.instReprCausalRelation.repr : CausalRelation → ℕ → Std.Format

Equations

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

instance Core.CausalBayesNet.instReprCausalRelation : Repr CausalRelation

Equations

• Core.CausalBayesNet.instReprCausalRelation = { reprPrec := Core.CausalBayesNet.instReprCausalRelation.repr }

instance Core.CausalBayesNet.instDecidableEqCausalRelation : DecidableEq CausalRelation

Equations

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

def Core.CausalBayesNet.instBEqCausalRelation.beq : CausalRelation → CausalRelation → Bool

Equations

• Core.CausalBayesNet.instBEqCausalRelation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Core.CausalBayesNet.instBEqCausalRelation : BEq CausalRelation

Equations

• Core.CausalBayesNet.instBEqCausalRelation = { beq := Core.CausalBayesNet.instBEqCausalRelation.beq }

def Core.CausalBayesNet.instInhabitedCausalRelation.default : CausalRelation

Equations

• Core.CausalBayesNet.instInhabitedCausalRelation.default = Core.CausalBayesNet.CausalRelation.ACausesC

instance Core.CausalBayesNet.instInhabitedCausalRelation : Inhabited CausalRelation

Equations

• Core.CausalBayesNet.instInhabitedCausalRelation = { default := Core.CausalBayesNet.instInhabitedCausalRelation.default }

instance Core.CausalBayesNet.instToStringCausalRelation : ToString CausalRelation

Equations

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

structure Core.CausalBayesNet.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)

def Core.CausalBayesNet.instReprNoisyOR.repr : NoisyOR → ℕ → Std.Format

Equations

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

instance Core.CausalBayesNet.instReprNoisyOR : Repr NoisyOR

Equations

• Core.CausalBayesNet.instReprNoisyOR = { reprPrec := Core.CausalBayesNet.instReprNoisyOR.repr }

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

Equations

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

instance Core.CausalBayesNet.instDecidableEqNoisyOR : DecidableEq NoisyOR

Equations

• Core.CausalBayesNet.instDecidableEqNoisyOR = Core.CausalBayesNet.instDecidableEqNoisyOR.decEq

instance Core.CausalBayesNet.instBEqNoisyOR : BEq NoisyOR

Equations

• Core.CausalBayesNet.instBEqNoisyOR = { beq := Core.CausalBayesNet.instBEqNoisyOR.beq }

def Core.CausalBayesNet.instBEqNoisyOR.beq : NoisyOR → NoisyOR → Bool

Equations

• Core.CausalBayesNet.instBEqNoisyOR.beq { background := a, power := a_1 } { background := b, power := b_1 } = (a == b && a_1 == b_1)
• Core.CausalBayesNet.instBEqNoisyOR.beq x✝¹ x✝ = false

def Core.CausalBayesNet.NoisyOR.pCGivenA (n : NoisyOR) : ℚ

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

Equations

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

def Core.CausalBayesNet.NoisyOR.pCGivenNotA (n : NoisyOR) : ℚ

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

Equations

• n.pCGivenNotA = n.background

def Core.CausalBayesNet.NoisyOR.isValid (n : NoisyOR) : Bool

Check if parameters are valid.

Equations

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

def Core.CausalBayesNet.NoisyOR.deterministic : NoisyOR

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

Equations

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

def Core.CausalBayesNet.NoisyOR.noEffect : NoisyOR

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

Equations

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

def Core.CausalBayesNet.NoisyOR.alwaysOn : NoisyOR

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

Equations

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

structure Core.CausalBayesNet.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)

instance Core.CausalBayesNet.instReprWorldState : Repr WorldState

Equations

• Core.CausalBayesNet.instReprWorldState = { reprPrec := Core.CausalBayesNet.instReprWorldState.repr }

def Core.CausalBayesNet.instReprWorldState.repr : WorldState → ℕ → Std.Format

Equations

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

instance Core.CausalBayesNet.instDecidableEqWorldState : DecidableEq WorldState

Equations

• Core.CausalBayesNet.instDecidableEqWorldState = Core.CausalBayesNet.instDecidableEqWorldState.decEq

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

Equations

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

instance Core.CausalBayesNet.instBEqWorldState : BEq WorldState

Equations

• Core.CausalBayesNet.instBEqWorldState = { beq := Core.CausalBayesNet.instBEqWorldState.beq }

def Core.CausalBayesNet.instBEqWorldState.beq : WorldState → WorldState → Bool

Equations

• Core.CausalBayesNet.instBEqWorldState.beq { pA := a, pC := a_1, pAC := a_2 } { pA := b, pC := b_1, pAC := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Core.CausalBayesNet.instBEqWorldState.beq x✝¹ x✝ = false

def Core.CausalBayesNet.WorldState.isValid (w : WorldState) : Bool

Check if a WorldState represents a valid probability distribution.

Equations

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

def Core.CausalBayesNet.WorldState.pANotC (w : WorldState) : ℚ

P(A ∧ ¬C)

Equations

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

def Core.CausalBayesNet.WorldState.pNotAC (w : WorldState) : ℚ

P(¬A ∧ C)

Equations

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

def Core.CausalBayesNet.WorldState.pNotANotC (w : WorldState) : ℚ

P(¬A ∧ ¬C)

Equations

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

def Core.CausalBayesNet.WorldState.pNotA (w : WorldState) : ℚ

P(¬A)

Equations

• w.pNotA = 1 - w.pA

def Core.CausalBayesNet.WorldState.pNotC (w : WorldState) : ℚ

P(¬C)

Equations

• w.pNotC = 1 - w.pC

def Core.CausalBayesNet.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.CausalBayesNet.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.CausalBayesNet.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.CausalBayesNet.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.CausalBayesNet.WorldState.isIndependent (w : WorldState) : Bool

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

Equations

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

def Core.CausalBayesNet.WorldState.isPositivelyCorrelated (w : WorldState) : Bool

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

Equations

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

def Core.CausalBayesNet.WorldState.isNegativelyCorrelated (w : WorldState) : Bool

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

Equations

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

def Core.CausalBayesNet.WorldState.independent (pA pC : ℚ) : WorldState

WorldState from marginals assuming independence.

Equations

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

def Core.CausalBayesNet.WorldState.perfectCorrelation (p : ℚ) : WorldState

WorldState with perfect correlation (A ↔ C).

Equations

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

def Core.CausalBayesNet.WorldState.mutuallyExclusive (pA pC : ℚ) : WorldState

WorldState where A ∧ C never happens.

Equations

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

def Core.CausalBayesNet.WorldState.IsValid (w : WorldState) : Prop

Propositional version of isValid for theorem proving.

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)

theorem Core.CausalBayesNet.WorldState.valid_implies_pA_bounded (w : WorldState) (h : w.IsValid) : 0 ≤ w.pA ∧ w.pA ≤ 1

theorem Core.CausalBayesNet.WorldState.valid_implies_pC_bounded (w : WorldState) (h : w.IsValid) : 0 ≤ w.pC ∧ w.pC ≤ 1

theorem Core.CausalBayesNet.WorldState.valid_implies_pAC_bounded (w : WorldState) (h : w.IsValid) : 0 ≤ w.pAC ∧ w.pAC ≤ min w.pA w.pC

theorem Core.CausalBayesNet.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.CausalBayesNet.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.CausalBayesNet.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.CausalBayesNet.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).