Interventions at the Cut

15.1 What is being built, and why here

A program in rho with graded where-clauses over \(\Rnn\) already carries a causal model. The likelihood of a causal history is a product over firing sites of a locally normalized factor (Theorem 26.1 will take its derivative); each site’s factor is its clause; each site’s parents are the data its pattern and clause read; and the resolver that settles its race is the exogenous noise. This chapter makes the model explicit and adds the one thing Pearl’s calculus of causation has that the clause language lacked: an operator that intervenes. It follows the working note in which the construction was first set out [287].

The operator is a scoped decoration on parallel composition, \[\dok(\,y_1 \models \varphi_1 \ \&\ \cdots\ \&\ y_n \models \varphi_n\,)\ \ink\ P ,\] read as: whenever a race for the binding of \(y_i\) arises inside \(P\), resolve it among the candidates satisfying \(\varphi_i\), with the site’s own weights restricted to that set. It is placed at the cut because an aperture is a property of the cut and of neither agent flanking it (Remark 14.7), and because whether a particular cut will ever occur is undecidable even in the sequential fragment, so an intervention cannot be a surgery on a known node and must be a policy conditional on an event. The construct lowers into the where-clause by the normal-form theorem (Theorem 14.4), so it is a conservative extension, and it sits beside the cost membrane of Chapter 16 as a second index on a polymorphic cut.

With it, Pearl’s causal Bayesian networks over finite domains embed exactly: a variable is a join on its parents’ channels together with an ancilla race over its domain, the conditional probability table is the clause in disjunctive normal form, and the truncated factorization is the likelihood of a causal history. Intervening on the ancilla binding deletes the incoming edges on the nose, the three rules of the do-calculus are theorems about the embedded fragment rather than axioms, and counterfactuals are replay from a recorded pre-state under the intervention.

The chapter sits here, directly after Chapter 14, because it is the first thing one builds with a graded clause that one could not have built with a weight map, and because two parts of the book downstream need it: the mortal scientist of Chapter 26, whose hypotheses become rung-two objects once they can be placed under a \(\dok\) (§15.8), and the Prestige’s argument that a proof system or a learner that cannot inhabit a race cannot do what evolved intelligence does — for which this construct is the constructive content. Pearl himself has not appeared in this book before now, so the ladder is introduced before it is climbed.

15.2 Three rungs

Pearl’s ladder of causation [282] has three rungs, and a learner’s power is where it stands on it. Association: what one can learn from a record of what happened — \(\Pr(y \mid x)\), the distribution of completed runs. Intervention: what one can learn by acting — \(\Pr(y \mid \dok(x))\), the distribution when \(X\) is set to \(x\) rather than observed to be \(x\). Counterfactual: what would have happened in the run that actually occurred, had \(X\) been otherwise — \(Y_x(u)\), with \(u\) the particular draw of everything the model does not explain. Each rung is strictly stronger than the one below, in the sense that there are pairs of models agreeing at one rung and disagreeing at the next.

A structural causal model refines this by writing each \(V_i = f_i(\mathrm{PA}_i, U_i)\) with \(U_i\) independent exogenous variables; a CBN is a structural model with the \(U_i\) marginalized, and §15.5.3 recovers the \(U_i\) as the record of the resolver’s draws.

The reader who has followed the book this far will notice that the ladder is a statement about time. Association is what a trace shows; a trace is linear time. Intervention is what an experimenter who supplies contexts can learn; that is branching time, and context-labeled bisimulation is its equivalence. Counterfactual is replay with the record held. The alignment is made exact below, and it is the reason this chapter is in the Machinery part and not in a chapter on statistics.

15.3 Interventions have one carrier

Before adding syntax it is worth settling what an intervention can touch, since the answer constrains the syntax.

To intervene at a deterministic site one must change the fibre — inject a datum or delete one — and the moment a datum is injected the site has two candidates and is a race. The carrier of intervention is therefore the candidate set at a receipt, and a nontrivial intervention exists exactly where that set has, or is given, more than one element.

So over \(\Rnn\) a hard intervention requires access to the clause: one must be able to write at the site, not merely around it. This is the observation/intervention gap in its sharpest form — what a context can do is observe and perturb; what an owner of the code can do is set — and it is why the construct below is a decoration the programmer writes rather than a context one composes. One qualification: the clause controls which candidate fires and not when. An intervention on timing is outside the clause, and outside this chapter, unless time is reified as data — at which point it is a race again.

15.4 The construct: a decorated cut

There is always a node in the syntax tree above a race, and it is a parallel composition: a race needs a receiver and at least two things it could meet. The cost membrane of Chapter 16 already made the cut polymorphic, indexing it by seals; an intervention is a second index on the same operator. And it cannot be anything more specific than a scoped decoration, for a halting reason: whether a particular cut will ever occur is undecidable, already in the sequential fragment, since “this receipt fires” is a nontrivial reachability property. So an intervention cannot be a surgery on a node known in advance. It is a policy conditional on an event — if a race for this binding arises, resolve it thus — vacuous if the race never arises. Pearl’s nearest object is a dynamic treatment regime rather than an atomic \(\dok\).

do( y = Q2 ) in { x!( Q1 ) | for( y <- x )P | x!( Q2 ) }

do( y1 |= phi1 & y2 |= phi2 ) in { P1 | P2 | P3 }

The gap between the two semantics is exactly the dynamic scope that reflection introduces: received code is the one route by which an unlisted binder — and, in the causal reading, an unlisted parent — enters. We take the membrane as the definition and the lowering as the optimization.

So several interventions compress into one expression for the reason weight maps have a normal form: a formula has one value. The \(\dok\) is a scoped weight map placed at the cut, and the normal-form theorem is what makes it a conservative extension. It is also, in the vocabulary Chapter 26 will use, the operator that takes a specification — the \(\nu\)-property “every binding of \(y\) satisfies \(\varphi\)”, which one would check — and installs it in guard position at every site in scope, including sites not yet visible.

15.5 The embedding of Pearl’s calculus

15.5.1 The variable gadget

For a variable \(V_i\) with children \(V_{j_1},\dots,V_{j_k}\), allocate fresh channels \(v_i^{(j_1)},\dots,v_i^{(j_k)}\), one per child, and a readout channel \(v_i^{\circ}\); emitting \(V_i\)’s value \(d\) is \(v_i^{(j_1)}!(d) \mid \cdots \mid v_i^{(j_k)}!(d) \mid v_i^{\circ}!(d)\).

new wi in {
    wi!(d1) | ... | wi!(ds)
  | for( p1 <- vp1_i & ... & pm <- vpm_i
       & u1 <- wi & ... & us <- wi
         where  [ *p1 = pa1 and ... and *pm = pam and *u1 = v ] * P_i(v | pa)
              + ...   // one summand per (pa, v) in the table
       )
    { emit_i( *u1 ) }
}

The join consumes all \(s\) ancilla messages, so there is no residual on \(w_i\) and no which-path record; the candidates are the \(s!\) bijections from \(u_1,\dots,u_s\) to \(D_i\), and the continuation mentions only \(u_1\), so the \(s!\) candidates fall into \(s\) outcome classes of \((s-1)!\) each. The clause is constant on each class. Under normalization within the contention component the \((s-1)!\) multiplicity cancels, and the probability that the gadget emits \(v\) given parent data \(\mathit{pa}\) is \(P_i(v \mid \mathit{pa})\).

The truncated-factorization form is not imposed on the semantics; it is the semantics. The staging that makes each gadget its own contention component is the condition under which local probabilistic choice composes to a global measure at all [285].

15.5.2 Surgery

The theorem is the reason to address the ancilla binding. Restricting a parent pattern instead would select on inputs — a conditioning — not sever a mechanism. The embedding fixes that the value of a variable is carried by its ancilla binding, and that is the whole of what makes the surgery exact: the gadget’s own gate is \(\top\), so restriction and override coincide, and the weights that encoded the mechanism are the thing normalization discards.

The content of the corollary is not that the rules are true — Pearl proved that — but that the object they are stated for is literally present in the semantics, so that nothing is being modeled. The d-separation premises are statements about \(G\), and \(G\) is the causal order of the staged term; whether they are expressible as crisp-sort formulae over \(\sem{M}\), and so dischargeable by the same checker that discharges everything else, is the first of the open items in §15.9.

15.5.3 Counterfactuals

Pearl’s third rung asks what \(Y\) would have been had \(X\) been \(x\), in the world that actually occurred. In a structural model this is abduction (infer \(U\) from the evidence), action (mutilate), prediction (compute).

The “otherwise sample” clause is where the general case lives: off the staged fragment an intervention can change what rests on a channel and thereby which candidates exist, and “the same draw” is no longer well defined. That the record of a run suffices for its counterfactuals is also the sense in which the history monad of Chapter 13 was always the third rung waiting to be read as one: \(\Hist\) records; replay under a \(\dok\) is the use of the record.

15.5.4 The dictionary

Table 15.1 collects the correspondence. Two entries deserve a word. Set-valued and graded constraints — \(\dok(y \in S)\) with \(|S| \geq 2\), or \(\dok(y \models \psi)\) with \(\psi\) graded — are not Pearl’s atomic \(\dok\) but the \(\sigma\)-interventions of Correa and Bareinboim [283], which replace a mechanism by an arbitrary new one and state their rules on the graph whose incoming edges at \(X\) are those of the new mechanism. Here the construct is natively a \(\sigma\)-intervention, and the new mechanism’s parent set is read off the free names of the constraint: a \(\dok\) whose constraint reads other variables is a policy, and its parents are written in the formula. The induced graph is syntactic, for the intervention as for the model. Conditioning is post-selection on histories, which costs \(1/\Pr(x)\) retries; the chapter on the complex instance met the same quantity as the price of a herald, and the ledger charges it the same way.

15.6 What it costs, and the fragment that tames it

The membrane semantics is simple to state and expensive to run, and the expense has three independent sources. The constraint language can contain modalities and fixed points, which cost what Chapter 14 said they cost: a clause that looks at successors is not local. The scope can be dynamic through reflection, in which case the \(\dok\) is a run-time membrane and not a rewrite. And restriction changes the normalization of contention components whose enumeration is permanent-shaped (Remark 14.12). A fourth question — whether a given \(\dok\) is vacuous, fatal, or neither — is reachability, hence undecidable in general.

The response is to grade the constraint language into fragments by evaluation cost and to impose type disciplines on the scope, and the disciplines are not new to this book. Staged: every receipt is its own contention component — the quantum-safe fragment of Chapter 39. Flat: no received code can come to contain a receipt — the hypothesis of Proposition 15.3. Finite-domain: channel types with finitely many values — what a language definition supplies for free. Confined: a \(\dok\) reaches only code its author has paid to deploy — the seal discipline of Chapter 16.

That four disciplines introduced for four purposes — a quantum state, an exact lowering, a decidable check, an owner’s seal — draw the same line is the best evidence we have that the line is real. Outside it nothing fails; Pearl’s calculus stops and the calculus of this book continues. Off staging, the contention components are the branching cells of a confused event structure [286] and a \(\dok\) that touches one is a restriction of the cell’s distribution; off flatness, a \(\dok\) is a run-time membrane; off finite domains, positivity is a reachability question; off confinement, an intervention on another’s code is a soft intervention by Proposition 15.2 — an experiment rather than a surgery, which is what Chapter 26’s scientist does to its environment all day.

15.7 Execution, briefly

The construct was designed against the execution framework of f1r3node rather than for a simulator, and Part Part II examines that framework in its own right. Four facts are worth recording here so that the reader knows the construct is not only a semantics. Lowering is one more rewrite in the elaboration pass that already normalizes every deployment, and leaves no run-time trace. Off the flat fragment the \(\dok\) is a run-time membrane and the twin of the cost membrane: a scoped decoration on the cut, read off the term by the reducer, altering the COMM rule within; the two commute, since metering does not read the clause and the clause does not read the meter. An intervention is priced as one COMM plus the marginal cost of its conjunct, by Principle 15.1 — though fixing the charge against the ledger is owed (§15.9). And a counterfactual needs a pre-state and a record of fired candidates, which is exactly what a validator that executes a block and records the winners already has; the losing candidates are recomputable from the pre-state, so the same instrumentation that serves counterfactual replay serves the gradient of Theorem 26.1, one number per firing.

One observation from the execution model belongs here as well as in Chapter 25, where it is developed, because it is the dictionary’s last row. A shard in which one node executes and the others replay to confirm the state change is an experimenter/spectator split: the executing node resolves the races and so stands on rung two; the replayers observe and stand on rung one. \(\Pr(y \mid x)\) estimated from the finalized trace is the trace distribution and no more. That a distributed ledger is, by its design, a machine that separates the two rungs is not something its designers set out to build.

15.8 What this does for the scientist

Chapter 26 will build a learner whose hypotheses are graded clauses and whose experiments are guards. Everything it does is, in Pearl’s vocabulary, rung one and a half: it observes, and it perturbs its environment by composing contexts with it, and by Proposition 15.2 a context perturbs without setting. The \(\dok\) is what gives it rung two over the code it owns. A hypothesis is a clause; a clause under a \(\dok\) is a hypothesis together with the experiment that would test it; and — this is the point the reproduction section of that chapter will make exact — a germ carrying both is a hedge that is inherited, since a \(\dok\) is a term and crossover on quoted code applies to it unchanged. The construct of this chapter is what the scientist’s germs were missing in order to be rung-two objects rather than rung-one ones.

The Prestige takes this up as the constructive half of an argument it makes three times: that a system whose witnesses reduce confluently can state a non-confluent phenomenon but cannot inhabit it, so that a proof assistant of the usual kind, and a transformer trained on completed runs, both stand on rung one by construction. Rung two is a graded race under a \(\dok\); rung three is its replay; and the smallest behavior invisible to a trace — Milner’s two vending machines, which agree on every completed run and differ in a refusal — becomes a one-line program that, under \(\dok(y = \mathit{tea})\), either delivers tea or starves. That chapter is where the argument is made. This one is where the thing it leans on is built.

15.9 What is owed

1. d-separation as a behavioral formula. Corollary 15.1 evaluates its premises on \(G\). Since \(G\) is the causal order of the staged term, the premises should be crisp-sort \(\nu\)-properties over \(\sem{M}\) — “no history has a causal path from a \(Z\)-firing to a \(Y\)-firing not passing through \(X\) or \(W\)” — dischargeable by the model checker. Stated, not proved.

2. The rules off the staged fragment. Outside staging the contention components are branching cells and the event structure may be confused. The conjecture is that the \(\sigma\)-calculus rules hold on the confusion-free fragment with d-separation read off the event structure, and on the confused fragment per cell with the cell’s distribution in place of the mechanism.

3. The price of a \(\dok\). Principle 15.1 says an intervention is a COMM. The marginal charge of the constraint conjunct, the budget charge of a modal constraint, and the charge for a counterfactual replay have not been fixed against the ledger of Chapter 16. Until they are, “an intervention costs one token” names an intention.

4. Identifiability across namespaces. Pearl’s question — when is \(\Pr(y \mid \dok(x))\) computable from observational data in the presence of hidden variables — has a sharp rendering: the hidden variables are the code one cannot read, the boundary is the namespace (Chapter 20), and the observational data is the finalized trace. The identification algorithm [284] should transfer to the staged fragment directly; what it says about a shard is the question.

5. Continuous domains and cycles. The gadget enumerates the domain on the ancilla channel; a continuous variable needs an ancilla carried as a density and the normalization become an integral, for which the Gillespie reading of Chapter 14 is the natural home. A recursive term has an acyclic event-level graph and a cyclic variable-level one; the cyclic structural models of the literature and the graded fixed point should meet there, with the budget as the unrolling depth.