Recursive succ addition in Prolog

Question

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

I don't understand how this one works. If I run the query:

add(succ(succ(succ(0))), succ(succ(0)), R)

How does it remove succ from the first argument?

If I run it:

X=succ(succ(succ(0)))
Y=succ(succ(0))
R=?

This satisfied the body. We input them into the head:

add(succ(X),Y,succ(Z)) %% becomes
add(succ(succ(succ(0))),succ(succ(0)),succ(R))

I.e. it looks to me as if it just adds succ, not removes them from the first argument? I saw that there's another post about this exact question but it does not make sense to me.

Answer 1

When you call the goal add(succ(succ(succ(0))), succ(succ(0)), R) and Prolog tries to execute the clause with the head add(succ(X),Y,succ(Z)), unification happens. Unification is one of the central concepts of Prolog, and it's important to understand it well. Unification is also the operation that is performed by the = operator. What happens when the head of the clause is executed is exactly the same as happens when you execute the following equivalent query:

?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).

It is important to understand that unification is not just "unpacking" or "building up" terms, but both at the same time.

It can "extract" information from terms:

?- X = f(a), Y = f(Z), X = Y.
X = Y, Y = f(a),
Z = a.

Here we found that a is the argument of the f functor in X.

It can "construct" terms:

?- X = f(Y), Y = g(h).
X = f(g(h)),
Y = g(h).

Here we "inserted" the term g(h) into the "hole" Y in X.

It can also do both at the same time to more than one term:

?- X = f(a, B), Y = f(A, b), X = Y.
X = Y, Y = f(a, b),
B = b,
A = a.

Here unification "unpacked" both f terms, then "filled in" a hole in each of them.

Now, armed with this knowledge, what does the unification in your example do?

?- add(succ(succ(succ(0))), succ(succ(0)), R) = add(succ(X),Y,succ(Z)).
R = succ(Z),
X = Y, Y = succ(succ(0)).

In particular, when succ(succ(succ(0))) is unified with succ(X), this will bind X to succ(succ(0)). X is not bound to the entire term succ(succ(succ(0))) but only to an "inner" part. This is what removes one level of succ from the argument.