Search code examples
prologstack-overflowfailure-slicesuccessor-arithmetics

Stackoverflow in Prolog Peano Arithmetic

I'm writing some Peano arithmetic to better learn Prolog. The following is the code I've come up with, and it seems equivalent of what I've seen elsewhere online:

add(X,z,X).
add(X,s(Y),s(Z)) :- add(X,Y,Z).
mult(_,z,z).
mult(X,s(Y),W) :- mult(X,Y,Z), add(X,Z,W).

However if I try to make a simple query, like the divisor pairs of 0, I run into problems:

| ?- mult(X,Y,z).

Y = z ? ;

X = z
Y = s(z) ? ;

X = z
Y = s(s(z)) ? ;

X = z
Y = s(s(s(z))) ? ;

Fatal Error: global stack overflow (size: 32768 Kb, reached: 32765 Kb, environment variable used: GLOBALSZ)

It really bugs me, as to how can it get all the way to Y = 3, but not to Y = 4?

Solution

  • The stack overflow occurs because, for your query, the predicate add/3 is eventually called with a variable as the middle argument. When you backtrack into it, you get a loop that leads to a stack overflow. Consider the call add(X,Y,Z). The first clause gives you a first solution, add(X,z,X). But, on backtracking, when you use the second clause, you unify your query with add(X,s(Y),s(Z)) and recursively call add(X,Y,Z), back to where you started (remember, the middle argument is not instantiated, so Y in s(Y) will also not be instantiated on the call. You're able to get the first four solutions, as you show above, only thanks to the base cases of both predicates. When usage of those base clause (on backtracking) is exhausted, you get into the loop I just explained above.

    Try add the following clause as the first clause of the add/3 predicate:

    add(X,Y,Z) :-
    write('Called: '), writeq(add(X,Y,Z)), nl, fail.

    Retrying the query you will get (hope you are quick with Control-C):

    | ?- mult(X,Y,z).

Y = z ? ;
Called: add(_279,z,z)

X = z
Y = s(z) ? ;
Called: add(_279,z,_307)
Called: add(_279,_279,z)

X = z
Y = s(s(z)) ? ;
Called: add(_279,z,_309)
Called: add(_279,_279,_309)
Called: add(z,z,z)

X = z
Y = s(s(s(z))) ? ;
Called: add(s(_307),_307,_309)
Called: add(s(z),s(s(z)),z)
Called: add(s(s(_311)),_311,_313)
Called: add(s(s(z)),s(s(s(s(z)))),z)
Called: add(s(s(s(_315))),_315,_317)
Called: add(s(s(s(z))),s(s(s(s(s(s(z)))))),z)
Called: add(s(s(s(s(_319)))),_319,_321)
Called: add(s(s(s(s(z)))),s(s(s(s(s(s(s(s(z)))))))),z)
Called: add(s(s(s(s(s(_323))))),_323,_325)
...

    Hope this helps.