No coinductive datatype of integers

An alternative phrasing:

In the Atlas Mountains, one can meet two species of Sphinxes: True Sphinxes and Hollow Sphinxes. Each True Sphinx has a secret number, and it will truthfully answer any question about it, provided it can do so in less than a hundred words. A Hollow Sphinx, however, just enjoys wasting people's time : it has no secret number but will pretend it does, and answers questions so as to never contradict itself and maintain uncertainty in the asker's mind.

While you can be sure you are speaking to a True Sphinx (for example, by guessing it's number), you can never be sure that you are speaking to a Hollow Sphinx - it might be a True Sphinx whose number is very large. In fact, no-one has been able to determine whether any Hollow Sphinxes still exist.

This phenomenon is noted in any handling of information theory that discusses "stream arithmetic coding". Those codes can be interpreted as a fraction written in binary, where each bit narrows down a region of the [0,1) numberline, with earlier-terminating bitstreams reserved for more likely source strings.

Any probability distribution on integers has a corresponding (optimal) arithmetic stream coder, and you can always make it indefinitely expect more input by feeding it the bit that corresponds to the least likely next character (which means it's not finished decompressing).

The human David MacKay discusses such encodings and their implicit unbounded length potential in Chapter 6 of his/her book which can be accessed without spending USD or violating intellectual property rights.

You're allowed to invent an arbitrary scheme for encoding integers as strings of bits. Whatever encoding you invent, I can give you an infinite input stream of bits that makes your decoder hang and never give a definite answer like "yes, this is an integer with such-and-such value" or "no, this isn't a valid encoding of any integer".

I find it annoying how my brain keeps saying "hah, I bet I could" even though I explained to it that it's mathematically provable that such an input always exists. It still keeps coming up with "how about this clever encoding?, blablabla" ... I guess that's how you get cranks.

Agree about the theorem. Not sure about the implication for explaining integers, since a human who has been assigned the task of decoding the string should have the same difficulty with that infinite input stream. His understanding of what an integer is doesn't protect him. What seems to me to protect the human from being mentally trapped by an endless input is that his tolerance for the task is finite and eventually he'll quit. If that's all it is, then what you need to teach the computer is impatience.

OK, here's my encoding (thanks Misha):

N is encoded by N triplets of bits of the form 1??, followed by a zero.

Each triplet is of the form (1, a(N, k), b(N, k)) (with 1 <= k <= N), where

• a(N, k) means "Turing machine number k halts in N steps or less, and it's final state has an even number of ones on the tape", and

• b(N, k) means "Turing machine number k halts in N steps or less, and it's final state has an odd number of ones on the tape".

By "Turing machine number k" I mean we have an infinite list containing all possible Turing machines, sorted by description length.

So to encode N, the encoder "just" simulates the N first turing machines for N steps, and notes which of them stops.

The decoder reads his input triplet-by-triplet. When reading input k, it simulates the k first Turing machines for k steps, and checks whether the results are consistent with all that it has read in the input so far : if one of the simulated machines halts in a way not announced in the input (or if a triplet is impossible like "111"), it stops reading.

While an "infinitely confusing" input stream does exist, generating it requires solving the halting problem, which is generally considered pretty hard.

The proof is obvious. (If it isn't obvious to you, work it out!)

I deem this obnoxious.

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.

Nice problem! I think this is a proof, but I don't know if it's your proof:

Vs K unf vasvavgryl znal inyvq fhssvkrf, ng yrnfg bar bs K0 be K1 zhfg unir vasvavgryl znal inyvq fhssvkrf. Fb yrg k_{x+1} = 0 vs k_1 ... k_x 0 unf vasvavgryl znal inyvq fhssvkrf, naq 1 bgurejvfr; gura k_1 gb k_x unf vasvavgryl znal inyvq fhssvkrf sbe nal x.

This seems like a decent place to ask: I'm slowly trying to learn Type Theory. I haven't seen a place where (Co)Inductive datatypes (as in the Calculus of (Co)Inductive Constructions) are explained formally (though preferably for novice readers); does anyone have a a suggestion?

After learning a bit more about inductive and coinductive types from Robert Harper's book in progress(which I found more lucid on the topic than Types and Programming Languages), I don't quite understand why it's important for the datatype to be coinductive. You can clearly encode the integers as inductive types, why doesn't that suffice for 'explaining to a computer what a "terminating computation" is'? Are computers 'naturally coinductive' in some sense?

To clarify, let's work through an example. Consider an unary encoding: 0 is 0, 1 is 10, 2 is 110, 3 is 1110, etc. In this case, if we feed the decoder an infinite sequence of 1's, it will remain forever undecided as to the integer's value. The result says we can find such pathological inputs for any other encoding system, not just unary.

I'm not sure this is particularly significant. If you haven't finished feeding in the input you can hardly expect the machine to give a complete output unless you have given a specific specification as to how to simplify or truncate. I perhaps would avoid saying that the decoder 'hung'. 'Hung' implies some sort of pathological error in the decoder, not just a decoder that is processing new input as fast as is possible in exactly the way it is supposed to.

That said, many things that seem bloody obvious and trivial are considered to be important mathematical principles once phrased in maths language. Maybe what you are describing is significant. It does seem like the sort of thing that usually gets a mathsy name. "Infinite Garbage In, Garbage Out" may not cut it. :)

Encoding is not definition. While it is true that we cannot decide the integer value of "1111..." as you describe, the reason behind it is obvious: you are trying to use an inductive algorithm on a co-inductive data structure.

Clearly, your proposed bits-to-ints encoding scheme is isomorphic to lists of unit, and it so happens that there is a one-to-one mapping between list-of-unit and inductively defined natural numbers, exactly so long as the lists in question are inductive and thefore finite. This isomorphism is made up of length :: list unit -> int and repeat unit :: int -> list unit, according to their usual definition. Proof of that this is isomorphic is left as an exercise to the reader.

Have you considered posting your observation/question to cstheory.stackexchange.com? I'd be interested in seeing the response there.

Curiously, if you replace "finite" with "countable" and "infinite" with "uncountable" then it is possible to devise such an encoding scheme. (This is connected with the existence of "Aronszajn trees".)

Suppose we have a countable alphabet of symbols A, and we want to encode countable ordinals using functions alpha -> A for countable ordinals alpha, then there exists an encoding scheme such that, after only countably many symbols have been received, you can either say "yes, this represents the countable ordinal x" or "no, this isn't a valid encoding".

(Consider the set of all increasing functions from alpha into the rationals, where alpha is a finite or countable ordinal.)

I'm pretty sure information theory books mention this phenomenon (though not explicitly as a theorem) in discussions of stream arithmetic coding. Those can be interpreted as a fraction written in binary, where each bit narrows down a region of the [0,1) numberline, with earlier-terminating bitstreams reserved for more likely source strings.

Any probability distribution on integers has a corresponding (optimal) arithmetic stream coder and you can always make it indefinitely expect more input by feeding it the bit that corresponds to the least likely next character (which means it's not finished decompressing).

MacKay discusses this in Chapter 6 of his free book.

As for your problem, Robert Harper (posts as 'Abstract Type') frequently notes that you cannot define the natural numbers or any inductive type in haskell because it is lazy so bottom (non-termination) is a member of all types and therefore requires coinductive types (for example see also the reddit discussion).

Whatever encoding you invent, I can give you an infinite input stream of bits that makes your decoder hang and never give a definite answer like "yes, this is an integer with such-and-such value" or "no, this isn't a valid encoding of any integer".

What if my encoding is: return TRUE(=is an integer) for all inputs?

That's not such a dumb thing to do. In fact, any encoding that didn't assign some integer outcome to any sequence of bits would be trivially suboptimal.

How would an infinite stream of bits possibly encode an integer in the first place? All integers are finite, so unless you did something stupid like assign the infinite sequence 11111111... to the integer 37, an infinite number of bits should never correspond to any integer.

Isn't this what Godel said?