Stablishing termination of the construction of infinite stream with ranking functions

Question

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.

Answer 1

I think Turing's method is probably fine, but you are mistaken about why exactly the code you wrote, "terminates."

First, note that this is not really (written as) a function at all. It is a self-referential value. And the reason the program terminates even though it's defined in it is that the program does not attempt to evaluate it fully. In this case, perhaps it would be all right, because a sufficiently smart evaluator would notice that there is a loop in the pointer structure, but there are other examples where that would not be sufficient.

So, these infinite structures are not something that you prove 'terminate' by showing they can be labelled by some finite size. Instead, they are not evaluated at all until something else demands to see the structure, and then they are unfolded as needed. This sort of structure is sometimes called, "coinductive," whereas the Turing methodology you're talking about is related to induction.

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."

The reason we care about this property is that we assume the parts of the program that cause the unfolding of the infinite values can only demand finite portions of them. If you can only look at a finite portion of a potentially infinite value, and the pieces each take a finite amount of time to produce, the overall computation terminates.

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.