Re: [isabelle] Executing real numbers as approximating functions



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







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