nLab
computable analysis

Context

Analysis

Constructivism, Realizability, Computability

Contents

Idea

computability in analysis, constructive 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

References

A standard textbook is

A survey is in

The Relation to realizability topos theory is discussed in