18

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.

false
  • 10,264
  • 13
  • 101
  • 209
  • 2
    Should the predicate fail if any of its two arguments is not a list of unique variables? – Tudor Berariu Jan 13 '15 at 17:30
  • 1
    Just waiting, maybe there are more and different answers. – false Jan 13 '15 at 17:32
  • 2
    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 Jan 13 '15 at 17:35
  • 2
    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 Jan 13 '15 at 17:40
  • 1
    I understand why. Thank you. I added this observation to my answer. – Tudor Berariu Jan 13 '15 at 17:58

4 Answers4

14

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.
Tudor Berariu
  • 4,910
  • 2
  • 18
  • 29
  • 2
    Your counterexample is really the best! It's a pity, because otherwise `term_variables/2` could exploit the fact that it has to check the wellformedness of its second argument anyway, so counting its length is free which then might be used to fail earlier. – false Jan 13 '15 at 17:59
  • I like this approach! But don't you also need to check if the lists are just bars? I'm not by my computer at the moment, but wouldn't `varset_seteq([A,B,a], [A,B])` succeed? – Shon Feb 25 '15 at 08:33
  • 2
    No, it doesn't succeed. What is a bar? – Tudor Berariu Feb 25 '15 at 09:05
  • Oh yeah. My bad. I brain short circuited. I see: because you test each list of term-vars against the respective lists. Very nice solution, I think. a bar is a typo for var. sorry :) – Shon Feb 25 '15 at 09:18
7

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.

Michael Ben Yosef
  • 476
  • 3
  • 7
4

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.
Paulo Moura
  • 18,373
  • 3
  • 23
  • 33
  • 1
    My original answer was just about that :), though I also had the addition of a `varlist/1` predicate to check if both lists were composed of variables. But then I realized, and Tudor Berariu pointed out, that this approach will succeed on, e.g., `As = [A,A,B,C], Bs = [B,C,B,C,A]`. I probably should have left my original attempt too.. – Shon Feb 25 '15 at 13:35
  • 2
    While this solution will work in concrete Prolog implementations, it relies on implementation dependent properties of a Prolog implementation. At the goal `Sa == Sb` it is no longer guaranteed that `Sa` and `Sb` are still sorted. Think of a GC happening in an implementation that does not preserve variable ordering - which might still be conforming when it does not invoke GC during `sort/2`. – false Feb 25 '15 at 14:35
  • 2
    @aBathologist Indeed :-) Detailing pitfalls of apparent alternative solutions is always worth it. Nevertheless, the original question does state that the input is "two lists of *unique* variables" (emphasis mine). – Paulo Moura Feb 25 '15 at 14:39
  • @PauloMoura Oh yeah. You're right! My reading has been faltering back and forth between whether or not falsel meant the predicate itself should fail if the lists aren't "varsets", or if it can expect that its arguments will be varsets. Now, with your emphasis, it seems clear that it can expect varsets (just like `ord_seteq/1` expects, but does not test for, ordered sets). – Shon Feb 25 '15 at 14:43
3

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

Shon
  • 3,989
  • 1
  • 22
  • 35