CODEWITHSUNDEEP
prologiso-prolog
false
false

Reputation: 10102

Equality of two lists of variables

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.

Upvotes: 18

Views: 1192

Answers (4)

Shon
Shon

Reputation: 4098

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" :)

Upvotes: 3

Michael Ben Yosef
Michael Ben Yosef

Reputation: 576

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.

Upvotes: 7

Paulo Moura
Paulo Moura

Reputation: 18663

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.

Upvotes: 4

Tudor Berariu
Tudor Berariu

Reputation: 4910

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.

Upvotes: 14

Related Questions