*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Executing real numbers as approximating functions*From*: Brian Huffman <huffman at in.tum.de>*Date*: Thu, 9 Aug 2012 07:14:17 +0200*Cc*: USR Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>*In-reply-to*: <801B131A-1811-42C5-806C-5269164FB93E@gmail.com>*References*: <5022C259.1030709@informatik.tu-muenchen.de> <CAAMXsibihwNp9LJ2OQjtkZ09X5GTcTeaZ3-=UjRWeCU5eJp+zw@mail.gmail.com> <801B131A-1811-42C5-806C-5269164FB93E@gmail.com>

On Wed, Aug 8, 2012 at 10:28 PM, Jasmin Blanchette <jasmin.blanchette at gmail.com> 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 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 The construction John Harrison describes in his thesis is very similar to the "Eudoxus reals"; see paper by Rob Arthan: http://arxiv.org/abs/math/0405454v1

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

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

**Re: [isabelle] Executing real numbers as approximating functions***From:*Jasmin Blanchette

- Previous by Date: Re: [isabelle] Syntax issue: lost between HOL and Isar
- Next by Date: Re: [isabelle] Applicability of LaTeXsugar and OptionalSugar
- 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