nLab constructive analysis

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.

	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

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

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]