In this post about the difference between the recursive and effective topos, Andrej Bauer said:
If you are looking for a deeper explanation, then perhaps it is fair to say that the Recursive Topos models computability a la Banach-Mazur (a map is computable if it takes computable sequences to computable sequences) and the Effective topos models computability a la Kleene (a map is computable if it is realized by a Turing machine). In many respects Kleene's notion of computability is better, but you'll have to ask another question to find out why 🙂
So I'm asking:
1) What is "computability a la Banach-Mazur"? I would guess it has something to do with Baire spaces and computable analysis, but I don't really know.
2) Why is Kleene's notion of computability better?
Best Answer
This answer requires a bit of background.
Definition 1: a numbered set $(X,\nu_X)$ is a set $X$ together with a partial surjection $\nu_X : \mathbb{N} \to X$, called a numbering of $X$. When $\nu_X(n) = x$ we say that $n$ is a code for $x$.
Numbered sets are a generalization of Gödel codes. Some typical examples are:
Numbered sets can be used to give effective structure to many mathematical structures. What should we take as a morphism between numbered sets? Presumably a map $f : X \to Y$ should be considered a morphism from $(X,\nu_X)$ to $(Y,\nu_Y)$ when it is "computable" in a suitable sense. We understand fairly well what it means to have a computable map $\mathbb{N} \to \mathbb{N}$, namely computed by a Turing machine, so let us take that for granted. It is easy to extend computability of sequences of numbers to computability of arbitrary sequences:
Defintion 2: A map $s : \mathbb{N} \to X$ is a computable sequence in $(X,\nu_X)$ when there exists a computable map $f : \mathbb{N} \to \mathbb{N}$ such that $s(n) = \nu_X(f(n))$ for all $n \in \mathrm{dom}(\nu_X)$.
Now suppose we think a bit like analysts. One way to define a continuous map is to say that it maps convergent sequences to convergent sequences. We could mimick this idea to define general computable maps.
Definition 3: A function $f : X \to Y$ where $(X,\nu_X)$ and $(Y,\nu_Y)$ are numbered sets is Banach-Mazur computable when $f \circ s$ is a computable sequence in $(Y,\nu_Y)$ whenever $s$ is a computable sequence in $(X,\nu_X)$.
How good is this notion? And how does it compare to the following notion, which is taken as the standard one nowadays?
Definition 3: A function $f : X \to Y$ where $(X,\nu_X)$ and $(Y,\nu_Y)$ are numbered sets is Markov computable, or just computable, when there exists a partial computable map $g : \mathbb{N} \to \mathbb{N}$ such that $f(\nu_X(n)) = \nu_Y(g(n))$ for all $n \in \mathrm{dom}(\nu_X)$.
In other words, $f$ is tracked by $g$ in the sense that $g$ does to codes what $f$ does to elements. (Note: in this MO I attributed this notion of computability to Kleene, but I think it's better to attach Markov's name to it, if any.)
Every Markov computable function is Banach-Mazur computable. In some cases the converse holds as well. For example, every Banach-Mazur computable map $\mathbf{N} \to \mathbf{N}$ is Markov computable. However, this is not the case in general:
R. Friedberg demonstrated that there is a Banach-Mazur computable map $\mathbf{N}^\mathbf{N} \to \mathbf{N}$ which is not Markov computable. [R. Friedberg. 4-quantifier completeness: A Banach-Mazur functional not uniformly partial recursive. Bull. Acad. Polon. Sci. Sr. Sci. Math. Astr. Phys., 6:1–5, 1958.]
P. Hertling constructed a Banach-Mazur computable map $\mathbf{R} \to \mathbf{R}$ which is not Markov computable. [P. Hertling. A Banach-Mazur computable but not Markov computable function on the computable real numbers. In Proceedings ICALP 2002, pages 962–972. Springer LNCS 2380, 2002.]
A. Simpson and I showed that there is a Banach-Mazur computable $\mathbf{X} \to \mathbf{R}$ that is not Markov computable when $\mathbf{X}$ is any inhabited computable complete separable metric space computably without isolated points. [A. Bauer and A. Simpson: Two Constructive Embedding-Extension Theorems with Applications to Continuity Principles and to Banach-Mazur Computability, Mathematical Logic Quarterly, 50(4,5):351-369, 2004.]
What this says is that Banach-Mazur computability is too general because it admits functions that cannot be computed in the standard sense of the word, i.e., computed by Turing machine (in terms of codes).