Edit detail for RealNumbers revision 4 of 5

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.

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

---

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

Bill, thanks for creating this page. I enjoyed reading the links.

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

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

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://keithbriggs.info/software.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:

http://www.cs.ru.nl/~milad/proefschrift/thesis.pdf

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.

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.

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?:

http://wiki.axiom-developer.org/axiom--test--1/src/algebra/ContfracSpad

http://daimi.au.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://daimi.au.dk/~barnie/

[ComputableRealNumbers]?