Search code examples
prologinfinite-loopexponentiationsuccessor-arithmetics

Prolog getting inifinite loop when asking for another solution


I am using SWI Prolog, the following code is used in my homework(the code is not the homework but needed to write the methods the course requires):

nat(0).
nat(s(X)) :-
    nat(X).

plus(0,N,N) :- 
    nat(N).
plus(s(M),N,s(Z)) :-
    plus(M,N,Z).

times(0,N,0) :-
    nat(N).
times(s(M),N,Z) :-
    times(M,N,W),
    plus(W,N,Z).

exp(s(M),0,0) :-
    nat(M).
exp(0,s(M),s(0)) :-
    nat(M).
exp(s(N),X,Z) :-
    exp(N,X,Y),
    times(X,Y,Z).

exp(a,b,c) means c=b^a.

It is copied directly from the book: "The Art of Prolog: Advanced Programming Techniques".

When I run the following query:

exp(s(s(0)),L,s(s(s(s(0))))).

I get an answer:

L = s(s(0))

But when I ask for another answer by entering ;

L = s(s(0)) ;

I get an infinite loop(ending in an out of stack error), I was expecting to get false.

What is the problem in the code? is there a code that does the same(with the same representation of natural numbers) but behaves the way I described? and if so, a few pointers or suggestions would be of great help.

Thanks in advance.


Solution

  • It's normal that it runs in to an infinite loop for the given program: if you call exp/3, With the second element being uninstantiated, it starts branching over all possible values for L. In other words, if you query:

    exp(s(s(0)),L,s(s(s(s(0))))).
    

    It acts as:

    I instantiate L to s(0), is s(0) (thus 1) correct?
    No! I instantiate L to s(s(0)) is 2 correct?
    Yes return 2. Hold on, the user asks for more answers....
    Is 3 correct? No
    Is 4 correct? No
    Is ... correct? (you get the idea)

    Each time you make an attempt, the stack is risen one level deeper (because it requires one more level to construct s(X) over X...

    You could try to use another way: there is a logical upperbound: the result (third argument), so you could first instantiate the second argument as the third and test and then decrement the second argument until you find the correct result.