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

Question

"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?

Answer 1

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.

Answer 2

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.