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
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 computability | type II computability | |
---|---|---|
typical domain | natural numbers $\mathbb{N}$ | Baire space of infinite sequences $\mathbb{B} = \mathbb{N}^{\mathbb{N}}$ |
computable functions | partial recursive function | computable function (analysis) |
type of computable mathematics | recursive mathematics | computable analysis, Type Two Theory of Effectivity |
type of realizability | number realizability | function realizability |
partial combinatory algebra | Kleene's first partial combinatory algebra | Kleene's second partial combinatory algebra |
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
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)
With emphasis on the use of the univalence axiom:
Auke Booij, Constructive analysis in univalent type theory, 2017 (pdf)
Auke Booij, Extensional constructive real analysis via locators (arXiv:1805.06781)
See also