2.7 Tracing §2.6: tuple indexing as choice
Applying a tuple to an argument means indexing: ⟨v0,…,vn⟩(i) looks up position i. With i an unconstrained existential it ranges over every valid index, and under all{…} every result is collected. So all{∃i. ⟨10,27,32⟩(i)} enumerates all three positions and gathers them into a fresh tuple — reconstructing ⟨10,27,32⟩ from the outside in.
This is the richest trace: 11 steps exercising every rule group except failure — APP-TUP, EXI-SWAP, VAR-SWAP, EQN-ELIM, CHOOSE, ALL-CHOICE, and ONE-VALUE. The three-way choice APP-TUP builds (x=0; 10 | x=1; 27 | x=2; 32, right-nested in the model’s choose) recurs through the first four steps; "paths.rkt" names it tup-body.
2.7.1 Step 1 — APP-TUP
APP-TUP turns indexing into choice: it introduces a fresh x equated with the argument, and (via index-choices) a body offering one alternative per index. Here that is x=i; (x=0; 10 | x=1; 27 | x=2; 32); since i is unconstrained, no alternative is ruled out.
2.7.2 Step 2 — EXI-SWAP
To eliminate i, ∃i must sit directly above the equation x=i (an execution context cannot cross a binder). EXI-SWAP permutes ∃i. ∃x. … to ∃x. ∃i. …. This is also the rule that makes greedy tracing loop — two adjacent binders can swap back and forth forever; the path uses it exactly once, on purpose.
2.7.3 Step 3 — VAR-SWAP
EQN-ELIM eliminates ∃y only when the equation has y on the left. The equation is x=i, so VAR-SWAP flips it to i=x. Its side condition uses var< (the model’s approximation of the paper’s "bound inside" order); for plain source names it falls back to lexical order, and i < x.
2.7.4 Step 4 — EQN-ELIM
With i=x under ∃i and i free nowhere else, EQN-ELIM removes the binder and equation together. What remains is ∃x scoping the three-way choice tup-body.
2.7.5 Step 5 — CHOOSE (first)
CHOOSE has the shape SX[CX[e1 | e2]] → SX[CX[e1] | CX[e2]], with SX a scope context (one{…}/all{…}) and CX ≠ ▢ a choice context. Here SX = all{…} and CX = ∃x. ▢, so the rule distributes ∃x over the outermost choose, duplicating the binder: the left split becomes (∃x. x=0; 10) and the right keeps (x=1; 27 | x=2; 32) under its own ∃x.
2.7.6 Step 6 — CHOOSE (second)
CHOOSE distributes once more, splitting the right branch into three independent alternatives, each with its own private x.
2.7.7 Steps 7–9 — EQN-ELIM ×3
In each branch x=k constrains an x absent from the branch’s result (10, 27, 32), so EQN-ELIM removes equation and binder. The path eliminates left to right; any order is valid here, and confluence (cross-checked by run) guarantees the same normal form.
2.7.8 Step 10 — ALL-CHOICE
ALL-CHOICE reifies a right-nested choice of values into a tuple (via flat-choice): all{10 | 27 | 32} reduces to ⟨10, 27, 32⟩. Unlike one, all keeps every solution.
2.7.9 Step 11 — ONE-VALUE
ONE-VALUE unwraps one{⟨10,27,32⟩} to (tup 10 27 32) — the original tuple, rebuilt by enumerating its indices.
