Geert Bosch wrote:
>
> On Nov 14, 2007, at 05:27, Vincent Lefevre wrote:
>
>>> Initially, float could simply use double and cast the result.
>>> For double->float the results will remain correctly rounded.
>>
>> Yes, very probably, but this needs to be proven for each supported
>> function, due to the double rounding problem (this may take some time
>> for functions like pow).
>
> If a real number is rounded to the nearest number in a binary floating
> point format with 2*p+1 bits and that result rounded again to
> a p-bit float, the result is the same as if the original value was
> rounded to a p-bit float directly.
>
> -Geert
>
> PS. Sorry, dont' have a reference to a proof handy at the moment.
In particular, when using x87 code to implement float, it makes no
difference for a single floating point operation followed by a store
whether 32- 53- or 64-bit precision mode is active. The double rounding
problem becomes a big issue when substituting 64-bit precision mode for
double operations; hence the policy of Microsoft and certain BSD
variants of setting 53-bit precision mode.
