And then there are all the programs that aren’t designed to normally terminate, and then we should be thinking about codata and coinduction.
Which raises a question I have never considered …
Is there something similar to the halting-problem theorem for this kind of computation?
That is, can we classify programs as either productive or non-productive, and then prove the non-existence of a program that can classify?
That’s a great question. I haven’t found anything on a brief search, but it seems like we can fairly readily embed a normal program inside a coinductive-style one and have it be productive after the normal program terminates.
Which raises a question I have never considered …
Is there something similar to the halting-problem theorem for this kind of computation?
That is, can we classify programs as either productive or non-productive, and then prove the non-existence of a program that can classify?
That’s a great question. I haven’t found anything on a brief search, but it seems like we can fairly readily embed a normal program inside a coinductive-style one and have it be productive after the normal program terminates.