login  home  contents  what's new  discussion  bug reports help  links  subscribe  changes  refresh  edit

# Edit detail for RealNumbers revision 1 of 5

 1 2 3 4 5 Editor: Time: 2008/03/21 09:12:43 GMT-7 Note: The RealLib Project

changed:
-
Axiom implements the number domains Integer, Float and even
Fraction(Integer) i.e. rational numbers, but it does not
implement anything called Real numbers. *Why is that?*

This subject was discussed in issue #167 Infinite Floats Domain

Real Numbers

In mathematics, the real numbers are intuitively defined as numbers
that are in one-to-one correspondence with the points on an infinite
line—the number line. The term "real number" is a retronym coined in
response to "imaginary number".

Real numbers may be rational or irrational; algebraic or transcendental;
and positive, negative, or zero. ...

A real number is said to be computable if there exists an algorithm that
yields its digits. Because there are only countably many algorithms, but
an uncountable number of reals, most real numbers are not computable. Some
constructivists accept the existence of only those reals that are computable.
The set of definable numbers is broader, but still only countable.

Computers can only approximate most real numbers with rational numbers;
these approximations are known as floating point numbers or fixed-point
numbers; see real data type. Computer algebra systems are able to treat
some real numbers exactly by storing an algebraic description (such as $\sqrt{2}$)
rather than their decimal approximation.

See: http://en.wikipedia.org/wiki/Real_number

Computable Numbers

In mathematics, theoretical computer science and mathematical logic,
the computable numbers, also known as the recursive numbers, are the
subset of the real numbers consisting of the numbers which can be
computed by a finite, terminating algorithm. They can be defined
equivalently using the axioms of recursive functions, Turing machines
or lambda-calculus. In contrast, the reals require the more powerful
axioms of Zermelo-Fraenkel set theory. The computable numbers form a
real closed field and can be used in the place of real numbers for some,
but by no means all, mathematical purposes.

See: http://en.wikipedia.org/wiki/Computable_number

<hr>
From wyscc Wed Jun 15 01:36:00 -4:00<br>

It is interesting to note that order relations are not computable and that sums of digit-enumerable real numbers are in general not digit-enumerable. This reminds me that when I teach power series solution to differential equations, I use the analog of decimal numbers and comment that power series are easier, because they involve no carry. The same reason shows the infinite sequence approach to infinite precision floating point (essentially using digit-enumeration Turing machines) discussed in #167 Infinite Floats Domain will not work. IPFP is different from power series!

Wikipedia also has an introduction to floating point systems::

http://en.wikipedia.org/wiki/Floating_point

For in depth study, I recommend the book::

Pat H. Sterbenz, Floating-Point Computation, Prentice Hall, 1974.

Sterbenz worked at IBM Systems Research Institute, New York at the time of writing the book.

William

<hr>
From daly@axiom-developer.org Wednesday, June 15, 2005 1:23 AM

Subject: Real Numbers

see http://cch.loria.fr/documentation/IEEE754

in particular see William Kahan and IEEE 754. William (Velvel aka Wolf) Kahan
is the curmudgeon of floating point "real" numbers.

t

From BillPage Wed Jun 15 03:21:53 -0500 2005
From: Bill Page
Date: Wed, 15 Jun 2005 03:21:53 -0500
Subject: Computing with Exact Real Arithmetic
Message-ID: <20050615032153-0500@page.axiom-developer.org>

There is apparently a lot of work on this subject.

Some History

http://www.rbjones.com/rbjpub/cs/cs006.htm

> The lazy digit sequence approach (similar to lazy power series) has,
> for example, been implemented by Michael Stoll in Common Lisp, 1988.

http://www.haible.de/bruno/MichaelStoll/reals.html

XR - Exact Real Arithmetic

Overview

This is an implementation of exact (or constructive) real arithmetic,
including python and C++ versions. It is an alternative to multiple-
precision floating-point codes. An important distinction is that in
multiple-precision floating-point one sets the precision before starting
a computation, and then one cannot be sure of the final result. Interval
arithmetic is an improvement on this, but still not an ideal solution
because if the final interval is larger than desired, there is no simple
way to restart the computation at higher precision. By constrast, in XR
no precision level is set in advance, and no computation takes place
until a final request takes place for some output.

http://more.btexact.com/people/briggsk2/XR.html

Others

A Calculator for Exact Real Number Computation

Abstract

The most usual approach to real arithmetic on computers consists
of using floating point approximations. Unfortunately, floating
point arithmetic can sometimes produce wildly erroneous results.
One alternative approach is to use exact real arithmetic. Exact
real arithmetic allows exact real number computation to be performed
without the roundoff errors characteristic of other methods.

http://www.dcs.ed.ac.uk/home/mhe/plume

Formalising exact Arithmetic

... deals with exact rational and real arithmetic in constructive type
theory. Parts of the thesis are formalised in Coq. The thesis can be

From BillPage Wed Jun 15 04:08:06 -0500 2005
From: Bill Page
Date: Wed, 15 Jun 2005 04:08:06 -0500
Subject: implementing Exact Real Numbers
Message-ID: <20050615040806-0500@page.axiom-developer.org>

A certified, corecursive implementation
of exact Real Numbers

Alberto Ciaffaglione a, Pietro Di Gianantonio

http://www.dimi.uniud.it/~ciaffagl/Papers/reals.pdf

Abstract
We implement exact real numbers in the logical framework Coq using streams, i.e.,
infinite sequences, of digits, and characterize constructive real
numbers through a minimal axiomatization. We prove that our
construction inhabits the axiomatization, working formally with
coinductive types and corecursive proofs. Thus we obtain reliable,
corecursive algorithms for computing on real numbers.

From billpage Mon Jan 23 19:54:58 -0600 2006
From: billpage
Date: Mon, 23 Jan 2006 19:54:58 -0600
Subject: Constructive Reals Calculator
Message-ID: <20060123195458-0600@wiki.axiom-developer.org>

http://www.hpl.hp.com/personal/Hans_Boehm/crcalc

Overview

This is a calculator that operates on constructive real numbers.
Numbers are represented exactly internally to the calculator, and
then evaluated on demand to guarantee an error in the displayed
result that is strictly less than one in the least significant
displayed digit. It is possible to scroll the display to the right
to generate essentially arbitrary precision in the result.

From BillPage Mon Jan 30 19:38:07 -0600 2006
From: Bill Page
Date: Mon, 30 Jan 2006 19:38:07 -0600
Subject: Exact real computer arithmetic with continued fractions
Message-ID: <20060130193807-0600@wiki.axiom-developer.org>

http://www.inria.fr/rrrt/rr-0760.html

RR-0760 - Exact real computer arithmetic with continued fractions::

Vuillemin, J.
Rapport de recherche de l'INRIA - Rocquencourt
49 pages - Novembre 1987 - Document en anglais
Fichier PostScript / PostScript file (1821 Ko) Fichier PDF / PDF file (1761 Ko)

- ftp://ftp.inria.fr/INRIA/publication/publi-ps-gz/RR/RR-0760.ps.gz

- ftp://ftp.inria.fr/INRIA/publication/publi-pdf/RR/RR-0760.pdf

Note that Axiom already has a domain for ContinuedFractions:

From billpage Tue Aug 8 20:35:04 -0500 2006
From: billpage
Date: Tue, 08 Aug 2006 20:35:04 -0500
Subject: The RealLib Project
Message-ID: <20060808203504-0500@wiki.axiom-developer.org>

http://www.brics.dk/~barnie/RealLib

RealLib is a real number computation package in C++. Its primary aim is to be efficient and to avoid the huge overheads usually associated with real number computations.

RealLib3, which is the current version of the library, makes this possible. In this version of the library, the user can work on both a layer where numbers are represented as terms describing the computation, and a layer where functions on real numbers compute on the level of approximations to the real number. The latter can be very fast, depending on the precision that is actually required by the computation. In the cases where machine precision is sufficient, exact real computations can be executed at a speed comparable to the speed of double precision arithmetic, sometimes even running on par with it.

Branimir Lambov's homepage --
http://www.brics.dk/~barnie


Axiom implements the number domains Integer, Float and even Fraction(Integer) i.e. rational numbers, but it does not implement anything called Real numbers. Why is that?

This subject was discussed in issue #167 Infinite Floats Domain

## Real Numbers

In mathematics, the real numbers are intuitively defined as numbers that are in one-to-one correspondence with the points on an infinite line—the number line. The term "real number" is a retronym coined in response to "imaginary number".

Real numbers may be rational or irrational; algebraic or transcendental; and positive, negative, or zero. ...

A real number is said to be computable if there exists an algorithm that yields its digits. Because there are only countably many algorithms, but an uncountable number of reals, most real numbers are not computable. Some constructivists accept the existence of only those reals that are computable. The set of definable numbers is broader, but still only countable.

Computers can only approximate most real numbers with rational numbers; these approximations are known as floating point numbers or fixed-point numbers; see real data type. Computer algebra systems are able to treat some real numbers exactly by storing an algebraic description (such as ) rather than their decimal approximation.

## Computable Numbers

In mathematics, theoretical computer science and mathematical logic, the computable numbers, also known as the recursive numbers, are the subset of the real numbers consisting of the numbers which can be computed by a finite, terminating algorithm. They can be defined equivalently using the axioms of recursive functions, Turing machines or lambda-calculus. In contrast, the reals require the more powerful axioms of Zermelo-Fraenkel set theory. The computable numbers form a real closed field and can be used in the place of real numbers for some, but by no means all, mathematical purposes.

From wyscc Wed Jun 15 01:36:00 -4:00

It is interesting to note that order relations are not computable and that sums of digit-enumerable real numbers are in general not digit-enumerable. This reminds me that when I teach power series solution to differential equations, I use the analog of decimal numbers and comment that power series are easier, because they involve no carry. The same reason shows the infinite sequence approach to infinite precision floating point (essentially using digit-enumeration Turing machines) discussed in #167 Infinite Floats Domain will not work. IPFP is different from power series!

Wikipedia also has an introduction to floating point systems::

http://en.wikipedia.org/wiki/Floating_point

For in depth study, I recommend the book::

Pat H. Sterbenz, Floating-Point Computation, Prentice Hall, 1974.

Sterbenz worked at IBM Systems Research Institute, New York at the time of writing the book.

William

From daly@axiom-developer.org Wednesday, June 15, 2005 1:23 AM

Subject: Real Numbers

in particular see William Kahan and IEEE 754. William (Velvel aka Wolf) Kahan is the curmudgeon of floating point "real" numbers.

t

Computing with Exact Real Arithmetic --Bill Page, Wed, 15 Jun 2005 03:21:53 -0500 reply
There is apparently a lot of work on this subject.

## Some History

The lazy digit sequence approach (similar to lazy power series) has, for example, been implemented by Michael Stoll in Common Lisp, 1988.

http://www.haible.de/bruno/MichaelStoll/reals.html

## XR - Exact Real Arithmetic

### Overview

This is an implementation of exact (or constructive) real arithmetic, including python and C++ versions. It is an alternative to multiple- precision floating-point codes. An important distinction is that in multiple-precision floating-point one sets the precision before starting a computation, and then one cannot be sure of the final result. Interval arithmetic is an improvement on this, but still not an ideal solution because if the final interval is larger than desired, there is no simple way to restart the computation at higher precision. By constrast, in XR no precision level is set in advance, and no computation takes place until a final request takes place for some output.

http://more.btexact.com/people/briggsk2/XR.html

Others

## A Calculator for Exact Real Number Computation

Abstract

The most usual approach to real arithmetic on computers consists of using floating point approximations. Unfortunately, floating point arithmetic can sometimes produce wildly erroneous results. One alternative approach is to use exact real arithmetic. Exact real arithmetic allows exact real number computation to be performed without the roundoff errors characteristic of other methods.

http://www.dcs.ed.ac.uk/home/mhe/plume

Formalising exact Arithmetic

... deals with exact rational and real arithmetic in constructive type theory. Parts of the thesis are formalised in Coq. The thesis can be downloaded at the following URL:

implementing Exact Real Numbers --Bill Page, Wed, 15 Jun 2005 04:08:06 -0500 reply
A certified, corecursive implementation of exact Real Numbers

Alberto Ciaffaglione a, Pietro Di Gianantonio

http://www.dimi.uniud.it/~ciaffagl/Papers/reals.pdf

Abstract We implement exact real numbers in the logical framework Coq using streams, i.e., infinite sequences, of digits, and characterize constructive real numbers through a minimal axiomatization. We prove that our construction inhabits the axiomatization, working formally with coinductive types and corecursive proofs. Thus we obtain reliable, corecursive algorithms for computing on real numbers.

Constructive Reals Calculator --billpage, Mon, 23 Jan 2006 19:54:58 -0600 reply
http://www.hpl.hp.com/personal/Hans_Boehm/crcalc

## Overview

This is a calculator that operates on constructive real numbers. Numbers are represented exactly internally to the calculator, and then evaluated on demand to guarantee an error in the displayed result that is strictly less than one in the least significant displayed digit. It is possible to scroll the display to the right to generate essentially arbitrary precision in the result.

Exact real computer arithmetic with continued fractions --Bill Page, Mon, 30 Jan 2006 19:38:07 -0600 reply
http://www.inria.fr/rrrt/rr-0760.html

RR-0760 - Exact real computer arithmetic with continued fractions:

    Vuillemin, J.
Rapport de recherche de l'INRIA - Rocquencourt
49 pages - Novembre 1987 - Document en anglais
Fichier PostScript / PostScript file (1821 Ko) Fichier PDF / PDF file (1761 Ko)


Note that Axiom already has a domain for ContinuedFractions?: