It is easy to get confused about what it means to "represent" or "implement" a real number. In fact, we are witnessing a discussion in the comments where the representation is contentious. So let me address this first.
How do we know that an implementation is correct?
The theory which explains how to represent things in a computer is realizability. The basic idea is that, given a set $X$, we pick a datatype $\tau$ and to every $x \in X$ a set of values of type $\tau$ which realize it. We write $v \vdash x \in X$ when $v$ is a value that realizes $x$. For example (I shall use Haskell for no good reason), a sensible implementation of $\mathbb{N}$ might be the datatype Integer
where $v \vdash k \in \mathbb{N}$ when $v$ evaluates to the numeral $\overline{k}$ (thus in particular -42
does not represent a natural number, and neither does a diverging program). But some joker could walk by and suggest that we use Bool
to represent natural numbers with $\mathtt{True} \vdash 42 \in \mathbb{N}$ and $\mathtt{False} \vdash n \in \mathbb{N}$ for $n \neq 42$. Why is this incorrect? We need a criterion.
In the case of "joker numbers" the easy observation is that addition cannot be implemented. Suppose I tell you I have two numbers, both represented by $\mathtt{False}$. Can you give a realizer for their sum? Well, that depends on whether the sum is 42, but you cannot tell. Since addition is an "essential part of what natural numbers are", this is unacceptable. In other words, implementation is not about sets, but about structures, i.e., we have to represent sets in such a way that it is possible to also implement the relevant structure. Let me stress this:
We implement structures, not bare sets. Therefore, we have to be able to implement the entire structure, together with operations and all the axioms, in order for the implementation to be correct.
If you do not abide by this principle, then you have to suggest an alternative mathematical criterion of correctness. I do not know of one.
Example: representation of natural numbers
For natural numbers the relevant structure is described by Peano axioms, and the crucial axiom that has to be implemented is induction (but also $0$, successor, $+$ and $\times$). We can compute, using realizability, what the implementation of induction does. It turns out to be a map (where nat
is the yet unknown datatype which represents natural numbers)
induction : 'a -> (nat -> 'a -> 'a) -> 'nat -> 'a
satisfying induction x f zero = x
and induction x f (succ n) = f n (induction x f n)
. All this comes out of realizability. We have a criterion: an implementation of natural numbers is correct when it allows an implementation of Peano axioms. A similar result would be obtained if we used the characterization of numbers as the initial algebra for the functor $X \mapsto 1 + X$.
Correct implementation of real numbers
Let us turn attention to the real numbers and the question at hand. The first question to ask is "what is the relevant structure of the real numbers?" The answer is: Archimedean Cauchy complete ordered field. This is the established meaning of "real numbers". You do not get to change it, it has been fixed by others for you (in our case the alternative Dedekind reals turn out to be isomorphic to the Cauchy reals, which we are considering here.) You cannot take away any part of it, you are not allowed to say "I do not care about implementing addition", or "I do not care about the order". If you do that, you must not call it "real numbers", but something like "real numbers where we forget the linear order".
I am not going to go into all the details, but let me just explain how the various parts of the structure give various operations on reals:
- the Archimedean axiom is about computing rational approximations of reals
- the field structure gives the usual arithmetical operations
- the linear order gives us a semidecidable procedure for testing $x < y$
- the Cauchy completeness gives us a function
lim : (nat -> real) -> real
which takes a (representation of) rapid Cauchy sequence and returns its limit. (A sequence $(x_n)_n$ is rapid if $|x_n - x_m| \leq 2^{-\min(n,m)}$ for all $m, n$.)
What we do not get is a test function for equality. There is nothing in the axioms for reals which asks that $=$ be decidable. (In contrast, the Peano axioms imply that the natural numbers are decidable, and you can prove that by implementing eq : nat -> nat -> Bool
using only induction
as a fun exercise).
It is a fact that the usual decimal representation of reals that humanity uses is bad because with it we cannot even implement addition. Floating point with infinite mantissa fails as well (exercise: why?). What works, however is signed digit representation, i.e., one in which we allow negative digits as well as positive ones. Or we could use sequences of rationals which satisfy the rapid Cauchy test, as stated above.
The Tsuyoshi representation also implements something, but not $\mathbb{R}$
Let us consider the following representation of reals: a real $x$ is represented by a pair $(q,b)$ where $(q_n)_n$ is a rapid Cauchy sequence converging to $x$ and $b$ is a Boolean indicating whether $x$ is an integer. For this to be a representation of the reals, we would have to implement addition, but as it turns out we cannot compute the Boolean flags. So this is not a representation of the reals. But it still does represent something, namely the subset of the reals $\mathbb{Z} \cup (\mathbb{R} \setminus \mathbb{Z})$. Indeed, according to the realizability interpretation a union is implemented with a flag indicating which part of the union we are in. By the way, $\mathbb{Z} \cup (\mathbb{R} \setminus \mathbb{Z})$ is a not equal to $\mathbb{R}$, unless you believe in excluded middle, which cannot be implemented and is therefore quite irrelevant for this discussion. We are of forced by computers to do things intuitionistically.
We cannot test whether a real is an integer
Finally, let me answer the question that was asked. We now know that an acceptable representation of the reals is one by rapid Cauchy sequences of rationals. (An important theorem states that any two representations of reals which are acceptable are actually computably isomorphic.)
Theorem: Testing whether a real is an integer is not decidable.
Proof. Suppose we could test whether a real is an integer (of course, the real is realized by a rapid Cauchy sequence). The idea, which will allow you to prove a much more general theorem if you want, is to construct a rapid Cauchy sequence $(x_n)_n$ of non-integers which converges to an integer. This is easy, just take $x_n = 2^{-n}$. Next, solve the Halting problem as follows. Given a Turing machine $T$, define a new sequence $(y_n)_n$ by
$$y_n = \begin{cases}
x_n & \text{if $T$ has not stopped within $n$ steps}\\
x_m & \text{if $T$ stopped in step $m$ and $m \leq n$}
\end{cases}$$
That is, the new sequence looks like the sequence $(x_n)_n$ as long as $T$ runs, but then it gets "stuck" at $x_m$ if $T$ halts in step $m$. Very importantly, the new sequence is also a rapid Cauchy sequence (and we can prove this without knowing whether $T$ halts). Therefore, we can compute its limit $z = \lim_n y_n$, because our representation of reals is correct. Test whether $z$ is an integer. If it is, then it must be $0$ and this only happens if $T$ runs forever. Otherwise, $z$ is not an integer, so $T$ must have stopped. QED.
Exercise: adapt the above proof to show that we cannot test for rational numbers. Then adapt it to show we cannot test for anything non-trivial (this is a bit harder).
Sometimes people get confused about all this testing business. They think we have proved that we can never test whether a real is an integer. But surely, 42 is a real and we can tell whether it is an integer. In fact, any particular real we come up with, $\sin 11$, $88 \ln 89$, $e^{\pi \sqrt{163}}$, etc., we can perfectly well tell whether they are integers. Precisely, we can tell because we have extra information: these reals are not given to us as sequences, but rather as symbolic expressions from which we can compute the Tsuyoshi bit. As soon as the only information we have about the real is a sequence of rational approximations converging to it (and I do not mean a symbolic expression describing the sequence, but a black box which outputs the $n$-th term on input $n$) then we will be just as helpless as machines.
The moral of the story
It makes no sense to talk about implementation of a set unless we know what sort of operations we want to perform on it.