= 27d567bc2d48d9f40e9ccc20ea370b15)
Perplexed comments on The Curve of Capability - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (264)
It's true that the result is "there exists programs such that", and it says nothing about the relative sizes of those that can be proved to terminate vs those that can't in the subset we care about and are likely to write.
Sometimes that purpose is to test mathematical conjectures. In that case, the straightforward and clear way to write the program actually is the one used, and is often apparently does fall into this subclass.
(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.