# Is there a formal way of defining a Zeno Machine?

The idea of a Zeno machine is pretty interesting to me, but I can't seem to find a formal definition for how a Zeno machine would work. I can find a couple of definitions around but they are all about the same (I suspect that everyone is cribbing off of each other) and lack any real formalism. A fairly representative definition is this one from the relevant wikipedium

More formally, a Zeno machine is a Turing machine that takes $$2^{-n}$$ units of time to perform its $$n$$-th step; thus, the first step takes $$0.5$$ units of time, the second takes $$0.25$$, the third $$0.125$$ and so on, so that after one unit of time, a countably infinite (i.e. $$\aleph_0$$) number of steps will have been performed.

This definitions is a little weird.

The biggest reason this definition is lacking is that the description doesn't really tell us anything about the state of the machine at any time $$t \geq 1$$.

Now if we look at an example of some psuedo-code for an accelerated Turing machine we have a bit of a conflict. Here is a sample slightly modified from C. Calude, L. Staiger. A Note On Accelerated Turing Machines

begin program
write 0 on the first position of the output tape
set i = 1
begin loop
simulate the first i steps of T on w
if T(w) has halted,
then
write 1 on the first position of the output tape
set i = i + 1
end loop
end program


Now this sample is intended to solve the halting problem on a Turing Machine. And according to the authors:

By inspecting the first position of the output tape we need one unit of time to run the above machine in order to decide whether $$T(w)$$ stops or not

Now here we are relying on some notion of the state of the machine at time $$t=1$$, which is out of the scope of our definition.

Now the intuitive patch here is to say that the state at time $$t=1$$ is just the limit of the states as time approaches $$1$$.[1] But there are some problems with this the most important being that not all sequences will converge. Take for example the following pseudo-code:

begin program
set i = 1
begin loop
write i on the first position of the output tape
if i is 1,
then
set i = 0
else
set i = 1
end loop
end program


The sequence of states here cannot converge (regardless of how we choose our metric) and thus this naïve patch does not completely fix the problem.

Is there a way of defining a Zeno machine that is formal and complete?

[1] : In fact while I was putting this question together I found this paper which pretty much outright states this definition.