nLab constructive analysis




Constructive analysis is the incarnation of analysis in constructive mathematics. It is related to, but distinct from, computable analysis; the latter is developed in classical logic explicitly using computability theory, whereas constructive analysis is developed in constructive logic where the computation is implicitly built-in. One can compile results in constructive analysis to computable analysis using realizability.

In applications in computer science one uses for instance the completion monad for exact computations with real numbers (as opposed to floating point arithmetic). Therefore one also sometimes speaks of exact analysis. See also at computable real number.


type I computabilitytype II computability
typical domainnatural numbers \mathbb{N}Baire space of infinite sequences 𝔹= \mathbb{B} = \mathbb{N}^{\mathbb{N}}
computable functionspartial recursive functioncomputable function (analysis)
type of computable mathematicsrecursive mathematicscomputable analysis, Type Two Theory of Effectivity
type of realizabilitynumber realizabilityfunction realizability
partial combinatory algebraKleene's first partial combinatory algebraKleene's second partial combinatory algebra


Introducing the formulation of analysis in constructive mathematics, together with the notions of Bishop set/setoid:

Introduction and review:

See also:

An undergraduate real analysis textbook taking a constructive approach using interval analysis is

  • Mark Bridger, Real Analysis: A Constructive Approach Through Interval Arithmetic, Pure and Applied Undergraduate Texts 38, American Mathematical Society, 2019.

Implementations of constructive real number analysis in type theory implemented in Coq via the completion monad:

(via Type classes in Coq)

Exposition in:

  • Bas Spitters, Verified Implementation of Exact Real Arithmetic in Type Theory, talk at Computable Analysis and Rigorous Numeric (2013) [pdf, pdf]

With emphasis on the use of the univalence axiom:

Implementation in Agda of Cauchy real numbers according to Bishop (1967):


For the alternative Dedekind real numbers or HoTT book real numbers, see the references there.

Last revised on February 22, 2023 at 07:38:57. See the history of this page for a list of all contributions to it.