newbie - order of terms in a clause

Hi,
I am a newbie at writing prolog software, I tried these four lines
with Gnu Prolog 1.3.0 :

sum(1,1,2).
sum(1,2,3).
sum(1,3,4).
sum(A,B,Z):-
sum(1,R,A), sum(R,B,S), sum(1,S,Z).

And these queries :

| ?- sum(3,1,X).

X = 4 ?

yes
| ?- sum(2,2,X).

X = 4 ?

yes
| ?- sum(3,X,4).

X = 1 ?

yes
| ?- sum(4,X,1).

CRASH with local stack overflow.

I suspect that this program has a theorical flaw due to my ignorance
of logic programming, but I cannot guess which one: could you please
point me in the right direction?

I tried to trace it, but I cannot understand which predicate is active
at a given step. I also noticed that the behaviour seems to be
dependent on the order of the term in the fourth clause, but I cannot
understand why it is so... Any help/hint would be really appreciated,

Thank you in advance,
Luca

luca.dallolio@gmail.com writes:

> And these queries :
>
> | ?- sum(3,1,X).
>
> X = 4 ?

Press ";" and see that even this does not work very well.

> I suspect that this program has a theorical flaw due to my ignorance
> of logic programming, but I cannot guess which one: could you please
> point me in the right direction?

I recommend SWI-Prolog's graphical tracer:

?- gtrace, sum(3,1,X).

> Any help/hint would be really appreciated,

What about this definition:

sum(0, X, X).
sum(p(X), Y, p(Z)) :- sum(X, Y, Z).

This program answers the equivalents of all your queries correctly:

%?- sum(p(p(p(0))), p(0), X).
%@ X = p(p(p(p(0)))) ;

%?- sum(p(p(0)), p(p(0)), X).
%@ X = p(p(p(p(0)))) ;

%?- sum(p(p(p(0))), X, p(p(p(p(0))))).
%@ X = p(0) ;

%?- sum(p(p(p(p(0)))), X, p(0)).
%@ No

As a general rule, mark different categories by different functors in
your Prolog programs. When working with natural numbers, there are 2
kinds of things: Zero, and successors of a natural number N. I used 0
for the former, and p(N) for the latter. You can also start from 1:

sum(1, X, p(X)).
sum(p(X), Y, p(Z)) :- sum(X, Y, Z).

Your examples:

%?- sum(p(p(1)), 1, X).
%@ X = p(p(p(1))) ;

%?- sum(p(1), p(1), X).
%@ X = p(p(p(1))) ;

%?- sum(p(p(p(1))), X, 1).
%@ No

--
comp.lang.prolog FAQ: http://www.logic.at/prolog/faq/

On Mon, 13 Aug 2007 10:31:00 +0000, luca.dallolio wrote:

> Hi,
> I am a newbie at writing prolog software, I tried these four lines
> with Gnu Prolog 1.3.0 :
>
> sum(1,1,2).
> sum(1,2,3).
> sum(1,3,4).
> sum(A,B,Z):-
> 	sum(1,R,A), sum(R,B,S), sum(1,S,Z).
...
>
> yes
> | ?- sum(4,X,1).

I assume that you expected an answer for X.
I assume that you intended to implement the relation sum(A,B,C)
where on success C equals the result of evaluating A+B, even if
not both A and B are given at the query.

So, did you expect that ?- sum(4,X,1). answers ... X = -3 ?

Consider that the constant -3 is not in your program, and that your
program does not generate new numbers, how could your program ever
generate the number -3 ?

Conclusion: you should expect that query to fail, or to loop.
If it loops, the chances that you get an out of stack error are getting
higher.

One more thing:

> I also noticed that the behaviour seems to be
> dependent on the order of the term in the fourth clause

Those things in the body of a clause are named "goals" (or literals,
and depending on the context also atoms).

BTW, the tracer output is perfect, because it shows where the loop is.
Have you looked up in the manual what e.g.
10    2  Call: sum(1,4,1) ?
means ? Especially the first two numbers ...

Cheers

Bart Demoen

ps. the suggestion by Markus (his alternative definition of sum/3)
seriously ducks your question, because you asked for understanding,
[which is good !], not for a definition of sum/3 that works

luca.dallolio@gmail.com writes:

> Hi,
> I am a newbie at writing prolog software, I tried these four lines
> with Gnu Prolog 1.3.0 :
>
> sum(1,1,2).
> sum(1,2,3).
> sum(1,3,4).
> sum(A,B,Z):-
> 	sum(1,R,A), sum(R,B,S), sum(1,S,Z).
>
> And these queries :
>
> | ?- sum(3,1,X).
>
> X = 4 ?
>
> yes
> | ?- sum(2,2,X).
>
> X = 4 ?
>
> yes
> | ?- sum(3,X,4).
>
> X = 1 ?
>
> yes
> | ?- sum(4,X,1).
>
> CRASH with local stack overflow.
>
> I suspect that this program has a theorical flaw due to my ignorance
> of logic programming, but I cannot guess which one: could you please
> point me in the right direction?

Well, strictly speaking I'd say your program has a practical flaw,
rather than a theoretical flaw.  When more than one clause applies in
a theorem prover, only an omniscient oracle can always be guaranteed
to choose the 'correct' one; Prolog, like any logic system, has rules
that are simpler than acquiring an omniscient oracle, but that
sometimes choose the wrong clause.

What you need to read up on is the difference between the declarative
and the procedural interpretation of Prolog programs.  Any Prolog
text will discuss the issue.

> I tried to trace it, but I cannot understand which predicate is active
> at a given step.

(It's always the same *predicate*, namely sum/3.  I think you mean you
don't understand which clause is being used at any given moment.)

Here, I can only say that practice interpreting trace output helps.
What follows is a manual trace.  Take it with a grain of salt: I am
not a Prolog implementor and I may have made careless errors in
writing up what happens.

1 Start with the query sum(4,X,1).  This doesn't unify with any of the
first three clauses, so it catches the fourth, binding A to 4, B to X,
and Z to 1.  To simplify keeping track of things when we have several
different clauses on the stack, with different variables which share
the same name, let's rewrite clauses as needed using variables named
V1, V2, V3, ....  (Your Prolog interpreter does the same thing when in
a trace it shows you variable names like _0046.)

The goal sum(4,X,1) can then be rewritten

sum(4,V1,1)
with V1 = X in query

By clause 4, we know that the goal sum(4,V1,1) can be proven if the body
of the fourth clause can be proven.

Rewriting that body's variable names, we now have the following list
of things to prove:

sum(1,V2,4),
sum(V2,V1,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of step 1's instantiation of sum/3,
V2 = R of step 1's instantiation of sum/3
V3 = S of step 1's instantiation of sum/3

2 Now try to prove sum(1,V2,4).  This doesn't match clause 1 or clause 2,
but it matches clause 3, binding V2 to 3.

The list now looks like:

sum(3,V1,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of step 1's instantiation of sum/3,
V3 = S of step 1's instantiation of sum/3

3 Now try to prove sum(3,V1,V3).  This doesn't match clauses 1-3, but
it matches clause 4, binding A to 3, B to V1, and Z to V3.  Replacing
sum(3,V1,V3) with the body of this second instantiation of clause 4,
we get the following list of things to prove:

sum(1,V4,3),
sum(V4,V1,V5),
sum(1,V5,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of step 1's instantiation of sum/3
= the B of step 2's instantiation of sum/3
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
V4 = R of step 2's instantiation of sum/3
V5 = S of step 2's instantiation of sum/3

4 The first subgoal matches the second clause, binding V4 to 2.  Our
list now looks like this:

sum(2,V1,V5),
sum(1,V5,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of the current instantiation (call it 1) of sum/3,
V3 = S of step 1's instantiation of sum/3
V5 = S of step 2's instantiation of sum/3

5 The subgoal sum(2,V1,V5) matches clause 4, binding A to 2, B to V1,
and Z to V5.  Placing the body of clause 4 into the list of pending
goals, we now have

sum(1,V6,2),
sum(V6,V1,V7),
sum(1,V7,V5),
sum(1,V5,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of the step 1's instantiation of sum/3,
= the B of the step 2's instantiation of sum/3,
= the B of the step 5's instantiation of sum/3,
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
V5 = S of step 2's instantiation of sum/3
= Z of step 5's instantiation of sum/3
V6 = R of step 5's instantiation of sum/3
V7 = S of step 5's instantiation of sum/3

6 The first subgoal, sum(1,V6,2) matches clause 1 and binds V6 to 1.
The list now is:

sum(1,V1,V7),
sum(1,V7,V5),
sum(1,V5,V3),
sum(1,V3,1)
with V1 = the X of the query
= the B of the step 1's instantiation of sum/3,
= the B of the step 2's instantiation of sum/3,
= the B of the step 5's instantiation of sum/3,
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
V5 = S of step 2's instantiation of sum/3
= Z of step 5's instantiation of sum/3
V7 = S of step 5's instantiation of sum/3

7 Now the first subgoal, sum(1,V1,V7), matches the first clause,
binding V1 to 1 and V7 to 2.  This means the value of X in the query
will be 1, if we can prove the items on the list.  The list now looks
like this:

sum(1,2,V5),
sum(1,V5,V3),
sum(1,V3,1)
with
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
V5 = S of step 2's instantiation of sum/3
= Z of step 5's instantiation of sum/3

8 The first subgoal, sum(1,3,V5), matches clause 2, binding V5 to 3.
The list is now

sum(1,3,V3),
sum(1,V3,1)
with
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3

9 The first subgoal matches clause 3, binding V3 to 4.  The list is
now

sum(1,4,1)

But there is no fact which matches this goal, so this step fails, and
we unwind the most recent bindings.  We revert to the list as shown in
step 8 above, and try for another way to prove the goal sum(1,3,V3).
The list is as shown in step 8.

10 The first subgoal, sum(1,3,V3), matches clause 4, binding A to 1,
B to 3, and Z to V3.  Replacing the head of clause 4 with the body,
we now have the list

sum(1,V8,1),
sum(V8,3,V9),
sum(1,V9,V3).
sum(1,V3,1)
with
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
= Z of step 10's instantiation of sum/3
V8 = R of step 10's instantiation of sum/3
V9 = S of step 10's instantiation of sum/3

If we can prove the items in the list, we will still have X=1.

11 The first subgoal now matches only clause 4, binding A to 1, B to V8,
and Z to 1.  The list is now:

sum(1,V10,1),
sum(V10,V8,V11),
sum(1,V11,1),
sum(V8,3,V9),
sum(1,V9,V3).
sum(1,V3,1)
with
V3 = S of step 1's instantiation of sum/3
= Z of step 2's instantiation of sum/3
= Z of step 10's instantiation of sum/3
V8 = R of step 10's instantiation of sum/3
= R of step 11's instantiation of sum/3
V9 = S of step 10's instantiation of sum/3
V10 = R of step 11's instantiation of sum/3
V11 = S of step 11's instantiation of sum/3

12 At this point, notice that the first subgoal, sum(1,V10,1), is
similar to the first subgoal at step 11: sum(1,V8,1), and will match
exactly the same clauses.  At this point, we're in an infinite loop:
the first subgoal in the list of pending goals will match clause 4 and
put three new items on the stack, but in each case clause 4 proposes a
new first subgoal which matches only clause 4, which means we make no
progress toward a solution.

> I also noticed that the behaviour seems to be
> dependent on the order of the term in the fourth clause, but I cannot
> understand why it is so...

Because Prolog's clause for choosing which goal to pursue next is
always:  take the first subgoal in the list of pending subgoals,
and try to resolve it completely.  If it matches the head of a
rule, then unify the arguments as needed and replace the subgoal
with the body of the rule whose head it matched.

This is simple to understand and manipulate, but does not find all
possible proofs.  Sometimes it fails and sometimes it loops.  Here,
it loops.

I hope this helps.

--Michael Sperberg-McQueen
World Wide Web Consortium