nLab
realizability

Context

Foundations

Constructivism, Realizability, Computability

Contents

Idea

The idea of realizability is a way of making the Brouwer-Heyting-Kolmogorov interpretation of constructivism and intuitionistic mathematics precise. It is related to the propositions as types paradigm. For instance, constructively a proof of an existential quantification xXϕ(x)\underset{x\in X}{\exists} \phi(x) consists of constructing a specific xXx \in X and a proof of ϕ(x)\phi(x), which “realizes” the truth of the statement, whence the name (see e.g. Streicher 07, section 1, Vermeeren 09, section 1 for introductions to the rough idea, or Bauer 05, page 12 and def. 4.7 for an actual definition).

computability

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

References

Realizability originates with the interpretation of intuitionistic number theory, later developed as Heyting arithmetic, in

  • Stephen Kleene, On the interpretation of intuitionistic number theory Journal of Symbolic Logic, 10:109–124, 1945. link

A historical survey of realizability (including categorical realizability) is in

A quick survey is in

being a summary of

  • Martin Hyland, The effective topos, in The L.E.J. Brouwer Centenary Symposium (A. S. Toelstra and D. van Dalen, eds.), North-Holland Publishing Company, 1982, pp. 165–216

A modern textbook account is

  • Jaap van Oosten, Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

Lecture notes include

and

  • 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)

based on

  • Andrej Bauer, The Realizability Approach to Computable Analysis and Topology, PhD thesis CMU (2000) (pdf)

  • Peter Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation (pdf.gz)

See also

Last revised on July 9, 2018 at 06:57:07. See the history of this page for a list of all contributions to it.