{\huge The Busy Beaver Problem}
Can the impossible become practical?
Tibor Radó was a mathematician who was the PhD advisor to a number of computer scientists. They include Shen Lin, Paul Young, and several others. All were his students while he was at Ohio State University. He is not the Rado of the Erd\Hs-Ko-Rado theorem}---that is Richard Rado, without an accent. Tibor Radó had an Erd\H{o}s Number of 3, through Lin and then Ron Graham.
Today we want to continue to talk about the famous ``Busy Beaver'' problem that we mentioned in our discussion on the Microsoft SVC lab closing.
The problem is actually quite neat, is still be studied after more than fifty years since Radó created it, and has interesting links to industrial labs. It, the busy beaver problem, is actually an important and cool problem. For starters we note that Radó's paper was published in the Bell System Technical Journal in 1962: On non-computable functions.
The Problem
The problem, which Radó called a game, is quite simple: Consider a Turing Machine with one tape two-way infinite tape, a finite deterministic state control of $latex {n}&fg=000000$ states, and alphabet $latex {\{0,1\}}&fg=000000$. There is no separate ``blank'' character---the tape initially holds all $latex {0}&fg=000000$'s (or $latex {0}&fg=000000$ is regarded as the blank). How long can the machine run? We do not allow machines to run forever, we insist that our machines halt. The question is. can such a simple device run for a long time and still stop?
Clearly with enough states the machine could compute $latex {f(m)}&fg=000000$ for some very fast growing function $latex {f}&fg=000000$ and a modest $latex {m}&fg=000000$ and then halt. This could easily take a huge amount of time. The reason the problem is interesting is that the number of states $latex {n}&fg=000000$ is quite small. So the ``game'' is to try and use very few states to encode some long running computation. This is not easy to do even for $latex {n}&fg=000000$ tiny, which is why the busy beaver problem is still interesting even today.
The function $latex {S(n)}&fg=000000$ is the number of steps that such a machine can take with $latex {n}&fg=000000$ finite control states and still halt. This is still known exactly only for $latex {n<5}&fg=000000$. The current $latex {5}&fg=000000$-state lower bound is
$latex \displaystyle S(5) \ge 47,176,870. &fg=000000$
This was discovered by Heiner Marxen and Jürgen Buntrock in 1989. The busy-beaver function $latex {B(n)}&fg=000000$ itself is reckoned as the number of $latex {1}&fg=000000$'s on the tape at the time of halting; the same machine gives $latex {B(5) \geq 4,098}&fg=000000$. There are still about 40 five-state programs whose status is unresolved. The number of different programs to consider grows hugely with $latex {n}&fg=000000$, but still it is surprising that small programs can run for so long.
A Six---or Three---State Beaver
What we find even more amazing is that some of the busiest machines can be described in a way that they seem to have only a few states. Let's describe one using an eco-friendly beaver who plants trees as well as chops them down. We figure the trees grow quickly in beaver-time to give shade, and we give our beaver some traits of a groundhog. He starts on a ridge that has been completely deforested, bare to his right and left as far as an eagle can see.
At any time, including the start, our beaver can decide to Plant Two Trees. This means finding the first bare spot at or rightward of his position and planting a tree there. If he can then plant in the spot immediately to its right, then he does so but stays under the first tree he planted, else he finds the first bare spot to his left, plants there, and steps left. Either way, he then pauses to Take Stock. Thus our beaver's first action is to plant two adjacent trees and Take Stock under the first, with the second to his right.
\includegraphics[width=1in]{BeaverPlantingTree.png}
In the Take Stock state, our beaver looks at the spots left and right, and acts according to these four rules:
When Looking For His Shadow, if he sees it, he gets frightened and halts by planting a tree and burrowing under it. Else, he steps left again. Then if in sun he steps left to Plant Two Trees, while if under a tree he chops it down, moves left yet again, and Takes Stock.
That's it. The second rule ends up the same way as the first rule, while in the third rule, the ``goes back'' part is unnecessary to say. Returning to our beaver taking stock for the first time, he is in shade with no tree on his left, and so he immediately plants one tree there and two more on the far right, making $latex {5}&fg=000000$ trees in all. He is under the $latex {4^{th}}&fg=000000$ tree, chops down the $latex {3^{rd}}&fg=000000$ (middle) tree, and next looks for his shadow when under the $latex {2^{nd}}&fg=000000$ tree.
\includegraphics[width=3.4in]{BeaverTrees.png}
Of course he doesn't see it, so he goes on beavering---until he has 95,524,079 trees in all, after over 8.69 trillion steps.
These rules can be coded by six Turing machine states, using two to plant trees, three to take stock, and one to check the shadow plus re-using one of the take-stock states. The take-stock state is reminiscent of a simple one-dimensional cellular automaton that depends only on its one-cell environment, but the planting step is decidedly non-local. This machine was discovered by Marxen and can be viewed in notes by Jeffrey Shallit. It is far from the record, however. The current busiest 6-state beaver, found by Pavel Kropitz and verified, is known to leave somewhat more than $latex {3.5 \times 10^{18267}}&fg=000000$ trees in over $latex {7.4 \times 10^{36534}}&fg=000000$ steps total.
The Current Approach
How do people prove such gargantuan bounds on $latex {S(n)}&fg=000000$? For starters one can try to create clever programs that take a long time. This will of course only yield lower bounds, but these are still quite interesting. For higher $latex {n}&fg=000000$ some machines have been constructed for which $latex {S(n)}&fg=000000$ cannot conveniently be expressed by conventional exponential notation, but requires something like Donald Knuth's arrow notation to estimate.
For upper bounds, this strategy must incorporate ``determining'' that certain machines will never halt, as well as those that halt. To quote from Marxen and Buntrock's 1990 online paper ``Attacking the Busy Beaver 5,'' here is how they proceed: Enumerate all $latex {n}&fg=000000$-state Turing machines $latex {M}&fg=000000$, and for each of them do the following.
The key to make this huge search possible, even for small $latex {n}&fg=000000$, relies on the ability to find and analyze ``macro phases'' of the computations. In the above example we were able to identify macro phases with subsets of the machine itself, but generally this requires hierarchically analyzing the trace of the computation. The art of this work is finding clever patterns that correctly predict non-halting yet are easy to apply. Ground-level patterns of the kind pictured on the left in the picture below can be abstracted and then organized in a hierarchical nested manner. Sometimes this is used to prove explosive growth before termination, and sometimes to prove non-termination.
\includegraphics[width=2.4in]{xmastree2.png}
Indeed, the drawing on the right comes from the 2005 MS thesis of Owen Kellett from 2004, which was part of a large project at RPI, and which includes and extends the specification by Rona Machlin and Quentin Stout of a ``Christmas Tree'' pattern that implies non-termination.
Thus the Busy Beaver problem becomes less about Turing machines and more about finding convergent and provably recurrent or divergent patterns in the kinds of bit-fields and word-fields in which machine-language programs operate.
Halting and the Impossible
Busy Beavers in any form represent the most extreme test cases of the Halting Problem in the sense of their raw step counts. They look like they will never halt but do. Unless there is some way a machine can look like it is going to halt but run forever, they are the only extreme in that sense. Of course, the functions $latex {B(n)}&fg=000000$ and $latex {S(n)}&fg=000000$ are uncomputable---for much the same reason that the Halting Problem is undecidable. They outgrow every computable function, and for any effective formal system $latex {F}&fg=000000$ of logic, there are only finitely many values $latex {B(n) = X}&fg=000000$ or $latex {S(n) = Y}&fg=000000$ that $latex {F}&fg=000000$ can verify.
So why should we try to compute them? The wider but commensurate question is, why should we try to solve the Halting Problem? After all, the Halting Problem is `impossible' to solve---everyone proves this in a typical theory course. With $latex {\mathsf{NP}}&fg=000000$-hard problems too, the popular subtext is not to try to solve them. So why try?
We could quote a well-known exchange between Alice and the Red Queen in Lewis Carroll's Through the Looking-Glass, or quote ``To Dream the Impossible Dream'' from the musical Man of La Mancha, or otherwise appeal to indomitable human spirit. But we can finally talk about another answer to: why try to solve impossible problems?
Because---it's good for business.
The Microsoft Terminator
Microsoft undertook to do exactly that. ``Terminator" was a doubly-thematic name for their project, which is now called T2. Not only is it about program termination, but its purpose was to do the Arnold Schwarzenegger ``Terminator'' business on unruly device drivers. To quote the most recent press article linked from that page,
To reduce the number of buggy device drivers, Microsoft embarked on what it called ``data-driven program verification.'' This is a process whereby ``you model a computer program as a mathematical system and the goal is to build tools that find proofs of correctness using mathematics and logic,'' said [project manager Byron] Cook. ...
Working out whether a device driver would get stuck in an infinite loop was a bit more tricky, as Microsoft was faced with the difficulty of addressing the halting problem. ...[which Alan Turing showed undecidable]... But Cook said the nature of device drivers meant there were ways to analyse drivers to see if they would terminate.
A May 2011 ACM Communications article by Cook with Andreas Podelski and Andrey Rybalchenko describes some of the formal logic ingredients. Their examples are mostly numerical, and we wonder how well the formal methods can be applied to analyze the patterns thrown up like sawdust by the beavers. They do conclude:
With fresh advances in methods for proving the termination of sequential programs that operate over mathematical numbers, we are now in the position to begin proving termination of more complex programs.
Open Problems
We have tried to re-position the Busy Beaver game in terms of brief prose descriptions of algorithmic procedures rather than Turing machines. Can this shift be cross-cut with practical examples? The succinct routines need not be maximum like the ``busy beaver'' for any size $latex {n}&fg=000000$. This may help.
Which other types of ``busy'' machines can be described nicely in prose? We have not found anything as neat for Kropitz's 6-state machine.