constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The subcategory on the effectively computable morphisms of the function realizability topos is the Kleene-Vesley topos . The category of “admissible representations” (whose morphisms are computable functions (analysis), see there) is a reflective subcategory of (BSS 07) and the restriction of that to is
type I computability | type II computability | |
---|---|---|
typical domain | natural numbers | Baire space of infinite sequences |
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)
Andrej Bauer and Andrew Swan, Every metric space is separable in function realizability, 2018, (arxiv:1804.00427)
Last revised on August 29, 2024 at 20:06:40. See the history of this page for a list of all contributions to it.