Re: [isabelle] Executing real numbers as approximating functions

On Wed, Aug 8, 2012 at 10:28 PM, Jasmin Blanchette
<jasmin.blanchette at> wrote:
> Am 08.08.2012 um 22:01 schrieb Brian Huffman:
>> On Wed, Aug 8, 2012 at 9:47 PM, Florian Haftmann
>> <florian.haftmann at> wrote:
>>> 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:
> Section 4 of Johannes's PLMMS '09 paper [1] states that Harrison's Ph.D. thesis [2] has something like that (with "nat => int"), but I couldn't find it in the thesis (cf. Sects. 2.3 to 2.7). The "positional expansion" of 2.4 seems the most closely related, but from what I understand it yields one digit at a time, not an approximation. Maybe Johannes can expand on this.
> [1]
> [2]

The construction John Harrison describes in his thesis is very similar
to the "Eudoxus reals"; see paper by Rob Arthan:

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