Prolog: for what terms t does the evaluation of the goal p(t) terminate and which does it not?

Question

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?

Answer 1

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.