Как реализовать предикат not_all_equal/1

Вот простой способ сделать это и сохранить логическая чистота!

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

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

Вот несколько примеров запросов с использованием SWI-Prolog 7.7.2.

Сначала самый общий запрос:

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

Затем запрос, который ОП дал в вопросе:

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

Наконец, давайте поставим перед собой подцель A=a, B=b:

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

Хорошо, но в идеале последний запрос должен был выполниться детерминировано!

Введите library(reif)

Индексирование первого аргумента принимает главный функтор первый предикатный аргумент (плюс несколько простых встроенных тестов) для улучшения детерминизма достаточно конкретизированных целей.

Это само по себе не удовлетворительно покрывает dif/2.

Что мы можем сделать? Работайте с определенным термином "равенство/неравенство" эффективно индексирует 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)
      ).                                   %    ).

Обратите внимание на сходство новой и старой реализации!

Выше цель X = E избыточна с левой стороны. Давайте удалим!

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

Отлично! Но, увы, мы еще не совсем закончили (еще)!

?- not_all_equal(Xs).
DOES NOT TERMINATE

Что происходит?

Оказывается, реализация dif/3 не позволяет нам получить красивую последовательность ответов на самый общий запрос. Чтобы сделать это без использования дополнительных целей, форсирующих справедливое перечисление, нам нужна подправленная реализация dif/3, которую я называю diffirst/3:

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

Давайте использовать diffirst/3 вместо dif/3 в определении предиката some_dif/2:

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

Итак, наконец, вот приведенные выше запросы с новым 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.

Запрос №1 не завершается, но имеет такую ​​же компактную последовательность ответов. Хорошо!

Запрос № 2 по-прежнему не является детерминированным. Хорошо. Для меня это настолько хорошо, насколько это возможно.

Запрос №3 стал детерминированным: Теперь лучше!

Вывод:

1. Используйте library(reif), чтобы укротить избыточный недетерминизм, сохранив при этом логическую чистоту!
2. diffirst/3 должен попасть в library(reif) :)

РЕДАКТИРОВАТЬ: более общее использование мета-предикат (предложено комментарием; спасибо!)

Давайте обобщим some_dif/2 так:

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

some/2 можно использовать с вещественными предикатами, отличными от diffirst/3.

Вот обновление для not_all_equal/1, которое теперь использует some/2 вместо some_dif/2:

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

Приведенные выше примеры запросов по-прежнему дают те же ответы, поэтому я не буду их здесь показывать.

Вот частичная реализация с использованием 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 !')).

Ответы точно такие же... что здесь происходит, думаю я. Является ли эта версия более слабой, менее последовательной?