Double negation and execution model in Prolog

Question

I’m trying to understand why the Prolog implementations do not behave according to the execution model in textbooks - for example, in Sterling and Shapiro's book “The Art of Prolog” (chapter 6, “Clean Prolog”, section 6.1, “Prolog Execution Model”).

The performance model to which I belong is (p. 93 Stirling and Shapiro):

Entrance: Goal G and Program P

Conclusion: An instance of G, which is a logical consequence of P, or else

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 selects goals ( choose goal A ) in the order from left to right and searches for offers ( choose renamed clause ... ) in the order in which they are displayed in the program.

The program below has the definition of not (called n in the program) and one fact.

 n(X) :- X, !, fail. n(X). f(a). 

If I try to prove n(n(f(X))) , it will succeed (according to two tutorials, as well as SWI Prolog, GNU Prolog and Yap). But isn't that weird? According to this execution model, which several books put up, this is what I would expect (skipping the renaming of variables so that everything is simple, since there will be no conflict anyway):

• RESOLVENT: n(n(f(Z)))

  Union

• matches X in the first sentence with n(f(Z)) and replaces the target with the tail of that sentence.

• RESOLVENT: n(f(Z)), !, fail .

• the union again combines X in the first section with f(Z) and replaces the first target in the resolution with the tail of the sentence

• RESOLVENT: f(Z), !, fail, !, fail .

• the union corresponds to f(Z) → success! Now this is excluded from the resolvent.

• RESOLVENT: !, fail, !, fail .

And " !, fail, !, fail " should not succeed! After the cut, a failure occurs. The end of the story. (And indeed, input !,fail,!,fail , because the request will fail on all Prolog systems to which I have access).

So, can I assume that the execution model in textbooks is not what Prolog uses?

edit : changing the first sentence to n(X) :- call(X), !, fail does not make any difference in all the prologs I tried.

Answer 1

When you reach the last step:

• RESOLVENT:!, Fail,!, Fail

cut ! here means "erase everything." Thus, the resolvent becomes empty. (this, of course, pretends to be, but close enough). cuts do not make sense at all, the first fail says to flip the solution, and the 2nd fail to throw it back. Now the resolution is empty - the solution was “YES”, and it remains so, it turned over twice. (this also pretends ... "flipping" makes sense only if there is a return stroke).

You cannot, of course, put a cut ! to the list of goals in the resolution, as this is not only one of the goals of fulfillment. It has operational meaning, it is usually said: “stop trying other options”, but this interpreter does not track any choices (it “as if” makes all the options at once). fail is not just a goal to fulfill it, it says: "Where you managed to say that you are not and vice versa ."

So, can I assume that the execution model in textbooks is not what Prolog uses?

yes, of course, real Prologs have cut and fail , unlike the abstract interpreter you were talking about. This interpreter does not have an explicit return and instead has several successes in magic (its choice is not inherently deterministic , as if all selections were performed immediately, in parallel - real Prologs only emulate this by sequential execution using explicit backtracking, to which refers to cut - it just doesn't make sense otherwise).

Answer 2

The heading below will tell you what this particular algorithm is:

Figure 4.2 Abstract interpreter for logical programs

In addition, his description reads:

Conclusion: Instance G , which is a logical consequence of P , or not.

That is, the algorithm in 4.2 only shows how to calculate the logical consequence for logical programs. This only gives you an idea of ​​how Prolog works. And, in particular, can not be explained ! . In addition, the algorithm in 4.2 can only explain how to find one solution (the “consequence”), but Prolog tries to find all of them in a systematic way called the chronological backtrack. The cut interferes with the chronological countdown in a very specific way that cannot be explained at the level of this algorithm.

You wrote:

Additionally (page 120 of the same book), Prolog selects goals (choose goal A) in the order from left to right and searches for offers (choose renamed clause ...) in the order in which they are displayed in the program.

This will skip one important point that you can read on page 120:

The Prolog execution engine is obtained from the abstract interpreter, choosing the leftmost target ... and replacing the non-deterministic choice of the sentence with a sequential search for a unified sentence and discarding .

So, this is a small “and rollback” addition, which complicates the situation. You cannot see this in an abstract algorithm.

Here is a tiny example showing that the algorithm does not explicitly handle backtracking.

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

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

Then q(X) is chosen, and θ = { X = 1}. So, as a resolvent, we have r(1) . But now we don’t have any corresponding sentence, 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 chosen, there was also another option for θ, that is, θ = { X = 2}. The algorithm itself does not reveal the mechanism for performing this operation. He only says: if you make the right choice everywhere, you will find the answer. To get a real algorithm from this abstract, we need some mechanism for this.

Answer 3

Your program is not a pure Prolog program, since it contains a! / 0 in n / 1. You can ask yourself a simpler question: with your definitions, why the request ?- n(f(X)). fails, although there is clearly the fact n (X) in your program, which means that n (X) is true for every X, and therefore has to be done in particular for f (X)? This is because the program offers can no longer be considered in isolation due to use! / 0, and the execution model for pure Prolog cannot be used. A more modern and cleaner alternative for such unclean predicates is often related to constraints, such as dif / 2, with which you can restrict a variable other than the term.

Answer 4

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

 n(n(f(X)) 

instead:

 n(f(X)) 

And indeed, if we try this, it will work 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 true, your test case was not!

Update

Display negation negation effects:

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

Answer 5

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

 RESOLVENT: !, fail, !, fail. 

First! and failure the second time coincide with the first sentence. The remaining two - the first time.

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

Cutting and failing affect the offer being processed - NOT the offer that "caused" it. If you follow the steps again, but using these annotations, you will get the correct result.

![2], fail[2] makes the second call of n unsuccessful without backtracking. But another call (first) can still retreat - and it will:

 RESOLVENT: n(_) 

And the result is yes.

This shows that Prolog stores return information using stack discipline. You may be interested in a virtual machine that is used as a model for implementing Prolog. This is more complicated than the execution model that you mentioned, but moving Prolog to a virtual machine will give you a much more accurate idea of ​​how Prolog works. This is Warren Abstract Machine (WAM). Hasan Aït-Kaci's tutorial is the best explanation you will find for him (and this explains the cut that, if I remember correctly, was missing from the original WAM description). If you are not using abstract theoretical texts, first try reading Peter Van Roy’s text: “ 1983-1993: The Wonderful Years of the Prolog Progressive Implementation ” This article is understandable and mainly goes through the history of the Prolog implementation, but focuses on WAM. However, it does not show how the reduction is performed. However, if you read it carefully, you can pick up Hassan’s textbook and read the section in which he implements the cut.

Answer 6

While mats are correct in that your program is not a pure prologue (and this is relevant, since the title of the chapter is Pure Prolog), not only since you use the cut, but also after you write the predicates that handle other predicates (pure prologs are a subset of first-order logic), this is not the main problem; you just do not have enough backtracking

While you do have a cut, this will not be achieved until goal n (f (X)) is reached. However, as you know, this will not succeed, and therefore the prologue will back off and correspond to the second sentence.

I do not see how this will contradict the model described in 6.1 (and it would be difficult to believe that other books describe a model in which execution will continue after a failure and, thus, will allow other solutions to be cut). In any case, I find that, going to the conclusion that "Prolog implementations do not behave according to the execution model in the textbooks", it is very similar to "there is an error for the compiler", especially since the "counter example" behaves like it must (not (not (truth)) be true)