Email Gateway (Mar 24 2021 at 16:47): Email Gateway (Mar 24 2021 at 16:47):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
Email Gateway (Mar 24 2021 at 17:11):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
Email Gateway (Mar 26 2021 at 12:37):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
Email Gateway (Apr 07 2021 at 15:35):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: Jan 04 2025 at 20:18 UTC