[net.lang.prolog] Negation Problem And Solution

OKeefe.R.A.@EDXA@sri-unix.UUCP (08/18/83)

From:  Richard  HPS (on ERCC DEC-10)  <OKeefe.R.A.@EDXA>

As I wrote the file in question ( Not.Hlp ), I am replying to the
following message ( lines beginning with @ ).

@   Date: Monday, 15 Aug 1983 16:41-PDT
@   From: Narain@Rand-Unix
@   Subject: Problem With "Not"
@
@   In browsing through the Prolog utilities today I came across 
@   one that advised using \+ instead of not ( or something ) 
@   and noticed the following example:
@
@		bachelor(X):-not(married(X)),male(X).

It would have been helpful to state which.  In fact it was not a 
utility(Not.Pl) but the help file (Not.Hlp), which gave me some 
trouble finding it again.  Yes, I did recommend using \+ instead 
of not.  There is a very simple and very good reason for that.  
Because people kept complaining that 'not'/1 was an "incorrect" 
implementation of negation, David Warren changed the symbol for 
it to \+ ( which is as close as you can get to |-/- without 
rewriting the tokeniser ), standing for "is NOW unprovable".  
'\+'/1 is part of the Dec-10 Prolog system, 'not'/1 is NOT.  
'not'/1 is defined in the utility file Invoca.Pl, and if you 
don't happen to have loaded that file, your program won't do 
what you expect.

Please quote me correctly.  My example was:

    bachelor(X) :- \+married(X), male(X).

@   If we add:
@	
@   married(a).
@   married(b).
@   male(c).
@
@   then :-bachelor(Y). fails. This is what the example said or 
    implied.

That isn't what I said, but it is what I implied.  By the way, even 
if :- bachelor(Y).  were to succeed, it wouldn't tell you who was a 
bachelor. You would have to use ?- bachelor(Y) for that ( in DEC-10
C , EMAS, & Perq Prolog ).

@   But if we rewrite the rule as:
@
@   bachelor(X):-male(X),not(married(X)).
@
@   then :-bachelor(Y). succeeds with Y=c.

If it tells you what Y got bound to, it isn't Dec-10 Prolog or C 
Prolog. There IS a Prolog system where this works both ways round, 
so it is quite important to say which Prolog you are talking about.

If it succeeds, either you have the naive not/1 built into your 
Prolog or you have Invoca.Pl or Not.Pl loaded.  I'm not picking on 
this writer, really I'm not.  I'm just taking the opportunity  to 
point out that Dec-10 Prolog does not include a predicate not/1.  
This had been reported in this Digest as a bug by someone who 
didn't get ( or read ? ) the current manual.

@   I think this is serious since the order of literals should not
@   affect what the program computes, only its efficiency if at all.

Come off it!  Consider the following:

          p(X) :- var(X), X=a.
          p :- read(X), write(X).

It is explicitly stated in Clocksin and Mellish, and in the Dec-10 
Prolog manual, that the Prolog evaluation strategy is top to bottom
for clauses and >>left to right<< for goals.  Goal order is very 
definitely part of the language definition.  It isn't just a matter 
of "efficiency" either. There are some problems where one goal 
ordering works just fine, and others fail to terminate.  Agreed, 
a pure logic-based language would not have this problem.  ( Yes, 
though I'm defending Dec-10 Prolog, I do agree that it is a problem 
when you are learning the language.  After a while you get used 
to thinking about data-flow and it stops bothering you. )

@  The problem arises since at runtime the argument to "not" 
@  contains a variable.  This changes the meaning of not(X) to:
@  there exists a Y such that not(married(Y)). In which case Y 
@  may be bound to any element in the set:
@  Herbrand-Universe for the program - {Y such that married(Y) 
@  be derivable} a potentially infinite set.

NO!! \+p(X) is a negation, right?  And variables on the right hand 
side of the clause arrow are implicitly EXISTENTIALLY quantified, 
aren't they? And (not exists X|p(X)) is (forall X|not p(X)) 
according to the logic texts.  So the meaning of \+p(X), when X is 
a variable, is:

               is it true that there is NO substitution
                     for X which makes p(X) true?

What the Dec-10 system does in this case ( I.e. check whether there
is an X such that married(X)) is CORRECT, it is just surprising if 
you don't think about the effect the negation has on that 
quantifier.  My interpretation of the negation problem is NOT 
that Dec-10 Prolog gets negation-with-variables wrong, BUT

   - there are TWO possible readings ( forall not, exists not )
   - some people expect one reading, some the other
   - Dec-10 Prolog only supplies ONE ( which I claim is correct )
	- people wanting the other don't realise they can't have it

Negation as failure has a lot of nice properties, see Llyod et al in 
the latest IJCAI Proceedings.  However, it ONLY has these properties 
when the negated goal is GROUND.  ( The Dec-10 treatment of \+p(X)
can be very useful on occasion, but there is no known theory 
for it. )

There are three solutions to this problem.

1. Always write generators (things that bind X) before tests (such as 
   \+p(X)). Rely on your own skill to always get it right, once you
   have worked out just what Dec-10 Prolog, C Prolog, PDP-11 Prolog, 
   Prolog-X, Expert Systems Ltd Prolog, PopLog, ... do.  A rule of
   thumb is to remember that negation never binds anything.

2. As 1, but use the utility Not.Pl to check at run-time that your 
   negated goals are in fact ground.  That's what it's there for.

3. Use a different Prolog system, which will suspend a negated goal 
   until it is ground, so that even if the generator comes after the 
   test it will run first.

In the long run, method 3 is the one to go for.  There is a coroutine
package available for the Dec-10, which can do this.  It runs at about
half the speed of the normal Dec-10 interpreter.  Better still, there
is a Prolog system called MU Prolog which was written at the University
of Melbourne, Australia, and is distributed by them, which has 
coroutining built in.  The bachelor example works just fine either
way around in MU Prolog.  MU Prolog is not quite in the Edinburgh 
tradition.  They deliberately decided to go for clarity and closeness
to logic rather than efficiency ( E.g. they haven't got a compiler
and don't care ), but their interpreter seems to be fast enough.  It
is written in C, runs on a variety of machines, and costs ( I think ) 
$100 Australian.  It also has ( or will soon have ) an efficient 
extensible hashing scheme for accessing external data, which is 
something almost all other Prologs ( including Dec-10 ) lack.

This message may look as though I'm holding two incompatible 
posistions.  They aren't really.  Position 1 is

   - ordering IS of great importance in most Prologs.
      There is nothing special in negation wanting a particular 
      order. Just consider what would happen if you moved the 
      cuts...
   - if you want efficiency, go for Dec-10 Prolog.


Position 2 is

   - ordering should NOT be important in a logic programming language.
   - MU Prolog comes closer to being a logic programming language than
      Dec-10 Prolog does, while remaining usable for real programs.

Here, by the way, is the file in question, in case you haven't got it.
The utility it describes is available in the <PROLOG> directory as
described in an earlier volume of this Digest.  I hope this message is
some help, and in case it gives offence, I apologise in advance.

File: Util:Not.Hlp	Author: R.A.O'Keefe	Updated: 12 July 1983

#source.
The simple-minded not/1 lives in Util:Invoca.Pl.
Whenever you could use it, you are strongly recommended to use \+ .
The suspicious not/1 lives in Util:Not.Pl.

#purpose.
The simple-minded not/1 was for compatibility with a long-dead version
of Dec-10 Prolog.  It has been retained because some other Prologs use
it.  However, it is always better to use \+ in Dec-10 Prolog, and it
is no worse in C Prolog.

There are problems with negated goals containing universally 
quantified variables.  For example, if you write

	bachelor(X) :- \+married(X), male(X).

you will not be able to enumerate bachelors.  To help you detect such
errors, there is a suspicious version of not/1 which will report any
negated goals containing universally quantified variables.  

#commands.
The source only defines one public predicate: not/1.

If it detects an error, not/1 will switch on tracing and enter a
break.

not/1 understands the existential quantifier ^ .  See the description
of bagof and setof in the Prolog manual to find out what that means.