Обоснование равенства/неравенства

Ответ 1

Ну, во-первых, имя должно быть более декларативным, например equality_truth/2.

Ответ 2

Следующий код основан на if_/3 и (=)/3 (aka equal_truth/3), как реализовано @false в Prolog union для AUBUC:

=(X, Y, R) :- X == Y,    !, R = true.
=(X, Y, R) :- ?=(X, Y),  !, R = false. % syntactically different
=(X, Y, R) :- X \= Y,    !, R = false. % semantically different
=(X, Y, R) :- R == true, !, X = Y.
=(X, X, true).
=(X, Y, false) :-
   dif(X, Y).

if_(C_1, Then_0, Else_0) :-
   call(C_1, Truth),
   functor(Truth,_,0),  % safety check
   ( Truth == true -> Then_0 ; Truth == false, Else_0 ).

По сравнению с occurrences/3 вспомогательный occurrences_aux/3 использует другой порядок аргументов, который передает список Es в качестве первого аргумента, который может включать индексацию первого аргумента:

occurrences_aux([], _, []).
occurrences_aux([X|Xs], E, Ys0) :-
   if_(E = X, Ys0 = [X|Ys], Ys0 = Ys),
   occurrences_aux(Xs, E, Ys).

Как указано @migfilg, цель Fs=[1,2], occurrences_aux(Es,E,Fs) должна завершиться неудачно, поскольку она логически ложна: occurrences_aux(_,E,Fs) указывает, что все элементы из Fs равны E. Однако сам по себе occurrences_aux/3 не заканчивается в таких случаях.

Мы можем использовать вспомогательный предикат allEqual_to__lazy/2 для улучшения поведения завершения:

allEqual_to__lazy(Xs,E) :-
   freeze(Xs, allEqual_to__lazy_aux(Xs,E)).

allEqual_to__lazy_aux([],_).
allEqual_to__lazy_aux([E|Es],E) :-
   allEqual_to__lazy(Es,E).

Со всеми вспомогательными предикатами на месте определите occurrences/3:

occurrences(E,Es,Fs) :-
   allEqual_to__lazy(Fs,E),    % enforce redundant equality constraint lazily
   occurrences_aux(Es,E,Fs).   % flip args to enable first argument indexing

Пусть есть несколько запросов:

?- occurrences(E,Es,Fs).       % first, the most general query
Es = Fs, Fs = []        ;
Es = Fs, Fs = [E]       ;
Es = Fs, Fs = [E,E]     ;
Es = Fs, Fs = [E,E,E]   ;
Es = Fs, Fs = [E,E,E,E] ...    % will never terminate universally, but ...
                               % that ok: solution set size is infinite

?- Fs = [1,2], occurrences(E,Es,Fs).
false.                         % terminates thanks to allEqual_to__lazy/2

?- occurrences(E,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1],     E=1                     ;
Fs = [2,2],                 E=2           ;
Fs = [3,3],                           E=3 ;
Fs = [],      dif(E,1), dif(E,2), dif(E,3).

?- occurrences(1,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1].                  % succeeds deterministically

?- Es = [E1,E2], occurrences(E,Es,Fs).
Es = [E,  E], Fs = [E,E],     E1=E ,     E2=E  ;
Es = [E, E2], Fs = [E],       E1=E , dif(E2,E) ;
Es = [E1, E], Fs = [E],   dif(E1,E),     E2=E  ;
Es = [E1,E2], Fs = [],    dif(E1,E), dif(E2,E).

?- occurrences(1,[E1,1,2,1,E2],Fs).
    E1=1 ,     E2=1 , Fs = [1,1,1,1] ;
    E1=1 , dif(E2,1), Fs = [1,1,1]   ;
dif(E1,1),     E2=1 , Fs = [1,1,1]   ;
dif(E1,1), dif(E2,1), Fs = [1,1].

Редактировать 2015-04-27

Несколько запросов для тестирования, если универсальное завершение occurrences/3 завершается в определенных случаях:

?-           occurrences(1,L,[1,2]).
false. 
?- L = [_|_],occurrences(1,L,[1,2]).
false.
?- L = [X|X],occurrences(1,L,[1,2]).
false.
?- L = [L|L],occurrences(1,L,[1,2]).
false.

Ответ 3

Кажется, лучше всего назвать этот предикат теми же аргументами (=)/3. Таким образом, условия, подобные if_/3, теперь более читабельны. И использовать вместо суффикса _t вместо _truth:

memberd_t(_X, [], false).
memberd_t(X, [Y|Ys], Truth) :-
   if_( X = Y, Truth=true, memberd_t(X, Ys, Truth) ).

Раньше:

memberd_truth(_X, [], false).
memberd_truth(X, [Y|Ys], Truth) :-
   if_( equal_truth(X, Y), Truth=true, memberd_truth(X, Ys, Truth) ).

Ответ 4

ОБНОВЛЕНИЕ: Этот ответ был заменен моим 18 апреля. Я не предлагаю удалить его из-за комментариев ниже.

Мой предыдущий ответ был неправильным. Следующее идет против тестового примера в вопросе, и реализация имеет желаемую особенность, избегая лишних точек выбора. Я предполагаю, что режим верхнего предиката равен?, +,? хотя другие режимы могут быть легко реализованы.

В программе есть 4 предложения: список во втором аргументе посещается, и для каждого члена есть две возможности: он либо объединяется с 1-м аргументом верхнего предиката, либо отличается от него, и в этом случае a dif применяется:

occurrences(X, L, Os) :- occs(L, X, Os).

occs([],_,[]).
occs([X|R], X, [X|ROs]) :- occs(R, X, ROs).
occs([X|R], Y, ROs) :- dif(Y, X), occs(R, Y, ROs).

Примеры запуска, используя YAP:

?- occurrences(1,[E1,1,2,1,E2],Fs).
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
E1 = 1,
Fs = [1,1,1],
dif(1,E2) ? ;
E2 = 1,
Fs = [1,1,1],
dif(1,E1) ? ;
Fs = [1,1],
dif(1,E1),
dif(1,E2) ? ;
no  

?- occurrences(E,[E1,E2],Fs).
E = E1 = E2,
Fs = [E,E] ? ;
E = E1,
Fs = [E],
dif(E,E2) ? ;
E = E2,
Fs = [E],
dif(E,E1) ? ;
Fs = [],
dif(E,E1),
dif(E,E2) ? ;
no

Ответ 5

Здесь еще более короткая логически-чистая реализация occurrences/3.

Мы построим его на meta-predicate tfilter/3, предикат равенства терминов (=)/3 и сопрограмма allEqual_to__lazy/2 (определенная в моем предыдущем ответе на этот вопрос):

occurrences(E,Xs,Es) :-
   allEqual_to__lazy(Es,E),
   tfilter(=(E),Xs,Es).

Готово! Чтобы облегчить сравнение, мы повторно запускаем те же запросы, что и в предыдущем ответе:

?- Fs = [1,2], occurrences(E,Es,Fs).
false.

?- occurrences(E,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1],     E=1                     ;
Fs = [2,2],                 E=2           ;
Fs = [3,3],                           E=3 ;
Fs = [],      dif(E,1), dif(E,2), dif(E,3).

?- occurrences(1,[1,2,3,1,2,3,1],Fs).
Fs = [1,1,1].

?- Es = [E1,E2], occurrences(E,Es,Fs).
Es = [E, E ], Fs = [E,E],     E1=E ,     E2=E  ;
Es = [E, E2], Fs = [E],       E1=E , dif(E2,E) ;
Es = [E1,E ], Fs = [E],   dif(E1,E),     E2=E  ;
Es = [E1,E2], Fs = [],    dif(E1,E), dif(E2,E).

?- occurrences(1,[E1,1,2,1,E2],Fs).
    E1=1 ,     E2=1 , Fs = [1,1,1,1] ;
    E1=1 , dif(E2,1), Fs = [1,1,1]   ;
dif(E1,1),     E2=1 , Fs = [1,1,1]   ;
dif(E1,1), dif(E2,1), Fs = [1,1].

?- occurrences(1,L,[1,2]).
false.

?- L = [_|_],occurrences(1,L,[1,2]).
false.

?- L = [X|X],occurrences(1,L,[1,2]).
false.

?- L = [L|L],occurrences(1,L,[1,2]).
false.

Наконец, самый общий запрос:

?- occurrences(E,Es,Fs).
Es = Fs, Fs = []      ;
Es = Fs, Fs = [E]     ;
Es = Fs, Fs = [E,E]   ;
Es = Fs, Fs = [E,E,E] % ... and so on ad infinitum ...

Мы получаем те же ответы.

Ответ 6

Реализация occurrences/3 ниже опирается на мои предыдущие ответы, а именно на получение прибыли от механизма индексирования предложения по 1-му аргументу, чтобы избежать некоторых точек выбора и устраняет все возникшие проблемы.

Кроме того, он справляется с проблемой во всех подчиненных реализациях до сих пор, включая тот, о котором идет речь в вопросе, а именно о том, что все они входят в бесконечный цикл, когда запрос имеет 2 первых аргумента бесплатно, а третий - с разными наземных элементов. Разумеется, правильное поведение - сбой.

Использование предиката сравнения

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

Реализация

В этом порядке рассматриваются три исключительных случая: если аргумент 2 аргументирован, то он посещается рекурсивно; в противном случае, если третий аргумент заземлен, он проверяется, а затем посещается рекурсивно; в противном случае для 2-го и 3-го аргументов создаются подходящие списки.

occurrences(X, L, Os) :-
  ( nonvar(L) -> occs(L, X, Os) ;
    ( nonvar(Os) -> check(Os, X), glist(Os, X, L) ; v_occs(L, X, Os) ) ).

При посещении земли 2-й аргумент имеет три случая, когда список не пуст: если его голова и X выше являются грубыми и унифицируемыми, X находится в начале результирующего списка вхождений, и нет другая альтернатива; в противном случае существуют две альтернативы: X отличается от головы или объединяется с ней:

occs([],_,[]).
occs([X|R], Y, ROs) :-
  ( X==Y -> ROs=[X|Rr] ; foccs(X, Y, ROs, Rr) ), occs(R, Y, Rr).

foccs(X, Y, ROs, ROs) :- dif(X, Y).
foccs(X, X, [X|ROs], ROs).

Проверка основного аргумента состоит в том, чтобы убедиться, что все его члены объединяются с X. В принципе эта проверка может выполняться с помощью glist/3, но таким образом избегаются неиспользованные точки выбора.

check([], _).
check([X|R], X) :- check(R, X).

Посещение основного 3-го аргумента со свободным 2-м аргументом должно заканчиваться добавлением переменных, отличных от X, в сгенерированный список. На каждом этапе рекурсии есть две альтернативы: текущая глава сгенерированного списка является текущим заголовком посещенного списка, который должен быть унифицирован с помощью X или является свободной переменной, отличной от X. Это теоретическое описание, потому что на самом деле существует бесконечное количество решений, и 3-е предложение никогда не будет достигнуто, когда голова списка является переменной. Поэтому приведено ниже третье предложение, чтобы избежать неприемлемых точек выбора.

glist([], X, L) :- gdlist(L,X).
glist([X|R], X, [X|Rr]) :- glist(R, X, Rr).
%% glist([X|R], Y, [Y|Rr]) :- dif(X, Y), glist([X|R], Y, Rr).

gdlist([], _).
gdlist([Y|R], X) :- dif(X, Y), gdlist(R, X).

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

v_occs([], _, []).
v_occs([X|R], X, [X|ROs]) :- v_occs(R, X, ROs).
%% v_occs([X|R], Y, ROs) :- dif(Y, X), v_occs(R, Y, ROs). % never used

Примеры тестов

?- occurrences(1,[E1,1,2,1,E2],Fs).
Fs = [1,1],
dif(E1,1),
dif(E2,1) ? ;
E2 = 1,
Fs = [1,1,1],
dif(E1,1) ? ;
E1 = 1,
Fs = [1,1,1],
dif(E2,1) ? ;
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
no

?- occurrences(1,L,[1,2]).
no

?- occurrences(1,L,[1,E,1]).
E = 1,
L = [1,1,1] ? ;
E = 1,
L = [1,1,1,_A],
dif(1,_A) ? ;
E = 1,
L = [1,1,1,_A,_B],
dif(1,_A),
dif(1,_B) ? ;
   ...