order of conditions in antecedent causes stackoverflow

Question

As a simple exercise, I wrote my own permutation.

This stack overflows:

without(_, [], []).
without(A, [A|T], T).
without(A, [H|T], [H|G]) :- without(A, T, G).

my_permutation([], []).
my_permutation([H|T], P) :- member(H, P), without(H, P, Pp), my_permutation(T, Pp).

this works partly, but still stack overflows after giving some of the solution space:

without(_, [], []).
without(A, [A|T], T).
without(A, [H|T], [H|G]) :- without(A, T, G).

my_permutation([], []).
my_permutation([H|T], P) :- my_permutation(T, Pp), member(H, P), without(H, P, Pp).

this also stack overflows:

without(A, [A|T], T).
without(A, [H|T], [H|G]) :- without(A, T, G).

my_permutation([], []).
my_permutation([H|T], P) :- without(H, P, Pp), my_permutation(T, Pp).

but this works perfectly:

without(A, [A|T], T).
without(A, [H|T], [H|G]) :- without(A, T, G).

my_permutation([], []).
my_permutation([H|T], P) :- my_permutation(T, Pp), without(H, P, Pp).

Can anyone please help me understand why?

Answer 1

The problem is this portion:

without(H, P, Pp)

Both P and Pp are uninstantiated, so without cheerfully goes into an infinite loop of giving them an increasingly longer length, as per the T and G variables.

Demonstration:

?- without(E, L, R).
L = [E|R] ;
L = [_A, E|_B],
R = [_A|_B] ;
L = [_A, _B, E|_C],
R = [_A, _B|_C] ;
L = [_A, _B, _C, E|_D],
R = [_A, _B, _C|_D] ;
... % Increasingly longer

The solution is to replace:

my_permutation([H|T], P) :- without(H, P, Pp), my_permutation(T, Pp).

... so that the list length is restricted, causing termination.

This would suffice (although using same_length makes it slower):

my_permutation([H|T], P) :-
    same_length([H|T], P),
    without(H, P, Pp),
    my_permutation(T, Pp).

Or, more efficiently (using E as a short name for "Element", i.e. element of a list):

my_permutation([H|T], [E|P]) :- without(E, [H|T], R), my_permutation(R, P).

This clearly ties both arguments of my_permutation to be the same length, and passes an instantiated list ([H|T]) to without.

However, it can still have the problem of passing an uninstantiated list to without, if its arguments are swapped:

?- my_permutation(L, [1,2,3]).
L = [1, 2, 3] ;
ERROR: Stack limit (1.0Gb) exceeded

The advantage of my_permutation(T, Pp), without(H, P, Pp) is that both arguments of my_permutation will have encountered [], [], and so have their length known. It is still not perfect, though:

?- my_permutation(L, [1,2]).
L = [1, 2] ;
L = [2, 1] ;
% Does not terminate

Note that permutation/2 does not have this problem.

To fix this termination issue, could enforce same_length in a more efficient way:

my_permutation2(L, P) :-
    same_length(L, P),
    my_permutation2_(L, P).

my_permutation2_([], []).
my_permutation2_([H|T], [E|P]) :-
    without(E, [H|T], R),
    my_permutation2_(R, P).

Although, it's faster with those 2 constraint lines flipped in order.

Other permutation methods are shown at https://stackoverflow.com/a/74655536