computability in nLab
Context
Constructivism, Realizability, Computability
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
Constructive mathematics
Realizability
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)).
Properties
Relation to intuitionistic mathematics
Computable mathematics is an instance of intuitionistic mathematics (see e.g. (Bauer 05, section 4.3.1)).
References
Textbook containing the basic notions:
- Michael Sipser, Introduction to the Theory of Computation, Third edition (2012), Course Technology Inc.
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
- Klaus Weihrauch, Computable Analysis Berlin: Springer, 2000
Last revised on November 27, 2022 at 14:13:28. See the history of this page for a list of all contributions to it.