Search code examples
prologsuccessor-arithmetics

How does prolog run through recursive queries using succ?


Can someone explain to me why this prolog query works the way it does. The definition is:

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

Given this:

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

Heres the trace of the query:

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))))))

The part that confused me the most about that tutorial was the fact that in the first argument, the succ is stripped, and it recurses. While recursing though, R gains a succ... HOW?! Also, where does the zero come from at the first exit (9)? I am new to prolog, and I am trying to understand the language for a homework. Any help much appreciated.

Note: for anyone interested, the link to this tutorial is http://www.learnprolognow.org/lpnpage.php?pagetype=html&pageid=lpn-htmlse9


Solution

  • "where does the zero come from at the first exit (9)?"

    The call add(0, succ(succ(0)), _G652) is unified with the first clause that says that if the first argument of add is zero, then the second and the third are the same. In this particular situatiob variable _G652 becomes succ(succ(0)).

    "While recursing though, R gains a succ... HOW?!"

    This is the result of the application of the second clause. This clause states (roughly) that you first strip succ from the first argument, then call add recursively, and, finally, add another "layer" of succ to the third argument coming back from this recursive call.

    The predicate add is nothing but a direct implementation of addition in Peano arithmetics: http://en.wikipedia.org/wiki/Peano_axioms#Addition