Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!cornell!rochester!udel!burdvax!pearl!lang
From: lang@pearl.PRC.Unisys.COM (Francois-Michel Lang)
Newsgroups: comp.lang.prolog
Subject: existential quantification in bagof and setof
Keywords: bagof setof quantification
Message-ID: <9150@burdvax.PRC.Unisys.COM>
Date: 2 Feb 89 18:59:23 GMT
Sender: news@PRC.Unisys.COM
Lines: 67


I have recently stumbled across what seems to be
an undocumented feature in certain popular dialects of Prolog.
This has to do with existential quantification of variables
in the second argument of calls to bagof/3 and setof/3.

Given the following clauses for likes/2

            likes(tom, beer).
            likes(dick, beer).
            likes(harry, beer).
            likes(bill, cider).
            likes(jan, cider).
            likes(tom, cider).

writing "Y^" is necessary in

            | ?- setof(X, Y^likes(X,Y), S).

in order to return in S the list [bill,dick,harry,jan,tom].

According to all the Prolog manuals I've seen,
Y in the above example is supposed to be variable.
By extension, a string of variables connected by ^/2
is also OK here, as in

             setof(X, V1^V2^...^Vn^Goal, Set).

However--and this is what seems to be undocumented--these variables
apparently do not have to appear *textually* as the left argument
of ^/2, and, in fact, arbitrary terms can appear as the left arg of ^/2,
and any variables contained in these terms will be existentially quantified.

E.g., given the DB

foo(1,2,3,4).
foo(2,3,4,5).
foo(3,4,5,6).
foo(4,5,6,7).

I can do

| ?- T = p(X,Y,Z), setof(First, T^foo(First,X,Y,Z), Set).

T = p(X,Y,Z),
X = _79,
Y = _94,
Z = _109,
First = _132,
Set = [1,2,3,4] 

| ?- 

That's not what the documentation I've seen for C-Prolog
and Quintus says, and this example runs in both.
I'd be curious to find out if other Prologs work like this.

This works no matter what the term T is,
as long as X, Y, and Z appear somewhere in T.
In general, as long as the variables I want to quantify over
are found *somewhere* in the term appearing
in the left arg of ^/2 in the 2nd arg of setof/bagof,
that's all that's necessary.
----------------------------------------------------------------------------
Francois-Michel Lang
Paoli Research Center, Unisys Corporation lang@prc.unisys.com (215) 648-7256
Dept of Comp & Info Science, U of PA      lang@cis.upenn.edu  (215) 898-9511