basic constructions:
strong axioms
further
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
The idea of realizability is a way of making the Brouwer-Heyting-Kolmogorov interpretation of constructivism and intuitionistic mathematics precise. It is related to the propositions as types paradigm. For instance, constructively a proof of an existential quantification $\underset{x\in X}{\exists} \phi(x)$ consists of constructing a specific $x \in X$ and a proof of $\phi(x)$, which “realizes” the truth of the statement, whence the name (see e.g. Streicher 07, section 1, Vermeeren 09, section 1 for introductions to the rough idea, or Bauer 05, page 12 and def. 4.7 for an actual definition).
One possible way to find a computational interpretation for univalence in homotopy type theory is to interpret it in using realizability. Stekelburg provides a univalent universe of modest Kan complexes.
Simplicial homotopy theory can be developed in an extensive locally cartesian closed category $A$. Such categories are also called Heyting bialgebras?. The category $A$ has a class of small maps which has a bundle of small assemblies. This provides an internal Heyting bialgebra? $S$ which we can use as a target for simplicial `sets'. There is a (Kan-) model structure on these simplicial sets.
Within $S$ we can define a universe $M$ and show that it is fibrant. This universe is even univalent.
Now, the category of assemblies in number realizability provides such a Heyting bialgebra. The modest sets, a small internally complete full subcategory, provide the univalent universe. Note that modest sets are an impredicative universe. It models the calculus of constructions.
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 |
Realizability originates with the interpretation of intuitionistic number theory, later developed as Heyting arithmetic, in
A historical survey of realizability (including categorical realizability) is in
A quick survey is in
being a summary of
Symposium (A. S. Toelstra and D. van Dalen, eds.), North-Holland Publishing Company, 1982, pp. 165–216
A modern textbook account is
Lecture notes include
and
based on
Andrej Bauer, The Realizability Approach to
Computable Analysis and Topology_, PhD thesis CMU (2000) (pdf)
Peter Lietz, From Constructive Mathematics to Computable Analysis via the Realizability Interpretation (pdf.gz)
For realizability of univalent universes:
See also
Steven Awodey, Andrej Bauer, Sheaf toposes for realizability (pdf)
Wouter Pieter Stekelenburg, Realizability Categories, PhD thesis, Utrecht 2013 (arXiv:1301.2134)
Martin Hyland, Variations on realizability: realizing the propositional axiom of choice, Mathematical Structures in Computer Science, Volume 12, Issue 3, June 2002, pp. 295 - 317 (doi:10.1017/S0960129502003651, pdf)
Last revised on June 9, 2022 at 19:05:10. See the history of this page for a list of all contributions to it.