Order of unification in lists when using pipe(|)

Question

I am having trouble trying to figure out in what order unification is done. I have the following query:

[X, like | Z] = [I, Y, Prolog, language].

This gives me the following result:

X = I,
Z = [Prolog, language],
Y = like.

However, what I was expecting is:

X = I,
Y = like,
Z = [Prolog, language].

Is there any specific order in which Prolog unifies terms?

EDIT: I have a feeling that Prolog is giving higher priority to unification of an atom with a variable over that of a variable with an atom. Is that so?

Answer 1

There is no order. Here is the mapping that is performed:

[I,  Y   , Prolog, language].
 |   |     +--------------+
 |   |           |
[X, like |       Z] 

if that mapping is possible (i.e. if the variables I ,Y, X, Z are bound to terms that allow unification to succeed)

In this case, assuming that all variables are unbound, then:

• Variables I and X will become "the same variable" (more clearly, the variable name I and X will designate the same empty storage cell)

• Variable Y will become the atom like' (more clearly, the storage cell designated by variable name Ywill be set tolike`)

• Variable Z takes up the "rest (or suffix) of the list" (everything behind the |) and will become the complex term `[Prolog, language]'.

• Variable Prolog is not changed and stays what it was.

Answer 2

The Prolog top-level is free to order the answer substitution however it likes. And the order of the answer substitution doesn't tell you in which order the unification is done. You might get an insight into the unification order by using freeze/2:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.17)

?- freeze(X, (write('X='), write(X), nl)), 
    freeze(Y, (write('Y='), write(Y), nl)),
    [X|Y] = [foo|bar].
X=foo
Y=bar
X = foo,
Y = bar.

?- freeze(Y, (write('Y='), write(Y), nl)),
    freeze(X, (write('X='), write(X), nl)),
    [X|Y] = [foo|bar].
X=foo
Y=bar
Y = bar,
X = foo.

At least you see that the freeze coroutines are sheduled after unification pattern and not after the way they were introduced, as does the top-level. Mostlikely in SWI-Prolog the freeze/2 result tells you the order how unification is performed.

But to the best of my knowledge the ISO core standard doesn't require a particular order. In this respect other Prolog systems might might have other preferences than SWI-Prolog. But I owe you a reference that supports this claim.