Thread Links Date Links
Thread Prev Thread Next Thread Index Date Prev Date Next Date Index

Re: Motion P1788.1/M004.01



ok, I agree with Vincent, and I also find some
claims about Unums to be a bit magical.

On Wed, May 18, 2016 at 5:15 AM, Vincent Lefevre <vincent@xxxxxxxxxx> wrote:
On 2016-05-18 03:56:56 -0300, Walter Mascarenhas wrote:
> > > Richardson's theorem does not apply to IEEE 754 (my context), since
> > > only finite sets of rational numbers are involved -- no Pi, log 2, or
> > > (to mention the one reamining requirement after some of the original
> > > ones were found to be inessential) an exact sin() function.
> >
> > The log and atan functions are part of IEEE 754. So, math expressions
> > as those involved in Richardson's theorem can be written with IEEE 754
> > constants and operations.
>
> The math expressions can be written in IEEE, but their meaning is
> different. In other words, the _expression_ "sin(sin(x))" in IEEE
> means something different from the _expression_ "sin(sin(x))" in the
> pure mathematical sense.

No, here this is not just IEEE. If the user considers tracking
exactness (which is the context of this thread[*]), what is sought
is to compute the mathematical value of sin(sin(x)). Otherwise
"tracking exactness" would mean nothing.

What I'm saying is that for math expressions using functions and
constants from IEEE 754, distinguishing between exact and inexact
results is not possible. And Unums (mentioned by Michel Hack)
cannot solve this either because the problem is undecidable.

[*] more precisely, distinguishing a real 0 from a very small value.

--
Vincent Lefèvre <vincent@xxxxxxxxxx> - Web: <https://www.vinc17.net/>
100% accessible validated (X)HTML - Blog: <https://www.vinc17.net/blog/>
Work: CR INRIA - computer arithmetic / AriC project (LIP, ENS-Lyon)