Double negation and execution model in Prolog
prolog, prolog-abstract-interpretation
Solution
When you reach the last step:
- RESOLVENT: !, fail, !, fail
the cut `!` here means, "erase everything". So the resolvent becomes empty. (this is faking it of course, but is close enough). cuts have no meaning at all here, the first `fail` says to flip the decision, and 2nd `fail` to flip it back. Now resolvent is empty - the decision was "YES", and remains so, twice flipped. (this is also faking it ... the "flipping" only makes sense in the presence of backtracking).
You can't of course place a cut `!` on the list of goals in the resolvent, as it is not just one of the goals to fulfill. It has an operational meaning, it normally says "stop trying other choices" but this interpreter keeps no track of any choices (it "as if" makes all the choices at once). `fail` is not just a goal to fulfill too, it says "where you've succeeded say that you didn't, and vice versa".
So may I presume that the execution model in textbooks is not precisely what Prolog uses?
yes of course, the real Prologs have `cut` and `fail` unlike the abstract interpreter that you referred to. That interpreter has no explicit backtracking and instead has multiple successes by magic (its choice is inherently non-deterministic as if all the choices are made at once, in parallel - real Prologs only emulate that through sequential execution with explicit backtracking, to which the `cut` is referring - it simply has no meaning otherwise).
Problem
I am trying to understand why Prolog implementations do not behave according to the execution model in textbooks -- for example, the one in the book by Sterling and Shapiro's "The Art of Prolog" (chapter 6, "Pure Prolog", section 6.1, "The Execution Model of Prolog"). The execution model to which I refer is this (page 93 of Sterling & Shapiro): Input: A goal G and a program P Output: An instance of G that is a logical consequence of P, or no otherwise Algorithm: ``` Initialize resolvent to the goal G while resolvent not empty: choose goal A from resolvent choose renamed clause A' <- B_1, ..., B_n from P such that A, A' unify with mgu θ (if no such goal and clause exist, exit the "while" loop) replace A by B_1, ..., B_n in resolvent apply θ to resolvent and to G If resolvent empty, then output G, else output NO ``` Additionally (page 120 of the same book), Prolog chooses goals (`choose goal A`) in left-to-right order, and searches clauses (`choose renamed clause ...`) in the order they show up in the program. The program below has a definition of `not` (called `n` in the program) and one single fact. ``` n(X) :- X, !, fail. n(X). f(a). ``` If I try to prove `n(n(f(X)))`, it succeeds (according to two textbooks and also on SWI Prolog, GNU Prolog and Yap). But isn't this a bit strange? According to that execution model, which several books expose, this is what I would expect to happen (skipping renaming of variables to keep things simple, since there would be no conflict anyway): RESOLVENT: `n(n(f(Z)))` unification matches `X` in first clause with `n(f(Z))`, and replaces the goal with the tail of that clause. RESOLVENT: `n(f(Z)), !, fail`. unification matches again `X` in the first clause with `f(Z)`, and replaces the first goal in the resolvent with the tail of the clause RESOLVENT: `f(Z), !, fail, !, fail`. unification matches `f(Z)` -> success! Now this is eliminated from the resolvent. RESOLVENT: `!, fail, !, fail`. And "`!, fail, !, fail`" should not succeed! After the cut there is a fail. End of story. (And indeed, entering `!,fail,!,fail` as a query will fail in all Prolog systems that I have access to). So may I presume that the execution model in textbooks is not precisely what Prolog uses? edit: changing the first clause to `n(X) :- call(X), !, fail` makes no difference in all Prologs I tried.