We are implementing diagnostic tools for explaining unexpected universal non-termination in pure, monotonic Prolog programs—based on the concept of the failure-slice.
As introduced in
the paper "Localizing and explaining reasons for nonterminating logic programs with failure slices", goals false/0
are added at a number of program points in an effort to reduce the program fragment sizes of explanation candidates (while still preserving non-termination).
So far, so good... So here comes my question1:
Why are there N+1 program points in a clause having N goals?
Or, more precisely:
How come that N points do not suffice? Do we ever need the (N+1)-th program point?
Couldn't we move that
false
to each use of the predicate of concern instead?Also, we know that the program fragment is only used for queries like
?- G, false.
Footnote 1: We assume each fact foo(bar,baz).
is regarded as a rule foo(bar,baz) :- true.
.
Why are there N+1 program points in a clause having N goals? How come that N points do not suffice?
In many examples, not all points are actually useful. The point after the head in a predicate with a single clause is such an example. But the program points are here to be used in any program.
Let's try out some examples.
A fact is a clause with zero goals. Now even a fact may or may not contribute to non-termination. As in:
?- p.
p :-
q(1).
p.
q(1).
q(2).
We do need a program point for each fact of q/1
, even if it has no goal at all, since the minimal failure slice is:
?- p, false. p :- q(1), p, false. q(1).q(2) :- false.
p :- q, p. p :- p. q :- s. s. s :- s.
So here the question is: Do we need two program points in q/0
? Well yes, there are different independent failure slices. Sometimes with false
in the beginning, and sometimes at the end.
What is a bit confusing is that the first program point (that is the one in the query) is always true
, and the last is always false
. So one could remove them, but I think it is clearer to leave them, as a false
at the end is what you have to enter into Prolog anyway. See the example in the Appendix. There, P0 = 1, P8 = 0
is hard coded.