*To*: Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*Subject*: Re: [isabelle] Executing real numbers as approximating functions*From*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Date*: Wed, 8 Aug 2012 22:28:52 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAAMXsibihwNp9LJ2OQjtkZ09X5GTcTeaZ3-=UjRWeCU5eJp+zw@mail.gmail.com>*References*: <5022C259.1030709@informatik.tu-muenchen.de> <CAAMXsibihwNp9LJ2OQjtkZ09X5GTcTeaZ3-=UjRWeCU5eJp+zw@mail.gmail.com>

Am 08.08.2012 um 22:01 schrieb Brian Huffman: > On Wed, Aug 8, 2012 at 9:47 PM, Florian Haftmann > <florian.haftmann at informatik.tu-muenchen.de> 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] http://home.in.tum.de/~hoelzl/documents/hoelzl09realinequalities.pdf [2] http://taha.e.twiki.net/twiki/pub/Teaching/617References_Fall09/Theorem-Proving-with-the-Real-Numbers.pdf Jasmin

**Follow-Ups**:**Re: [isabelle] Executing real numbers as approximating functions***From:*Brian Huffman

**Re: [isabelle] Executing real numbers as approximating functions***From:*Johannes Hölzl

**References**:**[isabelle] Executing real numbers as approximating functions***From:*Florian Haftmann

**Re: [isabelle] Executing real numbers as approximating functions***From:*Brian Huffman

- Previous by Date: Re: [isabelle] Executing real numbers as approximating functions
- Next by Date: Re: [isabelle] A trick with code generation from jEdit
- Previous by Thread: Re: [isabelle] Executing real numbers as approximating functions
- Next by Thread: Re: [isabelle] Executing real numbers as approximating functions
- Cl-isabelle-users August 2012 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list