Documentation

Linglib.Core.Causal.SEM.Interventional

SEM: Interventional Probability #

P(E = xE | do(C := xC)) — the interventional probability of an effect under Pearl's do-operator. Distinct from counterfactual reasoning: there is no observation conditioning, no abduction step.

This file is the home for probabilisticSuf (@cite{cao-white-lassiter-2025}'s graded ALT measure for causal sufficiency) and its deterministic-collapse bridge.

Why a separate file from Counterfactual.lean #

Counterfactual reasoning (Lewis 1973, N&L 2020 Defs 23/24/25, B&G 2025 W/H/S, Lassiter 2017) involves observation conditioning — given that we observed the actual world, what would have happened if X had been different? This requires an abduction step (Pearl 3-step: abduction-action-prediction).

Interventional probability skips abduction: just intervene and predict. Mathematically simpler; conceptually different. They share the substrate (develop, intervene) but answer different questions.

Mathlib analogue: Mathlib/Probability/Kernel/CondCDF.lean (conditional) vs Mathlib/Probability/Kernel/Defs.lean (unconditional kernel) — same substrate, distinct files for distinct mathematical questions.

Computability #

probabilisticSuf is noncomputable (uses tsum over PMF). The deterministic-collapse bridge probabilisticSuf_of_deterministic reduces it to a {0,1} indicator under IsDeterministic via develop_eq_pure_of_deterministic (Basic.lean). Sorry-free.

source
noncomputable def Core.Causal.SEM.probabilisticSuf {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) :
ENNReal

Interventional probability of an effect: P(effect = xE | do(cause := xC)). Pearl's do-operator gives the probability of the effect under forward intervention; no observation conditioning.

@cite{cao-white-lassiter-2025}'s graded ALT measure for causal sufficiency. PMF-valued via develop; reduces to a {0,1} indicator under IsDeterministic via probabilisticSuf_of_deterministic.

Equations
Instances For
    source
    theorem Core.Causal.SEM.probabilisticSuf_of_deterministic {V : Type u_1} {α : V → Type u_2} [Fintype V] [DecidableEq V] [DecidableValuation α] (M : SEM V α) [M.graph.IsDAG] [M.IsDeterministic] (s : Valuation α) (cause : V) (xC : α cause) (effect : V) (xE : α effect) :
    M.probabilisticSuf s cause xC effect xE = if ((M.intervene cause xC).developDet s).hasValue effect xE then 1 else 0

    Bridge: under IsDeterministic, probabilisticSuf is the {0,1} indicator of whether the deterministic intervened development hits effect = xE.