Consider the following logic program:
p(b) :- p(b).
p(X) :- r(b).
p(a) :- p(a).
r(Y).
For what terms t does the evaluation of the goal p(t) terminate and which does it not?
What you want is to determine all the queries that do not terminate. And I assume you mean terminate universally. That is, we are not only looking at the first answer, but we look at all of them.
There is a very quick answer to this, provided your program is pure, monotonic: Simply take the most general query. That is, if there is any possibility for any term T
to make p(T)
not terminating, then p(X)
will be non-terminating too.
If we want to known more, we have to look closer. With a failure-slice we may narrow down actual reasons for non-termination. By inserting goals false
into your program, we are reducing the number of inferences that are possible for a query. But if the remaining program still permits infinitely many inferences, we have found a loop. In this case:
p(b) :- false, p(b).p(X) :- false, r(b). p(a) :- p(a), false.r(Y) :- false.
Is one minimal failure-slice. That is, p(a)
will not terminate. Beware, however, that
simply querying p(a)
(in your original program) will succeed, you need to insist to look at further answers:
?- p(a). true % there is one answer ; loops. % loops "on backtracking"
To save you the labor of asking for further answers, simply use p(a), false
instead.
There is another minimal failure-slice:
p(b) :- p(b), false.p(X) :- false, r(b).p(a) :- false, p(a).r(Y) :- false.
See failure-slice for more examples.