With the classic definition of append/3
(which I’ve written as app/3
to avoid name clashes with builtins), there clearly is a choice point … but append/3
is written in C (see last part of the trace below), so why can’t it detect this situation?
?- listing(app).
app([], A, A).
app([X|Xs], Ys, [X|Zs]) :-
app(Xs, Ys, Zs).
true.
?- trace, app(A, [c,d], [a,b,c,d]).
Call: (10) app(_2492, [c, d], [a, b, c, d]) ?
Call: (11) app(_2836, [c, d], [b, c, d]) ?
Call: (12) app(_2842, [c, d], [c, d]) ?
Exit: (12) app([], [c, d], [c, d]) ?
Exit: (11) app([b], [c, d], [b, c, d]) ?
Exit: (10) app([a, b], [c, d], [a, b, c, d]) ?
A = [a, b] ;
Redo: (12) app(_2842, [c, d], [c, d]) ?
Call: (13) app(_2848, [c, d], [d]) ?
Call: (14) app(_2854, [c, d], []) ?
Fail: (14) app(_2854, [c, d], []) ?
Fail: (13) app(_2848, [c, d], [d]) ?
Fail: (12) app(_2842, [c, d], [c, d]) ?
Fail: (11) app(_2836, [c, d], [b, c, d]) ?
Fail: (10) app(_2492, [c, d], [a, b, c, d]) ?
false.
[trace] 3 ?- trace, app([a,b], B, [a,b,c,d]).
Call: (10) app([a, b], _3704, [a, b, c, d]) ?
Call: (11) app([b], _3704, [b, c, d]) ?
Call: (12) app([], _3704, [c, d]) ?
Exit: (12) app([], [c, d], [c, d]) ?
Exit: (11) app([b], [c, d], [b, c, d]) ?
Exit: (10) app([a, b], [c, d], [a, b, c, d]) ?
B = [c, d].
The trace is a bit different with the builtin:
?- listing(append/3).
lists:append([], L, L).
lists:append([H|T], L, [H|R]) :-
append(T, L, R).
true.
?- trace, append(A, [c,d], [a,b,c,d]).
Call: (10) lists:append(_5800, [c, d], [a, b, c, d]) ?
Exit: (10) lists:append([a, b], [c, d], [a, b, c, d]) ?
A = [a, b] ;
Redo: (10) lists:append([a, b|_6170], [c, d], [a, b, c, d]) ?
Fail: (10) lists:append(_5800, [c, d], [a, b, c, d]) ?
false.