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:

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:

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):

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.

(c) Skelet, Feb 2003 in terms of GNU GPL

Mail me at home or work