# Stablishing termination of the construction of infinite stream with ranking functions

I'm working with Turing's paradigm to prove termination of programs by annotating functions with ranking functions and I encounter the following example:

def zeros: Stream[Int] = 0 #:: zeros


This is Scala syntax for contructing a stream made of an infinite number of zeros. In this case, the evaluation terminates but there is no (evident) measure that would prove it so?

Does this mean that the ranking functions paradigm is limited? Or is there a function stablishing termination of zeros?

• Turing, A. Checking a large routine. In Report of a Conference on High Speed Automatic Calculating Machines, 1949.

However, there is a property related to termination for coinductive things. For termination of inductive definitions, we label inputs with natural numbers (say), and ensure that this number decreases for recursive calls, which ensures termination. For coinductive definitions, we consider things like #:: to increase size, and we want to ensure that the size of the result is bigger than the size of any recursive references. This ensures that we are incrementally producing more of the value after a finite amount of work, and this is referred to as the definition being, "productive."
But, there is also a way to apply a more Turing-like methodology to this, and it is to recognize that streams could be implemented as functions. Stream[Int] is the same, in a way, as Natural => Int, where you ask for the value of the stream at a particular index, and it returns the value. And in this representation, productivity corresponds to the termination of the function for every natural number. In this case it's easy, because the function is x => 0, but other examples could require more sophisticated arguments.