nLab
computability

Contents

Idea

Computability theory studies mathematical entities that may be obtained by actual computation (instead of by less concrete proofs of existence). As such computability theory is similar to constructive mathematics and to realizability; indeed (emphasized e.g. in (Bauer 05)):

Computable mathematics is the realizability interpretation of constructive mathematics.

Computability theory deals only with computability in principle and disregards the complexity of computation, that is instead the topic of complexity theory.

The key concept in computability theory is that of a computable function, hence of a function whose output may be determined from its input by an actual computation. There are two main types of computability, depending on whether one takes the domain and codomain of computable functions to be finite string from a finite alphabet, hence equivalently natural numbers, or infinite strings from a finite interval, hence sequence of natural numbers.

In the first case – “type I computability” – computable functions are partial recursive functions. In the second – “type II computability” – they are continuous functions on (quotients of) Bair space (see at computable function (analysis)).

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

Properties

Relation to intuitionistic mathematics

Computable mathematics is an instance of intuitionistic mathematics (see e.g. (Bauer 05, section 4.3.1)).

References

The relation to constructive mathematics and realizability is discussed in

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

For computable analysis see

Last revised on May 10, 2017 at 08:17:24. See the history of this page for a list of all contributions to it.