This situation crops up in total languages like Coq. For any iterative process, like the stepping of a Turing Machine, we can create an infinite stream of itera

This situation crops up in total languages like Coq. For any iterative process, like the stepping of a Turing Machine, we can create an infinite stream of iterations, eg. Cons (tape, head, state) (Cons (tape, head, state), (Cons ...))) But since our program is total, we can only extract the first N states, for some finite N. Compare this to a Turing Complete language like Haskell, where we can also define an infinite stream of iterations, but we can also traverse this stream indefinitely.