Do "seemingly impossible functional programs" work with arrow types interpreted as Turing machines?

Question

The title is a reference to this article by Martin Escardo, referring to work by originally by Ulrich Berger. It occurred that the programs described in this article can interpreted in the Turing machine model for higher order functions, where an element of type a -> b is encoded by a Turing machine takes encodings of elements of a and outputs encodings of elements of b. I'm wonder whether such programs are correct in this model.

More precisely, we say a natural number encodes a Cantor space element if it encodes a Turing machine which for any natural number input halts and returns a binary output (either 0 or 1). There's an equivalence relation $x \sim_C y$ iff $x$ and $y$ both encode Cantor space elements and the corresponding Turing machines return the same outputs for the same inputs.

Next, a natural number encodes a predicate on Cantor space if it encodes a Turing machine M such that

1. For any $x$ encoding a Turing machine element $M (x)$ halts and outputs a binary value.
2. For any $x, y$ with $x \sim_C y$ the outputs for $M (x), M (y)$ are the same.

Question: Consider the Haskell function forsome implemented in the link above, which depends on find_i (I'm not so interested in the more complicated versions of find described later in the article). Can this program be translated in a Turing maching which takes as input encodings of predicates $p$ on the Cantor, always halts for such inputs and outputs a binary value, and outputs $1$ iff there exists an encoding for a Cantor space element $x$ such that $p (x) = 1$?

I believe that translating the program into a Turing machine is (in principle) straightforward, and the question is whether this Turing machine has the desired behavior.

Side Question: Suppose the answer to the above question is yes. Does that imply that in the internal logic of the effective topos, the question of whether a decidable subset of the Cantor space is empty is itself decidable? I believe it does, but I'm not confident in my understanding of the semantics of the effective topos.

Answer 1

$\newcommand{\E}[1]{\mathtt{E}_{#1}}$

You are indeed using the model of computability that corresponds to the effective topos. It is also called hereditarily effective operators (HEO), Type I computability, and Russian constructivism. These things got invented several times.

Let us first recall a couple of definitions, and generally set things up in a reasonable way so that we do not have to fiddle with Turing machines. We work constructively, so that everything we say works in the effective topos, as well as in many other toposes (such as classical set theory).

For the purposes of this answer, say that a set $X$ is searchable if there exists a map $\E{X} : 2^X \to 2$, where $2 = \{0,1\}$ is the discrete two-point set, such that for all predicates $p : X \to 2$ $$\E{X}(p) = 1 \iff \exists x \in X \,.\, p(x) = 1.$$ We would like to know whether the Cantor space $\mathsf{C} = 2^\mathbb{N}$ is searchable in the effective topos.

We do not know how to directly construct the map $\E{\mathsf{C}}$, but we do know how to write it down as a relation, i.e., define $F \subseteq 2^\mathsf{C} \times 2$ by $$F(p, b) \iff ((\exists \alpha \in \mathsf{C} \,.\, p(\alpha) = 1) \iff b = 1).$$ This is a single-valued relation: for every $p \in 2^\mathsf{C}$ there is at most one $b \in 2$ such that $F(p, b)$. Therefore, a priori $F$ yields a partial map $E : 2^\mathsf{C} \rightharpoonup 2$, defined by, $$E(p) = b \iff F(p, b),$$ with the domain of definition $$D = \{ p \in 2^\mathsf{C} \mid \exists b \in 2 \,.\, F(p, b) \}.$$ The map $E$ is our candidate for $\E{\mathsf{C}}$, but we do not know whether its domain of definition $D$ is all of $2^\mathsf{C}$.

Recall that the Cantor space is a complete separable metric space, with the (ultra)metric defined by $$d(\alpha, \beta) = \lim_{k \to \infty} 2^{- \min \{i \leq k \mid i = k \lor \alpha_i \neq \beta_i\}}$$ The formula is written this way so that it works constructively (and therefore computably). We have $d(\alpha, \beta) = 2^{-i}$ if $i$ is the least index for which $\alpha_i \neq \beta_i$.

The domain $D$ is not small:

Proposition 1: $D$ contains the uniformly continuous predicates.

Proof. A uniformly continuous predicate $p : \mathsf{C} \to 2$ has a nice tree representation from which it is easy to calculate whether $p$ attains $1$. $\Box$

Proposition 1 explains that the Cantor space is searchable in toposes that validate the statement "every map $\mathsf{C} \to 2$ is uniformly continuous" (because then $2^\mathsf{C} \subseteq D \subseteq 2^\mathsf{C}$). An example is the Kleene-Vesley topos, also known as Type II computability and Brouwerian intuitionism.

However, in the effective topos things are strange. Recall that the Baire space $\mathsf{B} = \mathbb{N}^\mathbb{N}$ is also a complete separable metric space, with the metric defined by the same formula above as for the Cantor space. Many questions about Cantor space in the effective topos may be answered using the following theorem.

Theorem 2 (effective topos): The Cantor space and the Baire space are homeomorphic as complete metric spaces.

The proof relies on the existence of a Kleene tree. This is a strange theorem indeed, since classically the Cantor space is compact and the Baire space is locally non-compact (every open ball contains a sequence without an accumulation point).

Proposition 3: If $X$ is searchable and there is a surjection $s : X \to Y$ then $Y$ is searchable.

Proof. $\E{Y}(p) = \E{X}(p \circ s)$. $\Box$

Proposition 4: If $\mathbb{N}$ is searchable then LPO holds.

Proof. Exercise $\Box$.

Theorem 5 (effective topos): The Cantor space is not searchable.

Proof. Suppose we had $D = 2^\mathsf{C}$, so that $\mathsf{C}$ is searchable with $\E{\mathsf{C}} = E$. By Theorem 2 there is a surjection $\mathsf{C} \to \mathsf{B}$, therefore $\mathsf{B}$ is searchable. There is also a surjection $\mathsf{B} \to \mathbb{N}$, namely $\alpha \mapsto \alpha(0)$, hence $\mathbb{N}$ is searchable. By Proposition 4 LPO holds. But LPO is invalid in the effective topos, because it implies the existence of a Halting oracle. $\Box$

And lastly, let us explain why it is so easy to get confused about searchability of Cantor space. While we proved that in the effective topos $D$ is a proper subset of $2^\mathsf{C}$, the complement $2^\mathsf{C} \setminus D$ is always empty!

Proposition 6: $2^\mathsf{C} \setminus D = \emptyset$.

Proof. Notice that $$D = \{ p \in 2^\mathsf{C} \mid (\exists \alpha \in \mathsf{C} \,.\, p(\alpha) = 1) \lor (\forall \alpha \in \mathsf{C}\,.\, p(\alpha) = 0)\}.$$ Suppose we had $q \in 2^\mathsf{C} \setminus D$. Then it follows that $$\lnot ((\exists \alpha \in \mathsf{C} \,.\, q(\alpha) = 1) \lor (\forall \alpha \in \mathsf{C}\,.\, q(\alpha) = 0))$$ which is equivalent to $$(\forall \alpha \in \mathsf{C} \,.\, q(\alpha) = 0) \land \lnot (\forall \alpha \in \mathsf{C}\,.\, q(\alpha) = 0)$$ which is false. $\Box$

The conclusion is strange but not contradictory: we can never produce a concrete predicate $p \in 2^\mathsf{C}$ for which $E$ does not work, while on the other hand in the effective topos $E$ does not work correctly on all of $2^\mathsf{C}$. Translated to classical computability, the same conclusion is perhaps a little bit easier to swallow: every computable predicate on the computable Cantor space either attains $1$ or it does not, but there is no computable procedure for determining whether computable predicates on Cantor space attain $1$.

Answer 2

It helps to think topologically here. Any total Turing-computable function $2^{\omega} \rightarrow \{0,1\}$ is uniformly continuous. If an oracle Turing machine with oracle $x \in 2^{\omega}$ computing the predicate $P$ halts and outputs value 1, say, then some clopen neighborhood $U \supseteq x$ has $P(y) = 1$ for every $y \in U$ (this open neighborhood can be obtained from looking at the finitely bits of $x$ used in the computation). In this situation, $P^{-1}(0)$ and $P^{-1}(1)$ will turn out to both be clopen sets.

Asking whether some $x$ has $P(x) = 1$ is the same as asking whether $P^{-1}(0) \neq 2^{\omega}$, which is the same as asking whether $P^{-1}(1) \neq \emptyset$. We can "verify" with a finite witness that $P^{-1}(1) \neq \emptyset$ by finding a finite initial segment $\sigma$ such that our Turing machine with partial oracle $\sigma$ outputs 1. The tricky part is finding a way to "falsify" that $P^{-1}(1) \neq \emptyset$ with some kind of finite witness.

The idea here is to look at the tree of possible initial segments of elements of $2^{\omega}$, i.e. the tree of finite binary strings. Start coloring the nodes of this tree either red or blue, with $\sigma \in 2^{< \omega}$ colored red if the oracle Turing machine with partial oracle $\sigma$ halts in $|\sigma|$ steps and returns 1, and blue if it halts and returns 0, and uncolored otherwise. If it is not true that $P^{-1}(0) \neq 2^{\omega}$, i.e. if $P^{-1}(0) = 2^{\omega}$, then every branch through this tree (i.e., every element of Cantor space) passes through a blue node. This means the basic open sets $[\sigma] := \{x \in 2^{\omega} : \sigma \subseteq x\}$ for $\sigma$ a blue node cover $P^{-1}(0)$. But $P^{-1}(0)$ is compact, so some finite subcover suffices. So our "finite witness" to falisify $P^{-1}(0) \neq 2^{\omega}$ is just a finite set of nodes on this tree colored blue whose corresponding basic open sets cover $2^{\omega}$

Now to decide whether $P^{-1}(0) \neq 2^{\omega}$, simply search in parallel for a witness that $P^{-1}(0) \neq 2^{\omega}$, and for a witness that $P^{-1}(0) = 2^{\omega}$. We'll eventually find a witness to one or the other, and that's our answer.

Answer 3

Yes you can.
EDIT: That means find a computable program $H(e)$ taking an index $e$ for a predicate $P_e$ that returns $1$ (assuming $P_e$ satisfies above conditions) iff there is some code for an element of cantor satisfying $P_e$. Below I show you can't also require $H(e)$ to return $0$ if $P_e$ doesn't apply to any code for an element of cantor. Note that you can't just try $P_e$ on all indexes as we don't know how it behaves if fed an index that doesn't code for an element of cantor (given def above).

First, I note that it is sufficient to consider only those elements $k$ in the Cantor space such that $k(n)$ is $0$ for almost all $n$.

Suppose that a predicate $P_e$ on the cantor space is satisfied by some $i$ ($P_e(i)=1$). Let $f(j)$ be the computable function returning an index for a Turing machine such that $T_{f(j)}(n)$ behaves as follows: If $P_{e}(j)$ converges and outputs $1$ in less than $n$ stages then return $0$ otherwise return $T_i(n)$. Using the recursion theorem we can effectively find a value $j$ such that $T_{f(j)}$ is equivalent to $T_{j}$, i.e., $f(j) \sim j$. I claim that $P_e(j)=1$. If not then $T_{f(j)}$ agrees with $T_i$ everywhere and is total so $P_e(f(j))=1$ and thus $P_e(j) = 1$ as $f(j) \sim j$. But clearly $T_j$ is $0$ for almost all inputs establishing the claim.

So now we just need to write a program that searches through all codes for Cantor elements in this nice special form.

Given e coding a predicate $P_e$ on the Cantor space we implement forsome as follows where $c_d$ denotes a (effectively generated) code for the element of the Cantor space that begins with $d$ and is then $0$

At stage $s$ for every string of digits $d$ of length less than $s$ compute $P_e(c_d)$ for $s$ steps. If any of these computations halt and return $1$ then halt and return $1$. Otherwise proceed to stage $s+1$.

Clearly this program returns $1$ if $P_e$ evaluates to true for any element of the Cantor space that's almost always $0$ and by the result above this is equivalent to $P_e$ evaluating to true on a code for some element in the Cantor space.

EDIT: I should add that when we are restricting our attention to just these computable codes we can't guarantee that this function always terminates when there aren't any computable codes which satisfy $P_e$. Indeed, it's not possible to write such a function.

Suppose we have a computable function $H$ such that $H(e)=1$ if there is some computable code $c$ satisfying $P_e(c)$ and $H(e)=0$ otherwise. We now construct a relation $P_e$ which contradicts this assumption. It's easy to make sure that $H(e)$ doesn't converge the trick is to do it while ensuring that $P_e$ returns $0$ or $1$ for every cantor code.

Let $g$ be a computable function such that $g(e)$ gives an index for a Turing machine $P_{g(e)}$ which behaves as follows. $P_{g(e)}$ enumerates a set of axioms of the form $\sigma(k) = i$ in stages (described later).

At stage $s$ we first check if we've previously enumerated some axiom $\sigma(k) = i$ but $T_c(k)$ converges to $1-i$ in less than s steps and if so output $0$.

If not we check if $H(e)$ converges to $1$ in less than $s$ steps. If so $P_{g(e)}(c)$ outputs $0$. Since we've never returned the value $1$ on any input $P_{g(e)}$ satisfies the conditions for Predicate on Cantor.

On the other hand if $H(e)$ converges to $0$ in less than $s$ steps then we cease all enumeration of axioms. Now we run $T_c(k)$ for every $k$ we've enumerated an axiom for so for and if for every axiom $\sigma(k)=i$ we eventually see $T_c(k)=i$ we return $1$ and, as before, if for some axiom $\sigma(k)=i$ we see $T_c(k)=1-1$ we output $0$. Note that this returns a value for every $c$ coding an element of the Cantor set (we've only enumerated finitely many axioms) and since it only depends on the values $T_c$ takes on if $c \sim c'$ then $P_{g(e)}(c)=P_{g(e)}(c')$.

Finally, if none of the cases occur we look for new axioms to enumerate as follows. For each $k < s$ if $T_k(k)=i$ in less than $s$ steps output the axiom $\sigma(k)=1-i$. Now move to step $s+1$.

Again by the recursion theorem we let $e$ such that $P_e \sim P_{g(e)}$. Now suppose $H(e)=1$. Then by the above we have $P_e(c)=0$ for every $c$. Contradiction.

Suppose $H(e)=0$ then for some $s$ we see this computation after $s$ stages. Let $d$ be the bit string such that for all $k < s$ we have $d(k) = i$ if we enumerated the axiom $\sigma(k)=i$ by stage $s$. By construction $P_e(c_d)=1$ since $c_d$ agrees with every axiom enumerated by $P_{g(e)}$ before stage $s$. This contradicts the fact that $H(e)=0$.

Finally, we observe that if $H(e)$ doesn't converge then $P_e$ yields a valid predicate on codes for the Cantor space. In particular I claim that if $c$ is such a code then $P_e(c)=0$. To see this let $s > c$ large enough that $T_c(c)$ converges in less than $s$ steps and note that by stage $s$ $P_{g(e)}$ enumerates the axiom $\sigma(c)=1-T_c(c)$ and thus at stage $s+1$ $P_{g(e)}(c) = 0$. So $P_e$ is the empty predicate.

---

Note the proof above is essentially just a wrapper around the construction of a $\Pi^0_1$ class with an infinite path but no infinite computable path which we cut short if $H$ makes a decision about whether we are empty of not.

---

Note that the usual way to do this is to use oracle Turing machines which avoids much of the fuss like having to use the recursion theorem since we can just assume they don't consult the oracle beyond $s$ in the first $s$ stages.

That's actually what the code in the linked article is doing since when the Haskell code passes a function it is passing a black box and thus the predicates on the Cantor space only get access to a sequence of values and not the code which produces them. All the extra work here was to show that you can't do anything more just because you have access to the particular representation of a computable element of the Cantor space as your definition provides.