constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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)).
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 |
Computable mathematics is an instance of intuitionistic mathematics (see e.g. (Bauer 05, section 4.3.1)).
The relation to constructive mathematics and realizability is discussed in
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