I'd like someone to explain this procedure if possible (from the book 'learn prolog now'). It takes two numerals and adds them together.
add(0,Y,Y).
add(s(X),Y,s(Z)) :- add(X,Y,Z).
In principle I understand, but I have a few issues. Lets say I issue the query
?- add(s(s(0)), s(0), R).
Which results in:
R = s(s(s(0))).
Step 1 is the match with rule 2. Now X becomes s(0) and Y is still s(0). However Z (according to the book) becomes s(_G648), or s() with an uninstantiated variable inside it. Why is this?
On the final step the 1st rule is matched which ends the recursion. Here the contents of Y somehow end up in the uninstantiated part of what was Z! Very confusing, I need a plain english explanation.
Let's divide the problem in three parts: the issues concerning instantiation of variables and the accumulator pattern which I use in a variation of that example:
and a comment about your example that uses composition of substitutions.
What Prolog applies in order to see which rule (ie Horn clause) matches (whose head unifies) is the Unification Algorithm which tells, in particular, that if I have a variable, let's say, X and a funtor, ie, f(Y) those two term unify (there is a small part about the occurs check to...check but nevermind atm) hence there is a substitution that can let you convert one into another.
When your second rule is called, indeed R gets unified to s(Z). Do not be scared by the internal representation that Prolog gives to new, uninstantiated variables, it is simply a variable name (since it starts with '_') that stands for a code (Prolog must have a way to express constantly newly generated variables and so _G648, _G649, _G650 and so on). When you call a Prolog procedure, the parameters you pass that are uninstantiated (R in this case) are used to contain the result of the procedure as it completes its execution, and it will contain the result since at some point during the procedure call it will be instantied to something (always through unification). If at some point you have that a var, ie K is istantiated to s(H) (or s(_G567) if you prefer), it is still partilally instantiated and to have your complete output you need to recursively instantiate H. To see what it will be instantiated to, have a read at the accumulator pattern paragraph and the sequent one, tho ways to deal with the problem.
The accumulator pattern is taken from functional programming and, in short, is a way to have a variable, the accumulator (in my case Y itself), that has the burden to carry the partial computations between some procedure calls. The pattern relies on recursion and has roughly this form:
Finally, concerning your exemple, it follows another pattern, the composition of substitutions which I think you can understand better having thought about accumulator and instantiation via unification.
Here is the stack trace:
First premises:
s(X)
defined as the successor ofX
so basically s(X) = X+1Let's first look at another definition of addition with successors that I find more intuitive:
this does basically the same but the recursion is easier to see:
we ask
Now in the first step prolog says thats equivalent to
because we have
add(s(A),B,C) :- add(A,s(B),C)
and if we look at the question A = s(0) and B=s(0). But this still doesn't terminate so we have to reapply that equivalency with A=0 and B=s(s(0)) so it becomeswhich, given
add(0,Y,Y).
this means thatYour definition of add basically does the same but with two recursions:
First it runs the first argument down to 0 so it comes down to add(0,Y,Y):
with X=s(0), Y = s(0) and s(Z) = R and Z = _G001
with X = 0, Y=s(0) and s(s(Z)) = s(G_001) = R and Z = _G002
So now it knows that _G002 is s(0) from the definition add(0,Y,Y) but has to trace its steps back so _G001 is s(_G002) and R is s(_G001) is s(s(_G002)) is s(s(s(0))).
So the point is in order to get to the definition add(0,Y,Y) prolog has to introduce internal variables for a first recursion from which R is then evaluated in a second one.
If you want to understand the meaning of a Prolog program, you might concentrate first on what the relation describes. Then you might want to understand its termination properties.
If you go into the very details of a concrete execution as your question suggests, you will soon be lost in the multiplicity of details. After all, Prolog has two different interlaced control flows (AND- and OR-control) and in addition to that it has unification which subsumes parameter passing, assignment, comparison, and equation solving.
Brief: While computers execute a concrete query effortlessly for zillions of inferences, you will get tired after a screenful of them. You can't beat computers in that. Fortunately, there are better ways to understand a program.
For the meaning, look at the rule first. It reads:
See the
:-
in between? It is meant to symbolize an arrow. It is a bit unusual that the arrow points from right-to-left. In informal writing you would write it rather left-to-right. Read this as follows:So we assume that we have already some
add(X,Y,Z)
meaning "X+Y=Z". And given that, we can conclude that also "(X+1)+Y=(Z+1)" holds.After that you might be interested to understand it's termination properties. Let me make this very brief: To understand it, it suffices to look at the rule: The 2nd argument is only handed further on. Therefore: The second argument does not influence termination. And both the 1st and 3rd argument look the same. Therefore: They both influence termination in the same manner! In fact, add/3 terminates, if either the 1st or the 3rd argument will not unify with
s(_)
.Find more about it in other answers tagged failure-slice, like:
Prolog successor notation yields incomplete result and infinite loop
But now to answer your question for
add(s(s(0)), s(0), R).
I only look at the first argument: Yes! This will terminate. That's it.