Skelet page for Busy Beaver problem

Busy Beaver prover

This page explains my work on Busy Beaver problem.

Good definition and current state of the problem you may find on Heiner Marxen Busy Beaver page.

I preffer the form more closed to stoping problem:

The function S(n) denotes the maximal number of steps which a Turing Machine (TM) with n internal states and a two-way infinite tape can produce onto an initially empty tape and then halt.

It is well known from about 70 years that the function S(n) can't be computed. It grows faster than any computable numeric function.

BB(n) problem is an attempt to evaluate this function for small values of n.

My program, called bbfind enumerates the Turing machines and then tries to prove their infinitness.
As a side effect stoping machines are identified and checked for BB record.

Current version properly evaluates S(n) for class TM(4) and important subclass of TM(5), called RTM(5) (reversal turing machines with 5 states).

For class TM(5) the program leaves 164 machines unproven (some are isomorphic to other by trivial reasons).

Current version works slowly, and full scanning for TM(5) may take 1 or 2 weeks.

For class TM(5) the program enumerates about 150M machines.

It seems that all machines with nontrivial behavior may be divided in 3 big classes:

1. k-Linear sequence:

Tape of these machines may be represented by the form:

.i0(e1|n1)i1(e2|n2)i2(e3|n3)...(ek|nk)ik.

where n1..nk are natural numbers (repeaters), e1..ek are words of bits (i call thes word exones).

Notation '(a|n)' means that word a is repeated n times on tape.

i0,i1..ik are also words (i call them intrones).

This class may be divided in 3 specific subclasses:

lineary increasing sequence:
In this case k is limited by some constant N and all repeaters n1,n2..nk are nondecreasing during the tape transitions.
Infinitness of these machines is proved by the procedure TryL1Cnt, resolving about 95% of the nontrivial machines.
collatz-like sequence is similar to previous subclass, but some repeaters may decrease to zero.
Infinitness of these machines is proved by the procedure TryModFin.
Stopping machines from this subclass are interpreted by the procedure CollatzLoop and it gives all record machines for TM(5).
linear-binary sequence: In this case k is unlimited, there is only 1 exone, number of different intrones is limited by some small constant B.
If we ignore exone sequences (e|n), the remaining part of the tape form some B-nary counter during the tape transitions.
Infinitness of these machines is proved by the procedure TryBL_Proof.
Common method ExonesSpecFast proves many of these machines, but not all.

2. NonLinear sequence:

Tape of these machines may be usualy represented by the form:

.i0[l1..lN]i1Ci2[r1..rM]i3.

where i0..i3 are introne words, C is some central word (may contain head state/direction or may be fixed to position 0).

l1..lN are words from some set, called 'Left exones set' (L_set). Thepending of proof method, they are mixed in any order, without any regularity or may be treated as proper sequences in some formal grammar.
Similarly, the words r1..rM are from set, called 'Right exones set' (R_set).

This class may be divided in 2 specific subclasses:

fixed positions counter:
In this case word C is fixed around position 0.
All words from L_set have fixed size, the same is true for R_set.
Infinitness is proved by procedure TryPFin_2.
swiming head counter:
in this case C represents head state/move_direction.
Common method, called Chaotic Huffman test (procedure ExonesSpecFast) proves many of the machines from this subclass.
It uses for L_set and R_set randomly selected Huffman (or semi-Huffman) code sets (words are in reversed order, other parameters tunes the test).
procedure CreateHuffCodes generates all Huffman codes with limited set size.

3. Other types (nonregular):

It seems that some of the nonregular (unproven) machines are members of other types, that can't be handled by the current program methods.

Complexity and some other info about thes types you may find at the nonregular page.

Installation and usage instructions:

1. Installation:

You must have FreePascal installed.

If you use non Debian OS, read more on FreePascal.org.

If you use Debian Linux the installation is simple:

apt-get install fp-compiler binutils

After installation of FreePascal and downloading the program and
this small database file, type on the console:

gzip -d bbfind.pp.gz
fpc bbfind

The program will be compiled.

2. Usage:

After compilation type:

./bbfind

and TM checking will begin for class TM(5).

On your console something like this will apear:

M=  22976008 .__________..__________..__________.     V =   95 machines/sec 
nrm= 7188924 |A 30441   ||A 30411   ||A 30451   |     Collatz_cnt=200 
mov=       3 |  14352   ||  25243   ||  41325   |     IP_max=255 
tov=      32 |B 00100   ||B 00110   ||B 00001   |     T_eps=0,-1 TT       
b_t= 6998623 |  01111   ||  10010   ||  11011   |     PosLR=13|13  5
i_t=   73422 |C 11101   ||C 11111   ||C 11111   |     MH_cnt=1800 
c_l= 1061149 |  11110   ||  01110   ||  10101   |     SHG0=39 eps=2      
s_l=  634645 |c=11811040||c=23554764||c=47176870|     BL_Proof M=22452470  
m_l= 6661093 |6145/4097 ||6145/4097 ||12289/4098|
lNc=  337474 .__________..__________..__________.     G/A/m= 176/ 10/0
gMl=     226
p_l=   16382 .__________..__________..__________.  .__________.
pSl=       0 |A 30411   ||A 30435   ||A 30434   |  |A x0xxx   |
eH0=       0 |  14352   ||  31452   ||  11152   |  |  xxxxx   |
eH1=       0 |B 00100   ||B 00110   ||B 00101   |  |B 00xxx   |
e0l=     360 |  01111   ||  00010   ||  11011   |  |  xxxxx   |
e1l=      27 |C 11111   ||C 11101   ||C 11111   |  |C x1xxx   |
eS0=    3320 |  10111   ||  01011   ||  10010   |  |  xxxxx   |
eS1=     181 |c=11798826||c=   321  ||c= 20711  |  |c=  4000  |
eS2=       0 |6145/4098 ||19/16     ||162/161   |  |m=   250  |
B-L=      86 .__________..__________..__________.  .__________.
cl0=      53

Left column of counters have the following semantics:

M=  22976008 Machine enumeration counter.
nrm= 7188924 Finite machines.
mov=       3 Nonregular, last interpretation overflow the type.
tov=      32 Nonregular, last interpretation overflow the time.
b_t= 6998623 \           - backtrack test
i_t=   73422  \ Trivial  - isomorphic test
c_l= 1061149   >  tests: - circle on place test
s_l=  634645  /          - subdimension test
m_l= 6661093 /           - left/right infinite moving test
lNc=  337474 machines passed the test TryL1Cnt.
gMl=     226 test TryModFin
p_l=   16382 test TryPFin_2
pSl=       0 test BVortexLoop (not used now)
eH0=       0 not used
eH1=       0 not used
e0l=     360 Chaotic Huffman test Grammar_0 short sets
e1l=      27 Chaotic Huffman test Grammar_0 longer sets
eS0=    3320 Chaotic Huffman test Grammar_2 short sets
eS1=     181 Chaotic Huffman test Grammar_2 longer sets
eS2=       0 not used
B-L=      86 test TryBL_Proof
cl0=      53 Finite machines, interpreted by CollatzLoop.

Upper central part of the console shows 3 last record machines with bigger S(n).

Lower central part of the console shows 3 last record machines with bigger Sigma(n).

Lower right part shows the pattern machine for TM generator.

Right upper half-line shows the current speed.

Other text in right part of the console are for debuging.

3. Generated output files:

The program generates the following output files (??? is corresponding TM class - TM5, RTM5, TM4):

noreg_???.txt - info about first 40 nonregular machines.
nreg_???.txt - list of all nonregular machines - definition, enumeration id, spectral info.
ShRec_???.txt - info about nonregular machines of type 'Shift Recursive'. I use this info for proofs by hand. See nonregular page for details.
recrd_???.txt - interpretation of record machines.
proved_???.txt - first 20 proofs for each nontrivial test.
other_???.txt - debuging info.

4. Scanning other TM classes:

Change the constants at the lines 5-6 of the program source:

const dm=5;          { TM dimension. Must be 4,5 or 6 }
      reversal=true; { Reversal / Normal TM }

Upper seting is for class RTM(5).

The final screen for this class looks as follows:

M=    643264 .__________..__________..__________.     V =  117 machines/sec
nrm=  175096 |A 33412   ||A 23453   ||A 31412   |
mov=       0 |  10545   ||  05515   ||  50345   |     IP_max=10
tov=       0 |B 01101   ||B 00001   ||B 00110   |
b_t=  100259 |  00110   ||  00101   ||  00011   |     M_m=615832/2
i_t=    6677 |C 11111   ||C 11111   ||C 11111   |     MH_cnt=200
c_l=   26016 |  00000   ||  00000   ||  00000   |     mod=5:4|6/1 0
s_l=   28821 |c=  1136  ||c=   801  ||c=   860  |
m_l=  293698 |41/32     ||48/29     ||36/28     |
lNc=   12573 .__________..__________..__________.     G/A/m= 118/ 10/0
gMl=      17
p_l=      96 .__________..__________..__________.  .__________.
pSl=       0 |A 23453   ||A 33412   ||A 23453   |  |A xxxxx   |
eH0=       0 |  05515   ||  10545   ||  01324   |  |  x0xxx   |
eH1=       0 |B 00001   ||B 01101   ||B 01100   |  |B 0xxxx   |
e0l=       4 |  00101   ||  00110   ||  00110   |  |  x0xxx   |
e1l=       0 |C 11111   ||C 11111   ||C 11111   |  |C 11111   |
eS0=       7 |  00000   ||  00000   ||  00000   |  |  00000   |
eS1=       0 |c=   801  ||c=  1136  ||c=   256  |  |c=  4000  |
eS2=       0 |48/29     ||41/32     ||38/18     |  |m=   250  |
B-L=       0 .__________..__________..__________.  .__________.
cl0=       0

5. Some remarks:

The program is in active process of development and contains many redundant code.

It may contain also bugs and non-effective parts.

I will be happy to receive any comments or recomendations for future improvements.

This page was last modified at 13 May 2003.

Mail me at home or work