prolognegation-as-failure

Confusion in output of double negation as failure


I am trying to learn prolog and i came across the following problem:

Given -

try(X):-not(not((member(X,[a,b,c])))),write(X). 

I would expect the query ?- try(X)., for the following query to be something like

X=a
a;
X=b
b;
X=c
c.

But in fact, the output is:

?- try(X).
_12010
true.

Why is that? Why the variable is not initiated to some value?


Solution

  • In addition to what @VictoriaRuiz says, notice a few other things:

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

    This is false because member(X, [a,b,c]) has solutions, but the variable binding is lost when you negate it. So that means

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

    is the same as

    ?- \+ false.
    true.
    

    In other words, there's nowhere for X to materialize from. Your write(X) happens outside the scope of the variable binding for X, it's as though you did this:

    ?- \+ false, write(X).
    _4082
    true.
    

    which is basically the same as

    ?- write(X).
    _4014
    true.
    

    If you wanted to see evidence of backtracking in the negation, you might expect to see it with this query:

    ?- \+ \+ (member(X, [a,b,c]), write(X), nl).
    a
    true.
    

    But because you obtained a true solution on the first try, the negation of that is false. Then the negation of that is true. So we see that it produced a solution inside the goal (member(X, [a,b,c]), write(X), nl), which is enough to know that the negation of that is false. Negating false again gives you true, but no variable bindings.