5

Assume we have the following program:

a(tom). 
v(pat).

and the query (which returns false):

\+ a(X), v(X).

When tracing, I can see that X becomes instantiated to tom, the predicate a(tom) succeeds, therefore \+ a(tom) fails.

I have read in some tutorials that the not (\+) in Prolog is just a test and does not cause instantiation.

  1. Could someone please clarify the above point for me? As I can see the instantiation.

  2. I understand there are differences between not (negation as failure) and the logical negation. Could you refer a good article that explains in which cases they behave the same and when do they behave different?

logi-kal
  • 7,107
  • 6
  • 31
  • 43
Gurkan E.
  • 205
  • 1
  • 2
  • 7

2 Answers2

3

Great question.

Short answer: you stumbled upon "floundering".

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. link

If you invert the query

v(X), \+ a(X).

You'll get the right answer. Some implementations or meta interpreter detect floundering goals and delay them until all the variables are ground.

About your point 1), you see the instantiation inside the NAF tree. What happens there shouldn't affect variables that are outside (in this case in v(X)). Prolog often acts in the naive way to avoid inefficiencies. In theory it should just return an error instead of instantiating the variable.

2) This is my favourite article on the topic: Nonmonotonic Logic Programming.

NotAUser
  • 1,436
  • 8
  • 12
  • What do you understand by floundering? To my understanding it simply means that a coroutining goal like `safenot(G) :- when(ground(G), \+ G).` is part of an answer. But you seem to have a different notion. – false Feb 06 '13 at 15:23
  • 1
    2nd nit: Groundness is not required, it suffices to insist on groundness of the variables that occur outside the negated goal. Even that is too much to demand. – false Feb 06 '13 at 15:25
  • I'm not sure I understand your question. `safenot(G) :- when(ground(G), \+ G).` is a solution for floundering for those cases that have a solution. While for floundering I intend the occurrence of a goal that leads to a non-correct answer because of the Prolog notion of NAF. – NotAUser Feb 07 '13 at 16:49
  • §15, Lloyd87: ... *flounders* if at some point in the computation a goal is reached which contains only non-ground negative literals. Thus `\+a(X), v(X)` does not flounder but `\+a(X)` does. – false Feb 07 '13 at 18:13
  • Clearly your definition differs. What is it? Where do you have it from? – false Feb 07 '13 at 18:14
  • I'd say half of the definitions you see around intend floundering as the application of non-safe NAF. As opposed to the situation where the application of non-safe NAF is forced. I guess the former is a more Prolog-oriented definition, since that's what makes a difference in a Prolog query. While the second must be the right definition since Lloyd gives it :). – NotAUser Feb 08 '13 at 10:59
  • Any concrete ref? At least in the context of coroutining Lloyd's definition is taken. – false Feb 08 '13 at 16:05
  • 1
    Not sure about formal definitions but you find things like "For a given program and goal, floundering means selecting a non ground negative rule literal" around. (http://www.ida.liu.se/~wlodr/DHM.alpsws07.paper.pdf) – NotAUser Feb 08 '13 at 16:39
  • Thanks! That's the kind of source I was looking for. Clearly, floundering has widened its meaning. – false Feb 08 '13 at 19:12
1

WRT point 2, Wikipedia article seems a good starting point.

You already experienced that understanding NAF can be difficult. Part of this could be because (logical) negation it's inherently difficult to define even in simpler contest that predicate calculus (see for instance Russel's paradox), and part because the powerful variables of Prolog are domed to keep the actual counterexamples of failed if negated proofs. See if you can understand the actual library definition of forall/2 (please read the documentation, it's synthetic and interesting) that's the preferred way to run a failure driven loop:

%%  forall(+Condition, +Action)
%
%   True if Action if true for all variable bindings for which Condition
%   if true.

forall(Cond, Action) :-
    \+ (Cond, \+ Action).

I remember the first time I saw it, it looked like magic...

edit about a tutorial, I found, while 'spelunking' my links collection, a good site by J.R.Fisher. It's full of interesting stuff, just a pity it's a bit terse in explanations, requiring the student to answer itself with frequent execises. See the paragraph 2.5, devoted to negation by failure. I think you could also enjoy section 3. How Prolog Works

CapelliC
  • 59,646
  • 5
  • 47
  • 90