constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
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}$
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 |
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)