# Where can I find the proof of the theorem and what is the computational complexity of the computably isomorphic map?

"any two representations of reals which are acceptable are actually computably isomorphic",please see here for reference

where may proof of this theorem be found, and what is the the computational complexity of the computably isomorphic maps?

• Define "acceptable". Dec 11, 2014 at 3:11
• @TysonWilliams, see cstheory.stackexchange.com/questions/16512/… Dec 11, 2014 at 3:13
• Please make your question self contained. Dec 11, 2014 at 3:14
• In the referenced post, Andrej Bauer makes the parenthetical claim "(An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic.)" He never explicitly defines acceptable or cites the theorem. I assume the OPs question is really, What theorem is Andrej Bauer referring to? (An answer to this question would also answer @TysonWilliams question about what does "acceptable" mean.) Dec 11, 2014 at 14:26
• @TysonWilliams,"Which representations are appro- priate for doing real number computations? We show that with respect to computable equivalence there is one and only one equivalence class of representations of the real numbers which make the basic operations computable."cited from : onlinelibrary.wiley.com/doi/10.1002/malq.19990450202/abstract, this possibly is the definition of "acceptable" Dec 12, 2014 at 1:06

The first theorem of the form you are asking about was proved by Y. Moschovakis in Notation systems and recursive ordered fields, Compositio Mathematica 17:40–71 (1965). Then in the context of Type Two Effectivity a similar theorem was proved by P. Hertling, see A real number structure that is effectively categorical, Mathematical Logic Quarterly, 45(2):147–182 (1999). A generalization of these results (and several others) was proved by A. Bauer and J. Blanck in Canonical Effective Subalgebras of Classical Algebras as Constructive Metric Completions, Journal of Universal Computer Science, vol 16:2496–2522 (2010).

The paper I wrote with Jens is very general and maybe less accessible. Another good source to read about this is Peter Hertling's The Real Number Structure is Effectively Categorical.

I have nothing intelligent to say about computational complexity.

• I guess that the computational complexity would be $P− time$, without much reason, and the minimal length of the program is very short. Dec 12, 2014 at 1:48
• I am not sure. You could have a silly representation of reals. Pick an arbitrary computable subset $S \subseteq \mathbb{Q}$ of rationals. I could define that a real $x$ is encoded by a sequence $(q_n, b_n)_n$ where $(q_n)_n$ is a sequence of rationals which converge fast to $x$, and $b_n \in \{0,1\}$ is 1 iff $q_n \in S$. Now to convert from the usual representation of reals to this one, you need to calculate whether $q_n \in S$, and the complexity of that can be arbitrarily high. So I very much doubt you get just polytime. Dec 12, 2014 at 10:45

To turn my comment into an answer...

Andrej Bauer in this post makes the parenthetical claim

An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic.

He never explicitly defines acceptable or cites the theorem. I assume the OPs question is the following.

What theorem is Andrej Bauer referring to?

Here is a guess. It seems that earlier in the post, Andrej is implicitly suggesting that an acceptable representation of the reals is one in which the following properties hold:

1. One can effectively approximate a real by a rational to within a given precision.
2. Addition, multiplication, and inverse are computable.
3. The less-then relation, $<$, is semi-decidable.
4. There is a computable function which takes in a rapid sequence of reals (that is a sequence $(x_n)$ of reals such that $|x_n - x_m| \leq 2^{\min{n,m}}$ and outputs the limit.

Actually (1) and (4) are enough to prove (2) and (3), since to preform those operations: one only needs to approximate the real by a rational, do the operation, and convert back to a real. (Basic module of continuity will tell you how close the approximated answer is. Also, one needs to be able to convert from a rational to the corresponding real. This can be done by using (1) to find reals that are close enough to the rational, and then using (4) to take the limit of these approximations.)

Now, for any two representations satisfying (1) and (4) they are computably isomorphic. From (1), one can go from the first representation to the rapid Cauchy representation. (That is, represent a real as a rapid Cauchy sequence of rationals.) From (4), one can go the other way, taking a rapid Cauchy sequence of rationals and computing the real it converges to (using the second representation).

As for the question about complexity, I think it can't be anything better than just computable, but I realize I don't know for sure, mostly, because I don't know how to formulate the question formally.

• "Which representations are appropriate for doing real number computations? We show that with respect to computable equivalence there is one and only one equivalence class of representations of the real numbers which make the basic operations computable."cited from : onlinelibrary.wiley.com/doi/10.1002/malq.19990450202/abstract, this possibly is the definition of "acceptable" Dec 12, 2014 at 1:14