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

[Bill Page]

Changes http://page.axiom-developer.org/zope/mathaction/RealNumbers/diff
--
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
downloaded at the following URL:

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

--
forwarded from http://page.axiom-developer.org/zope/mathaction/address@hidden