BB(2)

The 2-state 2-symbol Busy Beaver problem BB(2) was solved by Tibor Radó using pencil and paper and announced in his seminal Busy Beaver paper, On Non-Computable Functions.

Current Work

Although the Coq-BB5 proof contains a proof of this case, investigations are ongoing to make a simpler proof that better captures the complexity of this problem.

The following command which uses code from Shawn Ligocki's GitHub repository to enumerate the BB(2) TMs in TNF, run each of them for 1000 steps, and look for TMs that are Translated Cyclers which never halt:

     > lr_enum 2 2 1000 halt.txt infinite.txt holdout.txt false

This is all that is needed to classify all the BB(2) TMs so a minimal proof only has to have this functionality.

Champions

S(2) = 6 and there are 5 shift champions in TNF:

• 1RB1LB_1LA1RZ (bbch) leaves 4 ones (the ones champion)
• 1RB0LB_1LA1RZ (bbch) leaves 3 ones
• 1RB1RZ_1LB1LA (bbch) leaves 3 ones
• 1RB1RZ_0LB1LA (bbch) leaves 2 ones
• 0RB1RZ_1LA1RB (bbch) leaves 2 ones

Σ(2) = 4 and there is one unique ones champion in TNF:

• 1RB1LB_1LA1RZ (bbch) runs for 6 steps (a shift champion)

Enumeration

In TNF-1RB there are exactly 41 BB(2) TMs of which 15 halt:

1RB1LB_1LA1RZ Halt 6 4
1RB1RZ_1LB1LA Halt 6 3
1RB0LB_1LA1RZ Halt 6 3
1RB1RZ_0LB1LA Halt 6 2
1RB1LA_1LA1RZ Halt 5 3
1RB1LA_0LA1RZ Halt 5 2
1RB1RZ_1LB1RA Halt 4 2
1RB1RB_1LA1RZ Halt 4 2
1RB1RZ_1LB0RA Halt 4 1
1RB0RB_1LA1RZ Halt 4 1
1RB1RZ_1LA--- Halt 3 2
1RB---_1LB1RZ Halt 3 2
1RB1RZ_0LA--- Halt 3 1
1RB---_0LB1RZ Halt 3 1
1RB---_1RZ--- Halt 2 2

and 26 are infinite:

1RB1RB_0LA---
1RB1RA_1LA---
1RB1RA_0LA---
1RB1LB_0LA---
1RB0RB_0LA---
1RB0RA_1LA---
1RB0RA_0LA---
1RB0LB_0LA---
1RB0LA_1LA---
1RB0LA_0LA---
1RB---_1RB---
1RB---_1RA---
1RB---_1LB1RB
1RB---_1LB1LB
1RB---_1LB0RB
1RB---_1LB0LB
1RB---_1LB0LA
1RB---_0RB---
1RB---_0RA---
1RB---_0LB1RB
1RB---_0LB1RA
1RB---_0LB1LB
1RB---_0LB0RB
1RB---_0LB0RA
1RB---_0LB0LB
1RB---_0LB0LA