Double negation and execution model in Prolog

Question

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.

Answer 1

Your program is not a pure Prolog program, since it contains a !/0 in n/1. You may ask yourself the simpler question: With your definitions, why does the query ?- n(f(X)). fail although there clearly is a fact n(X) in your program, meaning that n(X) is true for every X, and should therefore hold in particular for f(X) as well? This is because the program's clauses can no longer be considered in isolation due to the usage of !/0, and the execution model for pure Prolog cannot be used. A more modern and pure alternative for such impure predicates are often constraints, for example dif/2, with which you can constrain a variable to be distinct from a term.

Answer 2

The caption below does tell you what this particular algorithm is about:

Figure 4.2 An abstract interpreter for logic programs

Also, its description reads:

Output: An instance of G that is a logical consequence of P, or no otherwise.

That is, the algorithm in 4.2 only shows you how to compute a logical consequence for logic programs. It only gives you an idea for how Prolog actually works. And in particular cannot explain the !. Also, the algorithm in 4.2 is only able to explain how one solution ("consequence") is found, but Prolog tries to find all of them in a systematic manner called chronological backtracking. The cut interferes with chronological backtracking in a very particular manner which cannot be explained at the level of this algorithm.

You wrote:

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.

That misses one important point which you can read on page 120:

Prolog's execution mechanism is obtained from the abstract interpreter by choosing the leftmost goal ... and replacing the non-deterministic choice of a clause by sequential search for a unifiable clause and backtracking.

So it is this little addition "and backtracking" which makes things more complex. You cannot see this in the abstract algorithm.

Here is a tiny example to show that backtracking is not explicitly handled in the algorithm.

p :-
 q(X),
 r(X).

q(1).
q(2).

r(2).

We would start with p which is rewritten to q(X), r(X) (there is no other way to continue).

Then, q(X) is selected, and θ = {X = 1}. So we have r(1) as the resolvent. But now, we do not have any matching clause, so we "exit the while loop" and answer no.

But wait, there is a solution! So how do we get it? When q(X) was selected, there was also another option for θ, i.e. θ = {X = 2}. The algorithm itself is not explicit about the mechanism to perform this operation. It only says: If you make the right choice everywhere, you will find an answer. To get a real algorithm out of that abstract one, we thus need some mechanism to do this.

Answer 3

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

Answer 4

I think you got it almost right. The problem is here:

RESOLVENT: !, fail, !, fail.

The first ! and fail are from the second time that the first clause was matched. The other two are from the first time.

RESOLVENT: ![2], fail[2], ![1], fail[1].

The cut and fail have effect on the clause that is being processed -- NOT on the clause that "called" it. If you work through the steps again, but using these annotations, you'll get the right result.

![2], fail[2] makes the second call to n fail without backtracking. But the other call (the first) can still backtrack -- and it will:

RESOLVENT: n(_)

And the result is "yes".

This shows that Prolog keeps information about backtracking using a stack discipline. You may be interested in the the virtual machine that is used as a model for Prolog implementations. It is quite more complex than the execution model you mentioned, but the translation of Prolog into the VM will give you a much more accurate understanding of how Prolog works. This is the Warren Abstract Machine (WAM). The tutorial by Hasan Aït-Kaci is the best explanation you'll find for it (and it explains the cut, which if I remember correctly was absent from the original WAM description). If you are not used to abstract theoretical texts, you may try reading the text by Peter van Roy first: "1983-1993: the wonder years of sequential Prolog implementation". This article is clear and basically goes through the history of Prolog implementations, but giving special attention to the WAM. However, it does not show how the cut is implemented. If you carefully read it, however, you may be able to pick up Hasan's tutorial and read the section in which he implements the cut.

Answer 5

You have an extra level of nesting in your test goal:

n(n(f(X))

instead of:

n(f(X))

And indeed, if we try that, it works as expected:

$ prolog
GNU Prolog 1.3.0
By Daniel Diaz
Copyright (C) 1999-2007 Daniel Diaz
| ?- [user].
compiling user for byte code...
n(X) :- call(X), !, fail.
n(_X).
f(a).

user compiled, 4 lines read - 484 bytes written, 30441 ms

yes
| ?- f(a).

yes
| ?- n(f(a)).

no
| ?- n(f(42)).

yes
| ?- n(n(f(X))).

yes
| ?- n(f(X)).

no
| ?- halt.

So your understanding of Prolog is correct, your test case was not!

Updated

Showing the effects of negations of negations:

$ prolog
GNU Prolog 1.3.0
By Daniel Diaz
Copyright (C) 1999-2007 Daniel Diaz
| ?- [user].                                                            
compiling user for byte code...
n(X) :- format( "Resolving n/1 with ~q\n", [X] ), call(X), !, fail.
n(_X).
f(a) :- format( "Resolving f(a)\n", [] ).

user compiled, 4 lines read - 2504 bytes written, 42137 ms

(4 ms) yes
| ?- n(f(a)).
Resolving n/1 with f(a)
Resolving f(a)

no
| ?- n(n(f(a))).
Resolving n/1 with n(f(a))
Resolving n/1 with f(a)
Resolving f(a)

yes
| ?- n(n(n(f(a)))).
Resolving n/1 with n(n(f(a)))
Resolving n/1 with n(f(a))
Resolving n/1 with f(a)
Resolving f(a)

no
| ?- n(n(n(n(f(a))))).
Resolving n/1 with n(n(n(f(a))))
Resolving n/1 with n(n(f(a)))
Resolving n/1 with n(f(a))
Resolving n/1 with f(a)
Resolving f(a)

yes
| ?- halt.