2

Well i'm just wondering why does it work, where prolog loose variable.

?- \+ \+ member(X,[a]),X=b.
X=b.

Where X=a. automagicly vanished.

whd
  • 1,819
  • 1
  • 21
  • 52
  • See [this great answer](http://stackoverflow.com/questions/8523608/logical-not-in-prolog/8523825#8523825) by false for some precisions. – m09 May 29 '12 at 15:07

2 Answers2

4

\+/1 is not "not" in the logical sense, but is implemented through "negation as failure". That means, \+ Goal succeeds iff Goal fails.

Think of \+/1 as being implemented as:

\+(Goal) :- Goal -> fail ; true.

As you can see, in both cases can no variable in Goal become bound. In the "if" branch, any binding will be undone by backtracking, and in the "else" branch, no variable will have been become bound anyway.

In your example, member(X,[a] succeeds by binding X to a. This will have \+ member(X,[a]) fail, and so \+\+ member(X,[a]) succeeds because of this failure. Due to the intermediate failure, X will not be bound to a.

twinterer
  • 2,416
  • 1
  • 15
  • 13
1

the (\+)/1 operator in prolog is supposed to stand for not provable but corresponds to the older (not)/1 operator. So basically what you are doing here is:

not not member(X, [a]), X = b.

EDIT

If X is a list that contains a, the double negation of member(X, [a]) will have the same result as member(X, [a]) without any negations. X = b, just binds b to the list X.

Also here is a link I had bookmarked that has a list of all Prolog predicates and their meanings.

Hope this helps

m09
  • 7,490
  • 3
  • 31
  • 58
Hunter McMillen
  • 59,865
  • 24
  • 119
  • 170
  • The way you phrase things is very confusing to me. I don't understand your answer (especially the part under the code formatted block). – m09 May 29 '12 at 14:18
  • I just re-read what I posted and I can see why you are confused. Basically the member function returns true or false, true if a is in X, false if a is not in X. Saying `not not member(X, [a])` is the same as saying `member(X, [a])` because the not operators cancel out. – Hunter McMillen May 29 '12 at 14:22
  • that is false, obviously here you can't replace `not not member(X, [a])` with `member(X, [a])` precisely because the unification will take place in the second case and not in the first, hence the general result that will be false in the first case, and `X = b.` in the second. – m09 May 29 '12 at 14:24
  • but let aside the fact that this is true or false, you should edit your answer to make it more understandable so that we can comment about it in a clearer manner! :p – m09 May 29 '12 at 14:25
  • @Mog I edited above to make the post clearer. At least in the sense that this is what _I_ think is going on with the `\+ \+` ops. I may be wrong. – Hunter McMillen May 29 '12 at 14:53
  • Thanks, but as you can see, `?- member(X, [a]), X = b.` returns `false.` while `?- \+ \+ member(X, [a]), X = b.` returns `X = b.`. That's precisely the object of this question (the fact that those two queries are NOT equivalent). see twinterer's answer for an explanation of the `(\+)/1` operator. BTW, if you have to precise the "not provable" description, you should go for "not provable at this point in time" instead of "not". Just my .02! – m09 May 29 '12 at 15:04