analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A computable function is often taken to be one that acts on the natural numbers (a partial recursive function) but for purposes of analysis (computable analysis, exact analysis) and related fields (notably physics, see at computable physics) one considers computation on real numbers to finite but arbitrary precision. This means that in this context of analysis a computable function should be an algorithm that successively reads in natural numbers from a possibly infinite list (specifying an input to ever higher accuracy) and accordingly outputs a result as incrementally as an infinite list.
Mathematically this is captured by continuous functions on quotient spaces of Baire space (computability) and goes by the name Type Two Theory of Effectivity or similar. In implementations this is essentially what is known as exact real computer arithmetic.
In Type Two Theory of Effectivity for computable analysis (see Weihrauch 00) one considers the following definition:
A representation of a $T_0$-topological space $X$ is a presentation of it as a quotient space of a subspace $B$ of Baire space (the underlying space of Kleene's second algebra). See also at effective topological space.
Such a representation is called admissible if the quotient map $B \to X$ has the right lifting property against continuous functions out of other subspaces $B'$ of Baire space.
Given representations of $X$ and $X'$ in this way, then a function $f \colon X \to X'$ is called continuously realizable if there exists a continuous function $\phi \colon B \to B'$ between the corresponding subspaces of Baire space such that the evident diagram commutes.
For admissible representations a function $X\to X'$ is continuously realizable precisely if it is already continuous.
Write $AdmRep$ for the category of admissible representations in this sense, and continuously realizable (and hence continuous) functions between these.
The category $AmdRep$ is cartesian closed and has all countable limits and colimits (BSS 07 (4.10))
The category $AdmRep$ above is a reflective subcategory of the function realizability topos $RT(\mathcal{K}_2)$ (see vanOosten 08).
$AdmRep$ is equivalent to the full subcategory of that of topological spaces on the $T_0$-quotient spaces of countably based $T_0$ spaces (BSS 07).
Under the above inclusion, all complete separable metric spaces are in $AdmRep$.
Some standard classes of examples (with an eye towards applications in computable physics) are discussed in Weihrauch-Zhong 02, def. 2.6
Since the Sierpinski space is in $AdmRep$, and due to cartesian clossure above, for any $X \in AdmRep$ also its lattice of closed subspaces is in $AdmRep$.
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 |
The subcategory on the effectively computable morphisms of the function realizability topos $RT(\mathcal{K}_2)$ is the Kleene-Vesley topos. The category of “admissible representations” $AdmRep$ above is a a reflective subcategory of $RT(\mathcal{K}_2)$ and the restriction of that to $KV$ is $AdmRep_{eff}$
See also
Lecture notes include
A useful review is in section 4 of
Textbooks include
Klaus Weihrauch, Computable Analysis. Berlin, Springer, 2000
Jaap van Oosten, Realizability: an introduction to its categorical side, Studies in Logic and the Foundations of Mathematics, vol. 152, Elsevier, 2008 (preface pdf)
Concrete examples with an eye towards applications in computable physics are discussed in section 2 of
$\,$
$\,$
$\,$
$\,$
$\,$
$\,$
$\,$
$\,$