2.3 Tracing §1: two views of one tuple
The paper’s §1 opening example:
∃x y z. x=⟨y,3⟩; x=⟨2,z⟩; y |
x is described twice — as ⟨y,3⟩ and as ⟨2,z⟩. Unification reconciles the two views, forcing y=2 and z=3; the program returns y, so the answer is 2.
2.3.1 Step 1 — SUBST
x=⟨y,3⟩ defines x, and the SUBST side conditions hold (x occurs outside its equation; x ∉ fvs(⟨y,3⟩); the RHS is not a variable). It rewrites the occurrence of x in the second equation while leaving the defining one in place: the second conjunct becomes ⟨y,3⟩=⟨2,z⟩.
2.3.2 Step 2 — U-TUP
Both sides of ⟨y,3⟩=⟨2,z⟩ are equal-arity tuples, so U-TUP decomposes it componentwise into y=2; 3=z.
2.3.3 Step 3 — HNF-SWAP
3=z has a literal on the left and a variable on the right; HNF-SWAP flips it to z=3 (the model keeps equations variable-first).
2.3.4 Step 4 — EQN-ELIM
z occurs nowhere else, so EQN-ELIM drops z=3 and its ∃z binder together.
2.3.5 Step 5 — SUBST
SUBST fires for y=2, substituting leftward as well: the y inside x=⟨y,3⟩ and the y in result position both become 2. The equation y=2 is kept.
2.3.6 Step 6 — EQN-ELIM
y is now isolated; EQN-ELIM removes ∃y and y=2.
2.3.7 Step 7 — EQN-ELIM
x does not appear in the answer; EQN-ELIM removes ∃x and x=⟨2,3⟩.
2.3.8 Step 8 — ONE-VALUE
ONE-VALUE unwraps one{2} to 2.
2.3.9 Why a curated path?
From t0, EXI-SWAP can permute the adjacent ∃x ∃y ∃z binders endlessly, so a greedy stepper never terminates; SUBST also admits two directions at step 1. Confluence ("test/confluence-test.rkt") guarantees every terminating path agrees on 2, so checking one curated path — re-verified edge by edge against the model — suffices.