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:
>
>http://corn.cs.ru.nl/library/fastreal.html

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.

See:

http://arxiv.org/abs/1106.3448/
http://robbertkrebbers.nl/research/reals/

Freek





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