

last edited 4 years ago by test1 
1 2 3 4 5  
Editor:
Time: 2008/03/21 09:12:43 GMT7 

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 onetoone 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 fixedpoint 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 lambdacalculus. In contrast, the reals require the more powerful axioms of ZermeloFraenkel 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> 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 digitenumerable real numbers are in general not digitenumerable. 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 digitenumeration 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, FloatingPoint Computation, Prentice Hall, 1974. Sterbenz worked at IBM Systems Research Institute, New York at the time of writing the book. William <hr> From daly@axiomdeveloper.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 MessageID: <200506150321530500@page.axiomdeveloper.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 floatingpoint codes. An important distinction is that in multipleprecision floatingpoint 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: http://www.cs.ru.nl/~milad/proefschrift/thesis.pdf 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 MessageID: <200506150408060500@page.axiomdeveloper.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 MessageID: <200601231954580600@wiki.axiomdeveloper.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 MessageID: <200601301938070600@wiki.axiomdeveloper.org> http://www.inria.fr/rrrt/rr0760.html RR0760  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/publipsgz/RR/RR0760.ps.gz  ftp://ftp.inria.fr/INRIA/publication/publipdf/RR/RR0760.pdf Note that Axiom already has a domain for ContinuedFractions: http://wiki.axiomdeveloper.org/axiomtest1/src/algebra/ContfracSpad 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 MessageID: <200608082035040500@wiki.axiomdeveloper.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
In mathematics, the real numbers are intuitively defined as numbers that are in onetoone 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 fixedpoint 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
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 lambdacalculus. In contrast, the reals require the more powerful axioms of ZermeloFraenkel 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
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 digitenumerable real numbers are in general not digitenumerable. 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 digitenumeration 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, FloatingPoint Computation, Prentice Hall, 1974.
Sterbenz worked at IBM Systems Research Institute, New York at the time of writing the book.
William
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
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
This is an implementation of exact (or constructive) real arithmetic, including python and C++ versions. It is an alternative to multiple precision floatingpoint codes. An important distinction is that in multipleprecision floatingpoint 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
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 NumbersAlberto 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/crcalcThis 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.
RR0760  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?:
http://wiki.axiomdeveloper.org/axiomtest1/src/algebra/ContfracSpad
http://www.brics.dk/~barnie/RealLibRealLib? 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.