library(inquisitor) to find impure constructs

[dcnorris]

Given a predicate in a Prolog program, I would like to identify any use it makes — whether direct or indirect — of impure constructs. So, build something like a call graph with a focus on impure leaves. Presumably, some kind of meta-interpretation would be required? Initially, I could be happy with manually 'whitelisting' certain library predicates (e.g., reif:if_/3) known to use constructs such as (->)/2 safely. But in conjunction with such a facility, it might be nice to be able to annotate code itself ... or even reason automatically about it to identify where impure constructs may be granted a special dispensation.

[hurufu]

If you would like I can implement PoC as part of #2602, by introduction of a simple list of excluded terms, but I expect way too many false positives, because a lot of code uses those constructs correctly.

Later I think it can go even further then simply looking for terms. For example if left argument of (->)/2 is ground at the point of call then it is safe to use in pure code. Hey even cut can be used by an experienced Prologer without damaging monotonicity of a predicate.

[dcnorris]

I would certainly give your library(warnings) a try, if it included this kind of feature!

[hurufu]

So I've assembled a short list of impure constructs, by groups:

1. _ -> _, _ -> _; _, \+ _
2. !
3. var/1, nonvar/1, ground/1, (also other non si type checks).
4. asserta/1, assertz/1, retract/1, retractall/1, abolish/1.
5. repeat – Useless in pure predicates
6. is/2, (>)/2, (<)/2, ...
7. random/1
8. write/1, writeq/1, nl/0, etc.
9. shell/1 and other predicates from library(os)
10. (=..)/2, functor/3 – Can be used to construct impure goals dynamically which will be undetectable by simple static check.
11. bb_get/2 and other access to global state

What do you think? Which ones do you consider for warnings?

[hurufu]

Some of those predicates will become suddenly pure if used correctly with freeze/2, when/2 or when_si/2.

UPDT: Actually the more I think the harder this problem gets :)

[hurufu]

After more thinking about how to approach it I believe that #2532 needs to be solved first. I would like to have better interface to term expansion, otherwise it would be a half-backed sometimes working sometimes not library :)

[UWN]

This is a highly desirable venture, but there are many obstacles in the way.

First, it is necessary to precisely define what the goal is. My attempt is just such a definition but not a concrete implementation. Just think of number 7 (call/N) which would necessitate some dynamic checking.

Then, there is the question what algebraic properties a predicate must hold. Externally (that it behaves like a real relation) but (for some) also internally (that it can be generalized or specialized). Clearly, more than one notion of purity will be needed.

Then, there is goal expansion which blurs those notions once again. Think of clpz which expands many constraints into half-procedural goals. How to handle this in such a framework.

Here is a slightly less ambitious task, that is very much related and still non-trivial: Identify programs that can run on any conforming DCG implementation. That is, where all uses of non-terminals are via phrase/2/3, where non-terminals are never predicate definitions etc.

[hurufu]

The last point with DCG actually seems quite hard to implement too, because there is no clear way to distinguish for example a --> "". from a(A, A)., and term expansion blurs it even more.

[dcnorris]

Are these impure constructs used in library(lists) okay with respect to the external|internal concepts above? How would I reason directly from the code to see that these are relations and/or generalizable?

length(Xs0, N) :-
   '$skip_max_list'(M, N, Xs0,Xs),
   !,
   (  Xs == [] -> N = M
   ;  nonvar(Xs) -> var(N), Xs = [_|_], resource_error(finite_memory,length/2)
   ;  nonvar(N) -> R is N-M, length_rundown(Xs, R)
   ;  N == Xs -> failingvarskip(Xs), resource_error(finite_memory,length/2)
   ;  length_addendum(Xs, N, M)
   ).
length(_, N) :-
   integer(N), !,
   domain_error(not_less_than_zero, N, length/2).
length(_, N) :-
   type_error(integer, N, length/2).

%% reverse(?Xs, ?Ys).
%
% Xs is the Ys list in reverse order
%
%     ?- reverse([1,2,3], [3,2,1]).
%        true.
%
reverse(Xs, Ys) :-
    (  nonvar(Xs) -> reverse(Xs, Ys, [], Xs)
    ;  reverse(Ys, Xs, [], Ys)
    ).

reverse([], [], YsRev, YsRev).
reverse([_|Xs], [Y1|Ys], YsPreludeRev, Xss) :-
    reverse(Xs, Ys, [Y1|YsPreludeRev], Xss).

[dcnorris]

It's almost as if a reified predicate var_t/2 would assist in formalizing this argument.

[dcnorris]

Actually, maybe an argument of this kind could be factored out, using if_ as a lemma.

[UWN]

Speaking of reverse, the first two arguments should be exchanged such that Y1 is not a fresh new variable. And the naming of Xss in inappropriate, it is not a list of lists.

The simplest proof obligation is to show first, that the first two arguments mean the same/can be exchanged without changing the meaning. Then, the condition nonvar(Xs) can be ignored.

As for length/2, its objective is to be backwards compatible with a naive version up to the very kind of error issued (i.e. the resource errors).

[dcnorris]

This reminds me of a passage from Karl Popper's Logic of Scientific Discovery

But it would be nice to firm up the basis provided by our most basic libraries!

[hurufu]

I do this kind of semi-formal reasoning every time when I write my Prolog code (and when I care about those properties), but a good formal foundation would be appreciated.

[hurufu]

My idea was to deduce safe mode declarations for any given predicate and add them to internal database for future reference. For example when during compilation I discover a fact: a(1) then I assert this mode(a(any)). Further if I find for example predicate b(X, A) :- X -> A = 1; A =0. then I assert mode(b(ground, any)). Also I need to traverse subgoals and meta-predicates, but only if it is decidable during compile time. This way I can deduce mode for which any predicate will behave monotonically.