Baire space of sequences

This entry is about

theBaire space of sequences of natural numbers. For another concept of the same name in topology proper, see atBaire space.

**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

In the study of computability, descriptive set theory, etc, by *Baire space* is meant the topological space $\mathbb{N}^{\mathbb{N}}$ of infinite sequences of natural numbers equipped with the product topology.

The continuous functions from Baire space to itself serve the role of *computable functions* in computable analysis. 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 |

Lecture notes include

- Andrej Bauer, page 5 and section 5.3.1 of
*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)

Textbook accounts include

- Klaus Weihrauch, section 2.3 of
*Computable Analysis*Berlin: Springer, 2000

Last revised on June 11, 2020 at 10:50:18. See the history of this page for a list of all contributions to it.