THE WARREN ABSTRACT MACHINE — a dart

WARREN ABSTRACT MACHINE Prolog on a machine — unification and backtracking as instructions

The Warren Abstract Machine (WAM) is to Prolog what the stack machine is to C: a compact instruction set a logic program compiles to. Its two exotic operations are unification (make two terms equal by binding variables — f(X,2) and f(3,Y) unify with X=3, Y=2) and backtracking (on failure, undo the bindings and try the next clause, via a trail and choice points). Warren's design made Prolog fast enough to be practical and defined how logic languages are implemented to this day. It is the abstract machine for a paradigm where the runtime searches rather than merely evaluates.

THE TECHNIQUE unify terms by binding variables; backtrack on failure

Unifying f(X, 2) with f(3, Y). The demo binds the variables and reports success and the substitution: live demo

HISTORY & CREDIT David H. D. Warren, 1983

“A machine evaluates; it doesn't search.” — the WAM's instructions unify and backtrack, so its runtime explores a space of solutions, undoing bindings on failure. Search is a first-class execution model, not a library on top of one. cited

1983 · David H. D. Warren — “An Abstract Prolog Instruction Set” (SRI Note 309): the WAM — unification, choice points, the trail.
lineage · unification is Robinson (1965); the WAM made it an instruction set.
now · the basis of essentially every serious Prolog implementation.

Unify to bind, backtrack to undo, and the machine searches a space instead of walking a value. Warren's instruction set is why a declarative language runs at all. Warren 1983

RECOMMEND FOR I-13 unification, computed

On the canonical compiler, unifying f(X,2) with f(3,Y) succeeds (1) with X=3, Y=2 (sum 5):

$ i13 run m_wam.i13 # unify f(X,2) with f(3,Y) RUN OK . 41 step(s) . peak stack 4 . call depth 1 x = 3 y = 2 success = 1

Recommend: the WAM is the farthest machine from i13 in this batch, and instructively so. i13 evaluates, deterministically, in a single forward pass; the WAM searches, with backtracking and mutable bindings it must trail and undo. i13 has no unification, no choice points, no trail — and could not add them without abandoning its single-pass, no-store, no-backtrack identity (a WAM's trail is exactly the mutable store dart 268 showed i13 refuses). The WAM shows what an abstract machine looks like when the paradigm is search; i13's shows what one looks like when the paradigm is a proof that runs straight through.