Prolog list unification

Question

I am trying to further my understanding of Prolog, and how it handles list unification. So I am stuck with this example, that I know the answer as I execute the code, but I cannot understand how it works.

[X,a,X,f(X,a)|Y] = [Z,Z|Y]

The answer is:

X=Z
Z=a
Y=_
L=[a,f(a,a)|Y]

I know that the head unifies with the other head, so if I make some changes, like these:

let C=[X,a,X,f(X,a)]
let D=[Z,Z]

and the unification should go this way:

[C|Y]=[D|L]

so Y must be equal to L, not _, right? Can someone explain me this better and correct my mistake?

On SWI-Prolog it gives `X=Z, Z=a, Y = [a,f(a,a)|Y]` which I guess is the result you expected. — hynner, Apr 16 '15 at 18:14
Where does L come from? On SWI-Prolog it gives L=[a,f(a,a) | Y], but I am not sure how to come up with this solution. — badm, Apr 17 '15 at 11:28

score 0 · Answer 1 · answered Apr 17 '15 at 16:14

Please show your actual interraction with the interpreter.

For example,

$ swipl
Welcome to SWI-Prolog (Multi-threaded, 64 bits, Version 7.1.36-18-ga5e157c)
Copyright (c) 1990-2015 University of Amsterdam, VU Amsterdam
SWI-Prolog comes with ABSOLUTELY NO WARRANTY. This is free software,
and you are welcome to redistribute it under certain conditions.
Please visit http://www.swi-prolog.org for details.

For help, use ?- help(Topic). or ?- apropos(Word).

?- [X,a,X,f(X,a)|Y] = [Z,Z|Y].
X = Z, Z = a,
Y = [a, f(a, a)|Y].

(Note that Y is now a cyclic term.)

If you showed what it is that you actually doing, it might be easier to help you. Just edit your question.

score 0 · Accepted Answer · edited May 23 '17 at 12:22

There's nothing special or unique about lists. A list is just the data structure ./2. Prolog's list notation is just syntactic sugar on top of that. In a nutshell:

[] is an atom and denotes the empty list.
[a] is exactly equivalent to .(a,[]).
[a,b] is exactly equivalent to .(a,.(b,[])).
etc.

The head/tail construct [Head|Tail] is likewise syntactic sugar:

[H|T] is exactly equivalent to .(H,T).

Replace the list notation with the dot notation and your predicate will work exactly the same. Just not as convenient.

See my answer here for details.

Prolog list unification

2 Answers2