[mercury-users] Using existential quantification?

[David Overton]

Hi,

On Thu, Feb 06, 2003 at 05:54:11AM +0800, Douglas Auclair wrote:
> Dear all,
> 
> I'm curious about existential quantifiers.  I'm familiar using them for 
> first-order logical proofs:
> 
> (3x)(x <- ~p)  % '3' means 'there exists'
> 
> But I'm not understanding their utility in Mercury.  I've read the Mercury 
> Language reference manual on existential qualifiers, but the discussion and 
> examples will need some time and further explanation to me for them to sink 
> in.
> 
> That's what I'm asking here.  Are there papers (on the web) or books that 
> discuss using existential quantification in programming languages that I 
> can study?  Do you have examples of code (besides std_util's univ) that use 
> existential quantification?  Could you please provide some guidelines for 
> what classes of problems should use existential quantification?

There are two different uses for the existential quantification operator
'some' in the Mercury language.  When used as part of a goal, 'some' is
the same as existential quantification in predicate logic, e.g. you
example above could be written in Mercury as

	some [X] X <= not p

This is basically used for scoping variables.  You should not need to
use it very often because all variables that are not explicitly
quantified are implicitly existentially quantified to their closest
enclosing scope.

A construct that you may find useful sometimes is universal
quantification.  E.g.

	all [X] p(X) => q(X)

is a convenient shorthand for

	not (some [X] not (p(X) => q(X)))

which the compiler further expands to

	not (some [X] (p(X), not q(X)))

The other use of the 'some' operator is in existential types.  See the
other thread for information about those.


David
-- 
David Overton                  Uni of Melbourne     +61 3 8344 1354
dmo at cs.mu.oz.au                Monash Uni (Clayton) +61 3 9905 5779
http://www.cs.mu.oz.au/~dmo    Mobile Phone         +61 4 0337 4393
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------