nLab exact real computer arithmetic




Constructivism, Realizability, Computability



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.


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

A collection of further references is listed at

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

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

further discussed in:

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

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

Last revised on March 6, 2023 at 10:15:01. See the history of this page for a list of all contributions to it.