[std-interval] More on interval computations as proofs

[Gabriel Dos Reis]

Guillaume Melquiond <guillaume.melquiond at ens-lyon.fr> writes:

[...]

| So, to qualify your point on straightforward translation, I would say
| that you are right for resolution algorithms (finding roots, solving
| differential equations, and so on), as they simply won't work. But for
| evaluation functions, you don't have to rewrite them.

so, are you suggesting that basically x +-> x * x should return [-1,
1] on [-1,1], instead of [0, 1]? (I though a simple function to keep
the question simple).

[...]

| PS: obviously, it's always possible to build a floating-point function
| that will behave wrong once translated to intervals, for example by
| inserting (1. / (1e-300 + (x-x)) - 1. / 1e-300) in it.

-- Gaby