Does Prolog's toplevel use the wrong operator when printing results?

Question

I have been staring at Prolog toplevel results like these for some time now:

?- reverse([X,Y,Z],[Y,Z,Y]).
X = Y, Y = Z.

And it just occurred to me: Shouldn't it say

?- reverse([X,Y,Z],[Y,Z,Y]).
X == Y, Y == Z.

Because = is unification, and == is term equality. Which is what Prolog really wants to say: Those terms are equal! (They trivially unify, being unbound variables).

A bad case of historical raisins?

Answer 1

Logically X = Y, Y = Z and X == Y, Y == Z are not the same. You can try yourself:

?- X = f(_,a), Y = f(b,_), X = Y, Y = Z.
X = Y, Y = Z, Z = f(b, a).

?- X = f(_,a), Y = f(b,_), X == Y, Y == Z.
false.

So they say two different things. Only X = Y, Y = Z corresponds to what reverse does:

?- X = f(_,a), Y = f(b,_), reverse([X,Y,Z],[Y,Z,Y]).
X = Y, Y = Z, Z = f(b, a).