Чистые программы Пролога, которые различают равенство и неравенство терминов в чистом виде, страдают от неэффективности исполнения; даже когда все условия релевантности обоснованы.
Недавним примером SO является этот ответ. Все ответы и все сбои верны в этом определении. Рассмотрим:
?- Es = [E1,E2], occurrences(E, Es, Fs).
Es = Fs, Fs = [E, E],
E1 = E2, E2 = E ;
Es = [E, E2],
E1 = E,
Fs = [E],
dif(E, E2) ;
Es = [E1, E],
E2 = E,
Fs = [E],
dif(E, E1) ;
Es = [E1, E2],
Fs = [],
dif(E, E1),
dif(E, E2).
В то время как программа безупречна с декларативной точки зрения, ее прямое выполнение в текущих системах, таких как B, SICStus, SWI, YAP, излишне неэффективно. Для следующей цели точка выбора остается открытой для каждого элемента в списке.
?- occurrences(a,[a,a,a,a,a],M). M = [a, a, a, a, a] ; false.
Это можно наблюдать, используя достаточно большой список a следующим образом. Возможно, вам придется адаптировать I так, чтобы список мог быть представлен; в SWI это означало бы, что
1mo I должен быть достаточно мал, чтобы предотвратить ошибку ресурса для глобального стека, как показано ниже:
?- 24=I,N is 2^I,length(L,N), maplist(=(a),L). ERROR: Out of global stack
2do I должен быть достаточно большим, чтобы вызвать ошибку ресурса для локального стека:
?- 22=I,N is 2^I,length(L,N), maplist(=(a),L), ( Length=ok ; occurrences(a,L,M) ). I = 22, N = 4194304, L = [a, a, a, a, a, a, a, a, a|...], Length = ok ; ERROR: Out of local stack
Чтобы преодолеть эту проблему и по-прежнему сохранять хорошие декларативные свойства, необходим предикат сравнения.
Как следует определить этот предикат сравнения?
Вот такое возможное определение:
equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(X, Y).
Изменить: Возможно, порядок аргументов должен быть отменен, как и ISO, встроенный compare/3 (ссылка только на черновик).
Эффективная реализация его сначала обрабатывала бы быстро определенные случаи:
equality_reified(X, Y, R) :- X == Y, !, R = true. equality_reified(X, Y, R) :- ?=(X, Y), !, R = false. % syntactically different equality_reified(X, Y, R) :- X \= Y, !, R = false. % semantically different equality_reified(X, X, true). equality_reified(X, Y, false) :- dif(X, Y).
Изменить: мне непонятно, подходит ли X \= Y защитник при наличии ограничений. Без ограничений ?=(X, Y) или X \= Y совпадают.
Пример
Как показано в [user1638891], вот пример того, как можно использовать такой примитив. Исходный код матов был:
occurrences_mats(_, [], []).
occurrences_mats(X, [X|Ls], [X|Rest]) :-
occurrences_mats(X, Ls, Rest).
occurrences_mats(X, [L|Ls], Rest) :-
dif(X, L),
occurrences_mats(X, Ls, Rest).
Что можно переписать на что-то вроде:
occurrences(_, [], []).
occurrences(E, [X|Xs], Ys0) :-
reified_equality(Bool, E, X),
( Bool == true -> Ys0 = [X|Ys] ; Ys0 = Ys ),
% ( Bool = true, Ys0 = [X|Ys] ; Bool = true, Ys0 = Ys ),
occurrences(E, Xs, Ys).
reified_equality(R, X, Y) :- X == Y, !, R = true.
reified_equality(R, X, Y) :- ?=(X, Y), !, R = false.
reified_equality(true, X, X).
reified_equality(false, X, Y) :-
dif(X, Y).
Обратите внимание, что индексирование индекса второго индекса SWI активируется, после вводится запрос типа occurrences(_,[],_). Кроме того, SWI нуждается в неотъемлемо немонотонном if-then-else, поскольку он не индексируется на (;)/2 – дизъюнкции. SICStus делает это, но имеет только первый аргумент индексации. Таким образом, он оставляет один (1) выбор-точка открытым (в конце с []).
