From: Manuel Eberl <eberlm@in.tum.de>

I just noticed something wonky in the "approximation" package: addition

of two intervals is implemented by simply adding the two floats and

*then* rounding to the required precision.

This leads to pathological behaviour when the two numbers being added

are of greatly different orders of magnitude, e.g.

value "approx 10 (floatarith.Add

(floatarith.Num (Float 1 0))

(floatarith.Num (Float 1 (-100000)))) []"

This takes about 93 seconds. If you add a few more zeros, it runs out of

memory entirely. Surely one can do better than that!

Does anyone feel responsible for the approximation package and wants to

comment on if and how this should be repaired?

Manuel

smime.p7s

From: Manuel Eberl <eberlm@in.tum.de>

I think the solution is to use "float_plus_down"/"float_plus_up". I have

a student who needs this stuff, so unless anyone stops me, I will have

to student build a rounding addition for intervals and then change

"Approximation" to use that.

Manuel

smime.p7s

From: Fabian Immler via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>

Hi Manuel,

There used to be more instances of such computations with excessive precision,

A while ago, I addressed (most of) them in https://isabelle.in.tum.de/repos/isabelle/rev/bf498e0af9e3 <https://isabelle.in.tum.de/repos/isabelle/rev/bf498e0af9e3> .

Unfortunately I reintroduced the inefficient addition in https://isabelle.in.tum.de/repos/isabelle/rev/f630f2e707a6 <https://isabelle.in.tum.de/repos/isabelle/rev/f630f2e707a6> .

So what you proposed sounds very reasonable.

Fabian

From: Manuel Eberl <eberlm@in.tum.de>

I now addressed this in isabelle-dev/56db8559eadb:

https://isabelle.in.tum.de/repos/isabelle/rev/56db8559eadb

Fabian, note that while fixing this I saw some suspicious-looking

function definitions in Taylor_Models that, at least at a first glance,

look like addition and subtraction of floats is done without proper

rounding there as well.

Might be a good idea for someone familiar with this theory to check this.

Cheers,

Manuel

smime.p7s

Last updated: Dec 08 2021 at 10:22 UTC