bagof vs. findall and variable results
Mark-Jan Nederhof
| ?- [library(lists)].
| ?- findall(X, member(X,[Y,Y,Z]), R).
R = [_A,_B,_C] ?
where I would expect R = [Y,Y,Z] ?
In other words, findall/3 renames the variables in the result-list.
On the other hand, bagof/3 does not:
| ?- bagof(X, member(X,[Y,Y,Z]), R).
R = [Y,Y,Z] ?
and neither does setof/3:
| ?- setof(X, member(X,[Y,Y,Z]), R).
R = [Y,Z] ?
Nothing in the manual seems to explain this. What accounts for the
different behaviours of findall, bagof, and setof w.r.t. variables in
the result list? Is it a bug, a feature? Is this behaviour specific
for sicstus2.1.9 or does it generally hold for Prolog implementations?
PS you may ask what I need this for. Well, I wanted to make a list of pairs
connecting variable occurrences in terms to types in some type system.
So, what I'd like to do for some Term (a Prolog term) is
bagof( (Var,Type), var_type_occurrence(Term, (Var,Type)), List ).
where var_type_occurrence nondeterministically finds variable
occurrences in a term and associates them to some type.
I don't want renaming of Var's in List because afterwards I need to
be able to identify one occurrence of a particular variable with another.
By the way, bagof would not have been my first choice here because it may
fail instead of yielding the empty list in case there are no variable
occurrences in Term. In this respect, findall seemed preferable.
Thanks for any help,
Mark-Jan Nederhof
Univ. Groningen
Don Ferguson
>From: mar...@cs.kun.nl (Mark-Jan Nederhof)
>Subject: bagof vs. findall and variable results
>Date: Fri, 28 Apr 1995 11:45:44 GMT
>I noticed this (to me) unexpected behaviour of findall in sicstus2.1.9:
>| ?- [library(lists)].
>| ?- findall(X, member(X,[Y,Y,Z]), R).
>R = [_A,_B,_C] ?
>where I would expect R = [Y,Y,Z] ?
>In other words, findall/3 renames the variables in the result-list.
>On the other hand, bagof/3 does not:
>| ?- bagof(X, member(X,[Y,Y,Z]), R).
>R = [Y,Y,Z] ?
>and neither does setof/3:
>| ?- setof(X, member(X,[Y,Y,Z]), R).
>R = [Y,Z] ?
>Nothing in the manual seems to explain this. What accounts for the
>different behaviours of findall, bagof, and setof w.r.t. variables in
>the result list? Is it a bug, a feature? Is this behaviour specific
>for sicstus2.1.9 or does it generally hold for Prolog implementations?
Unlike setof and bagof, findall assumes unbound variables are
existentially quantified. Note that bagof returns the same result as
findall if it is called withY and Z existentially quantified, as in:
| ?- bagof(X, (Y,Z)^member(X, [Y,Y,Z]), L).
L = [_A,_B,_C]
So the renaming of unbound variables in the findall must be done
for the purposes of quantifying the variables so that they will not retain
their bindings.
Sicstus behaves identically to Quintus Prolog in this respect.
Mark-Jan Nederhof
> >| ?- [library(lists)].
> >| ?- findall(X, member(X,[Y,Y,Z]), R).
> >R = [_A,_B,_C] ?
>
> [...]
>
> Unlike setof and bagof, findall assumes unbound variables are
> existentially quantified.
My thanks to Don Ferguson and others who have helped me to understand what
happens with unbound variables in findall. I describe some of the
misunderstandings I had before posting my question. Perhaps I'm helping
some novices like me.
First I thought that the existential quantification only pertained to
the variables *textually* occurring in the goal (i.e. 2nd argument of
findall). This is not true:
| ?- L=[Y,Y,Z], findall(X, member(X,L), R).
gives the same result for R as the above.
Next I thought that the property of being unbound was something detected
at the beginning of the execution of the goal. This is also not true:
| ?- Y=Z, findall(X, (Y=a, X=Z), R).
R = [a], Z = Y ?
So although Z is unbound at first, it becomes bound later, resulting in
R = [a], rather than R = [_A].
So to me it seems that *after* a solution has been found for the goal,
all unbound variables in the template are (consistently) replaced by
fresh variables.
(I trust the experts will correct me if I told an untruth.)
Mark-Jan Nederhof
Univ. Groningen