The Busy Beaver Problem
Can the impossible become practical?
|
|
Complex analysts gallery source |
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ős-Ko-Rado theorem—that is Richard Rado, without an accent. Tibor Radó had an Erdős Number of 3, through Lin and then Ron Graham.
Today we want to continue to talk about the famous “Busy Beaver” problem which we mentioned in our discussion on the Microsoft SVC lab closing.
The problem is actually quite neat, is still 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 two-way infinite tape, a finite deterministic state control of 
Clearly with enough states the machine could compute 
The function 
This was discovered by Heiner Marxen and Jürgen Buntrock in 1989. The busy-beaver function 
A Six—or Three—State Beaver
What we also find amazing is that for some of the busiest machines, their few states can be made to seem even fewer with a simple prose description. 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.
|
|
source |
In the Take Stock state, our beaver looks at the spots left and right, and acts according to these four rules:
- If he finds himself in sun with no tree on his right, he decides to Plant Two Trees right there.
- If he finds himself in sun with a tree to his right, he chops it down and Takes Stock again in the place where he was.
- If he is in shade with no tree on his left, he plants there, goes back where he was, and decides to Plant Two Trees.
- If he is in shade with a tree on his left, he chops it down, steps left again, and Looks For His Shadow.
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 first two Take Stock rules can even be combined to say that if he’s in sun, he plants there, ensures the place to his right is planted, and then Takes Stock again where he was. In the third rule, the “goes back” clause 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 
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 
The Current Approach
How do people prove such gargantuan bounds on
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 
-
Simulate the behavior of
-
If
-
If
-
If the number of simulation steps exceeds a certain predefined limit, mark
-
Use rules that predict a machine will never halt. If they prove non-halting for
The key to make this huge search possible, even for small
|
|
Composite of src1, src2 (p78) |
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 
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 
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 analyze 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 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
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.
[added more links]
BB research is far more fundamental than many realize because of its deep link to automated theorem proving as hinted in the Podelski/ Rybalchenko quote. this is highlighted in a neat recent paper Problems in number theory from busy beaver competition p3. am planning on blogging on it also sooner or later.
In this same sense, studying the busy beaver problem is significantly harder than any other open mathematical problem. Mathematical intuition developed even over decades of studying decidable problems tends to break down in this area. a bit more on the theme in musings on automated theorem proving
Thanks for meaty comment—I (Ken) edited it to fix “jaggies”.
It occurred to me walking back from class just now that the 6-state example might also be expressible nicely by maintaining the “stump spots” (= bare spots that were previously visited, plus endpoints) in two stacks and doing a little arithmetic—just increment/decrement and comparison. That would bring it much closer to the kind of examples in the “Terminator” people’s CACM article.
Many GLL readers (including me) appreciate vznvzn’s ‘meaty comment’ (Pip’s phrase) … also valuable are the many references that vznvzn’s Turing Machine weblog provides in the essay Adventures and Commotions in Automated Theorem Proving.
Good on `yah, vznvzn!
Here are a few more references that I find valuable in explaining the “A” in STEAM to the many writers in my family.
To begin with computer-assisted proofs, an accessible non-technical essay — very much in the spirit of Doron Zeilberger — is the anonymously authored “QED Manifesto” (1993, see its Wikipedia page for details). The announcement this past August 10 of the formal proof of the Kepler Conjecture is among many ‘proofs’ that the QED Manifesto’s objectives are attainable.
The writers in my family appreciate the objectives of the QED Manifesto from a perspective that is compatible with Bill Thurston’s mathematical worldview (of “Proof and Progress in Mathematics) and they extend Thurston’s worldview it in a direction that is congenially natural, both mathematically and poetically.
In brief, a teaching of Fernando Pessao — “who made himself into nothing so that he could become everything“ — is this:
From a Pessao-esque perspective, what’s broadly radical about the QED Manifesto, and what’s specifically radical about the Hales/Flyspeck/Microsoft proof of the Kepler Conjecture — good on `yah, Microsoft for supporting this work! — is that the proof concretely constructs Pessao’s “completely erased text”.
This is a radical advance that can be appreciated in many ways (needless to say).
In particular, it is a mistake (as it seems to me) to regard these computer-checked STEAM texts as evidence not we can dispense with the “marginal notes” of human mathematicians, with a view toward compressing mathematics into a corpus of distilled truth.
Rather, these computer-proofs encourage us to reflect — Thurston-style and Passao-style — not only upon STEAM-texts that have been written and will be written, but also upon STEAM-texts that might have been written.
This point-of-view — that STEAM narratives are informed in equal measure by logic, science, and art — has been congenial to authors of many generations. Mark Twain says it plainly:
The Pessao/Twain Corollary The completion and fruition of the 20th century’s STEAM literature requires that its marginal defects be conscientiously corrected, so as to help the 21st century over its difficult places.
Nowadays many authors — Neil Stephenson, Cory Doctorow, David Eggers, and Eliezer Yudkowsky, to name a few (along with the writers among my family and friends) — are embarked upon this great 21st century margin-filling work.
Fortunately (and to echo Feynman) “There’s plenty of space in the margins.”
Good on `yah, 21st century STEAM-authors!
——
Note The greek historian Herodotus of course never said anything like the words that Twain ascribes to him; this has not prevented the world from accepting Twain’s faux-quotation as sober fact.
Further “A-team” literary references relating to the computational depth of truth-speaking — with especial reference to the works of Twain/Pessao/Stephenson/Eggers — can be found in comments #27-28 and #36 of Scott Aaronson’s essay “Speaking Truth to Parallelism at Cornell.”
Prediction The 21st century’s STEAM-marriage (of “A” to “STEM”) is bound to elicit much further creative work, that will bring out (hopefully) the best in all parties concerned. Good!
That is a very pleasing bit of mathematical prose. A similar class of problem is:
The canonical example is
, which formally cannot be generated by any deterministic algorithm, but in practice we do it all the time — “because it’s good for business” (as Dick and Ken say).
In this era of dystopian lab-closing, it was good to see Nippon Telegraph and Telephone (NTT) Laboratory tackling this class of question in “Will boson-sampling ever disprove the Extended Church-Turing thesis?” (arXiv:1401.2199v3).
Math Question What other dynamical processes generate data-streams that plausibly (and even provably) are hard to sample, but in practice are easy to sample (and even good business)?
STEAM Question With IBM and Microsoft both downsizing, is NTT Labs the world’s strongest remaining “fundamental research” corporate laboratory?