What's wrong with Prolog's append?

Question

According to my university's course in logic we could expect a different outcome than defined by Prolog for the following query:

append([], a, X)

(which unifies for X=a).

However I don't get what they're aiming at? What should be expected as a valid response, given that append should unify X for (in this example) the concatenation of [] and a?

I assume they may be expecting a return of false or [a]; however I suppose that should be the result of concatenating a and [], not [] and a (since [] is the tail of [a]).

Answer 1

The point here is that we expect append/3 to hold only for lists.

In the query you show, a is not a list, yet append/3 still holds.

Thus, the relation is in fact more general than we would initially expect: It holds for other cases too!

The reason why this is so can be soon from the first clause of the traditional definition of append/3:

append([], Bs, Bs).

This clause alone already makes the query succeed! No additional pure clause can prevent this. Thus, it is this clause that must be restricted if we want the relation to hold only for lists. This means, we must put a constraint on the second argument, which we do by stating it in the body of the clause:

append([], Bs, Bs) :- ... (left as an exercise)

This obviously comes at a price: Performance.

So, the trade-off here is between performance and precision. In Prolog, we often accept such a trade-off because we implicitly use such predicates only with the intended terms. On the other hand, for many predicates, we want to benefit from domain errors or type errors if they are not called with the expected types.

Answer 2

Your course is aiming at a very important point of Prolog programming.

Manuals are often quite sloppy on the precise definition of append/3 and similar predicates. In fact, the complete definition is so complex that it is often preferred to define only part of the actual relation. Consider the first definition in the Prolog prologue:

append(Xs, Ys, Zs) is true if Zs is the concatenation of the lists Xs and Ys.

Note the if. The definition thus gives cases, where the relation holds but does not explicitly exclude further cases. To exclude further cases, it would say iff instead. The cases mentioned (that we are talking about lists) are the intended use of the predicate. So which cases now may be additionally included? Those cases where the precondition (that the arguments are lists) does not hold.

Consider a definition of append/3 with 'iff' in place of 'if':

append([], Xs, Xs) :-
   list(Xs).
append([X|Xs], Ys, [X|Zs]) :-
   append(Xs, Ys, Zs).

list([]).
list([X|Xs]) :-
   list(Xs).

The cost for appending two lists is now |Xs|+|Ys|. That is quite an overhead compared to |Xs| alone.

But the situation is even worse. Consider the query:

?- append([1,2], Ys, Zs).
;  Ys = [], Zs = [1,2]
;  Ys = [_A], Zs = [1,2,_A]
;  Ys = [_A,_B], Zs = [1,2,_A,_B]
...

So we get infinitely many answers to this query. Contrast this to the usual definition:

?- append([1,2], Ys, Zs).
   Zs = [1,2|Ys].

There is a single answer only! It contains all the answers for all lists plus some odd cases as you have observed. So the usual definition for append has better termination properties. In fact, it terminates if either the first or the third argument is a list of known length¹.

Note that the answer contains Ys. In this manner infinitely many answers can be collapsed into a single one. This in fact is the power of the logical variable! We can represent with finite means infinitely many solutions. The price to pay are some extra solutions² that may lead to programming errors. Some precaution is thus required.

---

1 It also terminates in some further obscure cases like append([a|_],_,[b|_]).

2 append([a], Zs, Zs). produces (in many systems) an answer, too.