nLab computable analysis




Constructivism, Realizability, Computability



computability in analysis, constructive analysis


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


A standard textbook is

A survey is in

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

The Relation to realizability topos theory is discussed in

  • P. Lietz, From constructive mathematics to computable analysis via the realizability interpretation , Ph.D. dissertation, Fachbereich Mathematik, TU Darmstadt, Darmstadt, 2004.

  • Andrej Bauer, The realizability approach to computable analysis and topology, Ph.D. dissertation, School of Computer Science, Carnegie Mellon University, Pittsburgh, 2000.

  • Andrej Bauer, Realizability as connection between constructive and computable mathematics, in T. Grubba, P. Hertling, H. Tsuiki, and Klaus Weihrauch, (eds.) CCA 2005 - Second International Conference on Computability and Complexity in Analysis, August 25-29,2005, Kyoto, Japan, ser. Informatik Berichte, , vol. 326-7/2005. FernUniversität Hagen, Germany, 2005, pp. 378–379. (pdf)

Last revised on October 8, 2019 at 19:39:44. See the history of this page for a list of all contributions to it.