2.5 Tracing §2.1: first⟨2,5⟩
The paper’s §2.1 defines first := λp. ∃a b. p=⟨a,b⟩; a and applies it to ⟨2,5⟩, returning the first component.
The headline is APP-BETA: application does not substitute the argument into the body. Instead β-reduction introduces a fresh ∃p and an equation p=⟨2,5⟩ in front of the untouched body — application is call-by-unification. The rest of the trace is unification doing, one explicit step at a time, what substitution would have done. The result is 2.
2.5.1 Step 1 — APP-BETA
APP-BETA introduces a fresh existential for the parameter plus an equation binding it to the argument, both in front of the original body: ∃p. p=⟨2,5⟩; ∃a. ∃b. p=⟨a,b⟩; a. The body is untouched; ⟨2,5⟩ is not copied in. (The model picks the fresh name via variable-not-in; the curated term keeps p, α-equivalent to the model’s choice.)
2.5.2 Step 2 — SUBST
p=⟨2,5⟩ defines p (side conditions hold: p occurs in p=⟨a,b⟩; p ∉ fvs(⟨2,5⟩); the RHS is not a variable). SUBST rewrites the occurrence of p to give ⟨2,5⟩=⟨a,b⟩, keeping the defining equation.
2.5.3 Step 3 — EQN-ELIM
p is now consumed; EQN-ELIM removes p=⟨2,5⟩ and its ∃p binder.
2.5.4 Step 4 — U-TUP
U-TUP decomposes ⟨2,5⟩=⟨a,b⟩ componentwise into 2=a; 5=b.
2.5.5 Step 5 — HNF-SWAP
5=b has a literal on the left and a variable on the right; HNF-SWAP orients it to b=5. (2=a is equally mis-oriented — either swap is legal; the path picks 5=b first.)
2.5.6 Step 6 — EQN-ELIM
b is used nowhere else (the result is a), so EQN-ELIM removes ∃b and b=5 — without the value 5 ever flowing anywhere. Contrast a, whose equation cannot go until its value reaches the result position.
2.5.7 Step 7 — HNF-SWAP
HNF-SWAP flips the remaining 2=a to a=2.
2.5.8 Step 8 — SUBST
a=2 is solved; SUBST propagates 2 into the result position. The equation and ∃a binder remain for now.
2.5.9 Step 9 — EQN-ELIM
a is isolated; EQN-ELIM removes ∃a and a=2, leaving one{2}.
2.5.10 Step 10 — ONE-VALUE
ONE-VALUE unwraps one{2} to 2.
