# The semantics of (Goal,false) **URL:** \ **Category:** Nice to know\ **Created:** [October 31, 2021, 7:39am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616 "2021-10-31T07:39:13Z")\ **Posts on this page:** 11\ **Page:** 1
**Author:** ![oskardrums](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/oskardrums/32/3594_2.png) [@oskardrums](https://swi-prolog.discourse.group/u/oskardrums)\ **Post date:** [October 31, 2021, 7:39am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/1 "2021-10-31T07:39:13Z")
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: ```prolog ?- [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: ```prolog ?- [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: ```prolog ?- [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?.. ---
**Author:** ![EricGT](https://avatars.discourse-cdn.com/v4/letter/e/f1d935/32.png) [@EricGT](https://swi-prolog.discourse.group/u/EricGT)\ **Post date:** [October 31, 2021, 8:01am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/2 "2021-10-31T08:01:53Z")
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** > [@oskardrums](#): > > suggested references 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](http://www.worldcat.org/oclc/864586957)) ---
**Author:** ![oskardrums](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/oskardrums/32/3594_2.png) [@oskardrums](https://swi-prolog.discourse.group/u/oskardrums)\ **Post date:** [October 31, 2021, 11:19am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/3 "2021-10-31T11:19:37Z")
> [@EricGT](#): > > 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](http://www.worldcat.org/oclc/864586957)) I’ll check it out, thanks. ---
**Author:** ![EricGT](https://avatars.discourse-cdn.com/v4/letter/e/f1d935/32.png) [@EricGT](https://swi-prolog.discourse.group/u/EricGT)\ **Post date:** [November 1, 2021, 9:07pm UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/4 "2021-11-01T21:07:36Z")
Here is a suggestion that perhaps you might try. Prolog is more than [SLD resolution](https://en.wikipedia.org/wiki/SLD_resolution), [SLDNF](https://en.wikipedia.org/wiki/SLD_resolution#SLDNF), SLD resolution with cut, … SWI-Prolog also has [dialects](https://github.com/SWI-Prolog/swipl/tree/master/library/dialect), e.g. ```prolog eclipse hprolog iso sicstus sicstus4 swi xsb yap ``` It would be nice if there were dialects for [SLD resolution](https://en.wikipedia.org/wiki/SLD_resolution), [SLDNF](https://en.wikipedia.org/wiki/SLD_resolution#SLDNF), SLD resolution with cut, … ---
**Author:** ![grossdan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/grossdan/32/23_2.png) [@grossdan](https://swi-prolog.discourse.group/u/grossdan)\ **Post date:** [November 2, 2021, 6:58am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/5 "2021-11-02T06:58:57Z")
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 ---
**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\ **Post date:** [November 2, 2021, 7:36am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/6 "2021-11-02T07:36:42Z")
> [@EricGT](#): > > It would be nice if there were dialects for [SLD resolution](https://en.wikipedia.org/wiki/SLD_resolution), [SLDNF](https://en.wikipedia.org/wiki/SLD_resolution#SLDNF), SLD resolution with cut, … 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). ---
**Author:** ![oskardrums](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/oskardrums/32/3594_2.png) [@oskardrums](https://swi-prolog.discourse.group/u/oskardrums)\ **Post date:** [November 2, 2021, 7:39am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/7 "2021-11-02T07:39:37Z")
Here’s what I found in [McCabe 1989](https://spiral.imperial.ac.uk/bitstream/10044/1/47568/2/McCabe-FGC-1989-PhD-Thesis.pdf) (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. ---
**Author:** ![grossdan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/grossdan/32/23_2.png) [@grossdan](https://swi-prolog.discourse.group/u/grossdan)\ **Post date:** [November 2, 2021, 8:01am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/8 "2021-11-02T08:01:27Z")
> [@oskardrums](#): > > On the other hand this construct is found in abundance in the library and packages of [SWI-Prolog](https://www.swi-prolog.org/pldoc/doc_for?object=manual) 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 ---
**Author:** ![jan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/jan/32/4_2.png) [@jan](https://swi-prolog.discourse.group/u/jan)\ **Post date:** [November 2, 2021, 12:26pm UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/9 "2021-11-02T12:26:22Z")
> [@oskardrums](#): > > is the author a careful Prolog programmer in this case 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 🙂 ---
**Author:** ![peter.ludemann](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/peter.ludemann/32/48_2.png) [@peter.ludemann](https://swi-prolog.discourse.group/u/peter.ludemann)\ **Post date:** [November 2, 2021, 6:15pm UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/10 "2021-11-02T18:15:09Z")
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](https://github.com/SWI-Prolog/contrib-protobufs/blob/master/eventually_implies.pl) ---
**Author:** ![grossdan](https://yyz2.discourse-cdn.com/free1/user_avatar/swi-prolog.discourse.group/grossdan/32/23_2.png) [@grossdan](https://swi-prolog.discourse.group/u/grossdan)\ **Post date:** [November 3, 2021, 6:11am UTC](https://swi-prolog.discourse.group/t/the-semantics-of-goal-false/4616/11 "2021-11-03T06:11:55Z")
> [@peter.ludemann](#): > > useful but makes my head hurt … Indeed – i can’t get my head around the operational description of this …