Re: Existential quantification in expression
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
This archive was generated by hypermail 2.3.0
: Do Feb 01 2024 - 07:15:05 CET