ch:efficient-unification: ch:efficient-unification

Problem and invariant. Build a terminating first-order worklist solver that returns compact triangular recipes. Every residual equation must be an input equation after the accumulated eliminations, every accepted binding must pass the occurs check, and no variable may acquire two left-hand bindings. Successful output is checked separately against the original equations.

Representation tradeoff. A direct implementation of definition 113.7 would use mutable node identifiers, parent lists, link cursors, and owner fields. The finite companion instead makes the semantic clauses inspectable:

data Term : Type =
    Flex Variable
  | Rigid Symbol (List Term)
data Equation : Type = Equation Term Term
data Binding : Type = Binding Variable Term
data SolveResult : Type =
    Solved (List Binding)
  | Rejected Rejection

Sharing is represented by one named recipe per binding rather than by copying its expansion. This choice exercises compact output and failure boundaries, but it supplies no pointer-machine cost evidence.

Worklist solver. Implement structural equality, the occurs predicate, capture-free first-order replacement, rigid-spine zipping, and equation-list append. On each iteration delete equal endpoints. Orient a flexible endpoint to the left; reject it when it occurs in the right endpoint, otherwise replace it through the remaining worklist and record the binding. For two rigid endpoints, reject unequal symbols or arities and prepend corresponding child equations. A natural fuel decreases on every iteration; the corpus gives a bound above the number of generated equations, and reports exhaustion as a distinct internal rejection.

To validate success, reverse the solver’s newest-first binding list. Apply each binding once, in triangular order, to both sides of every original equation and compare the resulting terms. This checker is independent of the worklist control flow. Count bindings and binary recipes without expanding them. A separate recurrence computes $2^8=256$ for the triangular family’s expected leaf count.

Acceptance cases. Encode the opening shared-variable equation, unequal $F/G$ heads, the direct cycle $x=F(x)$, the three-variable cycle, and the triangular family through index eight. Require the exact transcript below. The fifth logical line is wrapped after its first comma; concatenating the centered fragments recovers the byte-for-byte stdout line.

shared-example=ok:x->G(y),y->G(a)
head-clash=reject:clash
occurs-self=reject:cycle
occurs-three=reject:cycle

All 5 Chapter 113 corpus cases passed.

The last line requires all five Boolean oracles simultaneously. The compact case is accepted only when there are nine bindings including $x_0\mapsto a$, exactly eight binary recipes, and the independent substitution checker validates the original family.

Occurs-check mutation. In the flexible-variable branch of occurs, return False instead of comparing variable identifiers. The source still passes kappa check, and kappa audit still prints []. Both cycle records change to FAIL, so the inline stdout oracle makes kappa test fail. Restore the accepted branch before release. Then replace the expected binary-recipe symbol in triangleRightHandSide. The cycle oracles remain accepted, but the local non-expanding certificate check changes only compact-eight to FAIL. Restore the expected symbol.

Acceptance test. Run the four commands recorded in appendix E. Require a silent check, one passing inline test, the exact six-line transcript, and an empty audit. Replay the mutation, require test failure, restore the source, replay the compact-recipe mutation, require test failure again, restore the source, and repeat all four commands. The accepted source and compiler hashes in Appendix E must equal those in the artifact README and transcript.

Mathematical boundary. The companion implements finite syntactic terms and a compact substitution list. It does not implement the root-class graph state or the Paterson–Wegman scheduling interface. It therefore proves neither theorem 113.6 nor theorem 113.9. Those claims remain the chapter’s mathematical proofs under their explicit graph and pointer-machine hypotheses.