Variable occurrence in a list of variables

Question

Consider a (meta-logical) predicate var_in_vars(Var, Vars) which takes a variable Var and a list of variables Vars and succeeds if Var occurs in Vars. So we do not need to ensure that Var is a variable, nor that Vars is a list of variables.

What is the most compact and canonical way to express this in ISO Prolog? Here is an overview of the built-ins in ISO/IEC 13211-1:1995 including Cor.2:2012.

?- var_in_vars(V, [U,V,W]).
true.

?- var_in_vars(V, [X,Y,Z]).
false.

Answer 1

Solution Synthesis

Solution : Short

var_in_vars(V, Vs) :- \+ subsumes_term(V, Vs).

Alternative 1 : Simple

var_in_vars(V, Vs) :- \+ unify_with_occurs_check(V, Vs).

Alternative 2 : Depending on circumstances, this could be more suitable

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Alternative 3 : More complex

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

Alternative 4 : Other possibility

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).

Links :

Standard

---

Note : The context of the question, which is a specific compactness challenge involving the expressivity of ISO predicates under given circumstances.

Answer 2

One possibility:

var_in_vars(V, Vs) :- \+ unify_with_occurs_check(V, Vs).

and shorter:

var_in_vars(V, Vs) :- \+ subsumes_term(V, Vs).

EDIT: Future readers, please take into account the context of the question, which is a specific compactness challenge involving the expressivity of ISO predicates under given circumstances.

In other circumstances, you will likely benefit more from a definition like:

var_in_vars(V, Vs) :-
        must_be(list, Vs),
        once((member(X, Vs), V == X)).

Answer 3

this definition passes the tests, but... do I miss some subtlety ?

var_in_vars(V, [H|_]) :- V == H, !.
var_in_vars(V, [_|T]) :- var_in_vars(V, T).

Answer 4

The solution @false can be simplified to:

var_in_vars(V, Vs) :-
    term_variables(Vs+V, Vs).

When V is a member of the Vs list, the second argument returns Vs (due to the left-to-right traversal of the Vs+V term). When V is not a member of Vs, the second argument returns a list that have one more element than Vs and thus cannot unify with it. Although there's an implicit unification in the second argument, in neither case there's a danger of creating a cyclic term. I.e. unification being STO is not a problem in this simplified solution.

But is the simplification worth it w.r.t. performance? The use of equality, (==)/2 have the potential of failing earlier and thus making the original solution faster.

Answer 5

An alternative solution is:

var_in_vars(V, Vs) :-
    \+ (V = Vs, acyclic_term(Vs)).

But the solutions by @mat are better and more elegant and the solution by @CapelliC was for a long time the most portable one (the subsumes_term/2 predicate was only standardized recently and not all systems provided the unify_with_occurs_check/2 predicate).

Answer 6

And here goes another one, although a bit more complex:

var_in_vars(V, Vs) :-
   term_variables(Vs+V, Ws),
   Ws == Vs.

So this relies on the precise order how variables are visited. And since this is well defined in the standard we can rely that they

... appear according to their first occurrence in left-to-right traversal ...

A drawback of this definition is that it has minimum cost proportional to the length of Vs. But since an internal traversal is often quite efficiently implemented, this is not such a problem.

It has one big advantage: It only succeeds if Vs is a list of variables.