UP

Implementation of Computation with Reals

Implementations

I'm not at present in a position to tell you whether these are any good. I don't think either will work straightforwardly on a PC (so its not so easy for me to try them).

The package C_CALC was written by Hans Boehm, Vernon Lee and Alan J. Demers in 1988-9 using the programming language Russell. It provides a calculator which does precise arithmetic on real numbers using functions to represent the numbers. The package is available from Xerox or from Rice University. It may well be defunct now, but Hans Boehm, now at HP, has implemented a constructive reals calculator in Java, which runs on the web. According to Boehm, in this implementation:

A constructive real number x is represented abstractly as a function fx, such that fx(n) produces a scaled integer approximation to x, with an error of strictly less than 2n.
More precisely: |fx(n) * 2n - x| < 2n

Sheng Liang and Rajiv Mirani wrote a Haskell implementation of Boehm's constructive reals. A version that works with Haskell 1.3 can be found at yale: symalg

David Plume has recently implemented exact real arithmetic in Haskell and his calculator performing exact real arithmetic is available on the web for all to try. He has some web pages on this project which point you to his project report, to the online calculator and also to a page of relevant links.

Keith Briggs of BTExaCT has an implementation of exact real arithmetic in C++.

Exact Real Computation in ProofPower


UP HOME © HOME created 1996-02-03 modified 2006-05-28