Reification of term equality/inequality

问题:

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

回答1:

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

回答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.

回答3:

It seems to be best to call this predicate with the same arguments (=)/3. In this manner, conditions like if_/3 are now much more readable. And to use rather the suffix _t in place of _truth:

memberd_t(_X, [], false).
memberd_t(X, [Y|Ys], Truth) :-
   if_( X = Y, Truth=true, memberd_t(X, Ys, Truth) ).

Which used to be:

memberd_truth(_X, [], false).
memberd_truth(X, [Y|Ys], Truth) :-
   if_( equal_truth(X, Y), Truth=true, memberd_truth(X, Ys, Truth) ).

回答4:

UPDATE: This answer has been superseded by mine of 18 April. I do not propose that it be deleted because of the comments below.

My previous answer was wrong. The following one runs against the test case in the question and the implementation has the desired feature of avoiding superfluous choice-points. I assume the top predicate mode to be ?,+,? although other modes could easily be implemented.

The program has 4 clauses in all: the list in the 2nd argument is visited and for each member there are two possibilities: it either unifies with the 1st argument of the top predicate or is different from it in which case a dif constraint applies:

occurrences(X, L, Os) :- occs(L, X, Os).

occs([],_,[]).
occs([X|R], X, [X|ROs]) :- occs(R, X, ROs).
occs([X|R], Y, ROs) :- dif(Y, X), occs(R, Y, ROs).

Sample runs, using YAP:

?- occurrences(1,[E1,1,2,1,E2],Fs).
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
E1 = 1,
Fs = [1,1,1],
dif(1,E2) ? ;
E2 = 1,
Fs = [1,1,1],
dif(1,E1) ? ;
Fs = [1,1],
dif(1,E1),
dif(1,E2) ? ;
no  

?- occurrences(E,[E1,E2],Fs).
E = E1 = E2,
Fs = [E,E] ? ;
E = E1,
Fs = [E],
dif(E,E2) ? ;
E = E2,
Fs = [E],
dif(E,E1) ? ;
Fs = [],
dif(E,E1),
dif(E,E2) ? ;
no

回答5:

Here\'s an even shorter logically-pure implementation of occurrences/3.

We build it upon the meta-predicate tfilter/3, the reified term equality predicate (=)/3, and the coroutine allEqual_to__lazy/2 (defined in my previous answer to this question):

occurrences(E,Xs,Es) :-
   allEqual_to__lazy(Es,E),
   tfilter(=(E),Xs,Es).

Done! To ease the comparison, we re-run exactly the same queries I used in my previous answer:

?- Fs = [1,2], occurrences(E,Es,Fs).
false.

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

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

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

At last, the most general query:

?- occurrences(E,Es,Fs).
Es = Fs, Fs = []      ;
Es = Fs, Fs = [E]     ;
Es = Fs, Fs = [E,E]   ;
Es = Fs, Fs = [E,E,E] % ... and so on ad infinitum ...

We get the same answers.

回答6:

The implementation of occurrences/3 below is based on my previous answers, namely by profiting from the clause-indexing mechanism on the 1st argument to avoid some choice-points, and addresses all the issues that were raised.

Moreover it copes with a problem in all submited implementations up to now, including the one referred to in the question, namely that they all enter an infinite loop when the query has the 2 first arguments free and the 3rd a list with different ground elements. The correct behaviour is to fail, of course.

Use of a comparison predicate

I think that in order to avoid unused choice-points and keeping a good degree of the implementation declarativity there is no need for a comparison predicate as the one proposed in the question, but I agree this may be a question of taste or inclination.

Implementation

Three exclusive cases are considered in this order: if the 2nd argument is ground then it is visited recursively; otherwise if the 3rd argument is ground it is checked and then visited recursively; otherwise suitable lists are generated for the 2nd and 3rd arguments.

occurrences(X, L, Os) :-
  ( nonvar(L) -> occs(L, X, Os) ;
    ( nonvar(Os) -> check(Os, X), glist(Os, X, L) ; v_occs(L, X, Os) ) ).

The visit to the ground 2nd argument has three cases when the list is not empty: if its head and X above are both ground and unifiable X is in the head of the resulting list of occurrences and there is no other alternative; otherwise there are two alternatives with X being different from the head or unifying with it:

occs([],_,[]).
occs([X|R], Y, ROs) :-
  ( X==Y -> ROs=[X|Rr] ; foccs(X, Y, ROs, Rr) ), occs(R, Y, Rr).

foccs(X, Y, ROs, ROs) :- dif(X, Y).
foccs(X, X, [X|ROs], ROs).

Checking the ground 3rd argument consists in making sure all its members unify with X. In principle this check could be performed by glist/3 but in this way unused choice-points are avoided.

check([], _).
check([X|R], X) :- check(R, X).

The visit to the ground 3rd argument with a free 2nd argument must terminate by adding variables different from X to the generated list. At each recursion step there are two alternatives: the current head of the generated list is the current head of the visited list, that must be unifiable with X or is a free variable different from X. This is a theoretic-only description because in fact there is an infinite number of solutions and the 3rd clause will never be reached when the list head is a variable. Therefore the third clause below is commented out in order to avoid unusable choice-points.

glist([], X, L) :- gdlist(L,X).
glist([X|R], X, [X|Rr]) :- glist(R, X, Rr).
%% glist([X|R], Y, [Y|Rr]) :- dif(X, Y), glist([X|R], Y, Rr).

gdlist([], _).
gdlist([Y|R], X) :- dif(X, Y), gdlist(R, X).

Finally the case where all arguments are free is dealt with in a way similar to the previous case and having a similar problem of some solution patterns not being in practice generated:

v_occs([], _, []).
v_occs([X|R], X, [X|ROs]) :- v_occs(R, X, ROs).
%% v_occs([X|R], Y, ROs) :- dif(Y, X), v_occs(R, Y, ROs). % never used

Sample tests

?- occurrences(1,[E1,1,2,1,E2],Fs).
Fs = [1,1],
dif(E1,1),
dif(E2,1) ? ;
E2 = 1,
Fs = [1,1,1],
dif(E1,1) ? ;
E1 = 1,
Fs = [1,1,1],
dif(E2,1) ? ;
E1 = E2 = 1,
Fs = [1,1,1,1] ? ;
no

?- occurrences(1,L,[1,2]).
no

?- occurrences(1,L,[1,E,1]).
E = 1,
L = [1,1,1] ? ;
E = 1,
L = [1,1,1,_A],
dif(1,_A) ? ;
E = 1,
L = [1,1,1,_A,_B],
dif(1,_A),
dif(1,_B) ? ;
   ...