Prolog successor notation yields incomplete result and infinite loop

I start to learn Prolog and first learnt about the successor notation.

And this is where I find out about writing Peano axioms in Prolog.

See page 12 of the PDF:

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N,M,K).

prod(0,M,0).
prod(s(N), M, P) :-
    prod(N,M,K),
    sum(K,M,P).

I put the multiplication rules into Prolog. Then I do the query:

?- prod(X,Y,s(s(s(s(s(s(0))))))).

Which means finding the factor of 6 basically.

Here are the results.

X = s(0),
Y = s(s(s(s(s(s(0)))))) ? ;
X = s(s(0)),
Y = s(s(s(0))) ? ;
X = s(s(s(0))),
Y = s(s(0)) ? ;
infinite loop

This result has two problems:

1. Not all results are shown, note that the result X=6,Y=1 is missing.
2. It does not stop unless I Ctrl+C then choose abort.

So... my questions are:

1. WHY is that? I tried switching "prod" and "sum" around. The resulting code gives me all results. And again, WHY is that? It still dead-loops though.
2. HOW to resolve that?

I read the other answer on infinite loop. But I'd appreciate someone answer basing on this scenario. It greatly helps me.

If you want to study termination properties in depth, programs using successor-arithmetics are an ideal study object: You know a priori what they should describe, so you can concentrate on the more technical details. You will need to understand several notions.

Universal termination

The easiest way to explain it, is to consider Goal, false. This terminates iff Goal terminates universally. That is: Looking at tracers is the most ineffective way - they will show you only a single execution path. But you need to understand all of them at once! Also never look at answers when you want universal termination, they will only distract you. You have seen it above: You got three neat and correct answers, only then your program loops. So better "turn off" answers with false. This removes all distraction.

Failure slice

The next notion you need is that of a failure slice. Take a pure monotonic logic program and throw in some goals false. If the resulting failure slice does not terminate (universally), also the original program won't. In your exemple, consider:

prod(0,M,0) :- false.
prod(s(N), M, P) :-
    prod(N,M,K), false,
    sum(K,M,P).

These false goals help to remove irrelevant adornments in your program: The remaining part shows you clearly, why prod(X,Y,s(s(s(s(s(s(0))))))). does not terminate. It does not terminate, because that fragment does not care about P at all! You are hoping that the third argument will help to make prod/3 terminate, but the fragment shows you it is all in vain, since P does not occur in any goal. No need for chatty tracers.

Often it is not so easy to find minimal failure slices. But once you found one, it is next to trivial to determine its termination or rather non-termination properties. After some time you can use your intuition to imagine a slice, and then you can use your reason to check if that slice is of relevance or not.

What is so remarkable about the notion of a failure slice is this: If you want to improve the program, you have to modify your program in the part visible in above fragment! As long as you do not change it, the problem will persist. A failure slice is thus a very relevant part of your program.

Termination inference

That is the final thing you need: A termination inferencer (or analyzer) like cTI will help you to identify the termination condition rapidly. Look at the inferred termination conditions of prod/3 and the improved prod2/3 here!

Edit: And since this was a homework question I have not posted the final solution. But to make it clear, here are the termination conditions obtained so far:

    prod(A,B,C)terminates_if b(A),b(B).
    prod2(A,B,C)terminates_if b(A),b(B);b(A),b(C).

So the new prod2/3 is strictly better than the original program!

Now, it is up to you to find the final program. Its termination condition is:

   prod3(A,B,C)terminates_if b(A),b(B);b(C).

To start with, try to find the failure slice for prod2(A,B,s(s(s(s(s(s(0)))))))! We expect it to terminate, but it still does not. So take the program and add manuallyfalse goals! The remaining part will show you the key!

As a final hint: You need to add one extra goal and one fact.

Edit: Upon request, here is the failure slice for prod2(A,B,s(s(s(s(s(s(0))))))):

prod2(0,_,0) :- false.
prod2(s(N), M, P) :-
   sum(M, K, P),
   prod2(N,M,K), false.

sum(0, M, M).
sum(s(N), M, s(K)) :- false,
    sum(N,M,K).

Please note the significantly simplified definition of sum/3. It only says: 0 plus anything is anything. No more. As a consequence even the more specialized prod2(A,0,s(s(s(s(s(s(0))))))) will loop whileprod2(0,X,Y) elegantly terminates ...

The first question (WHY) is fairly easy to spot, specially if know about left recursion. sum(A,B,C) binds A and B when C is bound, but the original program prod(A,B,C) doesn't use that bindings, and instead recurse with still A,B unbound.

If we swap sum,prod we get 2 useful bindings from sum for the recursive call:

sum(M, K, P)

Now M is bound, and will be used to terminate the left-recursion. We can swap N and M, because we know that product is commutative.

sum(0, M, M).
sum(s(N), M, s(K)) :-
    sum(N, M, K).

prod3(0, _, 0).
prod3(s(N), M, P) :-
    sum(M, K, P),
    prod3(M, N, K).

Note that if we swap M,K (i.e. sum(K,M,P)), when prod3 is called with P unknown we again have a non terminating loop, but in sum.

?- prod3(X,Y,s(s(s(s(s(s(0))))))).
X = s(s(s(s(s(s(0)))))),
Y = s(0) ;
X = s(s(s(0))),
Y = s(s(0)) ;
X = s(s(0)),
Y = s(s(s(0))) ;
X = s(0),
Y = s(s(s(s(s(s(0)))))) ;
false.

OT I'm perplexed by cTI report: prod3(A,B,C)terminates_if b(A),b(B);b(A),b(C).