list - 如何实现 not_all_equal/1 谓词

Question

如何实现一个 not_all_equal/1 谓词，如果给定列表包含至少 2 个不同的元素，则该谓词成功，否则失败？

这是我的尝试(不是很纯粹的尝试):

not_all_equal(L) :-
    (   member(H1, L), member(H2, L), H1 \= H2 -> true
    ;   list_to_set(L, S),
        not_all_equal_(S)
    ).

not_all_equal_([H|T]) :-
    (   member(H1, T), dif(H, H1)
    ;   not_all_equal_(T)
    ).

然而，这并不总是具有最佳行为:

?- not_all_equal([A,B,C]), A = a, B = b.
A = a,
B = b ;
A = a,
B = b,
dif(a, C) ;
A = a,
B = b,
dif(b, C) ;
false.

在这个例子中，只有第一个答案应该出现，其他两个答案是多余的。

Answer 1

这是使用 library(reif) 实现 SICStus 的部分实现| SWI 。这当然是正确的，因为当它无法继续时会产生错误。但它缺乏我们想要的通用性。

not_all_equalp([A,B]) :-
   dif(A,B).
not_all_equalp([A,B,C]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(B,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ; dif(B,C) ; dif(B,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
   throw(error(representation_error(reified_disjunction),'C\'est trop !')).

?- not_all_equalp(L).
   L = [_A,_B], dif(_A,_B)
;  L = [_A,_A,_B], dif(_A,_B)
;  L = [_A,_B,_C], dif(_A,_B)
;  L = [_A,_A,_A,_B], dif(_A,_B)
;  L = [_A,_A,_B,_C], dif(_A,_B)
;  L = [_A,_B,_C,_D], dif(_A,_B)
;  error(representation_error(reified_disjunction),'C\'est trop !').
?- not_all_equalp([A,B,C]), A = a, B = b.
   A = a, B = b
;  false.

编辑:现在我意识到我根本不需要添加那么多 dif/2 目标! 一个变量与第一个变量不同就足够了!无需相互排斥!我仍然觉得删除 dif(B,C) 目标有点不安全......

not_all_equalp([A,B]) :-
   dif(A,B).
not_all_equalp([A,B,C]) :-
   if_(( dif(A,B) ; dif(A,C) ), true, false ).
not_all_equalp([A,B,C,D]) :-
   if_(( dif(A,B) ; dif(A,C) ; dif(A,D) ), true, false ).
not_all_equalp([_,_,_,_,_|_]) :-
   throw(error(representation_error(reified_disjunction),'C\'est trop !')).

答案是完全相同的......我认为这里发生了什么。这个版本是否较弱，一致性较差？