Can someone explain the difference between the == and the = operator in Prolog? I know that X = Y means X unifies with Y and is true if X already unifies with Y or can be made to, but I don't understand how this differs from ==.
Follow up: That (see Accepted Answer) makes sense. One more question though, is there ever a situation where X \= Y is true and X \== Y is false (or vice-versa)? That is, does X \= Y test if they cannot be unified or if they are not currently unified?
The = "operator" in Prolog is actually a predicate (with infix notation) =/2 that succeeds when the two terms are unified. Thus X = 2 or 2 = X amount to the same thing, a goal to unify X with 2.
The == "operator" differs in that it succeeds only if the two terms are already identical without further unification. Thus X == 2 is true only if the variable X had previously been assigned the value 2.
Added: It's interesting to work through what happens when "not" gets mixed into these goals, per the comment by JohnS below. See the nice set of examples in the Amzi! Prolog documentation.
\= means the two terms cannot be unified, i.e. that unification fails. As with all applications of negation as failure, "not unified" does not (and cannot) result in any unification between terms.
\== means the two terms are not identical. Here also no unification takes place even if this succeeds.
Finally think about what not(not(X = Y)) will do. The inner goal succeeds if X and Y (which can be arbitrary terms) can be unified, and so will the double negation of that. However wrapping the inner goal inside the double negation produces a goal that succeeds if the two terms can be unified but without unifying those terms.
It is left as an exercise for the reader to contemplate whether not(not(X == Y)) has any similar utility.
= stands for unification, it means that it will try to bind the free variables to make them match the other members. for example : A = h(X) will turn A into the term h(X) if A is free, and will fail if A is bound to say 5. unification is great because you can do pattern matching with it, for example :
X-Y:Z = 5-[a, b, c]:y
will give you
X = 5, Y = [a, b, c] and Z = y
because prolog tries to make X-Y:Z fit the expression 5-[a, b, c]:y. It's very useful.
Note that unification is used when you call a predicate and some techniques ensue : say you want to return the value of an accumulator in a recursive predicate, you can do that :
recursive_predicate([], Accumulator, Accumulator).
recursive_predicate(Input, Accumulator, Output) :- %recursive stuff.
the first clause will try to unify the third and second argument, so if the third is free, it has now the same value as the second.
== is equality without trying to bind the variables.
=and==) started as Comments to my Answer. I suspect "That makes sense" is in reference to my first two paragraphs, after which I responded further. See if my Edit seems sufficient to clear up the sense of this. - hardmath