nLab exact real computer arithmetic

Idea

Exact real computer arithmetic refers to treatment of real number arithmetic on computers to finite (necessarily) but arbitrary precision. This is in contrast with what is called floating-point arithmetic? which uses just one fixed finite approximation of the real numbers by natural numbers.

Exact real computer arithmetic essentially implements what in mathematical computability theory is known as the type-II theory (in contrast to the “type-I” theory of partial recursive functions acting just on natural numbers). The formal mathematical definition of computable function (analysis) is the core topic of constructive analysis/exact analysis.

Related concepts

• topological domain theory

References

For more see the references at real number and at constructive analysis.

• Chee-Keng Yap, Thomas Dubé, The exact computation paradigm, in: Computing in Euclidean Geometry, Lecture Notes Series on Computing, World Scientific (1995) 452-492 [doi:10.1142/9789812831699_0011, pdf]

• Jean Vuillemin, Exact real computer arithmetic with continued fractions, in LFP ‘88: Proceedings of the 1988 ACM conference on LISP and functional programming (1988) 14–27 [doi:10.1145/62678.62681]

• Peter Potts, Abbas Edalat, Exact real computer arithmetic (1997) [pdf, pdf]

• Dave Plume (supervised by Martín Escardó, Alex Simpson): A Calculator for Exact Real Number Computation, University of Edinburgh (1998) [web]

A collection of further references is listed at

• Exact computation

Discussion relating to computability theory, Type Two Theory of Effectivity and constructive analysis/computable analysis includes

• Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk, Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science 17 01 (2007) 3-36 [doi:10.1017/S0960129506005834]

• The Haskell Wiki, Exact real arithmetic

Efficient exact representations of pi and related irrational numbers (Bailey-Borwein-Plouffe algorithm)

• David Bailey, Peter Borwein, Simon Plouffe: On the Rapid Computation of Various Polylogarithmic Constants, Math. Comp. 66 (1997) 903-913 [doi:1997-66-218/S0025-5718-97-00856-9, pdf]

further discussed in:

• Jerzy Karczmarczuk, Infinite precision real fractions, and lazy carry propagation or: The Most Unreliable Technique in the World to Compute $\pi$, A Braga School (1998) [pdf, pdf]

• Simon Plouffe, On the computation of the $n^{th}$ decimal digit of various transcendental numbers [arXiv:0912.0303]

• MathWorld, BBP-Type formula

Implementation of Cauchy real numbers (in Bishop-style constructive analysis) in Agda:

• Martin Lundfall, Formalizing real numbers in Agda (2015) [pdf, pdf, github]

• Zachary Murray, Constructive Analysis in the Agda Proof Assistant [arXiv:2205.08354, github]

Coding of something like the HoTT book real numbers in Coq:

• Gaëtan Gilbert, Formalising Real Numbers in Homotopy Type Theory, in CPP 2017: Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs (2017) 112–124 [arXiv:1610.05072, doi:10.1145/3018610.3018614]