*To*: Jasmin Blanchette <jasmin.blanchette at gmail.com>*Subject*: Re: [isabelle] Executing real numbers as approximating functions*From*: Johannes Hölzl <hoelzl at in.tum.de>*Date*: Thu, 09 Aug 2012 09:51:51 +0200*Cc*: Isabelle Mailinglist <isabelle-users at cl.cam.ac.uk>, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de>, USR*In-reply-to*: <801B131A-1811-42C5-806C-5269164FB93E@gmail.com>*Organization*: Technische Universität München*References*: <5022C259.1030709@informatik.tu-muenchen.de> <CAAMXsibihwNp9LJ2OQjtkZ09X5GTcTeaZ3-=UjRWeCU5eJp+zw@mail.gmail.com> <801B131A-1811-42C5-806C-5269164FB93E@gmail.com>

Am Mittwoch, den 08.08.2012, 22:28 +0200 schrieb Jasmin Blanchette: > 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. > Jasmin I'm refering to Section "4.5 Calculation with reals" of [2] where Harrison shows how he approximates reals with a sequence of integers. Generating theorems of the form: | k - x * 2^n | < 1 Here k / 2^n is a approximation of x with an error < 1 / 2^n. In Section 2 Harrison describes how he constructs the real numbers for abstract reasoning. In Section 4 he gives a computational approach. > [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

**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] Applicability of LaTeXsugar and OptionalSugar
- Next by Date: Re: [isabelle] isabelle/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