Path: utzoo!utgpu!jarvis.csri.toronto.edu!mailrus!purdue!decwrl!labrea!russell!pereira
From: pereira@russell.STANFORD.EDU (Fernando Pereira)
Newsgroups: comp.lang.prolog
Subject: Re: existential quantification in bagof and setof
Keywords: bagof setof quantification
Message-ID: <7413@russell.STANFORD.EDU>
Date: 3 Feb 89 07:34:35 GMT
References: <9150@burdvax.PRC.Unisys.COM>
Reply-To: pereira@russell.UUCP (Fernando Pereira)
Organization: Center for the Study of Language and Information, Stanford U.
Lines: 106

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.