Path: utzoo!attcan!uunet!lll-winken!lll-tis!ames!mailrus!purdue!decwrl!labrea!csli!johnson
From: johnson@csli.STANFORD.EDU (Mark Johnson)
Newsgroups: comp.lang.prolog
Subject: Re: Universal Quantification in PROLOG
Summary: Look at Kanamori and Horiuchi's paper in Logic Programming
Message-ID: <5336@csli.STANFORD.EDU>
Date: 31 Aug 88 17:46:33 GMT
Organization: Center for the Study of Language and Information, Stanford U.
Lines: 47

(1988)
Expires: 
References: <1600016@otter.hple.hp.com> <7000001@osiris.cso.uiuc.edu> <745@etive.ed.ac.uk>
Sender: 
Reply-To: johnson@csli.UUCP (Mark Johnson)
Followup-To: 
Distribution: 
Organization: Center for the Study of Language and Information, Stanford U.
Keywords: 



The paper by Kanamori and Horiuchi in vol 2. of the Proceedings of
the 4th Intl Conference on Logic Programming (MIT Press, 1988) is
relevant to the question of existential and universal quantifiers 
in Prolog.

They discuss (and prove "correct") the "Unfold-Fold" transformation, 
which, among other things, is capable of transforming a predicate
definition of the form:

less_than_all(X,L) :-   % X is less than _every_ member of L
	list(L),				% L must be a list
	(member(!Y,L) -> X < !Y).	% if Y is an elt of L, then X < L.

into a predicate definition of the form:

less_than_all(X,[]).
less_than_all(X,[Y|L]) :-
	X<Y,
	less_than_all(X,L).

The variable !Y in the first definition of less_than_all is called a
universal variable, because it is interpreted as being universally
quantified within the body of the clause.

In many circumstances the Unfold-Fold transformation can transform
a definite formula (containing universal variables) into a definite
clause that can be used by Prolog.  In its most general form the
Unfold-Fold transform can be difficult to apply usefully, since there 
are many ways of unfolding and then folding a set of formulae, and not
all of them result in useful programs.  I think that it may be possible,
however, to find a restricted class of formulae for which a simple
control strategy can direct the application of the Unfolding and Folding
operations in such a way that they result in predicate definitions
useful in Prolog systems.

Mark Johnson