Same_length/2 更好的纯版本

鉴于频繁的纯定义same_length/2 as

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

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

是否有一个纯粹的定义不会在这种情况下循环？类似于纯（但效率较低）版本的东西append/3 called append2u/3 https://stackoverflow.com/a/65361752/772868.

我知道如何手动捕获此类情况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]
;  ... .

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

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

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

它建立在'$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]).
   false.
?- sam_length([_],L).
   L = [_A].
?- sam_length(L,M).
   L = [], M = []
;  L = [_A], M = [_B]
;  ... .