Prolog list unification

0
votes

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?

2
listprologunification
On SWI-Prolog it gives X=Z, Z=a, Y = [a,f(a,a)|Y] which I guess is the result you expected. – hynner
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. – Teo
As I said, there is no L on my SWI-Prolog :-) – hynner
Teo, what Prolog interpreter are you using? – lurker

2 Answers

0
votes

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.

0
votes

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.