It comes down to how unification works in Prolog. Mostly:
- atoms combine only if they are identical
- variables are combined with anything and
- compounds join when each component can combine
So you call: append([a, b, c], [d, e, f], Y) , which is your first target. Note that to simplify the viewing, I changed the variable name from X to Y.
This should be combined with a fact or a rule: let's see if it will be combined with append ([], X, X)?
(1) append([a, b, c], [d, e, f], Y) (2) append([], X, X)
Both (1) and (2) have the same functor (append), so that’s good, and both of them have 3 arguments, so that’s also good. But in order to combine each corresponding argument, it is necessary to combine. So, the first list [a, b, c] in (1) will try to unify with the empty list in (2), but they cannot, because the list in (1) is not an empty list. Thus, unification fails.
Then we can try to combine with append ([H | T1], X, [H | T2]).
(1) append([a, b, c], [d, e, f], Y) (2) append([H|T1],X,[H|T2])
This time, the list [a, b, c] in (1) will try to merge with the list [H | T1] in (2). To make this possible, the variable H can bind to the atom a (H → a), and the list T1 can bind to the tail of the list in (1), T1 → [b, c]. So, the first argument works so that we have:
(1) append([a, b, c], [d, e, f], Y) (2)' append([a, b, c],X,[a|T2])
The second argument will also be unified because X is a variable and will bind to everything. X → [d, e, f]; therefore, we have:
(1) append([a, b, c], [d, e, f], Y) (2)'' append([a, b, c],[d, e, f],[a|T2])
And finally, the last argument is combined because Y → [a | T2]. So, now that it is combined with the head of the rule, we need to develop the body of the rule: now we set the goal append([b, c], [d, e, f], T2) .
Starting with the first fact, again we are looking for a proposal to which this goal will be tied. According to the same explanation above, it will not be combined with the first sentence, but it will be combined with the second with bindings: H → b, T1 → [c], X → [d, e, f] and T2 → [b |. T2 ']
We remain with the goal: append ([c], [d, e, f], T2 '). Again, it does not combine with the first sentence and does not combine with the second with bindings: H → c, T1 → [], X → [d, e, f], T2 '-> [c | T2 ''].
Now the goal: append ([], [d, e, f], T2 '').
Let's see what happens when we try to unify this with paragraph 1:
(1) append([], [d, e, f], T2'') (2) append([],X,X)
Two empty lists are combined, X → [d, e, f], and since T2 '' → X, then T2 '' → [d, e, f]. Now the tricky part keeps track of recursive calls so far and now it goes back through recursion to see the end result. recall that T2 '-> [c | T2 ''], so T2 'is actually [c, d, e, f]. And recall that T2 → [b | T2 '], so T2 is actually [b, c, d, e, f].
And finally, Y → [a | T2]; therefore, Y is [a, b, c, d, e, f]. Since Y is an external variable, it now displays that the original target is complete.