# What is the “continuity” as a term in computable analysis? # Background

I once implemented a datatype representing arbitrary real numbers in Haskell. It labels every real numbers by having a Cauchy sequence converging to it. That will let $$\mathbb{R}$$ be in the usual topology. I also implemented addition, subtraction, multiplication, and division.

But my teacher said, "This doesn’t seem to be a good idea. Since comparison is undecidable here, this doesn’t look very practical. In particular, letting division by 0 to fall in an infinite loop doesn’t look good."

So I wanted my datatype to extend $$\mathbb{Q}$$. Since equality comparison of $$\mathbb{Q}$$ is decidable, $$\mathbb{Q}$$ is in discrete topology. That means a topology on $$\mathbb{R}$$ must be finer than the discrete topology on $$\mathbb{Q}$$.

But, I think I found that, even if I could implement such datatype, it will be impractical.

# Proof, step 1

Let $$\mathbb{R}$$ be finer than $$\mathbb{Q}$$ in discrete topology. Then $$\{0\}$$ is open in $$\mathbb{R}$$. Assume $$+ : \mathbb{R}^2 → \mathbb{R}$$ is continuous. Then $$\{(x,-x): x \in \mathbb{R}\}$$ is open in $$\mathbb{R}^2$$. Since $$\mathbb{R}^2$$ is in product topology, $$\{(x,-x)\}$$ is a basis element of $$\mathbb{R}^2$$ for every $$x \in \mathbb{R}$$. It follows that $$\{x\}$$ is a basis element of $$\mathbb{R}$$ for every $$x \in \mathbb{R}$$. That is, $$\mathbb{R}$$ is in discrete topology.

# Proof, step 2

Since $$\mathbb{R}$$ is in discrete topology, $$\mathbb{R}$$ is computably equality comparable. This is a contradiction, so $$+$$ is not continuous, and thus not computable.

# Question

What is bugging me is the bolded text. It is well-known that every computable function is continuous (Weihrauch 2000, p. 6). Though the analytic definition and the topological definition of continuity coincide in functions from and to Euclidean spaces, $$\mathbb{R}$$ above is not a Euclidean space. So I’m unsure whether my proof is correct. What is the definition of "continuity" in computable analysis? Posted on Categories proxies