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.
Hamkins' survey Infinite time Turing machines, linked by Yuval Filmus, formally defines a computational model (Infinite time Turing machine) that meets the requirements of a Zeno machine.
The definition of ITTMs does not use the time based framing; instead it is an extension of classical binary TMs to be defined at transfinite ordinals.  A classical TM has a start status (empty tape, etc.) and a function to get the successive status; a ITTM just adds the status of the machine at limit ordinals.
Rather than taking the limit of the cells in the tape, as suggested and refuted in the question, we take the limit supremum.  Formally for
$$
T(\lambda)_k = \limsup_{n\rightarrow \lambda} T(n)_k
$$
where $\lambda$ is a limit ordinal, $k$ is the index of some cell, and $T$ is the function that gives the tape at some numbered step.
The $\limsup$ ensures that it will always be defined for any sequence (since the alphabet is bounded).  If the normal limit does not converge for some cell then (for a binary alphabet) the cell at time $\lambda$ will be $1$, since in order for it to not converge it must be $1$ at an infinite number of steps.
The state and the location of the read head are resolved much more simply.  Just as there is a start state, there is also a limit state.  At times corresponding to limit ordinals the machine is in the limit state, and the read head is set to the beginning of the tape.

The linked paper does not even mention &quot;Zeno machine&quot; (although it mentions Zeno) and ITTMs may not be the only formal model of a Zeno machine possible (beyond trivial modifications).  However it is a model of computation that allows a Turing machine to perform an infinite number of operations and then continue calculations, so if you are looking for a formal way to talk about Zeno Machines ITTMs work just fine.