Re: Existential quantification in expression

From: Herbert Kuchen <kuchen_at_uni-muenster.de>
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
non-Constraint-
types for "exp" in "let ... free in exp" does not increase the
expressivity

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)

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