Equality of two lists of variables

18
votes

How to define a meta-logical predicate that tests (thus succeeds or fails only) if two lists of unique variables contain exactly the same variables using the built-ins from the current ISO standard (ISO/IEC 13211-1:1995 including Cor.2).

Stated differently, the predicate should succeed if one list of unique variables is a permutation of the other. In analogy to library(ordsets), let's call this meta-logical predicate varset_seteq(As, Bs).

Note that, in contrast to ord_seteq/2, this predicate cannot be simply As == Bs.

4
prologiso-prolog
Should the predicate fail if any of its two arguments is not a list of unique variables? – Tudor Berariu
Just waiting, maybe there are more and different answers. – false
I was trying something different, but I had to check if As and Bs really are sets of free variables. In my answer that is guaranteed by the fact that they must unify with the second argument of term_variables/2. – Tudor Berariu
No, it is not guaranteed, you have to assume it, too. varset_seteq([A+B,a],[]) succeeds in many systems (by default). ... and unifies the arguments. – false
I understand why. Thank you. I added this observation to my answer. – Tudor Berariu

4 Answers

14
votes

The solution I propose uses term_variables/2 to check if Bs has no extra variables over As and that As has no variable that doesn't appear in Bs.

varset_seteq(As, Bs):-
    term_variables(As-Bs, As),
    term_variables(Bs-As, Bs).

The above solution can be tricked to succeed with arguments that are not sets of free variables:

 | ?- varset_seteq([A], [a]).

 A = a

 yes

To avoid that, unification can be replaced with equivalence test:

varset_seteq(As, Bs):-
    term_variables(As-Bs, A0),
    A0 == As,
    term_variables(Bs-As, B0),
    B0 == Bs.
7
votes

If we may assume that the two lists contain unique variables, then the following use of double negation works:

varset_seteq(As, Bs) :-
    \+ \+ (numbered_from(As, 1),
           sort(Bs, SBs),
           As == SBs).

numbered_from([], _).
numbered_from([X|Xs], X) :-
    X1 is X + 1,
    numbered_from(Xs, X1).

This is similar to Paulo's solution, but avoids the problem that variable ordering is only required by ISO/IEC 13211-1 to be consistent within a single execution of sort/2.

4
votes

Another solution, less efficient than Tudor's clever solution and thus not recommended, but still worth mentioning here as I see it being used on multiple occasions, is:

varset_seteq(As, Bs) :-
    sort(As, Sa), sort(Bs, Sb), Sa == Sb.
3
votes

Another approach. If we provide ourselves with these higher order predicates (which are each useful on their own),

select_with(_, _, [], []).
select_with(P, X, [Y|Ys], Ys)     :- call(P, X, Y), !.
select_with(P, X, [Y|Ys], [Y|Ks]) :-
    select_with(P, X, Ys, Ks).

foldl(_,[],Vn,Vn).
foldl(P,[X|Xs],V0,Vn) :- 
    call(P,X,V0,V1),
    foldl_(P,Xs,V1,Vn).

then we can easily define a predicate that is true if each member one list has an equal element in the other (using ==/2):

members_equal(A, B :-
    foldl(select_with(==), A, B, []).

This predicate can be specialized for the stated purpose if we verify that the incoming arguments are varsets. The following is the best I've been able to come up with in that direction (but it eats up quite a few inferences):

is_varset([]).
is_varset([V|Vs]) :-
    var(V),
    maplist(\==(V), Vs),
    is_varset(Vs).

(At least on SWI Prolog, using sort/2 takes fewer inferences than the above. Presumably this is because the sorting is done in C. Also, this answer still doesn't approach the elegance of the term_vars/2 approach——such is the power of "semantic ascent" :)