I’ve recently been thinking about the following question about the semantics of Prolog:
Given some Prolog goal G and SLD resolution, what do we know about the conjunction G, false?
I’ve come to ask myself this question while experimenting with static analysis for my Prolog code. I couldn’t find a clear answer in the literature, although I didn’t do a very thorough search. Are there any suggested references about static analysis / abstract interpretation for Prolog?
Anyway, here’s where I currently stand on this subject after doing some reading and some experimenting:
A purely logical reading of ,/2 as a conjunction would suggest that G,false fails for any goal G (1).
But we can easily produce a counter example to show that (1) needs some refinement:
?- [user].
% test that (G, false) fails regardless of G
|: test_hyp1(G) :- \+ (G, false).
|:
|: ^D% user://2 compiled 0.00 sec, 1 clauses
true.
?- test_hyp1(true). % holds for true/0.
true.
?- test_hyp1(false). % holds for false/0.
true.
?- test_hyp1(throw(ball)). % doesn't hold for throw/1!
ERROR: Unhandled exception: Unknown message: ball
?- [user].
|: loop :- loop;true.
|:
|: ^D% user://3 compiled 0.00 sec, 1 clauses
true.
?- test_hyp1(loop). % doesn't hold for loop/0!
% ...infinite loop...
^CAction (h for help) ? abort
% Execution Aborted
We can generalize from the above examples the following characterizations of G,false:
- If
Gfails, thenG,falsefails. (2) - If
Gthrows, thenG,falsethrows. (3) - If
Gdoesn’t terminate, thenG,falsedoesn’t terminate. (4)
And what do we know about G,false in the case that G succeeds?
The logical reading could still be salvaged if it were the case that if G succeeds, then G,false fails (5). Assuming (5) would entail, along with (2), that if G;true succeeds, then G,false fails (6).
But we can show that (6) does not in fact hold:
?- [user].
|: % For every goal G and inference limit L,
|: % if (G;true) can be proven in L inferences
|: % then \+ (G,false) can be proven in L + 1024 inferences
|: test_hyp6(L, G) :-
|: ( call_with_inference_limit(\+ \+ (G;true), L, R), R \== inference_limit_exceeded
|: -> plus(L, 1024, L2), % just to be on the safe side
|: call_with_inference_limit(\+ (G,false), L2, R2), R2 \== inference_limit_exceeded
|: ; true
|: ).
|: ^D% user://6 compiled 0.01 sec, 1 clauses
true.
% holds for true/0, false/0, !/0, and loop/0.
?- maplist(test_hyp6(2048), [true, false, !, loop]).
true.
?- test_hyp6(2048, repeat). % doesn't hold for repeat/0!
false.
?- test_hyp6(2048, length(_, _)). % doesn't hold for length(_, _)!
false.
We can see that G;true does not guarantee \+ (G,false) and (5) does not hold.
A more explicit example:
?- [user].
|: pool :- true;pool. % the opposite of loop/0, equivalent to repeat/0
|:
|: ^D% user://9 compiled 0.00 sec, 1 clauses
true.
?- pool.
true .
?- pool;true.
true .
?- \+ (pool,false).
% ...infinite loop...
^CAction (h for help) ? abort
% Execution Aborted
In general, G,false may, for some Gs, enter an infinite loop even when G succeeds, by virtue of backtracking.
The key characteristic of this class of goals is that, like pool/0 above and the classic definition of repeat/0, they always succeed with a choice point that always leads to a goal that is a variant of the original goal. Such goals yield infinite choice points upon backtracking.
To summarize, the semantics of G,false as a function of the semantics of G is given by:
- If
GthrowsBall,G,falsethrowsBall. - If
Gdoesn’t terminate,G,falsedoesn’t terminate. - If
Gyields infinite choice points upon backtracking,G,falsedoesn’t terminate. - Otherwise,
G,falsefails.
Now the next interesting question arises - how can we know in which of these branches a given goal G falls or at least in which branches G doesn’t fall?..
The construct was used in older code and some time critical code as it does not rely on garbage collection. There are also use cases in more recent code because it just does the right thing. This is IMHO similar to