How to stop the prologue from the endless study of impossible solutions?

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 fine for adding two numbers, but when I try to execute a query like this:

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

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

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

Answer 1

!/0 rather consistently is not a good solution for such tasks. This usually results in the loss of the correct solutions for more general queries.

Instead, consider using end-domain restrictions that work fine in this case:

 ?- use_module(library(clpfd)). true. ?- Z + Z #= 0. Z = 0. ?- Z + Z #= 0, Z #> 0. false. 

EDIT : Possible solution without CLP (FD), on request:

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

Answer 2

So, you are here to understand the exact properties of the completion of a particular program. The prologue here is completely different from other programming languages, because it has a relatively complex execution mechanism. In particular, backtracking is completely intertwined with “normal resolution” and then merged with aggregation.

The easiest way to understand the problem with your source program is to consider the following failure fragment (see 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 is not completed, then your original program will not be completed. Therefore, we can consider when this program will not be completed, first.

Consider the third argument: there is simply a C variable that is passed together. No one is interested in its value (in this fragment). Thus, the third argument will have no effect on termination at all!

Worse, the second argument is just the free variable B in the head, and again, the argument will never affect whether this fragment ends.

And thus: If you want this fragment to end, the first argument must be known. Otherwise, the program will loop. You can also use the termination terminator to see this , which gives a termination condition:

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

It is best to reformulate your program. Providing the following completion conditions :

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

In Prolog, we usually like to generalize programs even more, making some unexpected decisions, while improving the termination condition to an even better condition.

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

However, this latest version now allows solutions that are not always acceptable. For instance. plus(0, nonnumber, nonnumnber) now succeeds, while you may want it to work.

Of course, you can also do some abbreviation experiments, but be careful, using a cut is extremely error prone. At the very least, you should combine it with related tests, which often lead to "performance improvements."

Answer 3

I realized that I was approaching it wrong, I didn’t need a segment ( ! ), But a different set of rules that find X and Y by “destroying” Z until it reaches 0, since X and Y only increase with decreasing Z , 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).