next up previous contents
Next: Stratified Negation Up: Programming in Tabled Prolog Previous: Stratified Aggregation

Negation in XSB

Negation in the context of logic programming has received a lot of attention. Prolog implements a kind of negation-as-failure inference rule, succeeding the negation of a goal if the goal itself cannot be successfully proven. This implements a kind of closed-world assumption, in that a proposition is assumed to be false if it cannot be proven to be true. This is a useful operator, which can be used to represent (and program) interesting situations.

Consider the standard example of defining the predicate bachelor using the predicates married and male:

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

male(bill).
male(jim).

married(bill).
married(mary).

The rule says that an individual is a bachelor if it is male and it is not married. (\+ is the negation-as-failure operator in Prolog.) The facts indicate who is married and who is male. We can interrogate this program with various queries and we get the following:

| ?- [negation].
[Compiling ./negation]
[negation compiled, cpu time used: 0.1 seconds]
[negation loaded]

yes
| ?- bachelor(bill).

no
| ?- bachelor(jim).

yes
| ?- bachelor(mary).

no
| ?- bachelor(X).

X = jim;

no
| ?-
as expected. The closed-world assumption is applied here: for example, when there is no fact that says that jim is married, we assume that he is not married. Also when there is no fact saying that mary is male, we assume she is not.

Before we get completely carried away with using negation, we need to look at situations in which there are problems. There are two sources of problems: floundering and nonstratification. Let's first consider a floundering query and program. Say we wrote the bachelor rule as:

bachelor(X) :- \+ married(X), male(X).
This looks to be an equivalent definition, since after all, the comma is conjunction so the order of literals in the body of a program (as simple as this one) shouldn't matter. But now consider the results of the same queries as above when they are submitted to this program:
| ?- bachelor(bill).

no
| ?- bachelor(jim).

yes
| ?- bachelor(mary).

no
| ?- bachelor(X).

no
| ?-
The answers are fine for the specific queries concerning bill, jim and mary, but the general query asking for all bachelors fails, whereas we would expect it to generate the answer jim. The reason is that the generated subquery of \+ married(X) is able to prove married(X) is true (for X=bill (and X=mary as well)), and so \+ married(X) fails. The problem is that the implementation of the operator \+ only works when applied to a literal containing no variables, i.e., a ground literal. It is not able to generate bindings for variables, but only test whether subgoals succeed or fail. So to guarantee reasonable answers to queries to programs containing negation, the negation operator must be allowed to apply only to ground literals. If it is applied to a nonground literal, the program is said to flounder. Prolog systems in general allow the \+ operator to be applied to nonground literals and so the programmer may get unexpected results. Often another operator, not, is provided which acts just like \+ except that it gives an error message when applied to a nonground literal. (In XSB not and \+ give the same, unsafe, results.)

The other problem that may arise in programs with negation, that of nonstratification, is a bit more subtle. !!!Instead of this example, use shave/2 and say the barber shaves everyone who doesn not shave himself. Who shaves the barber?

shave(john,john). shave(bill,bill). shave(barber,X) :- not shaves(X,X).

:- shaves(barber,barber).

!!! Say we want to define a predicate, normal, that is true of all reasonable sets. A set is normal if it doesn't contain itself as a member. (A set containing itself is rather wierd; think about it.) So we give the rule:

normal(S) :- \+ in(S,S).
where the predicate in denotes membership. Now we want to have the constant n denote the set of all normal sets. So X is in n just in case X is a normal set. The following rule reflects this:
in(X,n) :- normal(X).
Now consider what happens if we ask this program whether n is a normal set: normal(n), which reduces to \+ in(n,n), which reduces to \+ normal(n). So to show that n is normal, we have to show that n is not normal. Clearly there is something a little odd here, and you may recognize a similarity to Russell's well-known paradox. The oddity is that the predicate normal is defined in terms of its own negation. Normally we consider rules to define predicates and this is an odd kind of cyclicity which we often want to avoid. Programs that avoid such cycles through negation in their definitions are called stratified programs. Notice that Prolog would go into an infinite loop whan asked queries that involve a cycle through negation.

XSB does not improve over Prolog in handling floundering queries; all calls to negative subgoals must be ground in XSB for the closed-world interpretation of negation to be computed. XSB does extend Prolog in allowing nonstratified programs to be evaluated, and we will discuss how it does that later in the chapter. However, first we will explore how we can use tabling with stratified programs to compute some interesting results.



 
next up previous contents
Next: Stratified Negation Up: Programming in Tabled Prolog Previous: Stratified Aggregation
David S. Warren
1999-07-31