constructive analysis



Constructivism, Realizability, Computability



Constructive analysis is the incarnation of analysis in constructive mathematics. Also known as computable analysis (see there for more).

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


The formulation of analysis in constructive mathematics was maybe inititated in

  • Errett Bishop, Foundations of constructive analysis. McGraw-Hill, (1967)

together with the basic notion of Bishop set/setoid.

A survey is in

  • Herman Geuvers, Milad Niqui, Bas Spitters, Freek Widijk?, Constructive analysis, types and exact real numbers, Science Mathematical Structures in Computer Science / Volume 17 / Issue 01 / February 2007, pp 3-36 (publisher)

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

  • R. O’Connor, A Monadic, Functional Implementation of Real Numbers. MSCS, 17(1):129{159, 2007.

  • R. O’Connor, Certied exact transcendental real number computation in Coq, In TPHOLs 2008, LNCS 5170, pages 246–261, 2008.

  • R. O’Connor, Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory, PhD thesis, Radboud University Nijmegen, 2009.

  • Robbert Krebbers, Bas Spitters, Type classes for efficient exact real arithmetic in Coq (arXiv:1106.3448)

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

Last revised on March 3, 2014 at 23:55:14. See the history of this page for a list of all contributions to it.