Re: Motion P1788.1/M004.01
On Wed, 18 May 2016 10:15:50 +0200, Vincent Lefèvre wrote:
> 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.
I'm not terribly famliar with Unums, but I think they propagate Inexactness
the same way 1788 propagates decorations. In practice this means that a
computation quickly degrades to Inexact, after which no further progress is
possible in tracking the distinction between tiny and zero.
But the reason Richardson's Theorem does not apply to 754 is very unsubtle:
everything is decidable by exhaustive search in a finite domain! For 1788
the question is a lot more interesting, however, and I don't know the answer.
Nor do I know whether Richardson's methods can be used to construct instances
with a provable excessively large lower bound on verification time.
Michel.
---Sent: 2016-05-18 14:15:47 UTC