Re: [isabelle] Executing real numbers as approximating functions

Hi Florian and Brian,

>> once I have heard about a formalisation to execute real numbers as
>> approximating functions, i.e. where each real number r is implemented
>> using a function
>>   R :: nat => float
>> such that R n equals r approximated to the n-th digit (or something
>> similar).
>> Can somebody give me a reference for that?
>Russell O'Connor has implemented a similar representation of the
>computable reals in Coq:

Bas Spitters points out to me that only in the work that
he and Robbert Krebbers did (which was a continuation of
Russell's work) floats were used in the representations.
Russell used rational numbers, I think.

I think that this move to floats (and other things that
they did, I'm sure) made the computations much faster.



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