The Prolog Language - Thinking as Computation - page 58

3.3.2 Renaming variables

While the unification process is not concerned with where the atoms come from
(query or program) during back-chaining, Prolog nonetheless renames the variables
in a query before attempting unification to ensure that there are no clashes.
Consider, for example, the likes.pl program in figure 3.11 and what happens with
a query such as

likes(X,pizza), \+ X=john.

This works roughly as follows:
1. Work on the atom likes(X,pizza) . First find the clause likes(john,pizza) in

the program (with no body). This eventually fails.

2. After the failure, backtrack and look for other clauses that will unify with

likes(X,pizza) . Find the clause whose head is likes(paul,X) , but this does
not (yet) unify with likes(X,pizza) , since there is no value for X that makes the
two atoms identical.

3. Rename the variable X in the query (in both literals) to a totally new variable,

such as X1 .

4. The atom likes(X1,pizza) now unifies with likes(paul,X) in the program,

and the query eventually succeeds.

This renaming of variables is evident when Prolog is asked to trace its behavior when
establishing a query.

The next section provides a more detailed picture of how back-chaining works in
Prolog on conjunctive queries. Most of the time, an informal description of back-
chaining is sufficient, but sometimes, it is useful to understand in more detail all the
steps involved, to see, for example, how and where backtracking occurs.

3.3.3 Back-chaining revisited

∗

To keep things simple, assume that the conjunctive query consists of atoms only; it is
not hard to extend it to negations and equalities.
Look at the back-chaining procedure in figure 3.12. The main step where all the
action happens in the procedure is step 3d. At that point, a clause of the program has
been found whose head H unifies with the first atom of the query, A 1 . Potentially,
this clause will give what is needed to establish A 1 . However, there may be problems.
Perhaps the body of that clause, B 1 ,..., B m , will not succeed for the values of variables