Re: [isabelle] Possible problem with floating-point addition in Approximation etc.



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


On 26/03/2021 13:37, Fabian Immler wrote:
> 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
> 
> 
>> On 24. Mar 2021, at 18:10, Manuel Eberl <eberlm at in.tum.de
>> <mailto:eberlm at in.tum.de>> wrote:
>>
>> 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
>>
>>
>> On 24/03/2021 17:46, Manuel Eberl wrote:
>>> 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
>>>
>>
> 

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.