Append/3 isn't deterministic if first arg is var?

When the first arg to append/3 is a var, there’s a choice point:

?- append(A, [c,d], [a,b,c,d]).
A = [a, b] ;
false.

By comparison:

?- append([a,b], B, [a,b,c,d]).
B = [c, d].

Is this working as intended?

The similar atom_concat/3 doesn’t leave a choicepoint:

?- atom_concat(A, cd, abcd).
A = ab.

?- atom_concat(ab, B, abcd).
B = cd.

If my logic is right then yes it is correct.

append/3 needs a base case for the empty list ([]) and and a recursive case for the non-empty list ([H|T]), thus a choice point.

atom_concat/3 only needs one case because there is only the base case, thus no choice point.

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.

In checking the source for SWI-Prolog at GitHub I only see append/3 implemented in Prolog.

In searching with PRED_IMPL I find no implementation for it in C.

If I use listing/1 on a predicate implemented in C it tells me the predicate is Foreign

?- listing(time_file).
%   Foreign: system:time_file/2

true.

I don’t know why the traces are different.

2 Likes

Some libraries use

:- set_prolog_flag(generate_debug_info, false).

which makes the tracer hide calls between predicates that are compiled under this condition. THe between implies that calls from normal code to this code is shown, as well as calls from such code back to normal predicates.

2 Likes

This would fix it (but probably not worth the performance penalty):

append2(Start, End, Both) :-
    once_only_if(
        at_least_n_true(2,
            [is_list(Start), is_list(End), is_list(Both)]
        ),
        append(Start, End, Both)
    ).

Using generic helper predicates:

once_only_if(OnceIf, Goal) :-
    call_t(OnceIf, Bool),
    t_once(Bool, Goal).

t_once(true, Goal) :-
    call(Goal),
    % Don't backtrack into Goal
    !.
t_once(false, Goal) :-
    call(Goal).

at_least_n_true(0, _) :- !.
at_least_n_true(Min, Goals) :-
    integer(Min),
    Min @> 0,
    at_least_n_true_(Goals, Min).

at_least_n_true_([H|T], Min) :-
    call_t(H, Bool),
    at_least_n_true_called_(Bool, T, Min).

at_least_n_true_called_(true, _T, 1) :- !.
at_least_n_true_called_(true, T, Min) :-
    Min0 is Min - 1,
    at_least_n_true_(T, Min0).
at_least_n_true_called_(false, T, Min) :-
    at_least_n_true_(T, Min).

% Don't use *-> because Goal might contain ";" alternatives
call_t(Goal, Bool) :-
    call(Goal),
    !,
    Bool = true.
call_t(_Goal, false).

There are other attempts at prolog - Pure append/3 for mode (-,+,+) that wouldn't leave a Choice Point - Stack Overflow

The condition is wrong. append/3 is (semi)det if the first argument is a list. I.d go for this when written as a wrapper.

append2(L1, L2, L3), is_list(L2), is_list(L3) => append(L1, L2, L3), !.
append2(L1, L2, L3) => append(L1, L2, L3).

I think you can so something better though. What about walking the normal append, checking the first argument to be nonvar and only doing the list checks if that happens?

As I understand it, the only slight inelegance with swi-prolog’s append/3 currently is the unwanted choicepoint when args 2 & 3 are lists, and arg 1 is var. This solves that issue, with a reasonable performance hit:

append2a(Start, End, Both) :-
    % Guard against unwanted choicepoint
    is_list(Both),
    is_list(End),
    !,
    append(Start, End, Both),
    !.
append2a(Start, End, Both) :-
    append(Start, End, Both).

I don’t see a need to check the first arg.

Edit: Tweaked to check Both then End vars, which seems like a slightly more sensible order, for performance/likelihood.

This is basically what jan already wrote above. I don’t see a better way.

Could you help me understanding the ! at the end? I thought the cut is already built into =>

If I’m understanding correctly: would a more acceptable (and short) predicate name than once_only_if be call_once_if ?

That particular cut is acting as once(append(L1, L2, L3)).

… to prevent the unwanted choicepoint.

1 Like

There’s also an unwanted choicepoint at the end of:

?- append(X, Y, [1]).
X = [],
Y = [1] ;
X = [1],
Y = [] ;
false.

… which is also fixed by:

append2(Start, End, Both) :-
    % Preventing unwanted choicepoint with append(X, [1], [1]).
    is_list(Both),
    is_list(End),
    !,
    append(Start, End, Both),
    !.
append2(Start, End, Both) :-
    append(Start, End, Both),
    % Preventing unwanted choicepoint with append(X, Y, [1]).
    (End == [] -> ! ; true).