prologfailure-slicenon-terminationlogical-purity

Prolog: redundant program points in failure-slice?


We are implementing diagnostic tools for explaining unexpected universal non-termination in pure, monotonic Prolog programs—based on the concept of the .

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..


Solution

  • 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.

    N = 0

    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.
    

    N = 1

    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.