Paper deep dive
Graph Surgery and the Do-Operator: A Precise Correspondence for Acyclic Structural Causal Models
Satpreet Makhija
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 91%
Last extracted: 8/19/2026, 5:15:10 AM
Summary
This paper establishes a precise mathematical correspondence between graph surgery (deleting incoming arrows) and the do-operator (replacing mechanisms with constants) in deterministic acyclic structural causal models. It proves that the dependency graph of an intervened mechanism family is identical to the graph obtained by surgically removing arrows to intervention targets. The work also defines sequential interventions, showing they combine by retaining the latest assigned value, and proves an ancestor theorem where outcomes depend only on interventions at actual dependency ancestors.
Entities (7)
Relation Signals (5)
Graph Surgery → correspondsto → do-operator
confidence 95% · Our central result says that the same dependency graph is reached in either order: update the mechanisms and then extract their dependencies, or first extract the dependencies and then perform graph surgery.
Mechanism Family → hasdependencygraph → Dependency Graph
confidence 94% · If Graph(F) extracts the dependencies of a mechanism family F... Graph(F^iota)=Surg(Graph(F),T_iota).
Causal Model → consistsof → Directed Acyclic Graph
confidence 93% · A deterministic acyclic structural causal model is a pair M:=(G,F), where G is a directed acyclic graph and F is a mechanism family
Outcome → dependson → Ancestor Interventions
confidence 92% · prove that an outcome depends only on interventions at its actual dependency ancestors.
Sequential Interventions → combineby → Retaining Latest Value
confidence 90% · If both assign a value to the same variable, the later value from kappa must prevail.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:The $\operatorname{do}$-operator is described graphically by deleting arrows into its targets and functionally by replacing their mechanisms with constants. To call these operations equivalent is not yet a mathematical statement: one returns a graph and remembers only the targets, whereas the other returns mechanisms and also remembers the imposed values. We make a dependency-level comparison precise for deterministic acyclic structural causal models with finitely many endogenous variables. If $\operatorname{Graph}(F)$ extracts the dependencies of a mechanism family $F$, our main theorem is $\operatorname{Graph}(F^\iota)=\operatorname{Surg}(\operatorname{Graph}(F),T_\iota)$. Thus replacing target mechanisms removes exactly the dependencies removed by graph surgery. For a model $M=(G,F)$ whose graph may contain unused arrows, we characterize when the same equality holds with $G$ in place of $\operatorname{Graph}(F)$; it holds for every intervention exactly when $G$ records the dependencies of $F$ exactly. We then define the intervened model, characterize its run, show how sequential interventions combine, and prove that an outcome depends only on interventions at its actual dependency ancestors.
Tags
Links
- Source: https://arxiv.org/abs/2608.17634v1
- Canonical: https://arxiv.org/abs/2608.17634v1
Trouble viewing inline? Open PDF directly →
Full Text
25,187 characters extracted from source content.
Expand or collapse full text
Graph Surgery and the Do-Operator A Precise Correspondence for Acyclic Structural Causal Models Satpreet Makhija Affiliation: Ashoka University, Sonipat, India Abstract The do -operator is described graphically by deleting arrows into its targets and functionally by replacing their mechanisms with constants. To call these operations equivalent is not yet a mathematical statement: one returns a graph and remembers only the targets, whereas the other returns mechanisms and also remembers the imposed values. We make a dependency-level comparison precise for deterministic acyclic structural causal models with finitely many endogenous variables. If Graph(F) (F) extracts the dependencies of a mechanism family F, our main theorem is Graph(Fι)=Surg(Graph(F),Tι). (F )= ( (F),T_ ). Thus replacing target mechanisms removes exactly the dependencies removed by graph surgery. For a model M=(G,F)M=(G,F) whose graph may contain unused arrows, we characterize when the same equality holds with G in place of Graph(F) (F); it holds for every intervention exactly when G records the dependencies of F exactly. We then define the intervened model, characterize its run, show how sequential interventions combine, and prove that an outcome depends only on interventions at its actual dependency ancestors. Keywords: Structural causal models Interventions Do-operator Graph surgery Dependency graphs. 1 Introduction The do -operator is the standard notation for an intervention in a structural causal model [4]. An expression such as do(A=a) (A=a) says that A is no longer computed by its ordinary mechanism: it is supplied by the experimenter and held at a. A formal semantics should identify the resulting model and explain how it behaves. Zhang conjectured that deleting incoming arrows and replacing mechanisms by constants are equivalent views of intervention [6, Sec. 6.4]. The word “equivalent” needs to be made precise. Graph surgery and mechanism replacement are not literally the same operation: they act on different objects and, more importantly, graph surgery cannot distinguish do(A=0) (A=0) from do(A=1) (A=1). A natural comparison is between the dependencies that remain. We formulate that comparison and prove it for deterministic acyclic structural causal models with finitely many endogenous variables. Our starting point is a causal model M≔(G,F)M (G,F) with two components. The directed acyclic graph G describes which variables may directly affect which others, and the mechanism family F says how their values are computed. Compatibility requires every dependency used by F to occur as an arrow of G; it does not require every arrow to be used. We call the model exact when the arrows of G are precisely the dependencies of F. For an exogenous state u, Run(M,u) (M,u) is the unique world generated by the mechanisms. We represent a simultaneous intervention by a type-respecting partial map ι on V, whose domain TιT_ is its target set. On the graph, Surg(G,Tι) (G,T_ ) deletes the arrows entering the targets. In the equations, FιF replaces the corresponding mechanisms with the constants supplied by ι . Our central result says that the same dependency graph is reached in either order: update the mechanisms and then extract their dependencies, or first extract the dependencies and then perform graph surgery. When the supplied graph G is exact, this is also the graph obtained by performing surgery directly on G. Our main results are: 1. an exact correspondence between graph surgery and constant mechanism replacement (Theorem 3.1); 2. a characterization of when this correspondence agrees with the graph supplied as part of a causal model (Corollary 1); 3. a law for combining sequential interventions, including the fact that a later assignment replaces an earlier one (Theorem 4.1); and 4. an ancestor theorem: the value of a set of variables depends only on the part of the intervention applied to their actual dependency ancestors (Theorem 5.1). 2 Structural causal models Let V be a finite set of endogenous variables. Each v∈Vv∈ V has a nonempty value set vX_v. Let ≔∏v∈VvX _v∈ VX_v be the set of complete assignments, which we call worlds. For S⊆VS V, write xSx_S for the restriction of a world x∈x to S. Let U be a nonempty set of exogenous states. An element u∈u may collect local disturbances, shared background factors, or any other information fixed outside the endogenous equations. No probability law is needed. A mechanism family on V is a collection of functions Fv:×⟶v(v∈V).F_v:U×X _v (v∈ V). We give every mechanism the common domain ×U×X deliberately. This avoids building an a priori parent set into the type of FvF_v and lets the dependencies be recovered from the functions themselves: a coordinate that FvF_v ignores contributes no arrow. Compatibility will require every coordinate that can affect FvF_v to be permitted by G, while acyclicity will make the resulting equations evaluable in topological order. Definition 1 (Dependency graph) A mechanism FvF_v depends on w∈Vw∈ V if changing only w can change the value returned by FvF_v. That is, there are u∈u and worlds x,y∈x,y that agree at every variable except possibly w, but for which Fv(u,x)≠Fv(u,y)F_v(u,x)≠ F_v(u,y). The dependency graph of F, written Graph(F) (F), has vertex set V and an arrow w→vw→ v exactly when FvF_v depends on w. Thus the graph records actual rather than merely permitted dependencies. Definition 2 (Causal model) A deterministic acyclic structural causal model is a pair M≔(G,F)M (G,F), where G is a directed acyclic graph and F is a mechanism family compatible with it: every arrow of Graph(F) (F) is also an arrow of G. A variable w is a parent of v when G has an arrow w→vw→ v. The model is exact when G=Graph(F)G= (F). Compatibility gives the graph and mechanisms distinct roles. The graph says which dependencies are permitted; the mechanisms determine which of them are used in a particular model. For example, G may contain w→vw→ v even when FvF_v ignores w; such a model is compatible but not exact. Although FvF_v is written with a whole world as input, compatibility ensures that its value depends only on the parents of v. Lemma 1 (Only parents matter) If M=(G,F)M=(G,F) is a causal model and two worlds x,y∈x,y agree on every parent of v, then Fv(u,x)=Fv(u,y)F_v(u,x)=F_v(u,y) for every u∈u . Proof The set V is finite. Pass from x to y by changing one variable at a time. Only nonparents need to be changed. If w is not a parent of v, compatibility implies that w→vw→ v is not an arrow of Graph(F) (F). By Definition 1, changing w alone therefore leaves the value returned by FvF_v unchanged. Lemma 2 (Unique evaluation) For every causal model M=(G,F)M=(G,F) and exogenous state u∈u , there is exactly one world x∈x satisfying xv=Fv(u,x)(v∈V).x_v=F_v(u,x) (v∈ V). Proof Order the variables as v1,…,vnv_1,…,v_n so that every parent comes before its children. Construct a world in that order. At step k, fill the unassigned coordinates arbitrarily and evaluate FvkF_v_k. Its parents already have values, so Lemma 1 makes the result independent of those temporary choices. Use it as xvkx_v_k. The completed world satisfies every equation. If x and y both satisfy the equations, induction along the same order shows that they agree. Indeed, they agree at the parents of vkv_k, so Lemma 1 gives Fvk(u,x)=Fvk(u,y)F_v_k(u,x)=F_v_k(u,y), and hence xvk=yvkx_v_k=y_v_k. Definition 3 (Run) For a model M=(G,F)M=(G,F) and exogenous state u∈u , define Run(M,u) (M,u) to be the unique world x∈x such that xv=Fv(u,x)for every v∈V.x_v=F_v(u,x) every v∈ V. 3 The do -operator An intervention supplies values at some variables and leaves all others unspecified. We represent it by listing values only for the variables it targets. Definition 4 (Intervention) An intervention ι is a type-respecting partial map on V. Its domain Tι≔dom(ι)⊆VT_ ( ) V is the target set, and ι(v)∈v (v) _v for every v∈Tιv∈ T_ . We write ιv≔ι(v) _v (v). The empty intervention is the empty map, written ∅ . For S⊆VS V, ι|S |_S denotes the ordinary restriction of ι to S. When Tι=AT_ =\A\ and ιA=a _A=a, we write the intervention as do(A=a) (A=a). Definition 5 (Graph surgery) For a directed graph G on V and a target set T⊆VT V, Surg(G,T) (G,T) has the same vertices as G and deletes exactly the arrows entering vertices in T. Graph surgery depends only on the target set and does not record the values imposed there. Those values enter through the following change to the mechanisms. Definition 6 (Mechanism replacement) For a mechanism family F on V and intervention ι , define FιF by Fvι(u,x)≔ιv,v∈Tι,Fv(u,x),v∉Tι.F _v(u,x) cases _v,&v∈ T_ ,\\ F_v(u,x),&v∉ T_ . cases Example 1 (A three-variable intervention) Let V≔A,B,CV \A,B,C\, let every endogenous value set be ℝR, and let ≔ℝ2U ^2. For u=(uA,uB)u=(u_A,u_B), define FA(u,x)≔uA,FB(u,x)≔xA+uB,FC(u,x)≔2xB.F_A(u,x) u_A, F_B(u,x) x_A+u_B, F_C(u,x) 2x_B. Thus Graph(F) (F) is the chain A⟶B⟶C.A B C. If ι≔do(B=7) (B=7), then FBιF _B is the constant 77, while the other two mechanisms are unchanged. Hence Graph(Fι) (F ) consists only of B→CB→ C, exactly the graph obtained by deleting the arrow entering B. The updated equations have the unique solution (A,B,C)=(uA,7,14).(A,B,C)=(u_A,7,14). Theorem 3.1 (Graph–mechanism correspondence) For every mechanism family F on V and intervention ι , Graph(Fι)=Surg(Graph(F),Tι). (F )= ( (F),T_ ). Proof Fix two variables w,v∈Vw,v∈ V. If v is a target, then FvιF _v is constant, so no arrow enters v in Graph(Fι) (F ); graph surgery likewise deletes every arrow entering v. If v is not a target, then Fvι=FvF _v=F_v, so w→vw→ v is an arrow of Graph(Fι) (F ) exactly when it is an arrow of Graph(F) (F); graph surgery leaves all such arrows unchanged. The two graphs therefore have the same arrows. The identity compares the graphical and functional descriptions at the level of dependencies. A separate question is whether surgery on a graph G supplied with the model gives that same graph. Corollary 1 (Agreement with the supplied graph) Let M=(G,F)M=(G,F) be a causal model and let ι be an intervention. Then FιF is compatible with Surg(G,Tι) (G,T_ ). Moreover, Graph(Fι)=Surg(G,Tι) (F )= (G,T_ ) if and only if every arrow of G that is absent from Graph(F) (F) enters an intervention target. Consequently, the equality holds for every intervention if and only if M is exact. Proof Compatibility says that Graph(F) (F) is a subgraph of G. Applying the same surgery to both graphs preserves this relation, and Theorem 3.1 identifies the smaller graph with Graph(Fι) (F ). This proves compatibility after intervention. The two surgically modified graphs are equal exactly when no extra arrow survives. An arrow survives surgery exactly when it does not enter a target. Thus equality holds exactly when every arrow of G absent from Graph(F) (F) enters a target. The uniform statement follows: exact models have no extra arrows, while equality for the empty intervention gives Graph(F)=G (F)=G. Example 2 (Why the supplied graph may differ) Let V≔A,BV \A,B\, let the only arrow of G be A→BA→ B, and suppose neither mechanism depends on an endogenous variable. Then Graph(F) (F) has no arrows, so (G,F)(G,F) is compatible but not exact. An intervention that does not target B leaves A→BA→ B in Surg(G,Tι) (G,T_ ), whereas Graph(Fι) (F ) has no arrows. If the intervention targets B, both graphs have no arrows and therefore agree. Thus exactness is sufficient for agreement under every intervention, but it is not necessary for agreement under a particular one. Having related the two separate edits, we now package their results as a complete intervened model. Definition 7 (Do-operation) For a causal model M=(G,F)M=(G,F) and intervention ι , define Do(M,ι)≔(Surg(G,Tι),Fι). (M, ) ( (G,T_ ),F ). This pair is a causal model: deleting arrows preserves acyclicity, and Corollary 1 supplies compatibility. The do-operation applies one edit to each component of the model. An alternative construction first replaces the mechanisms and then equips them with their exact dependency graph, giving (Graph(Fι),Fι) ( (F ),F ). Corollary 2 (Agreement of the two constructions) For every causal model M=(G,F)M=(G,F) and intervention ι , the pair (Graph(Fι),Fι) ( (F ),F ) is an exact causal model. For every exogenous state u, Run(Do(M,ι),u)=Run((Graph(Fι),Fι),u). ( (M, ),u)= (( (F ),F ),u ). If M is exact, the stronger model equality also holds: Do(M,ι)=(Graph(Fι),Fι). (M, )= ( (F ),F ). Proof Corollary 1 says that Graph(Fι) (F ) is a subgraph of the acyclic graph Surg(G,Tι) (G,T_ ), so it is acyclic. The displayed pair is therefore a causal model, and it is exact by construction. Both models use the mechanism family FιF , which determines their runs. If M is exact, Corollary 1 also gives Surg(G,Tι)=Graph(Fι) (G,T_ )= (F ), so the graphs, and hence the models, are equal. FιF Graph(F) (F)Graph(Fι) (F )replace target mechanismsextract dependenciesextract dependenciessurgery at TιT_ Figure 1: The correspondence of Theorem 3.1. Replacing target mechanisms and extracting dependencies yields the same graph as extracting dependencies first and then performing surgery. The intervened outcome is characterized directly by the following equations. Corollary 3 (Intervention equation) For every model M=(G,F)M=(G,F), intervention ι , exogenous state u∈u , and world x∈x , x=Run(Do(M,ι),u)⟺xv=ιv,v∈Tι,xv=Fv(u,x),v∉Tι.x= ( (M, ),u) casesx_v= _v,&v∈ T_ ,\\ x_v=F_v(u,x),&v∉ T_ . cases Proof By Definition 3, x is the run exactly when xv=Fvι(u,x)x_v=F _v(u,x) for every v. At a target, this says xv=ιvx_v= _v; at every other variable, it says xv=Fv(u,x)x_v=F_v(u,x). These are precisely the two displayed conditions. The corollary gives the complete test for an intervened outcome: each target has its assigned value, and every equation outside the target set remains unchanged. Because G is acyclic, these conditions determine exactly one world. 4 Sequential interventions Suppose ι is applied first and κ second. If both assign a value to the same variable, the later value from κ must prevail. Theorem 4.1 (Sequential interventions) For interventions ι and κ, define λ to be the partial map with domain Tι∪TκT_ ∪ T_κ that agrees with κ wherever κ is defined and otherwise with ι . Then, for every model M, Do(Do(M,ι),κ)=Do(M,λ). ( (M, ),κ )= (M,λ). Proof On both sides, the graph is obtained from G by deleting the arrows entering every variable targeted by either intervention. At a target of κ, the mechanism is the constant κv _v. At a target of ι but not κ, the constant ιv _v remains. Every other mechanism is FvF_v. Thus both the graphs and the mechanism families are equal. Corollary 4 (Basic intervention laws) For every model M and interventions ι,κ ,κ: 1. The empty intervention does nothing: Do(M,∅)=M (M, )=M. 2. Repeating an intervention changes nothing: Do(Do(M,ι),ι)=Do(M,ι) ( (M, ), )= (M, ). 3. Interventions with no common target may be applied in either order: Do(Do(M,ι),κ)=Do(Do(M,κ),ι). ( (M, ),κ)= ( (M,κ), ). 4. If both interventions target v, the later value wins: the mechanism at v in Do(Do(M,ι),κ) ( (M, ),κ) is the constant κv _v. Proof The first statement follows directly from Definition 7, since surgery with an empty target set leaves G unchanged and F∅=F =F. The remaining statements follow from Theorem 4.1 by checking the value retained at each target. For three or more interventions, the placement of parentheses does not matter: applying any finite sequence gives the same model as one intervention that collects all targets and keeps the last value assigned to each one. This is equality of the resulting models, not merely of their runs. 5 Dependence on ancestors For an outcome set O⊆VO V, write AnF(O) _F(O) for the variables in O and every variable from which a directed path in the actual dependency graph Graph(F) (F) reaches a variable in O. If v∈AnF(O)v∈ _F(O), then every parent of v in Graph(F) (F) also lies in AnF(O) _F(O). Consequently, the equation for any variable in this set depends only on variables in the same set. PPBBAAYYDDWW× × × AnF(Y) _F(\Y\)do(D=d) (D=d) Figure 2: The outcome at Y is determined inside its ancestor set. The dashed, crossed arrows are removed by do(D=d) (D=d); intervening on the downstream variable D cannot change Y. Theorem 5.1 (Dependence on ancestors) Let M=(G,F)M=(G,F) be a causal model and let O⊆VO V. If two interventions ι and κ agree on AnF(O) _F(O), so that ι|AnF(O)=κ|AnF(O) |_ _F(O)=κ|_ _F(O), then for every u∈u , Run(Do(M,ι),u)O=Run(Do(M,κ),u)O. ( (M, ),u)_O= ( (M,κ),u)_O. Proof Order the variables topologically in Graph(F) (F). We show by induction along this order that the two runs agree at every v∈AnF(O)v∈ _F(O). If v is targeted by either intervention, then the assumption says it is targeted by both with the same value. The two runs agree at v. Otherwise both runs use the original mechanism FvF_v. By the definition of AnF(O) _F(O), every parent of v in Graph(F) (F) lies in AnF(O) _F(O), and all such parents precede v. The induction hypothesis gives equal values at these parents. Since (Graph(F),F)( (F),F) is an exact causal model, Lemma 1 applied to that model gives equal values at v. Thus the runs agree throughout AnF(O) _F(O), and in particular on O⊆AnF(O)O _F(O). Corollary 5 (Discarding targets outside the ancestors) For every model M=(G,F)M=(G,F), outcome set O⊆VO V, intervention ι , and exogenous state u∈u , Run(Do(M,ι),u)O=Run(Do(M,ι|AnF(O)),u)O. ( (M, ),u)_O= ( (M, |_ _F(O)),u )_O. In particular, if ι has no target in AnF(O) _F(O), then Run(Do(M,ι),u)O=Run(M,u)O. ( (M, ),u)_O= (M,u)_O. Proof The interventions ι and ι|AnF(O) |_ _F(O) agree on AnF(O) _F(O). Apply Theorem 5.1. If ι has no target in AnF(O) _F(O), then ι|AnF(O)=∅ |_ _F(O)= , and the second equality follows from the first law in Corollary 4. Thus, to determine the outcome on O, one may discard all intervention targets outside AnF(O) _F(O). The condition is sufficient, not necessary. Cancellation can make interventions on an actual ancestor irrelevant to an outcome. Take V=A,B,YV=\A,B,Y\ and =A=B=Y=0,1U=X_A=X_B=X_Y=\0,1\, and define FA(u,x)=uF_A(u,x)=u, FB(u,x)=xAF_B(u,x)=x_A, and FY(u,x)=xA⊕xBF_Y(u,x)=x_A x_B. The model (Graph(F),F)( (F),F) is exact and A is an ancestor of Y, but under do(A=a) (A=a) we have B=aB=a and hence Y=a⊕a=0Y=a a=0. Thus do(A=0) (A=0) and do(A=1) (A=1) disagree on an ancestor while producing the same value of Y. 6 Related work The do -operator is central to Pearl’s account of structural causal models [4]. In the usual structural-equation account, an intervention replaces selected equations by assigned values; deleting their incoming arrows is the corresponding graphical operation. Peters, Janzing, and Schölkopf give a modern treatment of functional models, interventions, and causal graphs [5], while Halpern gives axioms for reasoning with interventions in recursive models [1]. String-diagram accounts give explicit graphical languages for causal models. Jacobs, Kissinger, and Zanasi make the syntax–semantics separation formal: string diagrams are interpreted as stochastic matrices, and intervention is an operation on the diagrammatic syntax [2]. Lorenz and Tull develop the approach for a broader class of causal models [3]. Our result addresses a different, narrower question for ordinary deterministic structural causal models: how extensional dependencies change under constant mechanism replacement, including when a graph supplied with the mechanisms contains unused arrows. Recent work uses mechanism functions to explain d-separation semantically [7]. Zhang’s earlier thesis describes incoming-edge deletion as the syntactic view of an intervention, constant replacement as its semantic view, and conjectures that the two are equivalent, with a formal proof in Coq proposed as the next step [6, Sec. 6.4]. Theorem 3.1 gives the conjecture a dependency-level formulation suitable for mechanization. The same formulation distinguishes the dependency graph from a compatible supplied graph, which may contain unused arrows. Corollary 1 characterizes exactly when surgery on the two graphs agrees. 7 Conclusion Graph surgery and constant mechanism replacement agree after dependency extraction: Graph(Fι)=Surg(Graph(F),Tι). (F )= ( (F),T_ ). For a graph supplied with the model, the analogous equality holds exactly when surgery removes all of its unused arrows; it therefore holds for every intervention if and only if the starting model is exact. The construction based on the supplied graph and the one based on the exact dependency graph always have the same run; for an exact starting model, they are the same intervened model. The intervention equation characterizes the resulting outcome. Sequential interventions combine by retaining the last value assigned to each target, and an outcome depends only on interventions at its actual dependency ancestors. Together these results specify the do -operator directly while keeping its structural and functional components distinct. Acknowledgements. This work was supported by the Anusandhan National Research Foundation (ANRF), Government of India, under the Prime Minister Early Career Research Grant ANRF/ECRG/2025/001136/ENS. I am grateful to Aalok Thakkar for helpful discussions. References [1] Halpern, J.Y.: Axiomatizing causal reasoning. Journal of Artificial Intelligence Research 12, 317–337 (2000). https://doi.org/10.1613/jair.648 [2] Jacobs, B., Kissinger, A., Zanasi, F.: Causal inference via string diagram surgery: A diagrammatic approach to interventions and counterfactuals. Mathematical Structures in Computer Science 31(5), 553–574 (2021). https://doi.org/10.1017/S096012952100027X [3] Lorenz, R., Tull, S.: Causal models in string diagrams (2023). https://doi.org/10.48550/arXiv.2304.07638, arXiv:2304.07638 [4] Pearl, J.: Causality: Models, Reasoning, and Inference. Cambridge University Press, Cambridge, UK, 2 edn. (2009). https://doi.org/10.1017/CBO9780511803161 [5] Peters, J., Janzing, D., Schölkopf, B.: Elements of Causal Inference: Foundations and Learning Algorithms. MIT Press, Cambridge, MA (2017) [6] Zhang, A.: Formalizing Causal Models Through the Semantics of Conditional Independence. Master of engineering thesis, Massachusetts Institute of Technology, Cambridge, MA (May 2025), https://adam.chlipala.net/theses/azhang03.pdf [7] Zhang, A., Luo, Q., Bielicke, L., Jun, E., Chlipala, A.: Causality and semantic separation. Proceedings of the ACM on Programming Languages 10(PLDI) (2026). https://doi.org/10.1145/3808274, arXiv:2604.22041