更好的纯版本 same_length/2

Question

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

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 的解决方案：

% 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 2

更新的解决方案

这是我的解决方案：

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]。但它是纯粹的，并且会为引用的查询产生正确的答案。