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.
BusyBeaver(BusyBeaver(BusyBeaver(BusyBeaver(3^^^3))))
This is the moral equivalent of saying BB(3^^^3)+1. Mere recursion is puny. At least jump from BB to BB_2!
determining say it's first 100 bits is uncomputable
Every sequence of 100 bits is computable.
Here's an encoding where the "infinitely confusing" input is uncomputable: take the unary encoding from my post and XOR it with some infinite uncomputable sequence, e.g. the halting oracle sequence. Unfortunately, you can't use this test in practice because you can't compute the required bits either.
<Can someone recall the title of Eliezer's parable in which the genius level humans spend thousands of years deciphering the messages sent by the not-so-smart universe simulators?>
You may be thinking of "That Alien Message." Best wishes, the Less Wrong Reference Desk.
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 poss...
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 g...
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...
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 -...
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 countab...
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 ch...
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.
I guess my objection is that your task is too obviously impossible. If I tell you that I can color any page in any coloring book, and you give me an infinite coloring book, I won't be able to finish, even though I know how to color. Similarly, if we have a decoder that can interpret infinitely many finite bit strings, it can be stumped by an infinite one, by virtue of its being infinite.
This reduces the problem of explaining "standard integers" to the problem of explaining "subsets", which is not easier. I don't think there's any good first-order explanation of what a "subset" is. For example, your definition fails to capture "finiteness" in some weird models of ZFC. More generally, I think "subsets" are a much more subtle concept than "standard integers". For example, a human can hold the position that all statements in the arithmetical hierarchy have well-defined (though unknown) truth values over the "standard integers", and at the same time think that the continuum hypothesis is "neither true nor false" because it quantifies over all subsets of the same integers. (Scott Aaronson defends something like this position here.)
I don't think there's any good first-order explanation of what a "subset" is.
Well, ZFC is a first-order theory...
Followup to: What's a "natural number"?
While thinking about how to make machines understand the concept of "integers", I accidentally derived a tiny little math result that I haven't seen before. Not sure if it'll be helpful to anyone, but here goes:
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 will make 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".
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.
The proof is obvious. (If it isn't obvious to you, work it out!) But it seems to strike at the heart of the issue why we can't naively explain to computers what a "standard integer" is, what a "terminating computation" is, etc. Namely, if you try to define an integer as some observable interface (get first bit, get last bit, get CRC, etc.), then you inevitably invite some "nonstandard integers" into your system.
This idea must be already well-known and have some standard name, any pointers would be welcome!