same_length/2 的更好的纯版本

Question

鉴于

same_length/2

的频繁纯定义 as

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

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

对于这种情况，是否存在不循环的纯定义？类似于

append/3

的纯（但效率较低）版本的东西称为

append2u/3

。

我知道如何使用

var/1

等手动捕获此类情况，但理想情况下，最好使用与原始定义一样纯净的版本。或者至少应该很简单。

我试过的是上面的定义

似乎有必要澄清一下：

请注意，某些查询本质上不得终止。想想：

?- 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]
;  ... .

没有其他方法可以使用句法答案替换的语言来枚举所有解决方案。

但是对于给定的查询，实现仍然可能会终止。

Answer 1

这个答案旨在最小化运行时成本。

它建立在

'$skip_max_list'/4

上并在Scryer Prolog上运行。

首先，一些辅助代码：

:- 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).

现在是主菜：

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)
            )
         )
      )
   ).

示例查询：

?- sam_length(L,[_|L])。
   错误的。
?- sam_length([_],L)。
   L = [_A]。
?- sam_length(L,M)。
   L = [], M = []
; L = [_A]，M = [_B]
; ……

Answer 2

使用

'$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).

查询：

?- 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 3

更新的解决方案

这是我的解决方案：

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

我不确定它是否具有您要查找的所有属性。例如，如果你打电话

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

然后它会列出许多答案，例如L = [_X, 2, 3]，而不仅仅是 [_X, _Y, _Z]。但它是纯粹的，并为引用的查询生成正确答案。

Answer 4

怎么样：

same_length2(L1, L2) :-
    list_end_len(L1, E1, Len1),
    list_end_len(L2, E2, Len2),
    % If ends are same, the length before the ends must be same
    (   E1 == E2
    ->  Len1 =@= Len2,
        same_length(E1, E2)
    ;   same_length(L1, L2) 
    ).
    
% Not using '$skip_list', to be portable
list_end_len(Lst, End, Len) :-
    list_end_len_(Lst, End, 0, Len).

list_end_len_(Lst, End, U, Len) :-
    (   (var(Lst) ; Lst == [])
    ->  End = Lst,
        Len = U
    ;   Lst = [_|T],
        U1 is U + 1,
        list_end_len_(T, End, U1, Len)
    ).

swi-prolog 中的结果：

?- 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 = [_, _] ;

类似于Perfoming member check on a difference list，但是怎么做呢？