MathOverflow is a question and answer site for professional mathematicians. It only takes a minute to sign up.
Sign up to join this community
Let $f_{=}$ be a function from $\mathbb{R}^{2}$ be defined as follows: (1) if $x = y$ then $f_{=}(x,y) = 1$; (2) $f_{x,y} = 0$ otherwise.
I would like to have a proof for / a reference to a textbook proof of the following theorem (if it indeed is a theorem):
$f_{=}$ is uncomputable even if one restricts the domain of $f_{=}$ to a proper subset of $\mathbb{R}^{2}$, viz. the set of the computable real numbers
Thanks!
Suppose that $f_=$ is computable when restricted to computable real numbers, which means that there exists a Turing machine that, given as input the encoding of two Turing machines $M_1$ and $M_2$ that compute the fractional digits of two computable real numbers $r_1$ and $r_2$ in $[0,1]$, produces $1$ if $r_1 = r_2$ and $0$ otherwise. I will use this assumption to show that the Halting problem is also computable, which is impossible.
Given a Turing machine $M$ and an input $x$ for which we want to know if $M$ on input $x$ halts or not, let $M_x$ be the Turing machine that acts as follows: given an integer $i$ as input, $M_x$ starts a simulation of $M$ on input $x$ for up to $i$ steps, and if the simulation does not halt within that number of steps, it outputs $0$ and otherwise it outputs $1$. By definition, $M_x$ computes the digits of a computable real number (more precisely, it computes the $i$-th digit for every given $i$). Moreover, that real number is $0$ if $M$ on input $x$ does not halt, and the real number $0.0\cdots 011 \cdots = 2^{-k}$ otherwise for some $k \geq 1$. In other words, $M_x$ computes the real number $0$ if and only if $M$ on input $x$ does not halt. To complete the argument, note that $0$ is a computable real number, so if you could tell whether two computable real numbers are equal you would also be able to tell if $M$ on input $x$ halts or not.
The main difficulty in finding a reference for this is that it's so well known :). The fact that equality of reals is only (negatively) semidecidable is a basic and important result in both computable analysis and constructive analysis.
The underlying phenomenon here is about continuity. As Gerald Edgar says, the equality function is not continuous (in particular, it's not sequentially continuous). The proof that slimton presents shows not only that it's discontinuous, but that it's effectively discontinuous: we can make an effective sequence of effective reals that witnesses the discontinuity.
This is closely related to the type-2 functional $E\colon \{0,1\}^\omega \to \{0,1\}$ defined such that $E(f) = 1 \leftrightarrow (\exists k)(f(k) = 1)$. This functional is not computable.
If you look more deeply at slimton's proof, you see that he actually proves that if you had a uniform way to test equality of reals, then you would have a uniform way to compute $E$. In particular the problem of computing equality of computable reals is no easier than that of computing $E$ on computable reals. It can be shown with only a little more work that these are equivalent problems.
This phenomenon is a particular instance of a general phenomenon first studied by Grilliot [1] and now called Grilliot's trick: a functional $\Phi$ is effectively discontinuous if and only if $E$ is computable from $\Phi$. In particular, no effectively discontinuous functional is computable.
1: Thomas J. Grilliot, "On Effectively Discontinuous Type-2 Objects", Journal of Symbolic Logic v. 36, n. 2 (Jun., 1971), pp. 245-248. http://www.jstor.org/stable/2270259
Aren't computable functions of reals automatically continuous? And isn't your function discontinuous? Of course you need a definition of computable in this setting to make sense of this...
It is entirely reasonable to ask for a continuous and computable equality-test function on~$\mathbb R$. The unreasonable thing is to expect it to take values in the discrete two-element space $\mathbf 2$.
The truth-value space that we need to use is the Sierpinski space, for which I write $\Sigma$. It has (in the classical interpretation) two elements,
This space has the property that there is a three-way bijection amongst
This is like the subobject classifier $\Omega$ in a topos, where "open subspace" becomes "subobject". Indeed, both in set theory and topology the classification properties are rather trivial in the classical case, but become powerful definitions when read constructively.
In particular, a space $X$ is Hausdorff iff the diagonal $X\subset X\times X$ is closed. This happens iff there is a continuous function $$ (\neq):X\times X\to\Sigma $$ for which $$ (\neq)(x,y) = \bot \iff x=y. $$
In the discrete space $\mathbf 2$ both points are both open and closed and there is a negation function $\lnot:\mathbf 2\to\mathbf 2$ that swaps them.
All of this is meaningful in both general topology and recursion theory, replacing - continuous function by computable function and - open subspace by recursively enumerable subspace.
In particular, a computable function $f:X\to\Sigma$ is one that may or may not terminate but otherwise has no return value, so it is like $\mathtt{void}$ in $C$ or $\mathtt{unit}$ in ML. Then $\top$ denotes termination and $\bot$ divergence.
There is no negation function on this $\Sigma$ because if there were it would be exactly a solution of the Halting Problem.
In particular, slimton is right in saying that a positive solution to the question as originally posed would be equivalent to the Halting Problem.
The interpretation of computation in general topology was pioneered by Dana Scott in the 1970s. Conversely, my research programme Abstract Stone Duality is about reformulating topology to make it equivalent to computation.
The best introduction to this programme for the general mathematician is my paper A Lambda Calculus for Real Analysis.
Dan Richardson in Bath has extensively studied the problem of recognizing zero under various hypotheses. I would be hard-pressed to give you an account of the details, because there is a lot of subtle and surprising results, but his page has all his papers and I'm sure you can find something of interest there.
