nLab function realizability

Contents

Contents

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

AdmRep eff ↪ KV ↓ ↓ AdmRep ↪ RT(𝒦 2) \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 (2017/18) (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 October 3, 2021 at 03:40:02. See the history of this page for a list of all contributions to it.