[mercury-users] Using existential quantification?

[Peter Moulder]

Btw, as a beginning user, you needn't bother looking at existential
types yet.  I don't think I've yet used this feature of the language.

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'

I didn't understand this example.  My understanding of the above is
as David gave,

  some[X] (X <= not p)

i.e.

  some[X] (X ; p)

(where `;' is how one writes the logical-or operator in Mercury).

I wonder whether this is indeed what you meant: it isn't a first-order
statement, and off-hand I wouldn't expect it in a proof of first-order
properties.

In Mercury, variable names must begin with a capital letter.  (Or with
an underscore, though that has a special meaning.)

As an example of how Mercury allows existential quantification to be
implicit, consider Ralph's `length' example in
http://www.cs.mu.oz.au/research/mercury/tutorial/lists-n-things.html.
[Btw, Ralph, there's a comma missing at the end of the `L = []' on that
page.]

The Mercury code

  length(L, N) :-
	(
		L = [],
		N = 0
	;
		L = [_Hd | Tl],
		length(Tl, N0),
		N = N0 + 1
	). 

is equivalent to the logical statement

all[L, N]
  ( length(L, N) <=>
      some[_Hd, Tl, N0]
	(
	    ( (L = nil) and (N = 0) )
	 ;
	    ( (L = cons(_Hd, Tl)) and length(Tl, N0) and (N = (N0 + 1)) )
	)
  )

I decided to rename the convenient syntax of [] and [|] to some more
traditional names of `nil' and `cons'.  I've also used parentheses
profusely.  I've retained the Mercury ways of writing
universal quantification (`all[VAR_LIST] ( EXPR )'),
existential quantification (`some[VAR_LIST] ( EXPR )').
I've used `and' to represent the logical-and operator (conjunctions).

Note that the variables _Hd, Tl and N0 aren't explicitly quantified in
the Mercury version.  Variables in the body of a definition are
implicitly understood to be existentially quantified, hence the
`some[_Hd, Tl, N0]' bit in the logic version.  For a programming
language, implicit existential quantification is a convenient
convention.

The exact rule for this transformation is given in section `Implicit
quantification' in the `Syntax' chapter of the reference manual.

> Do you have examples of code (besides std_util's univ) that use 
> existential quantification?

The `length' predicate above uses existential quantification (on the
_Hd, Tl and N0 variables), it just doesn't bother to do so explicitly.

The second part of that definition could equally have been written as

   some[_Hd, Tl, N0] (
   	L = ...,
	...,
	... = N0 + 1
     )

> Could you please provide some guidelines for 
> what classes of problems should use existential quantification?

Almost every predicate you write in Mercury will use (implicit)
existential quantification -- any time you use some temporary variables.


Incidentally (this is addressed principally to the Mercury developers),
I don't find that `Implicit quantification' section very clear.  For
example, it doesn't say what a scope is.  (E.g. I might have expected
that any `( GOAL )' parenthesized expression counts as a [potential]
scope, or perhaps even unparenthesized goals.)

When talking about negations, is that before or after applying the
various transformations mentioned in the `Goals' and (especially)
`Elimination of double negation' sections?  If after, then consider
moving that section earlier, e.g. to between the `DCG-Goals' and
`Data-terms' nodes, or perhaps immediately after the `Goals' section.

Now that we have state variables, DCG notation is less important, so one
might move the DCG things to about the end of the chapter, for the
benefit of people who try to read a reference manual as a means of
learning a language.  (I'm not as sure of this suggestion; there are
benefits in leaving the DCG where they are at the moment, after state
variables.)

I've just noticed that the relatively recent `Variable scoping' section
does clarify some of the confusion I had when first reading the Implicit
quantification section.

Another thing I didn't understand when learning Mercury was what the
scope of `_' variables was, or even whether it was considered a variable
for purposes of scoping rules.  (E.g. whether `not(p(_))' meant `not
some[X] p(X)' or `some[X] not p(X)'.)  I see in section `Tokens' that
the answer is that each `_' is considered as if it were a separate
spelling, and that these special variables can then have a large scope
(such as the whole of the predicate definition body).  Most of the
`Tokens' section is syntactic/lexicographic information, so someone
learning Mercury might easily decide to skim/skip that section.  I'm not
sure where a better place for this semantic information to go, but the
concept is sufficiently distinct that one might even have a separate
section `Anonymous variables' somewhere near the `Variable scoping' and
`Implicit quantification' sections.

One might be explicit that variables whose name merely begins with an
underscore (as distinct from the special `_' variable identifier) behave
just like variables whose name begins with a capital letter except for
what warnings are produced.  (I.e. multiple occurrences in the same
scope are considered to refer to the same variable.)

Another sort of anonymous variable is those implicitly created for
function application.  I think the semidet function examples I gave
under subject `Questions about declarative semantics of Mercury
programs' make these variables (and their quantification) visible; I
mean I think the best way of understanding the behaviour of those
examples is by transforming `<goal involving f(...)>' to
`<goal involving Tmp>, Tmp = f(...)' (after applying the "abbreviation"
expansion transformations mentioned in `Goals' section -- particularly
that for `\=').  The special `@' function is similar, but introduces two
extra conjuncts instead of one: `<goal involving (<LHS> @ <RHS>)>' being
transformed to `<goal involving Tmp>, Tmp = <LHS>, Tmp = <RHS>'.

I can't actually find existing text in the reference manual about how
functions are to be handled.  E.g. I suspect that the order of these
special conjuncts can matter to strict sequential semantics when an
atomic goal contains several function applications and `@' expressions,
perhaps nested.


Douglas, I'd suggest a reading order of

  - `Goals'

  - `Variable scoping' (but ignore the stuff on type variables)

  - A glance at the `Implicit quantification' section (but don't worry too
    much if you don't understand it, I seem to have got by without
    properly understanding it until today...)

  - If you're curious about anonymous variables (i.e. variables written as
    `_'), then see the relevant couple of lines under the `_variable_'
    item of the `Tokens' section of the `Syntax' chapter.  You'll see
    these anonymous variables being used a lot in Mercury code.

By the way, I cheated a bit in the `length' example by not introducing
new head variables, i.e.

  all[HeadVar1, HeadVar2]
    ( length(HeadVar1, HeadVar2) <=>
        some[L, N, _Hd, Tl, N0] (
	  ...
	)
    )

This doesn't matter for the length example, but it may make things
clearer for mercury code like `p(foo, bar(X, Y)) :- ...', which means
all[HeadVar1, HeadVar2]
  ( p(HeadVar1, HeadVar2) <=>
      some[X, Y, ...] (
        HeadVar1 = foo,
	HeadVar2 = bar(X, Y),
	...
      )
  ).

pjm.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------