how to stop prolog from examining impossible solutions infinitely?

Question

suppose the following program:

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

/* 0+b=b */
plus(0,B,B) :- nat(B).
/* (a+1)+b = c iff a+(b+1)=c */
plus(s(A),B,C) :- plus(A,s(B),C).

it works great for adding two numbers, but when i attempt a query of the following sort:

plus(Z,Z,s(0)).

it goes on to search possible values for Z long after it should be obvious that there is no solution (i.e. Z>s(0))

i'm familiar with the cut(!) operator and my intuition says the solution has something to do with it, i'm just not sure how to use it in this case.

Answer 1

!/0 is quite consistently not a good solution for such problems. It typically leads to loss of valid solutions for more general queries.

Instead, consider using finite domain constraints, which work perfectly well in this case:

?- use_module(library(clpfd)).
true.

?- Z + Z #= 0.
Z = 0.

?- Z + Z #= 0, Z #> 0.
false.

EDIT: A possible solution without CLP(FD), as requested:

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

Answer 2

So what you are here into is to understand the precise termination properties of a particular program. Prolog is here quite different to other programming languages since it has a relatively complex execution mechanism. In particular backtracking is quite intertwined with "normal resolution" and then combined with unification.

The easiest way to understand the problem with your original program is to consider the following failure slice (see the link for other examples):

plus(0,B,B) :- false, nat(B).
plus(s(A),B,C) :- plus(A,s(B),C), false.

If this tiny program will not terminate, then also your original program will not terminate. So we can consider the question when this program will not terminate, first.

Consider the third argument: There is simply a variable C that is passed along. Nobody is interested in its value (in this fragment). So the third argument will have no influence on termination whatsoever!

Worse, also the second argument is just a free variable B in the head, thus again, the argument will never influence whether or not this fragment terminates.

And thus: If you want that this fragment terminates, the first argument has to be known. Otherwise the program will loop. You can also use a termination inferencer to to see this yielding as termination condition:

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

The best seems to be to reformulate your program. Giving you the following termination condition:

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

In Prolog, we commonly like to generalize programs even further, accepting also some unexpected solutions while improving its termination condition to an even better condition:

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

However, this last version now admits solutions that are not always acceptable. E.g. plus(0, nonnumber, nonnumnber) now succeeds, whereas you might want it to fail.

Of course, you might also do some experiments with cuts, but be warned, using cut is extremely error-prone. At least you should combine it with appropriate tests which often nix the "efficiency gain".

Answer 3

i realized i was approaching it the wrong way, what i needed was not a cut(!) but a different set of rules that find X and Y by "breaking down" Z until it reaches 0, since X and Y are only incremented when Z is decremented, they will never be given impossible values :

plus(0,0,0).
plus(s(A),B,s(C)) :- plus(A,B,C).
plus(0,s(B),s(C)) :- plus(0,B,C).