Path: utzoo!utgpu!water!watmath!clyde!att!osu-cis!tut.cis.ohio-state.edu!mailrus!cornell!batcomputer!itsgw!nyser!cmx!hilbert!hamid
From: hamid@hilbert.uucp (Hamid Bacha)
Newsgroups: comp.lang.prolog
Subject: Re: Universal Quantification in PROLOG
Message-ID: <602@cmx.npac.syr.edu>
Date: 29 Aug 88 16:01:22 GMT
References: <1600016@otter.hple.hp.com> <7000001@osiris.cso.uiuc.edu>
Sender: usenet@cmx.npac.syr.edu
Reply-To: hamid@logiclab.cis.syr.edu (Hamid Bacha)
Organization: Logic Lab, CIS Dept., Syracuse University
Lines: 41
Sender:hamid@logiclab.cis.syr.edu (Hamid Bacha)


In his reply to: cwp@otter.hple.hp.com (Chris Preist),
   <7000001@osiris.cso.uiuc.edu> goldfain@osiris.cso.uiuc.edu writes:
>
>Clocksin and Mellish chapter 10 discusses this and related notions.
>
>Basically, all variables in a Prolog  clause are understood  to be universally
>quantified.   It is  existential  quantification that  is somewhat  harder  to
>express.


You seem to have some confusion concerning universal and existential
quantification. What the previous message was referring to was universal
quantification in the body of a clause. What Clocksin & Mellish were talking
about was universal quantification at the beginning of a clause. When you
move a universal quantifier from the body of a clause to the outside of
that clause, it becomes an existential quantifier. The following example
provides a distinction between the two cases:

	p(X) :- forall(Y) q(X,Y)       can be rewritten as:

	forall(X) (p(X) <- forall(Y) q(X,Y))
	forall(X) (p(X) v ~ forall(Y) q(X,Y))
	forall(X) (p(X) v exists(Y) ~q(X,Y))
	forall(X) exists(Y) (p(X) v ~q(X,Y))
	forall(X) exists(Y) (p(X) <- q(X,Y))

or in PROLOG (assuming it is allowed):

	exists(Y) p(X) :- q(X,Y). 

In fact, the above is not an acceptable logic program clause.
As the following example (supplied by VS Subrahmanian) shows:

	b <- forall(X) q(X)
	q(a) <-
	q(s(X)) <- q(X)

The least fixed point of this program is attained after omega+1 iterations
of the Tp operator, instead of omega steps which is the case for pure logic
programs.