# The semantics of (Goal,false)

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 `G` fails, then `G,false` fails. (2)
• If `G` throws, then `G,false` throws. (3)
• If `G` doesn’t terminate, then `G,false` doesn’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 `G`s, 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 `G` throws `Ball`, `G,false` throws `Ball`.
• If `G` doesn’t terminate, `G,false` doesn’t terminate.
• If `G` yields infinite choice points upon backtracking, `G,false` doesn’t terminate.
• Otherwise, `G,false` fails.

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

Have you considered

1. Do any of the hypothesis use something beyond the formal definition of SLD resolution? (thinking exception).
2. How the Prolog code relates to a Byrd Box?
3. Looking at how the Prolog code is translated into lower level instructions? (For SWI-Prolog the VM instructions)

EDIT

I don’t have this book yet but it seems to have what you seek.

“Foundations of Logic Programming” 2nd ed. by John W Lloyd (WorldCat)

I’ll check it out, thanks.

Here is a suggestion that perhaps you might try.

Prolog is more than SLD resolution, SLDNF, SLD resolution with cut, …

SWI-Prolog also has dialects, e.g.

``````eclipse
hprolog
iso
sicstus
sicstus4
swi
xsb
yap
``````

It would be nice if there were dialects for SLD resolution, SLDNF, SLD resolution with cut, …

McCabe in his Logic and Objects relates to the G, false construction (p5), when discussing soundness of programming languages.

He critiques this constructions because its interpretation can lead to ambiguity. Did G fail, or did G succeed with false failing the conjunction.

A client code calling such a construction would not be able to know which … hence, in my mind this could in fact be a (so called) code-smell to be avoided.

Dan

The dialect system is there to resolve (some) compatibility issues with other Prolog systems. It notably does not allow changing SLD resolution. Most of that can only be done using program transformation or meta-interpretation as we do in s(CASP).

1 Like

Here’s what I found in McCabe 1989 (thanks for pointing me to this treasure!):

we do not like to have unpleasant surprises especially not in programming languages.
There are a number of features in Prolog which the careful Prolog programmer stays well clear of; for example the `repeat-cut-fail` combination.
This … often leads to extremely obscure programs which are difficult to debug.

(Page 16)

The fact that this construct is non-trivial to reason about is exactly the point of my original point, so I fully agree at that level.
On the other hand this construct is found in abundance in the library and packages of SWI-Prolog (is the author a careful Prolog programmer in this case? I don’t know but I think the results speak for themselves), so whether I like `(G,false)` or not it should’t be ignored IMO if we want to reason about Prolog code.

1 Like

Indeed since its used in “legacy” code one has to know how to reason about it – however, after reading McCabe, i classified it as code smell and try to be explicit about looping and failure.

Also, O’Keefe’s Craft of Prolog book which i keep rereading in the hope to understand yet another tidbit helped me understand further code smells, such as cuts in client code when it really should be in the called code … something i carelessly did sprinkle across my code before

Dan

Sometimes yes, sometimes no 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 `goto` in imperative languages: it is a bad idea, unless it is a good idea

2 Likes

Here’s another interesting use of `fail` … useful but makes my head hurt …
https://github.com/SWI-Prolog/contrib-protobufs/blob/1bce71d445593a399c79a44106aa92478e20d1d4/eventually_implies.pl

Indeed – i can’t get my head around the operational description of this …