Программы на чистом Prolog, которые четко различают равенство и неравенство терминов, страдают от неэффективности выполнения; даже когда все относящиеся к делу термины заземлены.
Недавний пример 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
2должен ли 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, вот пример того, как можно использовать такой примитив. Исходный код mats был:
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) точка выбора открытой (в конце с []).
occurrences/3, которые были представлены к этой дате, кроме моей вчерашней, входят в бесконечный цикл, когда у запроса есть первые два аргумента свободными, а третий - это список с разными основными элементами, правильное поведение будучи, конечно, потерпеть неудачу. - person migfilg schedule 19.04.2015