It helps to understand how Prolog operates when figuring out an existing predicate, or when designing a new one. When you make a query such as:
sum( succ(succ(0)), succ(succ(succ(0))), Answer ).
Prolog will look for facts and rules matching sum(_, _, _)
(sum/3
) and select the first one that matches. The rules in place are:
(1) sum( succ(X), Y, succ(Z) ) :- sum( X, Y, Z ).
(2) sum( 0, X, X ).
If you look at the query, it clearly matches the pattern of rule #1. Remember that in Prolog, a variable can be instantiated to any kind of term, and variables of the same name are unified (instantiated to the same value). When Prolog unifies the "head" of rule #1 with the query, it does so by unifying the variables as follows:
X = succ(0)
Y = succ(succ(succ(0)))
(A) Answer = succ(Z)
Notice that Answer
has the value succ(Z)
even though Z
hasn't been bound (assigned a concrete value) yet. Now we follow the rule, which will query, sum(X, Y, Z)
, which will be the query:
sum( succ(0), succ(succ(succ(0))), Z )
| | |
X Y Z
Prolog will now start from the top again since this is a new query for sum/3
. Just like the first time, it matches rule #1 with the following unifications:
X = 0
Y = succ(succ(succ(0)))
(B) Z = succ(Z')
I am using Z'
above to distinguish it from the other variable Z
in the sum(succ(0), succ(succ(succ(0))), Z)
, since it is a different Z
than the one used in the head for sum(..., succ(Z))
. This is like if you have a function in C declared as int f(x) { return 2*x; }
and you call it with another local variable x
from somewhere, that name x
is used in two different places and represents two different variables).
Then we can follow the next recursive query, sum(X, Y, Z')
again, which becomes:
sum( 0, succ(succ(succ(0))), Z' )
| | |
X Y Z'
This recursive query doesn't match rule #1 since the first argument, 0
, doesn't match succ(X)
. However, it matches rule #2:
0 = 0
X = succ(succ(succ(0)))
(C) X = Z'
Now X = succ(succ(succ(0)))
so Z' = succ(succ(succ(0)))
. Since this rule has no more queries within it, it finally succeeds back to where it was queried from. Returning this back to (B) above:
Z = succ(Z') = succ(succ(succ(succ(0))))
and returning this back to (A):
Answer = succ(Z) = succ(succ(succ(succ(succ(0)))))
And there you have it. Using the trace
facility that @CapelliC mentioned, you can watch these successive steps occur in the Prolog interpreter and follow the instantiation of variables.