Developing an observation through a causal model

An observation s : ∀ v, Flat (α v) settles some variables and leaves the context unknown. Two local procedures propagate what it settles through the equations, each deciding a variable from what has been decided about its parents alone.

• In the strict development of Schulz and of Nadathur, a variable is settled once all its parents are, and its equation then gives the same value in every context (CausalModel.CausallyEntails).
• In the Kleene development used by Baglini and Bar-Asher Siegal, a variable is forced to a value when every completion of what is known about its parents gives that value in every context, so a turned handle on an unlocked door forces the door open while other inputs are unknown (CausalModel.Forced).

Both are fixed points of maps that compute each variable from its parents (WellFounded.fixedPoint). The strict development settles less than the Kleene one (CausalModel.Forced.of_causallyEntails), and the Kleene one is sound: what it forces holds in every context when the observation is imposed as an intervention (CausalModel.Forced.solve_eq_of_intervene), and in every context where the observation holds (CausalModel.Forced.solve_bot_eq).

Main definitions

• CausalModel.Forced: the Kleene development of an observation
• CausalModel.CausallyEntails: the strict development of an observation

Main results

• CausalModel.forced_iff, CausalModel.causallyEntails_iff: the defining equations
• CausalModel.Forced.of_causallyEntails: the strict development settles less
• CausalModel.Forced.solve_eq_of_intervene, CausalModel.Forced.solve_bot_eq: soundness for the observation imposed as an intervention and for the observation holding
• CausalModel.causallyEntails_congr: the strict development of a variable reads the observation only at its ancestors
• CausalModel.CausallyEntails.parent_eq: a settled variable settles each parent to the value its equation needs
• CausalModel.causallyEntails_solve_bot: when only the roots read the context, an observation whose development settles every root develops to the actual world of its contexts
• CausalModel.causallyEntails_iff_develop: the strict development computed one value per variable (CausalModel.develop), so that decide evaluates it in a finite model

Implementation notes

Uncertainty about exogenous variables is uncertainty about the context, so a variable whose equation reads the context is settled only when the equation gives the same value in every context. A model whose root variables read the context therefore leaves them unsettled unless the observation settles them, as the strict development of Schulz leaves undetermined background variables. Both developments are families of predicates ∀ v, α v → Prop, which spares choosing the value a variable is settled to.

Soundness has no converse. With b := ¬ a and v := a ∧ b, v is false in every context, but neither development settles it while a is unknown, since each looks only at what is settled about v's parents.

References

• [Sch11c]
• [Nad23b]
• [BBS25]
• [BS26b]

def CausalModel.forcedStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) (s : (v : V) → Flat (α v)) (P : (v : V) → α v → Prop) (v : V) : α v → Prop

M.forcedStep s P is one round of Kleene development from the observation s, given what P has settled. A variable is settled to x when s settles it so, or when s leaves it open and its equation gives x in every context and on every assignment agreeing with what P settles about its parents.

Equations

• M.forcedStep s P v x = (s v = ↑x ∨ s v = ⊥ ∧ ∀ (u : U) (y : (w : V) → α w), (∀ (w : V), M.graph.Adj w v → ∀ (z : α w), P w z → y w = z) → M.eqn v u y = x)

def CausalModel.entailsStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) (s : (v : V) → Flat (α v)) (P : (v : V) → α v → Prop) (v : V) : α v → Prop

M.entailsStep s P is one round of strict development from the observation s. It is forcedStep, except that a variable s leaves open is settled only once all its parents are.

Equations

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

theorem CausalModel.dependsOn_forcedStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} (s : (v : V) → Flat (α v)) (v : V) : DependsOn (fun (x : (i : V) → α i → Prop) => M.forcedStep s x v) {w : V | M.graph.Adj w v}

theorem CausalModel.dependsOn_entailsStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} (s : (v : V) → Flat (α v)) (v : V) : DependsOn (fun (x : (i : V) → α i → Prop) => M.entailsStep s x v) {w : V | M.graph.Adj w v}

theorem CausalModel.entailsStep_le_forcedStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} (s : (v : V) → Flat (α v)) {P Q : (v : V) → α v → Prop} (h : P ≤ Q) : M.entailsStep s P ≤ M.forcedStep s Q

A strict round settles no more than a Kleene round given more.

def CausalModel.Forced {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [hM : M.IsAcyclic] (s : (v : V) → Flat (α v)) (v : V) (x : α v) : Prop

M.Forced s v x says that the Kleene development of the observation s forces v to x.

Equations

• M.Forced s v x = WellFounded.fixedPoint hM (M.forcedStep s) v x

def CausalModel.CausallyEntails {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [hM : M.IsAcyclic] (s : (v : V) → Flat (α v)) (v : V) (x : α v) : Prop

M.CausallyEntails s v x says that the strict development of s settles v to x.

Equations

• M.CausallyEntails s v x = WellFounded.fixedPoint hM (M.entailsStep s) v x

theorem CausalModel.forced_iff {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.Forced s v x ↔ s v = ↑x ∨ s v = ⊥ ∧ ∀ (u : U) (y : (w : V) → α w), (∀ (w : V), M.graph.Adj w v → ∀ (z : α w), M.Forced s w z → y w = z) → M.eqn v u y = x

theorem CausalModel.causallyEntails_iff {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.CausallyEntails s v x ↔ s v = ↑x ∨ s v = ⊥ ∧ (∀ (w : V), M.graph.Adj w v → ∃ (z : α w), M.CausallyEntails s w z) ∧ ∀ (u : U) (y : (w : V) → α w), (∀ (w : V), M.graph.Adj w v → ∀ (z : α w), M.CausallyEntails s w z → y w = z) → M.eqn v u y = x

theorem CausalModel.causallyEntails_root_iff {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {t : (v : V) → Flat (α v)} {v : V} {x : α v} (hroot : ∀ (w : V), ¬M.graph.Adj w v) (hv : t v = ⊥) : M.CausallyEntails t v x ↔ ∀ (u : U) (y : (w : V) → α w), M.eqn v u y = x

A root the observation leaves unobserved is settled exactly when its equation is constant.

theorem CausalModel.Forced.of_causallyEntails {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} (h : M.CausallyEntails s v x) : M.Forced s v x

The strict development settles less than the Kleene one.

theorem CausalModel.CausallyEntails.parent_settled {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} (h : M.CausallyEntails s v x) (hv : s v = ⊥) {w : V} (hw : M.graph.Adj w v) : ∃ (z : α w), M.CausallyEntails s w z

A variable the strict development settles, unobserved, has every parent settled.

theorem CausalModel.causallyEntails_congr {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} {t : (v : V) → Flat (α v)} (h : ∀ (w : V), Relation.ReflTransGen M.graph.Adj w v → s w = t w) : M.CausallyEntails s v x ↔ M.CausallyEntails t v x

Observations that agree on a variable and all its ancestors settle it alike.

theorem CausalModel.causallyEntails_update_of_not_reflTransGen {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [DecidableEq V] {c : V} (h : ¬Relation.ReflTransGen M.graph.Adj c v) (y : Flat (α c)) : M.CausallyEntails (Function.update s c y) v x ↔ M.CausallyEntails s v x

Settling c leaves what the strict development settles about a variable c does not reach unchanged.

theorem CausalModel.forced_iff_iterate_card {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [Fintype V] : M.Forced s v x ↔ (M.forcedStep s)^[Fintype.card V] ⊥ v x

In a finite model, the Kleene development is reached by iterating its rounds once per variable.

theorem CausalModel.causallyEntails_iff_iterate_card {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [Fintype V] : M.CausallyEntails s v x ↔ (M.entailsStep s)^[Fintype.card V] ⊥ v x

In a finite model, the strict development is reached by iterating its rounds once per variable.

theorem CausalModel.Forced.solve_eq_of_intervene {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [∀ (v : V), Nonempty (α v)] (h : M.Forced s v x) (u : U) : M.solve s u v = x

The Kleene development is sound. What it forces from s holds in every context when s is imposed as an intervention.

theorem CausalModel.CausallyEntails.solve_eq_of_intervene {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [∀ (v : V), Nonempty (α v)] (h : M.CausallyEntails s v x) (u : U) : M.solve s u v = x

The strict development is sound for the interventional reading.

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

The Kleene development is sound for the observational reading. What it forces from s holds in every context where s holds.

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

The strict development is sound for the observational reading.

theorem CausalModel.causallyEntails_solve_bot {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} [∀ (v : V), Nonempty (α v)] [M.ContextAtRoots] {u : U} (hs : ∀ (v : V), (∀ (w : V), ¬M.graph.Adj w v) → ∃ (z : α v), M.CausallyEntails s v z) (hu : u ∈ M.contexts s) (v : V) : M.CausallyEntails s v (M.solve ⊥ u v)

When the context reaches the model only at its roots, an observation whose development settles every root develops, in a context where it holds, to that context's actual world.

theorem CausalModel.CausallyEntails.unique {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [∀ (v : V), Nonempty (α v)] [Nonempty U] {y : α v} (hx : M.CausallyEntails s v x) (hy : M.CausallyEntails s v y) : x = y

The strict development settles a variable to at most one value.

theorem CausalModel.CausallyEntails.eqn_eq {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [∀ (v : V), Nonempty (α v)] [Nonempty U] (h : M.CausallyEntails s v x) (hv : s v = ⊥) {y : (w : V) → α w} (hy : ∀ (w : V), M.graph.Adj w v → M.CausallyEntails s w (y w)) (u : U) : M.eqn v u y = x

A variable the strict development settles, unobserved, takes its equation's value at the values the development settles for its parents, in every context.

theorem CausalModel.CausallyEntails.parent_eq {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] {s : (v : V) → Flat (α v)} {v : V} {x : α v} [∀ (v : V), Nonempty (α v)] [Nonempty U] (h : M.CausallyEntails s v x) (hv : s v = ⊥) {w : V} (hw : M.graph.Adj w v) {z : α w} (hz : ∀ (u : U) (y : (w : V) → α w), M.eqn v u y = x → y w = z) : M.CausallyEntails s w z

A variable the strict development settles, unobserved, settles each parent to the value its equation needs for the result.

Computing the strict development

A variable the strict development settles has settled parents, so its value is its equation at their values, the same in every context. develop computes the development this way, one value per variable, and in a finite model decide evaluates it by iteration.

def CausalModel.developStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s p : (v : V) → Flat (α v)) (v : V) : Flat (α v)

M.developStep s p is one round of the strict development as values. A variable s settles keeps its value; one s leaves open is settled once p settles all its parents and its equation, at their values, gives the same value in every context.

Equations

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

theorem CausalModel.dependsOn_developStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : DependsOn (fun (x : (i : V) → Flat (α i)) => M.developStep s x v) {w : V | M.graph.Adj w v}

noncomputable def CausalModel.develop {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : Flat (α v)

The strict development of the observation s, as values.

Equations

• M.develop s = WellFounded.fixedPoint hM (M.developStep s)

theorem CausalModel.develop_apply {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : M.develop s v = M.developStep s (M.develop s) v

theorem CausalModel.causallyEntails_iff_develop {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.CausallyEntails s v x ↔ M.develop s v = ↑x

The strict development settles v to x exactly when its computation does.

theorem CausalModel.causallyEntails_iff_iterate {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.CausallyEntails s v x ↔ (M.developStep s)^[Fintype.card V] ⊥ v = ↑x

@[instance_reducible]

instance CausalModel.instDecidableCausallyEntails {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [Fintype V] [DecidableRel M.graph.Adj] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : Decidable (M.CausallyEntails s v x)

In a finite model, causal entailment is decided by computing the strict development.

Equations

• CausalModel.instDecidableCausallyEntails = decidable_of_iff ((M.developStep s)^[Fintype.card V] ⊥ v = ↑x) ⋯

Computing the Kleene development

A variable the Kleene development forces takes the value its equation gives at any completion of what is known about its parents, in any context. developKleene computes it by testing the value at one completion against every completion and context, one value per variable.

def CausalModel.developKleeneStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] (s p : (v : V) → Flat (α v)) (v : V) : Flat (α v)

M.developKleeneStep s p is one round of the Kleene development as values. A variable s settles keeps its value; one s leaves open is settled when its equation gives the same value in every context on every assignment extending what p settles about its parents.

Equations

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

theorem CausalModel.dependsOn_developKleeneStep {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : DependsOn (fun (x : (i : V) → Flat (α i)) => M.developKleeneStep s x v) {w : V | M.graph.Adj w v}

noncomputable def CausalModel.developKleene {U : Type u_1} {V : Type u_2} {α : V → Type u_3} (M : CausalModel U V α) [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : Flat (α v)

The Kleene development of the observation s, as values.

Equations

• M.developKleene s = WellFounded.fixedPoint hM (M.developKleeneStep s)

theorem CausalModel.developKleene_apply {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) : M.developKleene s v = M.developKleeneStep s (M.developKleene s) v

theorem CausalModel.forced_iff_developKleene {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.Forced s v x ↔ M.developKleene s v = ↑x

The Kleene development forces v to x exactly when its computation settles it so.

theorem CausalModel.forced_iff_iterate {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] {s : (v : V) → Flat (α v)} {v : V} {x : α v} : M.Forced s v x ↔ (M.developKleeneStep s)^[Fintype.card V] ⊥ v = ↑x

@[instance_reducible]

instance CausalModel.instDecidableForced {U : Type u_1} {V : Type u_2} {α : V → Type u_3} {M : CausalModel U V α} [hM : M.IsAcyclic] [Fintype U] [Inhabited U] [(v : V) → Inhabited (α v)] [(v : V) → DecidableEq (α v)] [(v : V) → Fintype (α v)] [Fintype V] [DecidableEq V] [DecidableRel M.graph.Adj] (s : (v : V) → Flat (α v)) (v : V) (x : α v) : Decidable (M.Forced s v x)

In a finite model, being forced is decided by computing the Kleene development.

Equations

• CausalModel.instDecidableForced s v x = decidable_of_iff ((M.developKleeneStep s)^[Fintype.card V] ⊥ v = ↑x) ⋯