Gah, that's what happens when I try to re-derive half-remembered proofs late at night :( Thanks for the clarifications. > That would be O(4^N) time, which is c

Gah, that's what happens when I try to re-derive half-remembered proofs late at night :( Thanks for the clarifications. > That would be O(4^N) time, which is certainly not O(2^N) Oops, I wanted it in twos and misplaced my parentheses. Should have been 4^N = (2×2)^N, but I mistakenly did 4^N = 2×(2^N), then simplified to 2^(N+1) ~= 2^N, which is nonsense. > But in fact each iteration does NOT take 4x as long. > Thanks to the prefix-free property, each iteration only takes twice as long. Yes, I knew being prefix-free meant the time fractions sum to one; but I wasn't sure what the total slowdown was (or rather, I was sure it was O(2^N), but got myself in a muddle trying to get there!). I like to think of the programs as being leaves of a tree, and their prefix-free encoding is the path from the root. We allocate 100% of the time to the root (whose path is the empty string), and nodes divide their allocated time uniformly between their sub-trees. The time allocated to a leaf tells us how long to run its corresponding program. That way, each iteration of the algorithm just doubles the number of steps allocated to the root, which "trickle down" the tree. We run all of the programs which get allocated at least one step (i.e. we don't follow subtrees which get 1/2 a step). It's probably worth pointing out that this scheme is a general search algorithm, which isn't specific to programs (it's like a fancier alternative to grid search). For example, if we have a long-running algorithm like a theorem prover, but we're unsure what inputs to give it, we can explore all the different input combinations by arranging them in a tree and using Levin Search, running the prover for longer and longer on more and more complicated inputs until it finds our desired output (e.g. a proof/disproof of a specified conjecture). Of course, as soon as we start to look at theorem proving, we soon stumble upon Hutter search, AKA "the fastest and shortest algorithm for all well-defined problems" ;) Lots of great links at http://www.scholarpedia.org/article/Universal_search http://www.scholarpedia.org/article/Universal_search