Reification of term equality/inequality
Asked Answered
I

6

40

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

Idaho answered 1/12, 2012 at 23:34 Comment(4)
This is indeed an interesting question. Could you add the code from the referenced SO question, or even better add an even more evident case?Dissogeny
@user1638891: Search prolog-dif - and please retag should you find other examples I missed.Idaho
@false, @mat, @Newby All the implementations of occurrences/3 that were submitted to this date except mine of yesterday enter an infinite loop when the query has the 1st two arguments free and the 3rd is a list with different ground members, the correct behaviour being of course to fail.Bahr
@Newby You are welcome. And thank you for having taken my warning as constructive as it intended to be.Bahr
K
10

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

Ketonuria answered 2/12, 2012 at 1:6 Comment(1)
I mean instead of equality_reified/2, it should be called more declaratively for example equality_truth/2 or maybe even equality_true/2 (since "false" as second argument can hardly be called a "truth"). "Reified" has the connotation that somebody did something, which is more imperative than declarative. We should choose a name with a connotation that something holds.Ketonuria
N
9

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.
Newby answered 17/4, 2015 at 20:22 Comment(3)
When compared to the code referred to by PO there is a change in the order of the arguments that should be stated clearly in the answer. So this implementation adopts the strategy in my previous answers of using the indexation on the 2nd argument of the original predicate to avoid some choice-points. Could you please direct me to where is a defintion of if_/3 and =/3?Bahr
Sorry, I missed your second line; maybe you should have given some credit for the idea... Thanks for the link. As to =/3 I do not see where you use it: is it inside your copy of if_/3?Bahr
I found out how =/3 is used.Bahr
I
5

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) ).
Idaho answered 13/4, 2015 at 20:45 Comment(0)
B
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
Bahr answered 15/4, 2015 at 16:58 Comment(0)
N
4

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

We build it upon the 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.

Newby answered 16/6, 2015 at 1:31 Comment(0)
B
3

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) ? ;
   ...
Bahr answered 18/4, 2015 at 14:49 Comment(6)
I applaud that occurrences(1,L,[1,2]). terminates (and correctly fails), however, why then does the specialization L = [_|_], occurrences(1,L,[1,2]). loop? The problem indeed is the case analysis. There is also a stylistic aspect: you mix the logic and procedural aspects. Some other approaches try to concentrate the impure code into some generally applicable pure predicates (if_/3, (=)/3) - such that the actual code remains pure.Idaho
I bet (I have not the time to test this) that all the implementations will loop if the list arguments given are not either free or properly closed lists, what is right because list without any qualification in Prolog means a closed list. So it is no wonder the specialization you mention will cause a loop. As to the stylistic aspect, that is open to discussion moreover when your question poses a problem of inefficiency at the implementation level. In my opinion "pure" does not mean "declarative" and when efficiency is at stake I prefer writing a Prolog program based on what Prolog is.Bahr
It is commonly assumed that also termination is monotone which is not the case in your case. That is, it is commonly assumed that if Q terminates, then also L = [_|_], Q will terminate.Idaho
Very interesting. Then maybe you wish to try the other implementations appearing here with this query L=[X|X], Q that it seems you expect to terminate in all of them except mine. As this discussion is leading nowhere I just quit here: have a good day.Bahr
I don't get your comment. For all other implementations it is true that: If Q terminates then L = [_|_], Q teriminates.Idaho
I assumed that you would understand my point: if the arguments can be anything then the description of the predicate is faulty as it says the last 2 are lists (=properly closed lists). I can assure you that I would otherwise avoid the case you mention in my program. But if any term can be used than I proposed you to test with a cyclic term, and maybe you would understand that more impure code in the other implementations would be needed to get rid of it. And from my part it is all I have to say.Bahr

© 2022 - 2024 — McMap. All rights reserved.