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
>> 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