Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Executing real numbers as approximating functions

view this post on Zulip Email Gateway (Aug 19 2022 at 08:12):

From: Johannes Hölzl <hoelzl@in.tum.de>
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@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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:12):

From: Freek Wiedijk <freek@cs.ru.nl>
Hi Florian and Brian,

Bas Spitters points out to me that only in the work that
he and Robbert Krebbers did (which was a continuation of
Russell's work) floats were used in the representations.
Russell used rational numbers, I think.

I think that this move to floats (and other things that
they did, I'm sure) made the computations much faster.

See:

http://arxiv.org/abs/1106.3448/
http://robbertkrebbers.nl/research/reals/

Freek

view this post on Zulip Email Gateway (Aug 19 2022 at 08:34):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,

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?

Thanks a lot,
Florian
signature.asc

view this post on Zulip Email Gateway (Aug 19 2022 at 08:34):

From: Brian Huffman <huffman@in.tum.de>
Russell O'Connor has implemented a similar representation of the
computable reals in Coq:

http://corn.cs.ru.nl/library/fastreal.html

This page contains links to a couple of related papers.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:34):

From: Jasmin Blanchette <jasmin.blanchette@gmail.com>
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

view this post on Zulip Email Gateway (Aug 19 2022 at 08:35):

From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
I'm far from being a math guru, but I dislike so called “reals” in
computer programs. You have alternatives like fixed‑point arithmetic
(common in the Ada world). Or you can work on an integer range instead of
working on a “real range” (ex. do you computation in the range 0::nat to
1000::nat instead in the range 0.0 to 1.0, as an example). If I'm not
wrong, I suspect it to be exactly the same as fixed point arithmetic, but
better ask a math or safe system guru.

Was my two cents beside of the two other replies.

view this post on Zulip Email Gateway (Aug 19 2022 at 08:35):

From: Brian Huffman <huffman@in.tum.de>
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

Last updated: Apr 27 2024 at 01:05 UTC