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

based on

For computable analysis see