Tri-abduction

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

Where bi-abduction stops

Bi-abduction infers the frame and anti-frame for a single execution path. A function reads some keys and 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 it leaves a crack. Think about making your morning drink. Want coffee, and you need beans and the grinder. Want tea, and you need a teabag and the kettle. Ask what the kitchen must have stocked before you can make your drink, and there is no single answer. It forks on which one you choose. Each needs different things, and the choice between them is the structure that matters.

The same fork, drawn out:

Read it as two analyses side by side. On the coffee branch, bi-abduction infers that beans must be stocked and that the teabag is left untouched. On the tea branch, it infers the teabag and leaves the beans alone. Two clean answers, one per branch, each correct on its own.

Which one does the kitchen actually need stocked? Both? Neither? It depends on which branch runs, which depends on the order. 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.

Mechanic, forked

Return to the engine. The complaint is an intermittent stall, but right now it idles fine. Two wiring connectors on the engine harness are suspect. From the same running state, the mechanic runs a wiggle test, working each connector by hand in turn:

Branch A: Wiggle connector A. The engine stalls.

Branch B: Wiggle connector B. The engine keeps running.

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

The diagnostic power is in the comparison between branches. Wiggling connector A caused a stall. Wiggling connector B did not. The engine was running in both cases before the wiggle. The shared ground (fuel, spark, the rest of the harness) was identical across both branches. The only difference is which connector was wiggled. The divergent outcomes (stall vs. no stall) localize the cause to connector A, the loose connection, not connector B.

This is the causal edge: what explains why two experiments from the same starting state produced different results. The branching condition (which connector was wiggled) 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 wiggles connector A; engine stalls. Branch B wiggles connector B; engine keeps running. The two outcomes converge into the causal edge: connector A, the loose connection, is the candidate cause. Only its perturbation changed the outcome. The shared ground (fuel, spark, the rest of the harness) rules out confounders.

Each step adds an operand

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

Diff answers: "what changed?" Bi-abduction answers: "what changed, and what must have been true for it to work?" 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

Abduction is the third mode of reasoning, distinct from deduction and induction: generating hypotheses from surprising observations. Diff is the primitive; bi-abduction automates it, inferring 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 connector A might be the problem. Causal inference says connector A is the problem, because wiggling it changed the outcome and wiggling connector B 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",
    "connector_a":  "settled",
    "connector_b":  "settled",
    "battery":      "12.6V",
    "fuel_pump":    "on",
    "spark":        "firing",
}

# Branch A: wiggle connector A -> engine stalls
branch_a_end = {
    "engine":       "stalled",
    "connector_a":  "wiggled",
    "connector_b":  "settled",
    "battery":      "12.6V",
    "fuel_pump":    "on",
    "spark":        "firing",
}

# Branch B: wiggle connector B -> engine keeps running
branch_b_end = {
    "engine":       "running",
    "connector_a":  "settled",
    "connector_b":  "wiggled",
    "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"    connector A wiggle -> stalled")
print(f"    connector B wiggle -> nominal")
print(f"    => connector A is causal, connector B 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 (connector_a, connector_b, engine) are the figure. Within the figure, the code identifies which perturbation (connector A vs. connector B) correlates with the outcome change (stalled vs. running).

Bi-abduction on branch A alone says: "connector A was wiggled and the engine stalled." True, but not causal. It could be coincidence. Tri-abduction adds the counterfactual: "connector B was wiggled 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.

Too many branches to test

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: wiggle connector A, wiggle connector B. A real harness has dozens of connectors to wiggle. 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 translates observations into hypotheses. It does not rank them. Each step so far produced a single candidate explanation at its own 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.

Sources