Observation and intervention in causal models

A partial assignment s : ∀ v, Flat (α v) can be read two ways in a causal model. As an intervention it holds the variables it settles at their values (CausalModel.solve). As an observation it picks out the contexts whose actual world agrees with it, CausalModel.contexts, the conditioning step of Pearl's evaluation of a counterfactual.

The solution at a variable depends only on the intervention at that variable and its ancestors (CausalModel.solve_congr), so an intervention leaves every variable it cannot reach as it was (CausalModel.solve_update_of_not_reflTransGen).

Main definitions

• CausalModel.world: the actual world of a context, as a total partial assignment
• CausalModel.contexts: the contexts in which an observation holds

Main results

• CausalModel.solve_congr: interventions agreeing on a variable's ancestors agree there
• CausalModel.solve_update_of_not_reflTransGen: intervening on c leaves what c does not reach unchanged
• CausalModel.solve_eq_solve_bot_of_mem_contexts: imposing an observation that holds changes nothing

References

• [Pea09]

theorem CausalModel.solve_congr {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] {I J : (v : V) → Flat (α v)} {v : V} (h : ∀ (w : V), Relation.ReflTransGen M.graph.Adj w v → I w = J w) (u : U) : M.solve I u v = M.solve J u v

Interventions that agree on a variable and all its ancestors give it the same value.

@[simp]

theorem CausalModel.solve_update_self {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] [DecidableEq V] (I : (v : V) → Flat (α v)) (c : V) (x : α c) (u : U) : M.solve (Function.update I c ↑x) u c = x

theorem CausalModel.solve_update_of_not_reflTransGen {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] [DecidableEq V] {c v : V} (h : ¬Relation.ReflTransGen M.graph.Adj c v) (I : (v : V) → Flat (α v)) (x : Flat (α c)) (u : U) : M.solve (Function.update I c x) u v = M.solve I u v

Intervening on c leaves every variable that c is not an ancestor of unchanged.

noncomputable def CausalModel.world {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] (u : U) (v : V) : Flat (α v)

M.world u is the actual world of the context u, the solution under no intervention with every variable settled.

Equations

• M.world u v = ↑(M.solve ⊥ u v)

def CausalModel.contexts {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] (s : (v : V) → Flat (α v)) : Set U

M.contexts s is the set of contexts in which the observation s holds, those whose actual world settles every variable s settles, at the same value.

Equations

• M.contexts s = {u : U | s ≤ M.world u}

@[simp]

theorem CausalModel.contexts_bot {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] : M.contexts ⊥ = Set.univ

theorem CausalModel.contexts_anti {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] : Antitone M.contexts

An observation that settles more holds in fewer contexts.

theorem CausalModel.solve_eq_solve_bot_of_mem_contexts {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {u : U} (hu : u ∈ M.contexts s) : M.solve s u = M.solve ⊥ u

In a context where the observation holds, imposing it as an intervention changes nothing.

theorem CausalModel.mem_contexts_update {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [∀ (v : V), Nonempty (α v)] [hM : M.IsAcyclic] [DecidableEq V] {s : (v : V) → Flat (α v)} {u : U} (hu : u ∈ M.contexts s) {c : V} {x : α c} (hx : M.solve ⊥ u c = x) : u ∈ M.contexts (Function.update s c ↑x)

An observation extended by a fact of the context's actual world still holds there.