> This constructive notion of formal describability is less restrictive
> than the traditional notion of computability, mainly because we do not
> insist on the existence of a halting program that computes an upper
> bound of the convergence time of p's n-th output bit. Formal
> describability thus pushes constructivism to the extreme, barely
> avoiding the nonconstructivism embodied by even less restrictive
> concepts of describability.
It certainly tests the limits, since there's in principle no way of
knowing in general at any time whether a particular bit of the answer
on the tape is yet the "final answer".
I see how you could compute Omega: both create and run all Turing
machines in a diagonalized way, and each time one halts, increase the
approximation of the halting probability by the appropriate amount.
But you'd never be sure of even bits near the front, because some
running small machines might halt anytime, altering those early bits.
> ... Machines with real-valued registers ...
> This does not lead outside the GTM realm as long as the indefinitely
> growing register contents are finite for each finite time step.
Well, I was thinking they would have operations like reciprocal (or
maybe 1/(x+1) to limit the range) which could instantly generate
non-terminating expansions. More interestingly they might include
transcendental operations to generate non-repeating expansions.
Hey, they could even have the "Omega" operation, which loads
a register with Omega, all bits finalized.
That certainly beats GTMs.