How the Slowest Computer Programs Illuminate Math’s Fundamental Limits
> The busy beaver game is all about the behavior of Turing machines
A busy beaver for lambda calculus is even easier to define:
the maximum normal form size of any closed lambda term of size n (or 0 if none exists).
The series [1] starts as 0, 0, 0, 4, 0, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 22, 24, 26, 30, 42, 52, 44, 58, 223, 160, 267, 298, 1812, 327686, 38127987424941,
578960446186580977117854925043439539266349923328202820197287920039565648199686
Results are more fine grained than for TMs because these sizes are in units of bits (lambda and application measuring as 2 bits, and a variable bound by n'th enclosing lambda as n+1 bits).
Graham's number is surpassed within 114 bits, while the smallest known TM for surpassing it takes 225 bits to describe.
One fascinating thing about the function BB(n) is that it grows faster than any computable function.
The proof of this is simple: if you had a computable function f(n), and f(n) >= BB(n) for all values of n, you could use that to solve the halting problem, which in itself is impossible.
I used to implicitly assume that we can make concrete, closed-form, functions that grow as fast as we want them to. The above shows that this is clearly false.
> Nevertheless, that incomprehensibly huge number is still an exact figure whose magnitude, according to Aaronson, represents “a statement about our current knowledge” of number theory.
This is, of course, contradicted later in the article in which they point out that `BB(800)` (or so) has been proved independent of ZFC; there's no really good reason to believe `BB(27)` is not likewise independent. There may still be a truth of the matter about the value of `BB(800)` or `BB(27)` (as the case may be), since ZFC hardly encompasses all truth, but calling such a number an "exact figure" is a bit like claiming to know the birth date of Julius Caesar down to the millisecond: Implausible to start with, and the closer you look the more you wonder, "what does the question even mean? Relative to what standard?" (In the one case, "of time"; in the other, "of mathematical truth".)
I created the visualization for this story by running BB(5). You can find the source code (a full Turing Machine implementation that runs BB) and visualizations of other BBs in my blog post https://catonmat.net/busy-beaver.
> If you knew all the busy beaver numbers, then you could settle all of those questions.
A lot of important questions in number theory could be answered, but not all. For example, the mentioned Collatz conjecture (3n+1) is of different type. To prove this conjecture you need to prove the halting for EVERY argument. Checking halting of a single program will not be enough, so busy beaver won't help. This is a next level task in the Arithmetical Hierarchy [1]. Though, in fact, you can define the next level Busy Beaver that could solve Collatz conjecture. To solve more complicated problems you need high-order Busy Beavers.
Very interesting. In the past, I spend some time on finding the largest number that could be calculated by a Brainfuck program when the memory cells can hold arbitrary large numbers (and not be restricted to bytes as with the official language). It takes a bit longer to take-off. For my findings, see: https://www.iwriteiam.nl/Ha_bf_numb.html
I wonder how one goes about proving that such large computations as BB(27) are physically impossible in our universe?
Andrej Bauer: Is it just me, or is the busy-beaver function a figment of classical mathematics?
> 6,561 possible machines with two rules
Huh? How do they get to that number? A TM state can be described with 4+2log2(N) bits, where N is the number of states, so a 2-state TM can be specified with 12 bits, so there are at most 4096 of them. Where do the extra 2465 come from?
After reading this kind of fascinating stuff, I feel ashamed that I am wasting the opportunity of having a human mind by writing CRUD applications (though I am nowhere near as smart as this stuff requires one to be - I can barely clear whiteboard coding interviews).
I too have read Scott Aaronson's blog.