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

2
votes

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?

1
prologprolog-toplevel
Please, no opinion! But, assuming you rephrased your question, consider: ?- X = Y. with answer X = Y or Y = X or X = _quelconque, Y = _quelconque. Now, take that answer and paste it back into the toplevel. With == in place of = this would be failure. – false
@false So, the idea would be that the toplevel gives you the constraint, that, when it precedes your goal, would make the goal succeed for sure (in a "logical setting" of course)? – David Tonhofer
The idea in systems like SWI, Scryer, SICStus is to produce the answer such that you can paste it back if you want to use that result for further queries. And in SWI you can even paste back all answers together. And in Scryer even indented as a regular disjunction. This idea works nicely for syntactic terms, quite nicely (as SWI shows) for rational trees, nicely for clpfd (need to be turned on in SICStus, and in SWI you have to wrap Query_0 as call_residuevars(Query_0, Vs)). What is displayed is called (the projection of) a (constraint) store. Much less nice for CHR. – false

1 Answers

0
votes

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).