prolog - Reification of term equality/inequality

Question

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 []).

Answer 1

Well for one thing, the name should be more declarative, like equality_truth/2.