RichardKennaway comments on No coinductive datatype of integers - Less Wrong

4 Post author: cousin_it 04 May 2011 04:37PM

You are viewing a comment permalink. View the original post to see all comments and the full post content.

Comments (138)

You are viewing a single comment's thread. Show more comments above.

Comment author: RichardKennaway 04 May 2011 08:24:48PM *  4 points [-]

No, it's completely different. The representation of integers as bit strings doesn't even have to be computable. There will always be an infinite string of bits of which no prefix represents any integer. This can be derived from König's Lemma, which says that if a finitely branching tree has paths of all finite lengths, it has an infinite path. Consider the infinite binary tree with the out-edges of each node labelled 0 and 1. Chop off all the descendants of every node that represents an integer and consider the tree that remains. Since there are infinitely many integers, there must be such nodes of arbitrarily large depth. Therefore the tree contains an infinite path.