constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A function is meant to be called computable if its values on given input may be obtained by an actual computation (an algorithm). Making this precise and studying properties of computable functions is the topic of computability theory.
There are two main concepts of computable functions, called “type I” and “type II”:
In the type I case one considers functions operating on “finite strings of a finite alphabet” hence equivalently on the set of natural numbers. The computable functions in this case are partial recursive functions.
In the type II case one considers functions operating on “infinite strings of a finite alphabet” hence equivalently on the set of infinite sequences of natural numbers (“Baire space”). The idea here is that the computation may be continued indefinitely to produce results always of finite but of ever increasing precision. Therefore this type II-concept is of relevance for computability in analysis, hence in computable analysis/constructive analysis. See at computable function (analysis).
The following table summarizes this and related concepts:
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 |
Lecture notes include