Yesterday I found out about a remarkable algorithm which can take any total predicate (function returing true or false) on infinite sequences of bits and find an infinite sequence which satisfies it (and implemented it). It’s a counterintuitive result, since you’d think that you can’t search the (uncountably) infinite space of bit sequences in a finite amount of time, but you can.
This implies some results about how much total functions can encode. For example, there must not be any total function from infinite sequences of bits onto the integers (such that any integer is reachable using a suitable infinite sequence). If there were, you could use this algorithm to decide any predicate on the integers, which would be a far-too-powerful mathematical tool.
But I couldn’t prove it, not without citing the algorithm. Why must there not be any such function, besides that it would make the algorithm incredibly powerful (so powerful that you could prove its impossibility, but that proof method was not good enough for me, because it could have been that the algorithm had an error).
The proof was actually hiding in the proof on sigfpe’s blog, but I couldn’t see it at first. So I’ll give a more explicit version here.
Let f be a total function from sequences of bits onto the integers (f : (Z -> Bool) -> Z). Let df(xs) denote the greatest index that f reads when given the argument xs. Now, for example, choose an xs such that f(xs) is 0. df(xs) is the greatest index that f reads, so f doesn’t depend on anything greater (for this argument), so every sequence with the prefix xs[0..df(xs)] has the value zero.
Now make a binary tree corresponding to the input sequence, where a node is a leaf iff the sequence leading to the node is the shortest prefix that completely determines f‘s output. Every possible extension of the sequence leading up to the leaf maps to the same value, so we informally say that the leaf itself maps to the value (even though the leaf represents a finite sequence and f takes infinite sequences).
This tree has infinitely many leaves, since there must be (at least) one leaf for each integer. And now, just as sigfpe did, invoke the König lemma, “every finitely branching tree with infinitely many nodes has at least one infinite path”. That infinite path represents an input to f for which it will not halt. That is to say, f was not total after all!