Causality and Semantic Separation
summary
Claim: a new semantic separation notion exactly matches graph-theoretic d-separation, with a full mechanized proof mechanized in Rocq. Construction uses structural causal models with unobserved terms, a catalyst/repair sequence semantics for perturbations and conditioning, and a multi-step propagation/repair process that captures colliders. Result gives a concrete recipe for building counterexamples: construct functions and unobserved assignments that propagate a change along an unblocked path, or else conclude no valid perturbation can affect the target, yielding an experimentally falsifiable prediction.
AI-written summary · about
chapters (9)
- 0:00Causality and semantic separation
- 1:07Causal inference with DAGs
- 3:35D-separation blocking paths
- 6:30Structural causal models
- 9:20Semantic separation with perturbations
- 13:21Multi-phase semantic separation
- 15:28Equivalence proof: semantic vs D-separation
- 16:34Applications in experiment design
- 17:58Q&A
related talks
20mInductive diagrams for causal reasoning
25mA Relational Separation Logic for Effect Handlers
05mNew foundations for probabilistic separation logic
18mCertified Semantics for Disequality
22mA case against semantic dependencies
22mImplementing separation logic using an SMT-backed Frame Rule
17mCalculational design of Incorrectness Separation Logic
21mOutcome Separation Logic: Local Reasoning for Correctness and Incorrectness with(…)