Re: about emp (was: Motion 42: NO)
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".]
> > > - 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.
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.
--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <http://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <http://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)