10

Say I have the following theory:

a(X) :- \+ b(X).

b(X) :- \+ c(X).

c(a).

It simply says true, which is of course correct, a(X) is true because there is no b(X) (with negation as finite failure). Since there is only a b(X) if there is no c(X) and we have c(a), one can state this is true. I was wondering however why Prolog does not provide the answer X = a? Say for instance I introduce some semantics:

noOrphan(X) :- \+ orphan(X).

orphan(X) :- \+ parent(_,X).

parent(david,michael).

Of course if I query noOrphan(michael), this will result in true and noOrphan(david) in false (since I didn't define a parent for david)., but I was wondering why there is no proactive way of detecting which persons (michael, david,...) belong to the noOrphan/1 relation?

This probably is a result of the backtracking mechanism of Prolog, but Prolog could maintain a state which validates if one is searching in the positive way (0,2,4,...) negations deep, or the negative way (1,3,5,...) negations deep.

Erik Kaplun
  • 37,128
  • 15
  • 99
  • 111
Willem Van Onsem
  • 443,496
  • 30
  • 428
  • 555
  • Might this have something to do with whether prolog makes a [closed world assumption](http://en.wikipedia.org/wiki/Closed_world_assumption)? – axblount Oct 14 '13 at 22:49
  • Well `\+` is based on two assumptions: negation as finite failure and the closed world assumption. However the binding is still valid under both assumptions as far as I know... – Willem Van Onsem Oct 14 '13 at 22:59
  • 1
    It's a semantic issue, `\+` as well as `not` does not mean `not` as in logic but simply *not provable* (under the cwa). This is the meaning of the negation as failure in the SLD. – rano Oct 15 '13 at 20:33

2 Answers2

8

Let's start with something simpler. Say \+ X = Y. Here, the negated goal is a predefined built-in predicate. So things are even clearer: X and Y should be different. However, \+ X = Y fails, because X = Y succeeds. So no trace is left under which precise condition the goal failed.

Thus, \+ \+ X = Y does produce an empty answer, and not the expected X = Y. See this answer for more.

Given that such simple queries already show problems, you cannot expect too much of user defined goals such as yours.

In the general case, you would have to first reconsider what you actually mean by negation. The answer is much more complex than it seems at first glance. Think of the program p :- \+ p. should p succeed or fail? Should p be true or not? There are actually two models here which no longer fits into Prolog's view of going with the minimal model. Considerations as these opened new branches to Logic Programming like Answer Set Programming (ASP).

But let's stick to Prolog. Negation can only be used in very restricted contexts, such as when the goal is sufficiently instantiated and the definition is stratified. Unfortunately, there are no generally accepted criteria for the safe execution of a negated goal. We could wait until the goal is variable free (ground), but this means quite often that we have to wait way too long - in jargon: the negated goal flounders.

So effectively, general negation does not go very well together with pure Prolog programs. The heart of Prolog really is the pure, monotonic subset of the language. Within the constraint part of Prolog (or its respective extensions) negation might work quite well, though.

Community
  • 1
  • 1
false
  • 10,264
  • 13
  • 101
  • 209
3

I might be misunderstanding the question, and I don't understand the last paragraph.

Anyway, there is a perfectly valid way of detecting which people are not orphans. In your example, you have forgotten to tell the computer something that you know, namely:

person(michael).
person(david).
% and a few more
person(anna).
person(emilia).

not_orphan(X) :- \+ orphan(X).
orphan(X) :- person(X), \+ parent(_, X).

parent(david, michael).
parent(anna, david).

?- orphan(X).
X = anna ;
X = emilia.

?- not_orphan(X).
X = michael ;
X = david ;
false.

I don't know how exactly you want to define an "orphan", as this definition is definitely a bit weird, but that's not the point.

In conclusion: you can't expect Prolog to know that michael and david and all others are people unless you state it explicitly. You also need to state explicitly that orphan or not_orphan are relationships that only apply to people. The world you are modeling could also have:

furniture(red_sofa).
furniture(kitchen_table).
abstract_concept(love).
emotion(disbelief).

and you need a way of leaving those out of your family affairs.

I hope that helps.

  • 1
    The fact is that from the moment the execution tree is nested 2 *negations* deep, one could derive that the status of `parent(_,X)` is equal to `a(X)` and thus enumerating the `no_orphan`s relation becomes feasible. – Willem Van Onsem Oct 15 '13 at 09:38
  • Of course, given the Prolog execution mechanism it is reasonable that the variable is unbounded, I was wondering why such bindings are not implemented in Prolog since at least some of them can be executed on the fly or at compile time. – Willem Van Onsem Oct 15 '13 at 09:54
  • @CommuSoft I finally understand your question. I guess the point here is that unless you define which ground terms can be (or cannot be) an orphan, anyone who is not an orphan (`\+ orphan(X)`) is `not_orphan`. In your original example, the implicit knowledge that `michael` and `david` are people is not available to Prolog. Of course, then, **anyone** can be `not_orphan` (which is why the query *correctly* succeeds with a variable). –  Oct 15 '13 at 10:13
  • 1
    well with double negation, it can be done. I have defined a transformation method who should be able to transform any Prolog program (except for metaprogramming and other complex stuff) to transform it to an equivalent program where values can be enumerated. Currently I'm writing a precompiler and planning to modify an existing Prolog implementation. – Willem Van Onsem Oct 15 '13 at 11:33
  • @CommuSoft I am probably wrong, but the only way that this can end in equivalent programs is to explicitly specify which predicate is supposed to make the term ground. At that point you have made a full circle. –  Oct 15 '13 at 11:48