How to implement a not_all_equal/1 predicate

问题:

How would one implement a not_all_equal/1 predicate, which succeeds if the given list contains at least 2 different elements and fails otherwise?

Here is my attempt (a not very pure one):

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

This however does not always have the best behaviour:

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

In this example, only the first answer should come out, the two other ones are superfluous.

回答1:

Here's a straightforward way you can do it and preserve logical-purity!

not_all_equal([E|Es]) :-
   some_dif(Es, E).

some_dif([X|Xs], E) :-
   (  dif(X, E)
   ;  X = E, some_dif(Xs, E)
   ).

Here are some sample queries using SWI-Prolog 7.7.2.

First, the most general query:

?- not_all_equal(Es).
   dif(_A,_B), Es = [_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_A,_A,_B|_C]
...

Next, the query the OP gave in the question:

?- not_all_equal([A,B,C]), A=a, B=b.
   A = a, B = b
;  false.                          % <- the toplevel hints at non-determinism

Last, let's put the subgoal A=a, B=b upfront:

?- A=a, B=b, not_all_equal([A,B,C]).
   A = a, B = b
;  false.                          % <- (non-deterministic, like above)

Good, but ideally the last query should have succeeded deterministically!

---

Enter library(reif)

First argument indexing takes the principal functor of the first predicate argument (plus a few simple built-in tests) into account to improve the determinism of sufficiently instantiated goals.

This, by itself, does not cover dif/2 satisfactorily.

What can we do? Work with reified term equality/inequality—effectively indexing dif/2!

some_dif([X|Xs], E) :-                     % some_dif([X|Xs], E) :-
   if_(dif(X,E), true,                     %    (  dif(X,E), true
       (X = E, some_dif(Xs,E))             %    ;  X = E, some_dif(Xs,E)
      ).                                   %    ).

Notice the similarities of the new and the old implementation!

Above, the goal X = E is redundant on the left-hand side. Let's remove it!

some_dif([X|Xs], E) :-
   if_(dif(X,E), true, some_dif(Xs,E)).

Sweet! But, alas, we're not quite done (yet)!

?- not_all_equal(Xs).
DOES NOT TERMINATE

What's going on?

It turns out that the implementation of dif/3 prevents us from getting a nice answer sequence for the most general query. To do so—without using additional goals forcing fair enumeration—we need a tweaked implementation of dif/3, which I call diffirst/3:

diffirst(X, Y, T) :-
   (  X == Y -> T = false
   ;  X \= Y -> T = true
   ;  T = true,  dif(X, Y)
   ;  T = false, X = Y
   ).

Let's use diffirst/3 instead of dif/3 in the definition of predicate some_dif/2:

some_dif([X|Xs], E) :-
   if_(diffirst(X,E), true, some_dif(Xs,E)).

So, at long last, here are above queries with the new some_dif/2:

?- not_all_equal(Es).                     % query #1
   dif(_A,_B), Es = [_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_B|_C]
;  dif(_A,_B), Es = [_A,_A,_A,_B|_C]
...

?- not_all_equal([A,B,C]), A=a, B=b.      % query #2
   A = a, B = b
;  false.

?- A=a, B=b, not_all_equal([A,B,C]).      % query #3
A = a, B = b.

Query #1 does not terminate, but has the same nice compact answer sequence. Good!

Query #2 is still non-determinstic. Okay. To me this is as good as it gets.

Query #3 has become deterministic: Better now!

---

The bottom line:

1. Use library(reif) to tame excess non-determinism while preserving logical purity!
2. diffirst/3 should find its way into library(reif) :)

---

---

---

EDIT: more general using a meta-predicate (suggested by a comment; thx!)

Let's generalize some_dif/2 like so:

:- meta_predicate some(2,?).
some(P_2, [X|Xs]) :-
   if_(call(P_2,X), true, some(P_2,Xs)).

some/2 can be used with reified predicates other than diffirst/3.

Here an update to not_all_equal/1 which now uses some/2 instead of some_dif/2:

not_all_equal([X|Xs]) :-
   some(diffirst(X), Xs).

Above sample queries still give the same answers, so I won't show these here.

回答2:

Here is a partial implementation using library(reif) for SICStus|SWI. It's certainly correct, as it produces an error when it is unable to proceed. But it lacks the generality we'd like to have.

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.

Edit: Now I realize that I do not need to add that many dif/2 goals at all! It suffices that one variable is different to the first one! No need for mutual exclusivity! I still feel a bit insecure to remove the dif(B,C) goals ...

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

The answers are exactly the same... what is happening here, me thinks. Is this version weaker, that is less consistent?