Re: Existential quantification in expression

From: Herbert Kuchen <>
Date: Fri, 23 Oct 1998 17:53:19 +0100

Michael Hanus wrote:

> [I changed the subject since this email concerns only one topic
> of the previous thread.]
> I'd like to discuss the necessity to allow existential quantifiers
> also for arbitrary expressions a little bit further.
> > let ... free in exp
> >
> > also with other types of exp, e.g. in
> >
> > let x free in parent x
> >
> > parent Bill = Maud
> > parent Maud = Jack
> >
> > it could be used to generate possible values.
> Here I am interested to see why you need the existential quantifier
> exact at this level. If "parent x" occurs only in a condition,
> you could raise the declaration of x to the entire condition, e.g.,
> So, I'd like to see an example where the existential quantification
> at exactly the scope of some non-constraint expression is really
> necessary.

I am (almost) sure that it is always possible to move the
existentialquantification to the outermost level. Thus, allowing
types for "exp" in "let ... free in exp" does not increase the

of the language. It might however be convenient for the programmer.
A piece of program might be easier to understand, if the declarations
are as close as possible to the place where they are used.
However, this is not a very strong argument taking into account that
typical rules only range over a few lines.
Thus, the original restriction is acceptable.

> Otherwise, I am in favor to omit this possibility
> due to two reasons:
> 1. The declarative meaning of existential quantifiers around
> arbitrary terms is unclear (at least for me).

well, the semantics could be a disjunctive expression,

Maud | Jack

in the above example (assuming that "parent" is flexible)

Received on Fr Okt 23 1998 - 19:01:00 CEST

This archive was generated by hypermail 2.3.0 : Di Sep 29 2020 - 07:15:02 CEST