Causal models #
This file defines causal models in the sense of Halpern and Pearl. A causal model has a type U
of exogenous contexts, a value type α v for each endogenous variable v, a directed graph on
the variables (mathlib's Digraph), and for each variable a structural equation that gives its
value from the context and the values of its parents in the graph. An intervention holds some
variables at fixed values, and the others obey their equations (CausalModel.step). When the
graph is well founded, every context and every intervention determine exactly one assignment
that satisfies the equations, CausalModel.solve.
The solution is characterized as the unique fixed point of step, and it is reached by
iterating step from any assignment once per rank of a ranking of the graph, which is how a
finite model computes it.
Main definitions #
CausalModel U V α: exogenous contextsU, a graph, and structural equationsCausalModel.IsAcyclic: the graph is well foundedCausalModel.ContextAtRoots: only the roots read the contextCausalModel.step: one round of the equations, with the intervened variables held fixedCausalModel.solve: the solution under an intervention in a context[c ← x, d ← y]: the partial assignment settlingcandd, scoped inCausalModel
Main results #
CausalModel.isFixedPt_solve,CausalModel.eq_solve_of_isFixedPt: the solution is the unique fixed point ofstepCausalModel.solve_eq_iterate,CausalModel.solve_eq_iterate_card: iteratingsteppast a ranking of the graph reaches it, so in a finite modeldecideevaluates the solution (CausalModel.decidableEqSolve)
Implementation notes #
An equation reads the whole assignment, and dependsOn_eqn says that it only reads the parents
(mathlib's DependsOn), so equations are written without the parents' subtype. For a finite
inductive type of variables the default proof of dependsOn_eqn discharges it. The graph is data,
the edges a paper draws, and bounds what an equation may read rather than recording what it does
read. An intervention is a partial assignment ∀ v, Flat (α v), the variables it settles being the
intervened ones. The solution is WellFounded.fixedPoint of step, whose construction fills the
coordinates an equation ignores arbitrarily, hence [∀ v, Nonempty (α v)].
A concrete model in a study is written to one recipe. The exogenous context is a structure whose
fields name what the paper leaves to the world (structure Context where match : Bool, with
deriving DecidableEq, Fintype, Inhabited, Repr), never a positional tuple. The edges are a
Finset (V × V) (def edges : Finset (V × V) := {(.match, .fire)}) with graph := ⟨fun w v ↦ (w, v) ∈ edges⟩, adjacency is decided by fun w v ↦ inferInstanceAs (Decidable ((w, v) ∈ edges)), and acyclicity by Finite.wellFounded_of_irrefl_transGen (by decide).
Partial assignments are written in the scoped notation, [c ← x, d ← y], and updates of a named
assignment as Function.update s c ↑x. A theorem quantifying over assignments or settlements
(necessity, sufficient sets) is proved structurally through the equations rather than by
decide, which enumerates them.
References #
A causal model is a directed graph on the variables V with a structural equation at each
variable. The equation gives the variable's value in α v from an exogenous context in U and
the values of the variable's parents, the sources of its incoming edges.
- graph : Digraph V
The causal graph, with an edge from
wtovwhenv's equation may readw. - eqn (v : V) : U → ((w : V) → α w) → α v
The structural equation of each variable, read in a context.
Each equation reads only the variable's parents. For a finite inductive type of variables whose equations match on the variable, the default proof rewrites each variable an equation reads by the hypothesis, deciding that it is a parent.
Instances For
A model is acyclic, or recursive, when its graph is well founded.
Instances For
The context reaches a model only at its roots when the equation of every variable with a parent gives the same value in every context, as in the dynamics of Schulz and Nadathur, whose inner variables are truth functions of their parents.
Instances
A model is acyclic when every edge climbs in depth.
[c ← x] is the partial assignment settling c to x and leaving every other variable
open, in the notation of Halpern and Pearl; [c ← x, d ← y] settles both. It serves as an
intervention and as an observation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
M.step I u x applies the equations once in the context u. A variable the intervention
I settles takes its intervened value, and any other variable takes the value its equation
gives to x.
Equations
- M.step I u x v = Flat.unbotD (M.eqn v u x) (I v)
Instances For
Each round computes a variable from its parents.
After k rounds of the equations, a variable of rank below k no longer depends on the
assignment the rounds started from.
The solution of the model under the intervention I in the context u, the unique fixed
point of step.
Equations
- M.solve I u = WellFounded.fixedPoint hM (M.step I u)
Instances For
The solution satisfies the equations.
An assignment satisfying the equations is the solution.
An intervened variable takes its intervened value.
A variable the intervention leaves alone obeys its equation.
Iterating the equations from any assignment past a ranking of the graph reaches the solution.
In a finite model, iterating the equations once per variable reaches the solution.
In a finite model the value of the solution at a variable is decided by iterating the
equations. It takes priority over the value type's own decidable equality, which cannot evaluate
solve.
Equations
- CausalModel.decidableEqSolve I u v x = decidable_of_iff ((M.step I u)^[Fintype.card V] default v = x) ⋯
In a finite model, whether two solutions agree at a variable is decided by iterating the equations for both.
Equations
- CausalModel.decidableEqSolveSolve I J u u' v = decidable_of_iff ((M.step I u)^[Fintype.card V] default v = (M.step J u')^[Fintype.card V] default v) ⋯