analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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.
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
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)
further discussed in:
Jerzy Karczmarczuk, Infinite precision real fractions, and lazy carry propagation or: The Most Unreliable Technique in the World to Compute , A Braga School (1998) [pdf, pdf]
Simon Plouffe, On the computation of the 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:
Last revised on March 6, 2023 at 10:15:01. See the history of this page for a list of all contributions to it.