# nLab function realizability

Contents

### Context

#### Constructivism, Realizability, Computability

intuitionistic mathematics

# Contents

The subcategory on the effectively computable morphisms of the function realizability topos $RT(\mathcal{K}_2)$ is the Kleene-Vesley topos $KV$. The category of “admissible representations” $AdmRep$ (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of $RT(\mathcal{K}_2)$ (BSS 07) and the restriction of that to $KV$ is $AdmRep_{eff}$

$\array{ AdmRep_{eff} &\hookrightarrow& KV \\ \downarrow && \downarrow \\ AdmRep &\hookrightarrow& RT(\mathcal{K}_2) }$

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

• Thomas Streicher, around p. 17 of Realizability (2007/08) (pdf)

• Jaap van Oosten, Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)

• Ingo Battenfeld, Matthias Schröder, Alex Simpson, A convenient category of domains, in L. Cardelli, M. Fiore and G. Winskel (eds.), Computation, Meaning and Logic, Articles dedicated to Gordon Plotkin Electronic Notes in Computer Science, 34 pp., to appear, 2007 (pdf)

Last revised on March 9, 2014 at 09:19:19. See the history of this page for a list of all contributions to it.