Is it true that there is no algorithm to approximate the least upper bound?

Question

I just read the following text below from Bishop's Foundations of Contructive Analysis, is it true that there is no such algorithm? The book is from 1967 - I don't know if someone managed to invent such algorithm until the present date.

Answer 1

It's not entirely clear to me which format the inputs and outputs to $M$ would be, but suppose it's something like

Input: A description of a Turing machine $T$ that computes the sequence $x_k$ given $k$ as an input, together with a rational $q>0$, and (just to be generous) a formal proof that the $T$ actually produces a strictly increasing bounded sequence.

Output: A rational number that is within $q$ of the supremum of the $x_k$s.

(Actually, reading the quote closer it seems like $M$ does this in two stages, first producing from $T$ a new Turing machine which again produces a stream of approximations. Never mind that, it doesn't change the argument).

In that case it is much worse than "nobody expects that one will ever be found" -- it is impossible for such an $M$ to exist, because if it did we could use it to decide the halting problem. To wit, suppose we want to know whether the Turing machine $U$ halts. Then construct the machine $T$ to compute the following sequence: $$ x_n = \begin{cases} 2-1/n & \text{if $U$ halts in fewer than $n$ steps} \\ 1-1/n & \text{otherwise} \end{cases}$$

Then $\sup x_n$ is $2$ if $U$ ever halts and $1$ otherwise (and it is trivial to supply proof that $x_n$ are strictly increasing and bounded by $2$), so if we ask $M$ to approximate $\sup x_n$ to within a tolerance $1/3$ it would implicitly tell us whether $U$ halts or not. And that is not possible, so $M$ can't exist.

---

(Note that it is essentially futile to want to remedy this by restricting the form in which $\{x_n\}$ is given as input to $M$, because the $\{x_n\}$ in this argument is extremely computable -- the sequences of its numerators and denominators are primitive recursive functions of $n$, and we certainly have to accept such specifications in anything that purports to handle general "constructively given" sequences of rationals.)