Free Variables in set_of/3

Appeared in Volume 9/4, November 1996

dwyer@cs.adelaide.edu.au
Barry Dwyer
1st June 1996

I understand that I can write 'set_of(X, Y^G(X,Y), L)', making Y a free variable in G. I have seen numerous examples of this in text books, etc. But what is the correct syntax if I want to have more than one free variable? Or must I always define the goal so that there is at most one free variable?

anewman@epidigm.geg.mot.com
M. Alan Newman
1st June 1996

set_of(X, Y^Z^...^g(X,Y,Z,...), L) will do it.

timm@insect.sd.monash.edu.au
Tim Menzies
2nd June 1996

Can someone explain why we have to do this? What extra information does this give to the Prolog compiler that is essential and vital?

fjh@mundook.cs.mu.oz.au
Fergus Henderson
2nd June 1996

The 'X^Goal' syntax means existential quantification. It affects the semantics. Consider the following two examples:

?- setof(Y, member(X - Y, [a - 1, a - 2, b - 3]), Set).
X = a, Set = [1, 2] ;
X = b, Set = [3] ;
fail.

?- setof(Y, X^member(X - Y, [a - 1, a - 2, b - 3]), Set).
Set = [1, 2, 3] ;
fail.

In the second example, we are asking: for what values of Set is Set a non-empty sorted list of all the values of Y for which there exists some X such that
member(X - Y, [a - 1, a - 2, b - 3]) is true?

Prolog assumes that variables in a clause are implicitly universally quantified over the whole clause, and variables in a query are implicitly existentially quantified over the whole query. This usually doesn't give the semantics you want in cases involving negation (and setof/3 implicitly involves negation). This rule means that you often have to explicitly quantify goals in setof/3.

The same problem comes up with if-then-else. The usual solution is to just use a non-logical if-then-else which ignores quantification. Some languages such as NU-Prolog and Goedel have a logical if-then-else; when using the logical if-then-else constructs in NU-Prolog and Goedel, it is often necessary to use explicit existential quantifiers.

The information provided by quantifiers is indeed "essential and vital". However, it is not essential to write the quantifiers explicitly. Mercury uses a different rule for implicit quantification: variables which do not occur in a clause head are existentially quantified over their closest enclosing scope. This convention avoids the need for explicit quantifiers in almost all circumstances.

ok@goanna.cs.rmit.edu.au
Richard A. O'Keefe
3rd June 1996

Tim Menzies writes:
Can someone explain why we have to do this?

In classic Prolog implementations (NU Prolog is, as ever, an exception), the information is not in fact given to the compiler, but is interpreted at run time by setof/3 and bagof/3.

This is explained in full in "The Craft of Prolog" and many other textbooks.

It is usually possible to rewrite a Prolog program by adding new predicates so that existential quantifiers are not needed, but that isn't always convenient.

paul@cs.keele.ac.uk
Paul Singleton
7th June 1996

Richard A. O'Keefe wrote:
It is usually possible to rewrite a Prolog program by adding new predicates so that existential quantifiers are not needed, but that isn't always convenient.

Isn't it always possible?

And, convenient or not, I think that writing a new predicate to allow a simple generator goal has some "software maintenance" advantages, e.g.

• any new "local" variables introduced by subsequent alterations to the goal are existentially quantified by default (if/since there has to be a default, this way around is probably preferable)

• such "local" variables are also made independent of similarly-named variables in previous (conjoined) goals, which can be a cause of annoying bugs

• the variables which are not existentially quantified are shown explicitly

Rather than complicate Prolog syntax (it would only be the syntax, I guess?) with something corresponding to this intuitive notion of "local" variable, it's neater to use an extra predicate.

With a structure editor, "proceduring" of a bunch of goals should anyway be just a matter of clicking with a mouse.

dbp@csli.stanford.edu
David Barker-Plummer
10th June 1996

No-one has mentioned that the use of "free" and its opposite "bound" here are interchanged.

The existential quantifier ^ turns Y into a bound variable, where it would otherwise be free. Notice that this is a logical, as opposed to programming, use of the term "bound variable".

ok@cs.rmit.edu.au
Richard A. O'Keefe
27th August 1996

It is normal for quantifiers to bind variables, so Prolog doesn't depart from logic here.