[comp.lang.prolog] existential quantification in bagof and setof

lang@pearl.PRC.Unisys.COM (Francois-Michel Lang) (02/03/89)

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

pereira@russell.STANFORD.EDU (Fernando Pereira) (02/03/89)

The behavior of setof/bagof that J-F Lang describes is definitely
intended, if undocumented, in DEC-10 Prolog, C-Prolog and Quintus
Prolog. I use it often in fragments of the form

	p(A, S) :- setof(X, A^q(A, X), S)

where A may be bound on call to an arbitrary nonground term and I want
to collect all solutions of q(A, S) regardless of the bindings they
impose on the variables in A. This is particularly useful for
metalogical hacking, as in the simple Earley deduction interpreter
below, which is explained in detail in my book with Stuar Shieber
"Prolog and Natural-Language Analysis"

-- Fernando Pereira
Artificial Intelligence Center
SRI International
pereira@ai.sri.com

% Earley deduction interpreter, Quintus Prolog version.
% Program clauses are represented by unit clauses of the form
%
%    Head <= [Goal1,...,Goaln].
%
% To try to prove Goal, call
%
%    prove(Goal).
%

:- op(500, xfx, <=).
:- op(500, xfx, <*=).

:- dynamic (<*=)/2, clause_counter/1.

prove(Goal) :-
   predict(Goal, Queue),
   process(Queue),
   Goal <*= [].

predict(Goal, Queue) :-
   all_solutions(Clause, Goal^prediction(Goal, Clause), Queue).

prediction(Goal, Goal <*= Body) :-
   Goal <= Body,
   store(Goal <*= Body).

complete(Fact, Queue) :-
   all_solutions(Clause, Fact^completion(Fact, Clause), Queue).

completion(Fact, Goal <*= Body) :-
   Goal <*= [Fact|Body],
   store(Goal <*= Body).

resolve(Clause, Queue) :-
   all_solutions(NewClause, Clause^resolution(Clause, NewClause), Queue).

resolution(Head <*= [First|Body], Head <*= Body) :-
   First <*= [],
   store(Head <*= Body).

process([]).
process([Head <*= Body | OldQueue]) :-
   process_clause(Head, Body, SubQueue),
   conc(SubQueue, OldQueue, Queue),
   process(Queue).

process_clause(Head, [], Queue) :-
   complete(Head, Queue).
process_clause(Head, [First|Body], Queue) :-
   predict(First, Front),
   resolve(Head <*= [First|Body], Back),
   conc(Front, Back, Queue).

store(Clause) :-
   \+subsumed(Clause),
   report(Clause),
   assert(Clause).

subsumed(Clause) :- 
   GenHead <*= GenBody,
   subsumes(GenHead <*= GenBody, Clause).

conc([], L, L).
conc([X|L1], L2, [X|L3]) :- conc(L1, L2, L3).

subsumes(General, Specific) :-
   \+ ( numbervars(Specific, 0, _), \+(General = Specific) ).

all_solutions(Var, Goal, Set) :-
   bagof(Var, Goal, Set) -> true ; Set = [].

report(Clause) :-
   new_clause(C),
   \+ \+ ( numbervars(Clause, 1, _),
           format('(~d) ~w.~n', [C, Clause])).

clause_counter(1).

new_clause(C) :-
   retract(clause_counter(C)), !,
   D is C + 1,
   assert(clause_counter(D)).

clear :-
   retract(_ <*= _),
   fail.
clear.

bimbart@kulcs.uucp (Bart Demoen) (02/06/89)

<9150@burdvax.PRC.Unisys.COM> lang@pearl.PRC.Unisys.COM (Francois-Michel Lang)
asks:

> I'd be curious to find out if other Prologs work like this.

BIMprolog works like this too - but its documentation is a bit confusing

bimbart@kulcs

rar@DEIMOS.ADS.COM (Bob Riemenschneider) (02/08/89)

=>   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] 
=>
=>   I'd be curious to find out if other Prologs work like this.

I tried this in AAIS Prolog version M-1.15 on my Mac and got:

   ?-  T = p(X,Y,Z), setof(First, T^foo(First,X,Y,Z), Set).
         T = p(2,3,4),
         X = 2, Y = 3, Z = 4, First = _4, Set = [1] ;
         T = p(3,4,5),
         X = 3, Y = 4, Z = 5, First = _4, Set = [2] ;
           ...

According to the AAIS manual, the "goal [VAR^GOAL] is equivalent
to just calling GOAL if the variable [VAR] is bound."

							-- rar