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.

mat · Accepted Answer · 2014-12-11T07:19:18.027

8

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)).

edited Dec 11 '14 at 07:19

answered Dec 10 '14 at 00:24

mat

40,498
3
51
78

Very nice, indeed! But there is one tiny little issue here (I admit it is out of scope of the standard): What if `V` is attached to some constraint, or just `freeze(V,eeek), var_in_vars(V, [A,B,C]).` – false Dec 10 '14 at 00:27
(For future readers): The second one is the accepted one. [`subsumes_term/2`](http://www.complang.tuwien.ac.at/ulrich/iso-prolog/dtc2#subsumes_term) is a pure test predicate, with no unifications, wherease `unify_with_occurs_check/2` actually unifies the variable. – false Dec 10 '14 at 00:48

score 7 · Answer 2 · answered Dec 09 '14 at 21:51

7

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).

answered Dec 09 '14 at 21:51

CapelliC

59,646
5
47
90

1

It is certainly a good solution. Definitely not the most compact or canonical one. – false Dec 09 '14 at 21:52
2

Very nice first attempt! It takes courage to participate --> +1! – mat Dec 10 '14 at 00:58
@mat: thanks! that was definitely the spirit I decided to post such naive answer. Since I read the clear hints in the questions (`we do not need to ensure that Var is a variable, nor that Vars is a list of variables`) that clearly indicate a list scan should not be required, I was lost browsing the docs... Your answer is very instructive indeed – CapelliC Dec 10 '14 at 09:49
@CapelliC: Your solution needs that assumption, too, for `var_in_vars(V.[V|nonlist])` succeeds – false Dec 10 '14 at 15:08

false · Answer 3 · 2014-12-10T01:03:32.687

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.

score 2 · Answer 4 · answered Jun 03 '15 at 09:26

2

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).

answered Jun 03 '15 at 09:26

Paulo Moura

18,373
3
23
33

`V = Vs` might be STO, and thus the behaviour is undefined. – false Jun 03 '15 at 09:28
Yes, and one of the reasons I hesitated to post this solution for some time. Yet, so far, the only systems where I found this definition problematic is in systems that don't yet provide the `acyclic_term/1` standard predicate. – Paulo Moura Jun 03 '15 at 09:36

Paulo Moura · Answer 5 · 2015-06-03T10:34:44.307

2

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.

edited Jun 03 '15 at 10:34

answered Jun 03 '15 at 10:16

Paulo Moura

18,373
3
23
33

This succeeds if the length of both lists are of the same length, however, it might produce unexpected unifications in case of, say `var_in_vars(V,[a])` – false Jun 03 '15 at 11:27
That's outside **your** stated conditions: "So we do not need to ensure that Var is a variable, nor that Vars is a list of variables.". – Paulo Moura Jun 03 '15 at 11:45
Right, but that a pure testing predicate actually unifies something is nevertheless something rather unexpected. You could put a `\+ \+` around, but then it **still** will unify, which might be observed via constraints. – false Jun 03 '15 at 11:48
In an ideal implementation of `term_variables(Vs+V,Ws)` the variable `Ws` might point directly to `Vs` should `V` occur in `Vs`. That is, at first the new `Ws` list is created, but upon success, it is realized that the "olde" `Vs` is good enough, the temporary `Ws` list might thus be immediately reclaimed. – false Jun 03 '15 at 16:01

intika · Answer 6 · 2015-06-03T04:40:45.353

-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.

edited Jun 03 '15 at 04:40

answered Jun 03 '15 at 02:34

intika

8,448
5
36
55

1

**All** code of alternatives 1..4 comes from other answers. What's **your** contribution? – repeat Jun 03 '15 at 03:18
i am new to SO, and according to what "Joel Spolsky" said, it's good to make an answer that is full and clear even if the answer is taken from other users, the plus here is to make a full clear synthetic answer in one single place... i know it's debatable i agree. please let me know what you think and point me if i am wrong. – intika Jun 03 '15 at 04:39
3

No offense, really. I was just surprised, when I was scanning through the answer and "connected the dots", to find out you digested the other answers. There is nothing wrong with that, but it's a first for me as a reader. – repeat Jun 03 '15 at 05:28
1

A compilation might be interesting if you are actually highlighting the differences. After all, there are minimal differences between all of them. – false Jun 03 '15 at 16:05

Variable occurrence in a list of variables

6 Answers6

Solution Synthesis

Linked