различный / 2 - существует ли чистое, детерминированное определение?

Давайте доведем его до предела --- с помощью list_nonmember_t/3, _ 2_ и or_/2!

some_absent_t(Xs,Ys,Truth) :-
   exists_in_t(list_nonmember_t(Ys),Xs,Truth).

different(Xs,Ys) :-
   or_(some_absent_t(Xs,Ys),
       some_absent_t(Ys,Xs)).

Первая попытка!

Следующий код основан на мета-предикатах tfilter/3 и _ 2_, монотонная управляющая конструкция« если-то-еще », if_/3, овеществленная унарная логическая связка not_t/3 и обобщенный термин предикат равенства _ 5_:

different([],[_|_]).
different([X|Xs0],Ys0) :-
   tpartition(=(X),Ys0,Es,Ys1),
   if_(Es=[], true, (tfilter(not_t(=(X)),Xs0,Xs1),different(Xs1,Ys1))).

Пример запроса:

?- different([A,B],[X,Y]).
                A=Y ,           dif(B,Y),     X=Y
;     A=X           ,     B=X           , dif(X,Y)
;     A=X           , dif(B,X), dif(B,Y), dif(X,Y)
;               A=Y ,               B=Y , dif(X,Y)
;               A=Y , dif(B,X), dif(B,Y), dif(X,Y)
; dif(A,X), dif(A,Y).

Соблюдаем детерминизм при работе с наземными данными:

?- different([5,4],[1,2]).
true.

Вышеупомянутый подход кажется шагом в правильном направлении ... Но, как есть, я бы не назвал его идеальным.

Вот еще одна попытка! Мы используем монотонную управляющую конструкцию if-then-else if_/3 в сочетании с предикатом членства в реифицируемом списке memberd_t/3 и индексация первого аргумента, чтобы избежать создания бесполезных точек выбора.

different(Xs,Ys) :-
   different_aux(Xs,Ys,Xs,Ys).

different_aux([],[_|_],Xs0,Ys0) :-
   different_aux(Ys0,[],Ys0,Xs0).     % swap Xs/Ys pair
different_aux([X|Xs],Ys,Xs0,Ys0) :-
   if_(memberd_t(X,Ys0),
       different_aux(Ys,Xs,Ys0,Xs0),  % variant: different_aux(Xs,Ys,Xs0,Ys0)
       true).

Сначала мы выполняем запрос, который ожидаем неудачи:

?- different([1,2,3],[2,3,1]).
false.

Следующие запросы похожи на приведенный выше ошибочный запрос; в каждом из них есть один «другой» элемент x, помещенный в разные индексы в первом [1,2,3] или втором списке [2,3,1]:

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]),
   different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]),
   different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]).
true.                                 % all subgoals succeed deterministically

Хорошо! Давайте запустим еще один (довольно общий) запрос, который я использовал в моем предыдущем ответе:

?- different([A,B],[X,Y]).
      A=X ,               B=X , dif(Y,X)
;     A=X ,           dif(B,X), dif(Y,B)
;               A=Y , dif(B,X), dif(Y,X)
; dif(A,X), dif(A,Y).

Компактность! Большое улучшение по сравнению с тем, что я представил ранее!

(Во многом вдохновленный последним ответом @ repeat, имена все еще слишком неуклюжие)

different(Xs, Ys) :-
   if_(tnotexists_inlist_t(list_memberd_t(Ys), Xs),
      true,
      tnotexists_inlist_t(list_memberd_t(Xs), Ys)).

tnotexists_inlist_t(_P_2, [], false).
tnotexists_inlist_t(P_2, [E|Es], T) :-
   if_(call(P_2, E),
      tnotexists_inlist_t(P_2, Es, T),
      T = true).

Вернуться к истокам! Этот вариант очень близок к коду, указанному OP в вопросе.

Следующее основано на if_/3 и memberd_t/3.

different(Xs,Ys) :-
   if_(some_absent_t(Xs,Ys),
       true,
       some_absent_t(Ys,Xs,true)).

some_absent_t([]    ,_ ,false).
some_absent_t([X|Xs],Ys,Truth) :-
   if_(memberd_t(X,Ys), some_absent_t(Xs,Ys,Truth), Truth=true).

Вот наземный запрос:

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]),
   different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]),
   different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]).
true.                                 % all subgoals succeed deterministically

И вот (более общий) запрос, который я использовал в предыдущих ответах:

?- different([A,B],[X,Y]).
      A=X ,               B=X ,           dif(Y,X)
;     A=X ,           dif(B,X), dif(B,Y)
;               A=Y ,               B=Y , dif(Y,X), dif(Y,X)
;               A=Y , dif(B,X), dif(B,Y), dif(Y,X)
; dif(A,X), dif(A,Y).

Следующая участница конкурса красоты! -)

В этом ответе показан измененный вариант кода, показанный в предыдущем ответе. Он использует овеществленное соединение и дизъюнкцию:

and_(P_1,Q_1) :-
   and_t(P_1,Q_1,true).

or_(P_1,Q_1) :-
   or_t(P_1,Q_1,true).

and_t(P_1,Q_1,Truth) :-
   if_(P_1, call(Q_1,Truth), Truth=false).

or_t(P_1,Q_1,Truth) :-
   if_(P_1, Truth=true, call(Q_1,Truth)).

Обратите внимание на две версии для «и» и «или»; те, у которых есть суффикс _t, имеют дополнительный аргумент для значения истинности, те, у которых нет суффикса, нет и предполагают, что Truth=true должно выполняться.

На основе and_t/3 и предиката неравенства обобщенных терминов dif/3 мы определяем nonmember_t/3:

nonmember_t(X,Ys,Truth) :-
   list_nonmember_t(Ys,X,Truth).

list_nonmember_t([]    ,_, true).
list_nonmember_t([Y|Ys],X,Truth) :-
   and_t(dif(X,Y), list_nonmember_t(Ys,X), Truth).

Теперь давайте определим some_absent_t/3, different_t/3 и different/2, вот так:

some_absent_t([]    ,_ ,false).
some_absent_t([X|Xs],Ys,Truth) :-
   or_t(nonmember_t(X,Ys), some_absent_t(Xs,Ys), Truth).

different_t(Xs,Ys,Truth) :-
   or_t(some_absent_t(Xs,Ys),
        some_absent_t(Ys,Xs),
        Truth).

different(Xs,Ys) :-
   different_t(Xs,Ys,true).

Он все еще работает?

?- different([A,B],[X,Y]).
      A=X ,               B=X ,           dif(Y,X)
;     A=X ,           dif(B,X), dif(B,Y)
;               A=Y ,               B=Y , dif(Y,X), dif(Y,X)
;               A=Y , dif(B,X), dif(B,Y), dif(Y,X)
; dif(A,X), dif(A,Y).                     % same result as before

?- different([4,2,3],[2,3,1]), different([1,2,3],[4,3,1]),
   different([1,4,3],[2,3,1]), different([1,2,3],[2,4,1]),
   different([1,2,4],[2,3,1]), different([1,2,3],[2,3,4]).
true.                                    % same result as before

Выглядит хорошо!

В целом, это не огромное улучшение по сравнению с существующими ответами, но IMO несколько более читаемый код и обновленная версия different/2 в качестве дополнительного бонуса!

Не так давно была предложена следующая жирным шрифтом (+500):

^{Идиоматический ответ здесь все еще отсутствует. Например, or_t / 3 должно быть (;) / 3. Это еще не все.}

Вызов принят! Этот ответ является продолжением предыдущего ответа.

1. Мы используем овеществленную логическую связку (;)/3, которую можно определить так:

   ';'(P_1,Q_1,T) :- if_(P_1, T=true, call(Q_1,T)).
   

2. Затем мы определяем мета-предикат call_/1. Это полезно с овеществленными предикатами, используемыми в этом ответе. По своему названию и семантике call_/1 следует за if_/3, and_/2 и or_/2!

   call_(P_1) :- call(P_1,true).
   

3. Используя (;)/3, call_/1 и some_absent_t/3, мы реализуем different/2:

   different(As,Bs) :- call_((some_absent_t(As,Bs) ; some_absent_t(Bs,As))).
   

Готово! Вот и все.

Давайте повторно запустим запросы, которые мы использовали в предыдущих ответах!

?- different([5,4],[1,2]).
true.

?- different([1,2,3],[2,3,1]).
false.

?- different([4,2,3],[2,3,1]), different([1,4,3],[2,3,1]), different([1,2,4],[2,3,1]),
   different([1,2,3],[4,3,1]), different([1,2,3],[2,4,1]), different([1,2,3],[2,3,4]).
true.

Те же вопросы, те же ответы ... Мне кажется, хорошо!

Что касается решений, в которых используется if_, я бы сказал, что альтернативным подходом было бы использование конструктивного отрицания с самого начала. Конструктивное отрицание исследовалось еще в 80-х годах. , пионером был Дэвид Чан, и до сих пор время от времени всплывает.

Предположим, у нас есть интерпретатор Пролога, который имеет конструктивное отрицание (~)/2. Это конструктивное отрицание (~)/2 можно использовать для определения декларативного if-then-else следующим образом, позвольте вызвать этот оператор (~->)/2:

  (A ~-> B; C) :- (A, B); (~A, C).

Если интерпретатор Пролога также имеет встроенную импликацию (=>)/2 помимо конструктивного отрицания, можно в качестве альтернативы определить декларативное if-then-else следующим образом, позвольте вызвать этот оператор (~=>)/2:

  (A ~=> B; C) :- (A => B), (~A => C).

Обратите внимание на переход от дизъюнкции (;)/2 к соединению (,)/2. Спросите людей, использующих бинарную диаграмму решений (BDD), почему они логически эквивалентны. Процедурно есть нюансы, но через черный ход встроенной импликации для определенного A второй вариант if-then-else также привнесет недетерминированность.

Но как бы мы могли обойтись и ввести, например, конструктивное отрицание в интерпретаторе Пролога? Самый простой способ - делегировать конструктивное отрицание решателю ограничений. Если решатель ограничений реализовал отрицание, это можно сделать следующим образом:

 ~ A :- #\ A.

Но существует не так много решателей ограничений, которые позволили бы разумно использовать такие примеры, как member/2 и т. Д. Поскольку часто они обеспечивают овеществленное отрицание только для таких областей, как конечные целые числа, рациональные числа и т. Д. Но для предиката, такого как member/2, мы для вселенной Хербранда потребуется овеществленное отрицание.

Также обратите внимание, что обычные подходы к конструктивному отрицанию также предполагают, что импликация обычного правила получает другое прочтение. Это означает, что обычно при конструктивном отрицании мы могли бы выбрать обычное определение member/2 и получить такие результаты запроса, как:

?- ~ member(X, [a,b,c]).
dif(X, a),
dif(X, b),
dif(X, c).

Но опять же, овеществленное отрицание вряд ли будет легко работать с определенными предикатами, поэтому следующий запрос, вероятно, не будет работать:

?- #\ member(X, [a,b,c]).
/* typically won't work */

Если вышеперечисленное завершится успешно, то любой из декларативных if-then-else, таких как (~->)/2 или (~=>)/2, будет реже использоваться, поскольку обычные определения предикатов уже доставляют декларативную интерпретацию интерпретатором Пролога. Но почему конструктивное отрицание не имеет широкого распространения? Одной из причин может быть большое пространство для дизайна такого интерпретатора Пролога. Я заметил, что у нас будут следующие варианты:

Обратная цепочка. Мы бы разделили обычный интерпретатор solve/1 на два предиката solvep/1 и solven/1. solvep/1 отвечает за решение положительных целей, а solven/1 отвечает за решение отрицательных целей. Когда мы попробуем это сделать, мы рано или поздно увидим, что нам нужно более внимательно относиться к кванторам и, вероятно, в конечном итоге получим метод исключения кванторов для области Herbrand.

Прямая цепочка. Мы также заметим, что при обратной цепочке мы столкнемся с проблемами при моделировании предложений с дизъюнкцией или экзистенциальным квантификатором в голове. Это связано с тем, что исчисление секвенций, подходящее для Пролога, имеет только одну формулу в правой части. Таким образом, либо мы перейдем к нескольким формулам с правой стороны и потеряем параконсистентность, либо мы будем использовать прямую цепочку.

Волшебные наборы: но прямая цепочка неконтролируемым образом загрязняет пространства решений. Так что нам может понадобиться какая-то комбинация прямого и обратного связывания. Я не имею в виду только то, что мы должны иметь возможность динамически переключаться между ними во время процесса решения, но я имею в виду, что нам также необходимы средства для создания наборов, которые направляют процесс прямой цепочки.

Дополнительные проблемы также отмечены в этом ответе здесь. Это не означает, что рано или поздно будет найдена формула, которая объединит все пары проблемы и решения, но это может занять некоторое время.

Пока