List unification in Prolog

Question 1

To unify means, in a very simplified way, to match patterns. When you unify:

[a, b, c] = [a | T]

you're saying, in the right side, that the first list contains an element a followed by a tail T. Now, if you say:

[a, b, c] = [b | T]

the previous statement does not apply, since you do not have, on the left side, a list that begins with a and is followed by a tail-list T, i.e., the [a, b, c] does not unify with the list [b | T].

Question 2

Because b is not the head of the list [a,b,c]. Prolog list notation is syntactic sugar over a very simple structure.

The empty list is represented as the atom [].
Non-empty lists (that is, list of length 1 or more) are represented as a single ./2 structure (.(A,B)) where the first (leftmost) argument to the structure is the head (first item) of the list and the second (rightmost) argument is the tail (the list that is the remainder of the list of the list, which may be either the empty list or — recursively — another non-empty list. So
- A list of one item, [a], is represented internally as this prolog term:
```
.(a,[]).
```
- A list of two items, [a,b] is represented internally as you might expect:
```
.(a,.(b,[]))
```
- A list of three items, [a,b,c] is represented in the same way:
```
.(a,.(b,.(c,[])))
```
And so on.

The vertical bar (|) operator in prolog list notation, used to divide a list into its head and tail, is likewise syntactic sugar for the same ./2 structure. The term

[H|T]

is exactly identical to

.(H,T)

And an expressions like

[A,B|Rest]
[A,B,C|Rest]

are, respectively, identical to

.(A,.(B,Rest))
.(A,.(B,.(C,Rest)))

Given all that, it should be pretty obvious why an expression like

[a,b,c] = [b|T]

fails, because it's exactly identical to:

.(a,.(b,.(c,[]))) = .(b,T)

The first elements of each side, respectively a and b are different and so the unification fails.