nLab
constructive analysis

Context

Analysis

Constructivism, Realizability, Computability

Contents

Idea

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.

computability

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

References

The formulation of analysis in constructive mathematics was maybe inititated in

together with the basic notion of Bishop set/setoid.

A survey is in

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

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

With emphasis on the use of the univalence axiom:

See also