Re: about emp (was: Motion 42: NO)
Le jeudi 07 février 2013 à 16:11 +0100, Vincent Lefevre a écrit :
> On 2013-02-07 15:07:27 +0100, Guillaume Melquiond wrote:
> > Le jeudi 07 février 2013 à 14:50 +0100, Vincent Lefevre a écrit :
> > > On 2013-02-06 22:07:15 +0100, Guillaume Melquiond wrote:
>
> [Note: this was together with your "I feel that def, dac, and com,
> should not require the inputs to be nonempty".]
And I still think so, due to the propagation rule below.
> > > > - Finally, the emp decoration seems superfluous to me. There is no point
> > > > in decorating a nonempty interval with an emp decoration (except maybe
> > > > for wreaking havoc in an interval library), so the emp decoration could
> > > > just as well be removed. An empty interval would then be decorated with
> > > > trv when it does not designate a NaI.
> > >
> > > IIRC, there can be problems with that. For instance, take zz = g(yy)
> > > where yy is Empty. Since g is defined and continuous on the empty set
> > > yy, one can return zz = (Empty,dac). But now assume that yy wasn't
> > > actually an input, but yy = f(xx) for some non-empty xx, e.g.
> > > sqrt([-2,-1]). So, one would get:
> > >
> > > (g o f)(xx) = (Empty,dac)
> > >
> > > which is wrong.
> >
> > As I understand it, decorations propagate from inputs to output and you
> > can never get an output with a stronger decoration than an input.
>
> IIRC, in our discussions it was allowed to improve a decoration
> if the condition associated with the property was satisfied.
According to 8.8.6/25, this is not allowed. (And I am perfectly fine
with it not being allowed. I think it is the only way of defining it
correctly.)
> Otherwise...
>
> > So, on your example, you would get:
> >
> > f(xx) = (Empty,trv)
> > g(f(xx)) = (Empty,trv)
> >
> > which is right.
>
> OK. I wonder whether this can be a way to re-introduce the empty
> input under some other form: (Empty,dac). Otherwise, if you decide
> that Empty as an input has the trv decoration, this would mean that
> (Empty,def) and (Empty,dac) would not be possible in practice, which
> can be expressed by the current condition "x nonempty" for def and
> dac.
Just to clear any potential misunderstanding, I was not saying that
empty is only allowed to have the trv decoration. What I was saying is
that the emp decoration is redundant with the trv decoration: there is
no situation that I can think of where empty_emp could not be encoded by
empty_trv, and since nonempty_emp does not make sense, that does not
leave any purposeful meaning for decoration emp.
In other words, I could well live with empty_dac and empty_def for the
sake of uniformity and mathematical cleanness. To summarize, these are
all the possible cases:
f(empty_dac) = empty_dac (or empty_def or empty_trv)
f(empty_def) = empty_def (or empty_trv)
f(empty_trv) = empty_trv
f(empty_ill) = empty_ill
newDec(empty) = empty_trv
sqrt([-2,-1]_dac) = empty_trv
sqrt([-2,-1]_def) = empty_trv
sqrt([-2,-1]_trv) = empty_trv
Best regards,
Guillaume