Negation as Failure

Appeared in Volume 9/4, November 1996

ridoux@calypso.irisa.fr
Olivier Ridoux
20th May 1996

Fergus Henderson writes:
The issue of negation and if-then-else is important. The reason that Mercury and Goedel can handle negation and if-then-else in a logically sound manner is that their semantics are based on the Clark completion of the program. However, Lambda-Prolog's theoretical foundation is not based on the completion semantics, and in particular Lambda-Prolog's intuitionistic implication construct (an essential part of how it handles meta-progamming) would not make any sense in the completion semantics.

There has been some work on intuitionistic negation, but they do not have the operational appeal of negation-as-failure. I think there is a way negation-as-failure can be incorporated into LambdaProlog. However, the relation with implication will not be the classical one. This is not a problem since it is already the case that negation-as-failure does not behave classically (e.g. fail(fail(P)) is not equivalent to 'P').

fjh@mundook.cs.mu.oz.au
Fergus Henderson
20th May 1996

Negation-as-failure in Mercury and Goedel does behave "classically", i.e. it obeys the usual laws of predicate calculus. Indeed, both the Mercury compiler and the Goedel implementation will automatically replace 'not(not(P))' (or in Goedel '~ ~ P') with 'P' whenever it occurs.

ridoux@calypso.irisa.fr
Olivier Ridoux
21st May 1996

Consider the following example:

R :- not(P).
Q :- not(R).

T' :- X = X.       % or anything that makes T' true
R' :- not(P'), T'.
Q' :- not(R').

Olivier Ridoux writes:
Is it true that P and Q are equivalent in Mercury?

Yes, presuming they are both legal, the declarative and operational semantics of Q are exactly same as those of P.

The compiler is not guaranteed to generate exactly identical code - the operational semantics doesn't nail down every little detail of code generation. In this particular case, I think it probably would, if you enable optimization.

I'm assuming that P and Q are meta-variables here, i.e. they are supposed to stand for some predicates 'p' and 'q', possibly with some arguments variables.

ridoux@calypso.irisa.fr
Olivier Ridoux
22nd May 1996

Your assumption is correct.

I conclude that negated goals compute a solution substitution. Is that still negation-as-failure? It seems closer to constructive negation or similar devices.

fjh@mundook.cs.mu.oz.au
Fergus Henderson
22nd May 1996

I'm sorry, I didn't really explain things. "Presuming they are both legal" is an important phrase. In Mercury, negated goals are not allowed to bind any non-local variables. So if P above is a goal which binds some non-local variables (i.e. some of the arguments to R) then the code is not legal Mercury.

If you write a negation which would bind a non-local variable, the compiler will first try to reorder the code so that it can schedule a producer for that variable before the negation. If it can't do that, it will report a mode error.

lee@cs.mu.oz.au
Lee Naish
23rd May 1996

Fergus Henderson writes:
Negation-as-failure in Mercury and Goedel does behave "classically"

Using a rather strict meaning of "equivalent", as I think Olivier intends, Mercury and Goedel do not behave classically. In fact, P is not even equivalent to P. Because the clause selection rule is unspecified, P may succeed today and loop tomorrow; ie. different operational behaviour with the same declarative semantics.

Is this a problem? I think not. Such programs should be considered buggy, just like programs with errors which lead to wrong answers or type errors or syntax errors. What I believe we should be aiming for in logic programming languages is a nice declarative semantics, a nice procedural semantics, and a nice relationship between them for nice programs (niceness is partly a matter of personal taste).

In the conventional view of Horn Clause programs (pure Prolog without negation) nice programs are simply those which are syntactically correct. In Goedel, programs must also be well typed, and in Mercury they must be well moded to be considered nice. Introducing negation increases the richness of the language - the semantics is nicer - but there are also some nasty consequences. Much research in logic programming is involved in coming up with new models which move this nastiness around, trying to reduce it. The most obvious place for the nastiness to sit is with the relationship between the declarative and procedural semantics, hence this thread about NAF not behaving classically. A second possibility is to use a different declarative semantics, one which is closer to the procedural semantics (this makes the declarative semantics nastier). A third possibility is to adapt the procedural semantics, e.g. introduce fairness (which has nasty efficiency consequences). The final possibility, which I have advocated, is to expand the class of programs which are considered nasty, e.g. those which don't terminate. See http://www.cs.mu.oz.au/~lee/papers/prune for some discussion.

fjh@mundook.cs.mu.oz.au
Fergus Henderson
23rd May 1996

I agree with almost all of the points Lee Naish makes in his article. I do have a couple of comments, however.

Lee Naish writes:
Mercury and Goedel do not behave classically...

What Lee says above is not entirely true of Mercury.

I think it is useful to distinguish between operational semantics and behaviour: the operational semantics may specify a set of allowed behaviours. An implementation correctly implements a particular operational semantics iff the behaviour of programs run with that implementation is one of the behaviours allowed by the operational semantics. An operational semantics for which the set of behaviours allowed is always a singleton set could be called deterministic, but most existing programming languages have non-deterministic operational semantics.

In Mercury, 'P' and 'not(not(P))' always have the same operational semantics, presuming that both are legal. (As noted previously, in some circumstances 'P' may be legal but 'not(not(P))' may be a mode error.)

Does that mean that they have the same behaviour? Not necessarily. The same behaviour would be guaranteed only if you have a deterministic operational semantics.

We recently revised the definition of the operational semantics of Mercury, partly to deal with these conflicting aims. The situation in Mercury is a little bit complicated, because in order to satisfy the conflicting goals that Lee refers to in his article, we've defined two different operational semantics: a deterministic one called the "strict sequential" semantics, and a non-deterministic one called "commutative" semantics. Implementations of Mercury are required to support both. Since any implementation of the "strict sequential" semantics is also an implementation of the "commutative" semantics, this does not impose any additional difficulty on implementations. Users of Mercury may use whichever they prefer; the Univ. of Melbourne Mercury implementation allows users to select between them using command line options.

So in Mercury, 'P' and 'not(not(P))' always have the same operational semantics, whether you are using the "strict sequential" semantics or the "commutative" semantics, and since the "strict sequential" semantics is a deterministic semantics, this means that 'P' and 'not(not(P))' have exactly the same behaviour if you are using that operational semantics. In the "strict sequential" semantics, the clause selection rule is specified.

Interested readers should consult the "Semantics" chapter of the latest Mercury language reference manual, available from http://www.cs.mu.oz.au/mercury/doc/reference_manual.html#SEC33.