Re: min / max and empty intervals (was: Friendly amendment to Motion 25)
On 2011-06-07 03:41:01 -0700, Dan Zuras Intervals wrote:
> > Date: Tue, 7 Jun 2011 12:18:19 +0200
> > From: Vincent Lefevre <vincent@xxxxxxxxxx>
> > To: "stds-1788@xxxxxxxx" <stds-1788@xxxxxxxx>
> > Subject: Re: min / max and empty intervals (was: Friendly amendment to Motion 25)
> > . . .
> >
> > Moreover if I is a subset of J, then f(I) should be a subset of f(J),
> > even in the case where I is empty. This would no longer be true with
> > (2). For instance, min(sqrt(X),[3,4]) with:
> > * X = [-2,-1] -> result = [3,4]
> > * X = [-2,0] -> result = [0,0]
>
> OOoo, Vincent. I find your example both illuminating
> & disturbing.
>
> If we have a min that returns the non-empty interval
> in the case where the other is empty then, as you say:
>
> xx = [-2,-1] \subset yy = [-2,0] but for
> f(tt) = min(sqrt(tt),[3,4]) we have that
> f(xx) = [3,4] NOT \subset of f(yy) = [0,0].
>
> But if we use a min that returns the empty we have:
>
> f(xx) = empty \subset of f(yy) = [0,0].
>
> Is this a fluke of this example or the nose in the tent
> of a more general principle?
The general principle is that the natural extension of real-point
functions to intervals (here, this natural extension implies
min(Empty,X) = Empty) guarantees the inclusion isotonicity. If
you try to introduce an exception for whatever reason, this may
no longer be true.
IMHO, inclusion isotonicity is just as important as FTIA. Proofs
can be based on it (whether Empty can be involved or not).
> Actually, it is sufficient to simplify your example to
> f(tt) = min(tt,[3,4]). Then the interval returning min
> has:
>
> f(empty) = [3,4] NOT \subset f([0,1]) = [0,1]
>
> and with the empty returning min we have
>
> f(empty) = empty \subset f([0,1]) = [0,1].
>
> This suggests the more general principle to me.
Yes, I could have simplified the example, but I wanted to choose
one where the input interval was not empty, i.e. where Empty
would appear only in intermediate computations.
> If this is convincing to all of you I entirely withdraw
> my argument for the other approach.
>
> Wow, I didn't see that one coming.
>
>
> Dan
--
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 / Arénaire project (LIP, ENS-Lyon)