****NOTE: There is a mistake in the Unify pseudo-code on p. 303 in the book. The last line of the algorithm should say 'add{var/x}' rather than 'add{x/var}'. The example below shows a reasonably complicated unification example where this change plays a role.**** Unify ( g(b,b), g(y, g(y,Z)) ) ->Unify-Internal ( g(b,b), g(y, g(y,Z)), {} ) the "compound?" check is the one that gets executed and results in a recursive call to Unify-Internal... -->Unify-Internal ( (b,b), (y, g(y,Z)), Unify-Internal (g, g, {}) ) | |-> this recursive call returns {} since g=g. the "list?" check is the one that gets executed; also first (b,b) = b; rest (b,b) = b and first (y, g(y,Z)) = y; rest (y, g(y,Z)) = g(y,Z) so we get another recursive call to Unify-Internal... --->Unify-Internal ( b, g(y,Z), Unify-Internal (b, y, {}) | |-> this calls Unify-Var (b, y, {}) which returns {{b/y}} (NOT {{y/b}}) as the algorithm without the fix above would produce... now we've got a call to Unify-Var since b is a variable ---->Unify-Var (b, g(y,Z), {{b/y}}) since {b/y} is in the list of existing substitutions, the first "if" statement in Unify-Var is executed, causing yet another call to Unify-Internal... -----> Unify-Internal (y, g(y,Z), {{b/y}}) y is a variable, so we get another call to Unify-Var ------> Unify-Var (y, g(y,Z), {{b/y}}) this time, nothing of the form {y/VAL} is in the list of existing substitutions, so the first "if" statement is not executed; the first else-if clause is also not executed since there is nothing of the form {g(y,Z)/VAL} in the list of substitutions; but the following else-if clause IS executed since y occurs in g(y,Z). so the occurs-check line returns FAILURE <------ FAILURE this is passed all the way back up to the topmost call to Unify and returned.