Prolog X=f(X). does not evalute true for ?-X==f(X)

Question

I know I am missing something very simple, but this bothers me a lot. I want to test how Prolog would handle the below

    X=f(X).
    X=Z:- X==Y,Y==Z.
?- X==f(f(X)).

but obviously I am missing very basic as even ?-X=f(X). returns "false". Could you please point out where I am wrong.

Thank you!

For me, ?- X = f(X). on the top level succeeds, and replies X = f(X). Of course, unification (=/2) and equivalence (==/2) are not the same thing! You need to make it a bit clearer in your question what is your query, what is your consulted program, and what you are trying to achieve. — user1812457

Unknown Unknown · Accepted Answer · 2016-08-31T04:13:28

Use =/2 for unification:

?- X = X.
true.

?- X = f(X).
X = f(X).

?- f(f(X)) = X.
X = f(f(X)).

?- X = Y, X = Z.
X = Y, Y = Z.

As long as you have a free variable on one side of the unification, it will succeed.

Equivalence, with ==/2, is different. It only succeeds if both sides are the same variable or the same ground value:

?- X == X.
true.

?- Y == Z.
false.

?- X = Y, X = Z, Y == Z.
X = Y, Y = Z.

?- X == 3.
false.

?- X = 3, X == 3.
X = 3.