Better pure version of same_length/2

Question

Given the frequent pure definition of same_length/2 as

same_length([],[]).
same_length([_|As], [_|Bs]) :-
   same_length(As, Bs).

?- same_length(L, [_|L]).
   loops.

Is there a pure definition that does not loop for such cases? Something in analogy to the pure (but less efficient) version of append/3 called append2u/3.

I know how to catch such cases manually with var/1 and the like, but ideally a version that is just as pure as the original definition would be desirable. Or at least it should be simple.

What I have tried is the definition above.

One clarification seems to be in order:

Note that there are certain queries that inherently must not terminate. Think of:

?- same_length(Ls, Ks).
   Ls = [], Ks = []
;  Ls = [_A], Ks = [_B]
;  Ls = [_A,_B], Ks = [_C,_D]
;  Ls = [_A,_B,_C], Ks = [_D,_E,_F]
;  Ls = [_A,_B,_C,_D], Ks = [_E,_F,_G,_H]
;  ... .

There is no other way to enumerate all solutions using the language of syntactic answer substitutions.

But still an implementation may terminate for the queries given.

Answer 1

A solution using '$skip_max_list'/4:

% Clause for `?- L = [a|L], same_length(L, _)`.
same_length(As, Bs) :-
    (Cs = As ; Cs = Bs),
    '$skip_max_list'(_, _, Cs, Cs0),
    subsumes_term([_|_], Cs0), !,
    false.
% Clause for `?- same_length(L, [_|L])`.
same_length(As, Bs) :-
    As \== Bs,
    '$skip_max_list'(S, _, As, As0),
    '$skip_max_list'(T, _, Bs, Bs0),
    As0 == Bs0,
    S \== T, !,
    false.
same_length(As, Bs) :-
    same_length_(As, Bs).

same_length_([], []).
same_length_([_|As], [_|Bs]) :-
   same_length_(As, Bs).

Queries:

?- L = [a|L], same_length(L, _).
   false.
?- same_length(L, [_|L]).
   false.
?- same_length([_], L).
   L = [_A].
?- same_length(L, M).
   L = [], M = []
;  L = [_A], M = [_B]
;  ... .

Answer 2

UPDATED SOLUTION

Here is my solution:

same_length(A, A).
same_length([_|A], [_|B]) :- same_length(A, B).
    
?- same_length(L, [_|L]).
  L = [_1696|L]

I am not sure if it has all the properties you're looking for. For example if you call

? - same_length(L, [1,2,3]).

then it lists many answers, e.g. L = [_X, 2, 3], rather than just [_X, _Y, _Z]. But it's pure and produces a correct answer for the query quoted.

Answer 3

This answer aims at minimising runtime costs.

It is built on '$skip_max_list'/4 and runs on Scryer Prolog.

First up, some auxiliary code:

:- use_module(library(lists)).

'$skip_list'(N,Xs0,Xs) :-
   '$skip_max_list'(N,_,Xs0,Xs).

is_list([]).
is_list([_|Xs]) :-
   is_list(Xs).

sam_length_([],[]).
sam_length_([_|Xs],[_|Ys]) :-
   sam_length_(Xs,Ys).

Now the main dish:

sam_length(Ls1,Ls2) :-
   '$skip_list'(L1,Ls1,Rs1),
   (  Rs1 == []
   -> length(Ls2,L1)
   ;  var(Rs1),
      '$skip_max_list'(L2,L1,Ls2,Rs2),
      (  L2 < L1
      -> var(Rs2),
         Rs1 \== Rs2,
         '$skip_max_list'(_,L2,Ls1,Ps1),
         sam_length_(Ps1,Rs2)
      ;  '$skip_list'(N2,Rs2,Ts2),
         (  Ts2 == []
         -> M1 is N2-L1,
            length(Rs1,M1)
         ;  var(Ts2),
            (  N2 > 0
            -> Ts2 \== Rs1,
               sam_length_(Rs2,Rs1)     % switch argument order
            ;  Rs1 == Rs2
            -> is_list(Rs1)             % simpler enumeration
            ;  sam_length_(Rs1,Rs2)
            )
         )
      )
   ).

Sample queries:

?- sam_length(L,[_|L]).
   false.
?- sam_length([_],L).
   L = [_A].
?- sam_length(L,M).
   L = [], M = []
;  L = [_A], M = [_B]
;  ... .

Answer 4

How about:

same_length2(L1, L2) :-
    lists2_end_len(L1, E1, Len1, L2, E2, Len2),
    % If ends are same, the length before the ends must be same
    (   E1 == E2
    % == is fastest portable integer comparison in swi-prolog
    ->  Len1 == Len2,
        same_length(E1, E2)
    ;   same_length(L1, L2)
    ). 

lists2_end_len(L1, E1, Len1, L2, E2, Len2) :-
    lists2_end_len_(L1, E1, _, 0, Len1Calc, L2, E2, _, 0, Len2Calc),
    Len1 = Len1Calc,
    Len2 = Len2Calc.
    
% Not using '$skip_list', to be portable
lists2_end_len_(L, E, Cl, U, Len, L2, E2, Cl2, U2, Len2) :-
    (   \+ \+ L = []
    % Found end of list
    ->  E = L,
        Len = U,
        (   L == []
        ->  Cl = true,
            % Can fail fast if other list is longer
            (   integer(U2)
            ->  U >= U2
            )
        ;   Cl = false
        ),
        (   nonvar(Len2)
        % Both lists traversed
        ->  true
        ;   lists2_end_len_(L2, E2, Cl2, U2, Len2, L, E, Cl, U, Len)
        )
    ;   L = [_|T],
        % Occurs check 
        T \== L,
        U1 is U + 1,
        lists2_end_len_(L2, E2, Cl2, U2, Len2, T, E, Cl, U1, Len)
    ).

Results in swi-prolog:

?- length(L, 10_000_000), time(same_length2(L, [])).
% 6 inferences, 0.000 CPU in 0.000 seconds (89% CPU, 253336 Lips)
false.

?- freeze(R, R=[_|L]), same_length2(L, R).
false.

?- L = [_|L], same_length2(L, []).
false.

?- same_length2([1,2|L], [3,4,5|L]).
false.

?- same_length2(L, [_|L]).
false.

?- same_length2(L, [_,_|L]).
false.

?- same_length2([_|L], L).
false.

?- same_length2([_,_|L], L).
false.

?- same_length2(non_list, non_list).
false.

?- same_length2([a,b,c], [1,2,3]).
true.

?- same_length2(L1, L2).
L1 = L2, L2 = [] ;
L1 = [_],
L2 = [_] ;
L1 = [_, _],
L2 = [_, _] ;

?- same_length2([1|L], [3,4,5|R]).
L = [_, _],
R = [] ;
L = [_, _, _],
R = [_] ;
L = [_, _, _, _],
R = [_, _] ;

Answer 5

This is reasonably elegant, but with performance degradation:

% Using a previously-seen-tails list
same_length2(L, M) :-
    same_length2_(L, M, []).

same_length2_([], [], _).
% P is list of tails previously visited
same_length2_([HL|L], [HM|M], P) :-
    same_length2_chk_([HL|L], P),
    same_length2_chk_([HM|M], P),
    % Append after checking, to never see again
    append([[HL|L], [HM|M]], P, P1),
    same_length2_(L, M, P1).

same_length2_chk_(T, P) :-
    % Ensure no match with previously-seen tails
    \+ (
        member(E, P),
        T == E
    ).

Results in swi-prolog:

?- same_length2([_|L], [_|L]).
L = [] ;
L = [_] ;
L = [_, _] ;

?- length(L, 10_000_000), time(same_length2(L, [])).
% 3 inferences, 0.000 CPU in 0.000 seconds (88% CPU, 153249 Lips)
false.

?- freeze(R, R=[_|L]), same_length2(L, R).
false.

?- L = [_|L], same_length2(L, []).
false.

?- same_length2([1,2|L], [3,4,5|L]).
false.

?- same_length2(L, [_|L]).
false.

?- same_length2([_|L], L).
false.

?- same_length2(L, [_,_|L]).
false.

?- same_length2([_,_|L], L).
false.

?- same_length2(non_list, non_list).
false.

?- same_length2([a,b,c], [1,2,3]).
true.

?- same_length2([1|L], [3,4,5|R]).
L = [_, _],
R = [] ;
L = [_, _, _],
R = [_] ;
L = [_, _, _, _],
R = [_, _] ;

% Increasingly slow
?- time(same_length2(L1, L2)).
% 1 inferences, 0.000 CPU in 0.000 seconds (61% CPU, 116455 Lips)
L1 = L2, L2 = [] ;
% 13 inferences, 0.000 CPU in 0.000 seconds (87% CPU, 729354 Lips)
L1 = [_],
L2 = [_] ;
% 15 inferences, 0.000 CPU in 0.000 seconds (82% CPU, 795123 Lips)
L1 = [_, _],
L2 = [_, _] ;
% 19 inferences, 0.000 CPU in 0.000 seconds (82% CPU, 1558399 Lips)
L1 = [_, _, _],
L2 = [_, _, _] ;