2.4 Tracing §2.2: residuation
∃x y. y=7; x=add⟨3, y⟩; x |
The call add⟨3,y⟩ is stuck initially: APP-ADD fires only when both arguments are integer literals, and y is still unknown. Functional-logic programs do not evaluate left-to-right; the call residuates — it suspends until unification supplies y=7, after which the arithmetic proceeds.
2.4.1 Step 1 — SUBST
APP-ADD cannot fire while y is unbound, so the productive move is to propagate y=7 into the rest of the sequence (side conditions hold: y occurs later, 7 is not a variable, y ∉ fvs(7)). The suspended call becomes add⟨3,7⟩ — residuation in action.
2.4.2 Step 2 — EQN-ELIM
y now occurs nowhere outside y=7, so EQN-ELIM removes the equation and its ∃y binder.
2.4.3 Step 3 — APP-ADD
Both arguments are now literals, so the call wakes up: add⟨3,7⟩ reduces to 10 (the evaluator’s compatible closure reaches it inside the equation’s RHS). The equation becomes x=10.
2.4.4 Step 4 — SUBST
x=10 is solved; SUBST propagates 10 into the result position. The equation and ∃x binder remain for now.
2.4.5 Step 5 — EQN-ELIM
x is isolated; EQN-ELIM removes ∃x and x=10, leaving one{10}.
2.4.6 Step 6 — ONE-VALUE
ONE-VALUE unwraps one{10} to 10.
