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

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.

Solution

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.