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.

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

4 Answers 4

14
+850

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.
4
  • 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, 2015 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, 2015 at 8:33
  • 2
    No, it doesn't succeed. What is a bar? Feb 25, 2015 at 9: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, 2015 at 9: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.

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.
4
  • 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, 2015 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, 2015 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). Feb 25, 2015 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, 2015 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" :)

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.