nLab constructive analysis

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.

Related concepts

computability

	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

• computable real number

• exact real computer arithmetic

• computable physics

• constructive set theory

• constructive algebraic topology

References

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

• Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)

• Errett Bishop, Douglas Bridges: Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer (1985) [doi:10.1007/978-3-642-61667-9]

Introduction and review:

• Douglas Bridges, Constructive mathematics: a foundation for computable analysis, Theoretical Computer Science 219 1–2 (1999) 95-109 [doi:10.1016/S0304-3975(98)00285-0]

• Herman Geuvers, Milad Niqui, Bas Spitters, Freek Wiedijk, Constructive analysis, types and exact real numbers, Mathematical Structures in Computer Science 17 01 (2007) 3-36 [doi:10.1017/S0960129506005834]

• Helmut Schwichtenberg, Constructive analysis with witnesses (2013) [pdf, pdf]

• Fredrik Johansson, Reliable real computing, talk at Mathematical Institute of Oxford (2019) [pdf]

See also:

• Helmut Schwichtenberg, Program Extraction in Constructive Analysis, in Logicism, Intuitionism, and Formalism, Synthese Library, 341 Springer (2009) [doi:10.1007/978-1-4020-8926-8_13]

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:

• Russell O'Connor, A Monadic, Functional Implementation of Real Numbers, Math. Struc. Comp. Sci. 17 1 (2007) 129-159 [arXiv:cs/0605058, doi:10.1017/S0960129506005871]

• Russell O'Connor, Certified exact transcendental real number computation in Coq, in Theorem Proving in Higher Order Logics. TPHOLs 2008, Lecture Notes in Computer Science 5170 (2008) 246-261 [arXiv:0805.2438, doi:10.1007/978-3-540-71067-7_21]

• Russell O'Connor, Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory, PhD thesis, Radboud University Nijmegen (2009) [ubn:2066/76032, author webpage]

• Robbert Krebbers, Bas Spitters, Type classes for efficient exact real arithmetic in Coq, Logical Methods in Computer Science, 9 1 (2013) lmcs:958 [arXiv:1106.3448, doi:10.2168/LMCS-9(1:1)2013]

(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:

• Auke Booij, Constructive analysis in univalent type theory, 2017 (pdf)

• Auke Booij, Extensional constructive real analysis via locators, Mathematical Structures in Computer Science 31 1 (2021) 64-88 [arXiv:1805.06781, doi:10.1017/S0960129520000171]

• Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]

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

• Martin Lundfall, Formalizing real numbers in Agda (2015) [pdf, pdf, github]

• Zachary Murray, Constructive Analysis in the Agda Proof Assistant [arXiv:2205.08354, github]

review:

• Zachary Murray, Constructive Real Numbers in the Agda Proof Assistant, talk at CQTS, (Feb 2023) [video:YT]

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