[Top][All Lists]

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Axiom-developer] [RealNumbers] Computing with Exact Real Arithmetic

From: Bill Page
Subject: [Axiom-developer] [RealNumbers] Computing with Exact Real Arithmetic
Date: Wed, 15 Jun 2005 03:21:54 -0500

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.

XR - Exact Real Arithmetic


    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.


A Calculator for Exact Real Number Computation


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.

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:

forwarded from

reply via email to

[Prev in Thread] Current Thread [Next in Thread]