What are the steps that Prolog follows with the definition of natural numbers?

Question

I'm learning how to program in Prolog and I found the next program that defines the natural numbers and their sum:

sum( succ( X ), Y, succ( Z )) :- sum( X, Y, Z ).
sum( 0, X, X ).
?- sum( succ( succ(0)), succ( succ( succ(0))), Answer ).
Answer = succ( succ( succ( succ( succ(0)))))

(found here)

The problem is that I'm struggling with the execution flow of this program. To tell the truth I don't know what it does. How can Prolog figure out the Answer's value? What are the steps that Prolog follows to find the Answer's value?

Thanks in advance.

Answer 1

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.

Answer 2

Prolog's "evaluation" proceeds by matching the given query to the program's rules' heads, and proceeding with the matching rule's body, under the matching substitution. When a rule is selected, its variables are uniformly renamed, for uniqueness:

(1) sum( succ( X ), Y, succ( Z )) :- sum( X, Y, Z ).
(2) sum( 0, X, X ).

    ?- sum( succ( succ(0)), succ( succ( succ(0))), Answer    ).
(1) -> sum( succ(   X1   ),  Y1                  , succ( Z1 )) :- sum( X1, Y1, Z1 ).

        %%  X1 = succ(0), Y1 = succ( succ( succ(0))), succ(Z1) = Answer. %%

    -? sum( X1,              Y1,                   Z1        ).
    -? sum( succ( 0  ),      Y1,                   Z1        ). 
(1) -> sum( succ( X2 ),      Y2,                   succ( Z2 )) :- sum( X2, Y2, Z2 ).

        %%  X2 = 0, Y2 = Y1, succ(Z2) = Z1. %%

    -? sum( X2,              Y2,                   Z2        ).
    -? sum( 0,               Y2,                   Z2        ).
(2) -> sum( 0,               X3,                   X3        ).     %% DONE. %%

        %%  X3 = Y2, X3 = Z2. %%

From here, Answer = succ(Z1) = succ( succ(Z2)) = succ( succ(X3)) = succ( succ( Y2)) = succ( succ (Y1)) = succ( succ( succ( succ( succ(0))))).

Answer 3

for such a simple program, trace/0 it's the way to go. leash/1 (that not totally obvious to newbies) allows controlling debugger interface:

21 ?- leash(-all),trace.
true.

[trace] 22 ?- sum( succ( succ(0)), succ( succ( succ(0))), Answer ).
   Call: (6) sum(succ(succ(0)), succ(succ(succ(0))), _G710)
   Call: (7) sum(succ(0), succ(succ(succ(0))), _G789)
   Call: (8) sum(0, succ(succ(succ(0))), _G791)
   Exit: (8) sum(0, succ(succ(succ(0))), succ(succ(succ(0))))
   Exit: (7) sum(succ(0), succ(succ(succ(0))), succ(succ(succ(succ(0)))))
   Exit: (6) sum(succ(succ(0)), succ(succ(succ(0))), succ(succ(succ(succ(succ(0))))))
Answer = succ(succ(succ(succ(succ(0))))).

You can see that your program does a bounded recursive search on first argument, unifying it with either the first clause (calls marked 6,7) or the second one (call marked 8).