same_length/3有没有cut-less的实现方式？

Question

假设我想断言三个列表的长度相同。我可以这样做：

same_length(First, Second, Third) :-
  same_length(First, Second),
  same_length(Second, Third).

当实例化 First 或 Second 时，这会做正确的事情。当所有三个参数都被实例化时，它也有效！然而，像 length(Third, 3), same_length(First, Second, Third) 这样的调用会导致它 return 带有选择点的正确答案（所有三个列表的长度都是 3），然后永远循环生成永远不会匹配的解决方案。

我写了一个我认为在任何情况下都能做正确事情的版本：

same_length(First, Second, Third) :-
  /* naively calling same_length(First, Second), same_length(Second, Third) doesn't work,
     because it will fail to terminate in the case where both First and Second are
     uninstantiated.
     by always giving the first same_length/2 clause a real list we prevent it from
     generating infinite solutions */
  ( is_list(First), same_length(First, Second), same_length(First, Third), !
  ; is_list(Second), same_length(Second, First), same_length(Second, Third), !
  ; is_list(Third), same_length(Third, First), same_length(Third, Second), !
    % if none of our arguments are instantiated then it's appropriate to not terminate:
  ; same_length(First, Second), same_length(Second, Third) ).

我一直听说应该如何尽可能避免切割，这里可以避免吗？

作为奖励问题，我认为这些是绿色削减，因为最终谓词是完全相关的，这是真的吗？

Answer 1

为什么不按照通常定义 same_length/2 的方式定义 same_length/3？

same_length([], [], []).
same_length([_| T1], [_| T2], [_| T3]) :-
    same_length(T1, T2, T3).

在所有参数未绑定的情况下调用时效果很好：

?- same_length(L1, L2, L3).
L1 = L2, L2 = L3, L3 = [] ;
L1 = [_990],
L2 = [_996],
L3 = [_1002] ;
L1 = [_990, _1008],
L2 = [_996, _1014],
L3 = [_1002, _1020] ;
L1 = [_990, _1008, _1026],
L2 = [_996, _1014, _1032],
L3 = [_1002, _1020, _1038] ;
...

在您提到的情况下没有虚假的选择点或非终止回溯：

?- length(L3, 3), same_length(L1, L2, L3).
L3 = [_1420, _1426, _1432],
L1 = [_1438, _1450, _1462],
L2 = [_1444, _1456, _1468].

same_length/3有没有cut-less的实现方式？

Is there a cut-less way to implement same_length/3?

prolog

logical-purity

non-termination