I've got the following knowledge base, which is supposed to add two arguments and give the results:
add(0,X,X).
add(succ(X),Y,succ(R)):- add(X,Y,R).
Now this is my query:
?- add(succ(succ(succ(0))), succ(succ(0)), Result).
The 0 does not unify with the first argument so it goes to the second add/3 clause. Now here is the thing i can't figure out. The book (LPN) tells me that the outermost succ factor is stipped off the first argument, but I can't figure out why? In my mind it adds a succ functor. Could someone please explain why it is stripping it off?
Thanks in advance!
Luuk
Try this at your top level prompt:
?- succ(succ(0)) = succ(X).
Before you type <Enter>, what do you think the solution will be?
The "stripping" that the book talks about happens between the head of the second clause, add(succ(X), ...) and the recursive call add(X, ...).
I don't really see the added value of talking about "stripping" here. What actually happens is that if the first argument to add/3 is a term with the functor succ/1 (so anything at all that looks like succ(<Whatever>), then, X will be unified with this <Whatever>. In the case of the query:
?- add(succ(succ(succ(0))), succ(succ(0)), Result).
<Whatever> is succ(succ(0)), so the X is unified with succ(succ(0)), and this is the first argument to the recursive call to add/3.