Pure Prolog programs that distinguish between the equality and inequality of terms in a clean manner suffer from execution inefficiencies ; even when all terms of relevance are ground.
A recent example on SO is this answer. All answers and all failures are correct in this definition. Consider:
?- 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).
While the program is flawless from a declarative viewpoint, its direct execution on current systems like B, SICStus, SWI, YAP is unnecessarily inefficient. For the following goal, a choicepoint is left open for each element of the list.
?- occurrences(a,[a,a,a,a,a],M).
M = [a, a, a, a, a] (;
false).
This can be observed by using a sufficiently large list of as as follows. You might need to adapt the I such that the list can still be represented ; in SWI this would mean that
1mo the I must be small enough to prevent a resource error for the global stack like the following:
?- 24=I,N is 2^I,length(L,N), maplist(=(a),L).
ERROR: Out of global stack
2do the I must be large enough to provoke a resource error for the local stack:
?- 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
To overcome this problem and still retain the nice declarative properties some comparison predicate is needed.
(How should this comparison predicate be defined?)
Here is such a possible definition:
equality_reified(X, X, true).
equality_reified(X, Y, false) :-
dif(X, Y).
Edit: Maybe the argument order should be reversed similar to the ISO built-in compare/3 (link links to draft only).
An efficient implementation of it would handle the fast determinate cases first:
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).
Edit: it is not clear to me whether or not X = Y is a suitable guard in the presence of constraints. Without constraints, ?=(X, Y) or X = Y are the same.
Example
As suggested by @user1638891, here is an example how one might use such a primitive. The original code by mats was:
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).
Which can be rewritten to something like:
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).
Please note that SWI's second-argument indexing is only activated, after you enter a query like occurrences(_,[],_). Also, SWI need the inherently nonmonotonic if-then-else, since it does not index on (;)/2 – disjunction. SICStus does so, but has only first argument indexing. So it leaves one (1) choice-point open (at the end with []).
question from:https://stackoverflow.com/questions/13664870/reification-of-term-equality-inequality 
