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

Comment author: [deleted] 04 May 2011 07:01:25PM 4 points [-]

Here is a related well-known idea: in nonstandard analysis, a subset B of the real numbers is infinite if and only if its extension B* contains nonstandard numbers.

It might be equivalent, actually. Think of infinite bit streams as hyperintegers (e.g. the infinite sequence of 1s is the hyperinteger (1, 11, 111, 1111...), in binary if you like). Let E be the set of encodings of all integers, and all their prefixes. E is infinite, so E* contains a nonstandard element. I believe (here is where my nonstandard analysis fails me) that such a nonstandard element gives us an infinite bit stream which can't be rejected by the decoder.

A less serious but also related idea is the Frivolous Theorem of Arithmetic, which states that almost all positive integers are really, really, really, really large.