Problems understanding a specific Prolog recursive predicate

Question

I'm in the process of learning Prolog.
I have this recursive predicate:

add(0,Y,Y).
add(succ(X),Y,succ(Z)) :-
add(X,Y,Z).

Alright, so experienced Prolog programmers will probably understand what this predicate does. At first sight it doesn't look too hard to understand; when given two numerals as the first and second argument, it will return the result of adding them up as its third argument. Sounds simple? Indeed.

But I have a major problem comprehending how this actually works. I've re-read the description of this predicate many times but yet I am not able to understand how it actually works. And that's why I'm asking for help.

By querying this:
add(succ(succ(succ(0))), succ(succ(0)), R).
Prolog will instantiate and thus return R as succ(succ(succ(succ(succ(0))))). Fine. This must be correct. However I have no clue why it is so.

What I have problems understanding is how and why Prolog strips off the outermost succ functor from the original query. Again, as it is recursive, it passes on the results as arguments onto itself, and thus stripping off the outermost succ functor until the goal can be unified. I do understand how the succ(Z) and the argument R works, but I am seemingly unable to comprehend how it actually strips off the outermost succ functor, as mentioned. For me, it seems like it's adding a succ instead of stripping it, because of succ(X) in the predicate definition.

Any help is greatly appreciated. Thanks in advance!

Answer 1

Prolog sees the line add(succ(X),Y,succ(Z)) ... and thinks "oh, it can be matched to the query add(succ(succ(succ(0))), succ(succ(0)), R)., because I can set (unify) X=succ(succ(0)), Y=succ(succ(0)), succ(Z)=R !" The important condition for Prolog, the one that determines it can do it is that succ(succ(succ(0))) can be matched to succ(X), the rest is just simple, because Y and R can be in this first step set arbitrarily (they are not unified yet). And succ(succ(succ(0))) can be matched to succ(X) just because succ(A) can be matched to succ(B) any time A can be matched to B - you see it is not very hard for computer to decide it.

The next step is that Prolog looks at the rest of the line (:- add(X,Y,Z)) and generate query add(succ(succ(0)), succ(succ(0)), Z). Remember that succ(Z)=R and it won't change until (if) the computation path is rejected. The next query will be add(succ(0), succ(succ(0)), Z'), where succ(Z')=Z. Then add(0, succ(succ(0)), Z''), where succ(Z'')=Z'.

Then can Prolog use the first rule, determine that Z''=Y=succ(succ(0)). Then there is nothing left to do, so it just write to the output that R=succ(Z)=succ(succ(Z'))=succ(succ(succ(Y)))=succ(succ(succ(succ(succ(0))))).