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.

Answer 2

The following code is based on if_/3 and (=)/3 (a.k.a. equal_truth/3), as implemented by @false in Prolog union for A U B U C:

=(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 ). 

Compared to occurrences/3, the auxiliary occurrences_aux/3 uses a different argument order that passes the list Es as the first argument, which can enable first-argument indexing:

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

As pointed out by @migfilg, the goal Fs=[1,2], occurrences_aux(Es,E,Fs) should fail, as it is logically false: occurrences_aux(_,E,Fs) states that all elements in Fs are equal to E. However, on its own, occurrences_aux/3 does not terminate in cases like this.

We can use an auxiliary predicate allEqual_to__lazy/2 to improve termination behaviour:

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

With all auxiliary predicates in place, let's define 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 

Let's have some queries:

?- 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's 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]. 

---

Edit 2015-04-27

Some more queries for testing if the occurrences/3 universal terminates in certain cases:

?-           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.