Re: your mail
On 2012-03-01 08:35:45 -0800, Dan Zuras Intervals wrote:
> > Date: Thu, 1 Mar 2012 17:09:54 +0100
> > From: Vincent Lefevre <vincent@xxxxxxxxxx>
> > To: stds-1788 <stds-1788@xxxxxxxxxxxxxxxxx>
> > Subject: Re: your mail
> >
> > On 2012-02-29 11:43:45 -0500, Michel Hack wrote:
> > > Vincent Lef?vre wrote, in reply to Dan Zuras:
> > > > > Coercion: mid_F(X) = if (abs_F(round2Nearest_F(mid(X))) = +inf)
> > > > > then roundToZero_F(mid(X))
> > > > > else round2Nearest_F(mid(X))
> > > >
> > > > For X = [0,+inf], this would give:
> > > > * mid(X) = +inf
> > > > * abs_F(round2Nearest_F(mid(X))) = +inf
> > > > * roundToZero_F(mid(X)) = roundToZero_F(+inf) = +inf
> > > >
> > > > while I think you wanted Fmax_F. I don't think you can avoid it,
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
> > > > except artificially, e.g. with nextDown(+inf).
> > >
> > > The "roundToZero" applies to the entire operation, in the spirit of 754,
> > > where there is only one rounding after a conceptually-exact computation.
> > > So there is nothing artificial about ending up with Fmax_F.
> >
> > No, roundToZero does not apply to entire operations (this makes no
> > sense), but to unrounded results. Here the unrounded result mid(X)
> > is +inf, because at Level 1:
> >
> > (inf(X) + sup(X)) / 2 = (0 + (+inf)) / 2 = (+inf) / 2 = +inf
> >
> > Then the rounded result is roundToZero_F(+inf) = +inf.
>
> Whether the rounding applies to the entire expression
> or not is not important. What IS important is that
> Michel has correctly devined my intent. Namely that
> mid always returns a finite value even when an infinity
> comes up for one reason or another.
>
> If I have incorrectly formulated that intent, it is not
> his fault but mine.
This was my point that the formulation was incorrect.
> The current formulation was my attempt to embody that
> intent without reference to the underlying arithmetic.
> If you have a better one, I'll use it.
The result (Fmax_F) depends on the underlying arithmetic. So,
necessarily, you'll have a reference to the underlying arithmetic.
But this is not specific to mid(). Every function has a reference
to the underlying arithmetic, due to the rounding function. But
perhaps you meant that the *only* allowed reference is the final
rounding. However this is not possible here. Indeed you would need
a datum x (not depending on the underlying arithmetic, i.e. some
Level 1 datum) such that roundToZero_F(x) = Fmax_F for any underlying
arithmetic. Since you can define arithmetics with arbitrary large
real values (just use an Emax as large as you want), you would need
a datum x that is larger than any real number but less than +inf.
So, unless you modify Level 1 to include such a datum[*], you won't
be able to ignore the underlying arithmetic in the formulation.
[*] Since this datum would never be created at Level 1, you wouldn't
need to specify operations on it (except rounding).
> I'd still like to avoid references to Fmax_F or anything
> similar. But if that is required to get the idea across,
> so be it.
nextDown_F(+inf) is an articifial reference to it (you're saying the
same thing): how would you define nextDown_F() without a reference
to Fmax_F?
> A finite value for the purpose of splitting is more
> important than the simplicity of the formula.
I agree.
--
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)