Why is Prolog's failure by negation not considered logical negation?

Question

In many Prolog guides the following code is used to illustrate "negation by failure" in Prolog.

not(Goal) :- call(Goal), !, fail. 
not(Goal).

However, those same tutorials and texts warn that this is not "logical negation".

Question: What is the difference?

I have tried to read those texts further, but they don't elaborate on the difference.

Spinster

Answer 1

I like @TesselatingHeckler's answer because it puts the finger on the heart of the matter. You might still be wondering, what that means for Prolog in more concrete terms. Consider a simple predicate definition:

p(something).

On ground terms, we get the expected answers to our queries:

?- p(something).
true.

?- \+ p(something).
false.

?- p(nothing).
false.

?- \+ p(nothing).
true.

The problems start, when variables and substitution come into play:

?- \+ p(X).
false.

p(X) is not always false because p(something) is true. So far so good. Let's use equality to express substitution and check if we can derive \+ p(nothing) that way:

?- X = nothing, \+ p(X).
X = nothing.

In logic, the order of goals does not matter. But when we want to derive a reordered version, it fails:

?- \+ p(X), X = nothing.
false.

The difference to X = nothing, \+ p(X) is that when we reach the negation there, we have already unified X such that Prolog tries to derive \+p(nothing) which we know is true. But in the other order the first goal is the more general \+ p(X) which we saw was false, letting the whole query fail.

This should certainly not happen - in the worst case we would expect non-termination but never failure instead of success.

As a consequence, we cannot rely on our logical interpretation of a clause anymore but have to take Prolog's execution strategy into account as soon as negation is involved.

Weapon

hi @Weapon 0 thanks for elaborating. What you highlight is a peculiarity of prolog's design, that \+ p(X) is always false where X is unbound. As you say, prolog's designers chose this to always fail, even if logically it is not true. You later explain that ordering can change this because we can the ground the variable. My question, going back to the original question, is the reason we can't say negation by failure is the same as logical because of the incoherent design decision we just talked about - rather than issues of order? – Spinster

ps @Weapon I really appreciate your answer - it has helped more than anything I've seen the far. My last comment, poorly worded, is trying to disentangle the ordering of a query from the - what I think - is the core issue: that prolog's designers let \+ p(X) fail in all cases. – Spinster

The issue here is that in general \+ p(X) fails because if you try to derive p(X), you correctly get a counterexample with X=something. What happens in the \+ p(X), X = nothing case is that X is still unbound in the first goal of the query such that it already fails there without ever checking for X = nothing. This is due to the non-constructive way negation is defined. From a logical point of view it should be different though, because from ∃X ¬p(X) ∧ X = nothing i can certainly infer ¬p(nothing) ∧ nothing = nothing - it's just not what happens in Prolog. – Weapon

Answer 2

• Logical claim: "There is a black swan".

• Prolog claim: "I found a black swan".

Finding a black swan is strong support for the claim that there is one.

• Logical negation: "There isn't a black swan".

• Prolog negation: "I have not found a black swan".

This is not strong support for the claim. "Did you even look? Did you look over there?". The logical version has no room for black swans anywhere, the Prolog version could have poor quality code, computing limits to searching the entire planet down to swan size areas, time limits for how long to spend searching before stopping; it leaves room for a black swan somewhere which the code didn't find. At worst there are black swans all around but a mistake in the code meant it didn't search anywhere.

The logical negation doesn't need anyone to look anywhere, the claim stands alone separate from any proof or disproof. The Prolog logic is tangled up in what Prolog can and cannot prove using the code you write.

Popcorn

Answer 3

There are a couple of reasons why,

Insufficient instantiation

A goal not(Goal_0) will fail, iff Goal0 succeeds at the point in time when this not/1 is executed. Thus, its meaning depends on the very instantiations that happen to be present when this goal is executed. Changing the order of goals may thus change the outcome of not/1. So conjunction is not commutative.

Sometimes this problem can be solved by reformulating the actual query.

Another way to prevent incorrect answers is to check if the goal is sufficiently instantiated, by checking that say ground(Goal_0) is true producing an instantiation error otherwise. The downside of this approach is that quite too often instantiation errors are produced and people do not like them.

And even another way is to delay the execution of Goal_0 appropriately. The techniques to improve the granularity of this approach are called constructive negation. You find quite some publications about it but they have not found their way into general Prolog libraries. One reason is that such programs are particularly hard to debug when many delayed goals are present.

Things get even worse when combining Prolog's negation with constraints. Think of X#>Y,Y#>X which does not have a solution but not/1 just sees its success (even if that success is conditional).

Semantic ambiguity

With general negation, Prolog's view that there exists exactly one minimal model no longer holds. This is not a problem as long as only stratified programs are considered. But there are many programs that are not stratified yet still correct, like a meta-interpreter that implements negation. In the general case there are several minimal models. Solving this goes far beyond Prolog.

When learning Prolog stick to the pure, monotonic part first. This part is much richer than many expect. And you need to master that part in any case.

Hydrodynamics

hi @Hydrodynamics where can I read more about "minimal models"? – Spinster

Start with: p :- p. where p can be true or false to make this true. Prolog opts for false. – Hydrodynamics