Search code examples
recursionprologadditionsuccessor-arithmetics

Recursive addition in Prolog

Knowledge Base

add(0,Y,Y). // clause 1
add(succ(X),Y,succ(Z)) :- add(X,Y,Z). // clause 2

Query

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

Trace

Call: (6) add(succ(succ(succ(0))), succ(succ(0)), R)
Call: (7) add(succ(succ(0)), succ(succ(0)), _G648)
Call: (8) add(succ(0), succ(succ(0)), _G650)
Call: (9) add(0, succ(succ(0)), _G652)
Exit: (9) add(0, succ(succ(0)), succ(succ(0)))
Exit: (8) add(succ(0), succ(succ(0)), succ(succ(succ(0))))
Exit: (7) add(succ(succ(0)), succ(succ(0)), succ(succ(succ(succ(0)))))
Exit: (6) add(succ(succ(succ(0))), succ(succ(0)), succ(succ(succ(succ(succ(0))))))

My Question

  • I see how the recursive call in clause 2 strips the outermost succ() at each call for argument 1.
  • I see how it adds an outer succ() to argument 3 at each call.
  • I see when the 1st argument as a result of these recursive calls reaches 0. At that point, I see how the 1st clause copies the 2nd argument to the 3rd argument.

This is where I get confused.

  1. Once the 1st clause is executed, does the 2nd clause automatically get executed as well, then adding succ() to the first argument?

  2. Also, how does the program terminate, and why doesn't it just keep adding succ() to the first and 3rd arguments infinitely?

Explanation from LearnPrologNow.com (which I don't understand)

Let’s go step by step through the way Prolog processes this query. The trace and search tree for the query are given below.

The first argument is not 0 , which means that only the second clause for add/3 can be used. This leads to a recursive call of add/3 . The outermost succ functor is stripped off the first argument of the original query, and the result becomes the first argument of the recursive query. The second argument is passed on unchanged to the recursive query, and the third argument of the recursive query is a variable, the internal variable _G648 in the trace given below. Note that _G648 is not instantiated yet. However it shares values with R (the variable that we used as the third argument in the original query) because R was instantiated to succ(_G648) when the query was unified with the head of the second clause. But that means that R is not a completely uninstantiated variable anymore. It is now a complex term, that has a (uninstantiated) variable as its argument.

The next two steps are essentially the same. With every step the first argument becomes one layer of succ smaller; both the trace and the search tree given below show this nicely. At the same time, a succ functor is added to R at every step, but always leaving the innermost variable uninstantiated. After the first recursive call R is succ(_G648) . After the second recursive call, _G648 is instantiated with succ(_G650) , so that R is succ(succ(_G650) . After the third recursive call, _G650 is instantiated with succ(_G652) and R therefore becomes succ(succ(succ(_G652))) . The search tree shows this step by step instantiation.

At this stage all succ functors have been stripped off the first argument and we can apply the base clause. The third argument is equated with the second argument, so the ‘hole’ (the uninstantiated variable) in the complex term R is finally filled, and we are through.

Solution

  • Let us start by getting the terminology right.

    These are the clauses, as you correctly indicate:

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

    Let us first read this program declaratively, just to make sure we understand its meaning correctly:

    1. 0 plus Y is Y. This makes sense.
    2. If it is true that X plus Y is Z then it is true that the successor of X plus Y is the successor of Z.

    This is a good way to read this definition, because it is sufficiently general to cover various modes of use. For example, let us start with the most general query, where all arguments are fresh variables:

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

    In this case, there is nothing to "strip", since none of the arguments is instantiated. Yet, Prolog still reports very sensible answers that make clear for which terms the relation holds.

    In your case, you are considering a different query (not a "predicate definition"!), namely the query:

    ?- add(succ(succ(succ(0))), succ(succ(0)), R).
R = succ(succ(succ(succ(succ(0))))).

    This is simply a special case of the more general query shown above, and a natural consequence of your program.

    We can also go in the other direction and generalize this query. For example, this is a generalization, because we replace one ground argument by a logical variable:

    ?- add(succ(succ(succ(0))), B, R).
R = succ(succ(succ(B))).

    If you follow the explanation you posted, you will make your life very difficult, and arrive at a very limited view of logic programs: Realistically, you will only be able to trace a tiny fragment of modes in which you could use your predicates, and a procedural reading thus falls quite short of what you are actually describing.

    If you really insist on a procedural reading, start with a simpler case first. For example, let us consider:

    ?- add(succ(0), succ(0), R).

    To "step through" procedurally, we can proceed as follows:

    1. Does the first clause match? (Note that "matching" is already limited reading: Prolog actually applies unification, and a procedural reading leads us away from this generality.)
    2. Answer: No, because s(_) does not unify with 0. So only the second clause applies.
    3. The second clause only holds if its body holds, and in this case if add(0, succ(0), Z) holds. And this holds (by applying the first clause) if Z is succ(0) and R is succ(Z).
    4. Therefore, one answer is R = succ(succ(0)).. This answer is reported.
    5. Are there other solutions? These are only reported on backtracking.
    6. Answer: No, there are no other solutions, because no further clause matches.

    I leave it as an exercise to apply this painstaking method to the more complex query shown in the book. It is straight-forward to do it, but will increasingly lead you away from the most valuable aspects of logic programs, found in their generality and elegant declarative expression.

    Your question regarding termination is both subtle and insightful. Note that we must distinguish between existential and universal termination in Prolog.

    For example, consider again the most general query shown above: It yields answers, but it does not terminate. For an answer to be reported, it is enough that an answer substitution is found that makes the query true. This is the case in your example. Alternatives, if any potentially remain, are tried and reported on backtracking.

    You can always try the following to test termination of your query: Simply append false/0, for example:

    ?- add(X, Y, Z), false.
nontermination

    This lets you focus on termination properties without caring about concrete answers.

    Note also that add/3 is a terrible name for a relation: An imperative always implies a direction, but this is in fact much more general and usable also if none of the arguments are even instantiated! A good predicate name should reflect this generality.