Tri-abduction

Chapter 6 · Zilberstein et al. 2024, Calcagno et al. 2009, O'Hearn 2019

Where bi-abduction stops

Chapter 5 showed how bi-abduction infers the frame and anti-frame for a single execution path. The checkout function reads some keys, writes others; bi-abduction figures out what must exist beforehand and what stays untouched. Each function analyzed in isolation, results composed across the call graph. Polynomial per function, linear composition.

But chapter 5 ended on a crack. Consider a function with an if/else:

def process_payment(state):
    if state["payment_method"] == "credit_card":
        # Branch A: reads card_number, writes authorization_code
        validate(state["card_number"])
        state["authorization_code"] = charge(state["card_number"])
    else:
        # Branch B: reads bank_account, writes transfer_id
        verify(state["bank_account"])
        state["transfer_id"] = transfer(state["bank_account"])

Branch A touches {card_number, authorization_code}. Branch B touches {bank_account, transfer_id}. Run bi-abduction on branch A: the anti-frame says card_number must exist, the frame excludes authorization_code. Run bi-abduction on branch B: the anti-frame says bank_account must exist, the frame excludes transfer_id. Two separate analyses, two separate answers.

Which precondition does the caller need to establish? Both? Neither? It depends on which branch executes, which depends on payment_method. Bi-abduction gives you one (anti-frame, frame) pair per path. It cannot tell you how the paths relate to each other: that the branch condition itself determines the outcome, that the choice between paths is the real structure.

The same limitation shows up everywhere programs fork: if/else, try/catch, pattern matching, concurrent threads racing to a shared resource. Each branch has its own footprint. Bi-abduction analyzes them independently. What's missing is the joint analysis: a single precondition valid for all branches.

Outcome separation logic

Zilberstein, Saliling, and Silva (2024) introduced Outcome Separation Logic at OOPSLA. The key move: extend the separating conjunction from two-part separation (footprint * frame) to n-part separation across outcomes. Where separation logic says "the heap splits into what the function touches and what it doesn't," outcome separation logic says "the heap splits into what each branch touches and what none of them touch." The methodeutic reading below, recasting this as causal inference, is our extrapolation, not theirs.

Bi-abduction solves for two unknowns along one execution path: anti-frame and frame. We use tri-abduction as this book's name for the N=2 outcome-separation case. It solves for three: the precondition before the fork, plus the frame and postcondition for each branch. "Tri" because the minimum branching program has three logical parts: shared prefix, branch A, branch B.

The tri-abduction judgment looks like this:

Given:
  Branch A:  {P_A} C_A {Q_A}
  Branch B:  {P_B} C_B {Q_B}

Find:
  Pre  — a precondition valid for BOTH branches
  F    — a frame untouched by EITHER branch

Such that:
  Pre * F  ⊢  P_A * F_A    (Pre plus frame entails branch A's needs)
  Pre * F  ⊢  P_B * F_B    (Pre plus frame entails branch B's needs)

Where bi-abduction infers one (anti-frame, frame) pair, tri-abduction infers a precondition valid for all branches simultaneously. The frame is the intersection: heap no branch touches. The precondition is the union: everything any branch might need, conditioned on the branching predicate.

The mechanic, forked

Return to the engine. The mechanic starts from the same state: engine running, all gauges nominal. She performs two perturbations:

Branch A: Tap the alternator. Engine stalls.

Branch B: Tap the radiator. Engine keeps running.

Same starting state. Two perturbations. Two outcomes. The unary diff (chapter 4) analyzes each branch in isolation. Branch A's figure: alternator tapped, engine stalled. Branch B's figure: radiator tapped, engine unchanged. Bi-abduction (chapter 5) infers the frame for each branch independently.

The diagnostic power is in the comparison between branches. The alternator tap caused a stall. The radiator tap didn't. The engine was running in both cases before the tap. The shared ground (fuel, spark, wiring, battery) was identical across both branches. The only difference is which component was tapped. The divergent outcomes (stall vs. no stall) localize the cause to the alternator, not the radiator.

This is the causal edge: what explains why two experiments from the same starting state produced different results. The branching condition (which component was tapped) is the candidate cause. The divergent outcomes are the evidence. The shared ground is the control.

The diagram reads left to right. A shared starting state (engine running) forks into two branches. Branch A taps the alternator; engine stalls. Branch B taps the radiator; engine keeps running. The two outcomes converge into the causal edge: the alternator is the candidate cause: only its perturbation changed the outcome. The shared ground (fuel, spark, wiring, battery) rules out confounders.

Each step adds an operand

Chapters 4–6 are a single pattern with increasing arity:

Chapter 4's diff answers: "what changed?" Chapter 5's bi-abduction answers: "what changed, and what must have been true for it to work?" Chapter 6's tri-abduction answers: "what changed, and why did it change here but not there?"

One snapshot pair gives one frame. Two snapshot pairs (actual and counterfactual) give one causal edge. The primitive stays diff; the arity grows. Unary diff partitions state into figure and ground. Bi-abduction infers the partition autonomously. Tri-abduction compares partitions across branches to isolate the cause.

Zilberstein et al. show this generalizes to arbitrary arity. A program with N branches yields N outcomes from one shared starting state. Comparing all N outcomes identifies which branching conditions explain which outcome differences. Tri-abduction is the N=2 case. The general case is outcome separation across N outcomes.

Controlled experiments are tri-abduction

Chapters 1–3 established abduction as the third mode of reasoning, distinct from deduction and induction: generating hypotheses from surprising observations. Chapter 4 defined the primitive: diff. Chapter 5 automated it: bi-abduction infers the frame without the observer choosing what to snapshot.

Tri-abduction adds branching. The question moves from "what explains this observation?" to "what explains why this observation differs from that one?" That is the gap between diagnosis and causal inference. Diagnosis says the alternator might be the problem. Causal inference says the alternator is the problem, because tapping it changed the outcome and tapping the radiator didn't.

The controlled experiment is tri-abduction performed by a human. Hold starting conditions constant. Vary one thing. Observe whether the outcome changes. If it does, the varied thing is a candidate cause, subject to confounding, measurement quality, and power. Mill's method of difference, read through a separation logic lens.

Code: three snapshots find the cause

Given two experimental outcomes from the same starting state with different perturbations, identify the branching condition that explains the divergence.

from dataclasses import dataclass

@dataclass
class CausalEdge:
    """The output of tri-abduction: a branching condition
    that explains why two experiments diverged."""
    condition: str
    branch_a_perturbation: dict
    branch_a_outcome: str
    branch_b_perturbation: dict
    branch_b_outcome: str
    shared_ground: dict


def tri_abduce(shared_start, branch_a_end, branch_b_end):
    """Tri-abduction: given a shared start and two branch endpoints,
    infer the causal edge.

    shared_start:  dict — the state before the fork
    branch_a_end:  dict — the state after branch A
    branch_b_end:  dict — the state after branch B

    Returns a CausalEdge identifying what diverged and what held.
    """
    all_keys = set(shared_start) | set(branch_a_end) | set(branch_b_end)

    # Shared ground: keys unchanged in BOTH branches
    shared_ground = {}
    # Per-branch diffs
    a_changed = {}
    b_changed = {}

    for key in all_keys:
        start_val = shared_start.get(key)
        a_val = branch_a_end.get(key)
        b_val = branch_b_end.get(key)

        if start_val == a_val and start_val == b_val:
            # Unchanged in both branches — ground
            shared_ground[key] = start_val
        else:
            if start_val != a_val:
                a_changed[key] = (start_val, a_val)
            if start_val != b_val:
                b_changed[key] = (start_val, b_val)

    # The causal edge: what changed in A but not B (or vice versa)
    # tells us which perturbation caused the outcome difference.
    a_only = set(a_changed) - set(b_changed)
    b_only = set(b_changed) - set(a_changed)

    # Identify the perturbation (input) vs outcome (output)
    # by checking which changed keys are shared between branches
    perturbation_keys = a_only | b_only

    return CausalEdge(
        condition=f"diverged on: {perturbation_keys}",
        branch_a_perturbation={k: a_changed[k] for k in a_only if k in a_changed},
        branch_a_outcome="stalled" if any("stalled" in str(v) for v in a_changed.values()) else "nominal",
        branch_b_perturbation={k: b_changed[k] for k in b_only if k in b_changed},
        branch_b_outcome="stalled" if any("stalled" in str(v) for v in b_changed.values()) else "nominal",
        shared_ground=shared_ground,
    )


# --- The mechanic: two perturbations from the same start ---

shared_start = {
    "engine":     "running",
    "alternator": "untouched",
    "radiator":   "untouched",
    "battery":    "12.6V",
    "fuel_pump":  "on",
    "spark":      "firing",
}

# Branch A: tap alternator -> engine stalls
branch_a_end = {
    "engine":     "stalled",
    "alternator": "tapped",
    "radiator":   "untouched",
    "battery":    "12.6V",
    "fuel_pump":  "on",
    "spark":      "firing",
}

# Branch B: tap radiator -> engine keeps running
branch_b_end = {
    "engine":     "running",
    "alternator": "untouched",
    "radiator":   "tapped",
    "battery":    "12.6V",
    "fuel_pump":  "on",
    "spark":      "firing",
}

edge = tri_abduce(shared_start, branch_a_end, branch_b_end)

print("Tri-abduction result:")
print(f"  {edge.condition}")
print(f"\n  Branch A: {edge.branch_a_perturbation}")
print(f"    Outcome: {edge.branch_a_outcome}")
print(f"\n  Branch B: {edge.branch_b_perturbation}")
print(f"    Outcome: {edge.branch_b_outcome}")
print(f"\n  Shared ground (control): {list(edge.shared_ground.keys())}")
print(f"\n  Causal conclusion:")
print(f"    alternator perturbation -> stalled")
print(f"    radiator perturbation -> nominal")
print(f"    => alternator is causal, radiator is not")

The function takes three snapshots instead of two. The shared start is the control. The two branch endpoints are the experimental outcomes. The shared ground (battery, fuel pump, spark) is what held across both experiments, ruling out those variables as causes. The divergent keys (alternator, radiator, engine) are the figure. Within the figure, the code identifies which perturbation (alternator vs. radiator) correlates with the outcome change (stalled vs. running).

Bi-abduction on branch A alone says: "the alternator changed and the engine stalled." True, but not causal. It could be coincidence. Tri-abduction adds the counterfactual: "the radiator changed and the engine didn't stall." The comparison between branches supports a causal claim: same starting state, different perturbation, different outcome. Under controlled conditions (no hidden confounding, adequate measurement), the perturbation that changed the outcome is the candidate cause.

Beyond programs: branching in the wild

The fork structure appears everywhere experiments branch:

A/B testing. Randomized comparable populations (shared start), two UI variants (branches), different conversion rates (outcomes). The causal edge is the UI difference explaining the conversion gap. Shared ground: user demographics, time of day, device type.

Compiler optimization. Same source program, two tile sizes in a GPU kernel. One runs in 4ms, the other in 12ms. The causal edge is tile size. Shared ground: instruction count, memory layout, thread count.

Clinical trials. Randomized comparable groups, drug vs. placebo. Different recovery rates. The branching condition is whether the patient received the drug. Shared ground: age, severity, diet, exercise. Randomization makes the shared ground trustworthy.

Every case has the same structure: shared starting conditions, a fork, divergent outcomes, a causal edge extracted from the comparison. The controlled experiment is tri-abduction. Mill described the method of difference in 1843. Outcome separation logic (Zilberstein et al. 2024) offers a formal framework for reasoning about such branching contrasts.

Tri-abduction composes

Bi-abduction's power came from compositionality: analyze each function once, infer its contract, compose contracts across call boundaries. Does tri-abduction compose the same way?

Yes, because outcomes separate. If function A branches internally and function B branches internally, their outcome sets multiply. But the separation guarantee means A's branches don't interfere with B's frame. Zilberstein et al. prove this: outcome separation logic inherits the frame rule from standard separation logic. Local reasoning stays sound across branching boundaries.

The practical consequence: compositional analysis handles nested branching. Function A has an if/else. It calls function B, which also has an if/else. Outcome separation logic analyzes each function independently, infers preconditions valid for all branches, and composes. The same architecture that scaled bi-abduction to millions of lines in Infer scales tri-abduction to branching programs.

What breaks

The arity grows cleanly. N branches from a shared state produce N outcomes; comparing outcomes isolates the causal branching conditions. The primitive scales. Compositionality holds.

But now there is a new problem. The mechanic had two branches: tap alternator, tap radiator. A real engine has dozens of components to tap. A compiler has thousands of configurations. A drug trial has millions of candidate molecules. Each is a potential branch. Each produces a candidate causal edge.

The primitive generates hypotheses. It does not rank them. Chapters 4–6 formalized candidate-explanation machinery at increasing arity: one diff, one frame inference, one causal edge. But N possible perturbations yield N candidate hypotheses. Which ones are worth testing?

Testing is expensive. Every experiment costs time, compute, or reagents. The abductive primitive produces dozens of candidates from a single fork. Running all of them is rarely feasible. We need a theory of which hypotheses to invest in: a theory of the economy of research.

That is Chapter 7.

Sources