Explanation of Prolog recursive procedure

问题:

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.

回答1:

First premises:

• We have s(X) defined as the successor of X so basically s(X) = X+1
• The _G### notation is used in the trace for internal variables used for the recursion

Let's first look at another definition of addition with successors that I find more intuitive:

add(0,Y,Y).
add(s(A),B,C) :- add(A,s(B),C).

this does basically the same but the recursion is easier to see:

we ask

add(s(s(0)),s(0),R).

Now in the first step prolog says thats equivalent to

add(s(0),s(s(0)),R)

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 becomes

add(0,s(s(s(0))),R)

which, given add(0,Y,Y). this means that

R = s(s(s(0)))

---

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

add(s(s(0)),s(0),R)

with X=s(0), Y = s(0) and s(Z) = R and Z = _G001

add(s(0),s(0),_G001)

with X = 0, Y=s(0) and s(s(Z)) = s(G_001) = R and Z = _G002

add(0,s(0),_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.

回答2:

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:

add(s(X),Y,s(Z)) :- add(X,Y,Z).

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:

Provided, add(X,Y,Z) is true, then also add(s(X),Y,s(Z)) is true.

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.

回答3:

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:

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

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:

• The base step of the recursion (my first rule ie) says always that since you have reached the end of the computation you can copy the partial result (now total) from your accumulator variable to your output variable (this is the step in which, through unification your output var gets instantiated!)
• The recursive step tells how to create a partial result and how to store it in the accumulator variable (in my case i 'increment' Y). Note that in the recursive step the output variable is never changed.

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.

• Its base step is the same as the accumulator pattern but Y never changes in the recursive step while Z does
• It uses to unify the variable in Z with Y by partially instantiating all the computation at the end of each recursive call after you've reached the base step and each procedure call is ending. So at the end of the first call the inner free var in Z has been substituted by unification many times by the value in Y. Note the code below, after you have reached the bottom call, the procedure call stack starts to pop and your partial vars (S1, S2, S3 for semplicity) gets unified until R gets fully instantiated

Here is the stack trace:

add(s(s(s(0))),s(0),S1).          ^ S1=s(S2)=s(s(s(s(0))))
add(  s(s(0)) ,s(0),S2).          | S2=s(S3)=s(s(s(0)))
add(    s(0)  ,s(0),S3).          | S3=s(S4)=s(s(0))
add(      0   ,s(0),S4).          | S4=s(0)
add(      0   ,s(0),s(0)).  ______|