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
A real number object interpreted in computable mathematics (in realizability) yields the computable real numbers (often just called computable numbers). This is a core object in computable analysis/exact analysis.
Typically a computable real number is an algorithm that successively produces a sequence of rational numbers that approximate a given real number ever more closely.
Klaus Weihrauch, section 4.1 of Computable Analysis Berlin: Springer, 2000
Andrej Bauer, section 5.2 of Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)
Wikipedia, Computable number
Last revised on January 20, 2024 at 12:27:47. See the history of this page for a list of all contributions to it.