Advanced topics on Busy Beavers

Contents

The methods used to find busy beavers

Busy beavers and unprovability

Tables normalization

Last update: August 2022

The methods used to find busy beavers

The machines presented in these pages were discovered by means of computer programs. These programs contain procedures that achieve the following tasks:

1. To enumerate Turing machines without repetition.
2. To simulate Turing machines efficiently.
3. To recognize non-halting Turing machines.

If the purpose is to prove a value for the busy beaver functions, then all Turing machines in a class have to be studied. The machines that pass through the three procedures above are either halting machines, from which the better one is selected, or holdouts waiting for better programs or for hand analyses.

If the purpose is to find lower bounds, a systematic enumeration of machines is not necessary. Terry and Shawn Ligocki said they used simulated annealing to find some of their machines.

The following references can be consulted for more information.

• For (4,2)-TM:
  
  • Brady A.H. (1983)
    The determination of the value of Rado's noncomputable function Sigma(k) for four-state Turing machines
    Mathematics of Computation 40 (162), April 1983, 647-665.

  • Machlin R. and Stout Q.F. (1990)
    The complex behavior of simple machines
    Physica D 42, June 1990, 85-98.

• For (5,2)-TM:
  • Marxen H. and Buntrock J. (1990)
    Attacking the Busy Beaver 5
    Bulletin of the EATCS No 40, February 1990, 247-251.

  • Hertel J. (2009)
    Computing the uncomputable Rado sigma function
    The Mathematica Journal 11 (2), 2009, 270-283.

• For (2,3)-TM:
  • Lafitte G. and Papazian C. (2007)
    The fabric of small Turing machines
    in: Computation and Logic in the Real World, Proceedings of the Third Conference on Computability in Europe, June 2007, 219-227.

• Page about Macro Machines on Marxen's website.

• Articles by James Harland:
  • Harland J. (2016)
    Busy beaver machines and the observant otter heuristic (or how to tame dreadful dragons)
    Theoretical Computer Science 646, 2016, 61-85.
    Preprint available at arXiv:1602.03228.

  • Harland J. (2022)
    Generating candidate busy beaver machines (or how to build the zany zoo)
    Theoretical Computer Science 922, 2022, 368-394.
    preprint available at arXiv:1610.03184.

Busy beavers and unprovability

• Let S(n) = S(n,2) be Rado's busy beaver function. We know that S(2) = 6, S(3) = 21, S(4) = 107, and we can hope to prove that S(5) = 47,176,870. As we will see below, the fact that the busy beaver function S is not computable implies that it is not possible to prove that, for any natural number n, S(n) has its true value.

  Formally, we have the following theorem.

  Theorem. Let T be a well-known mathematical theory such as Peano arithmetic (PA) or Zermelo-Fraenkel set theory with axiom of choice (ZFC). Then there exist numbers N and L such that S(N) = L, but the sentence "S(N) = L" is not provable in T.

  This theorem is an easy consequence of the following proposition.

  Proposition. Let T be a well-known mathematical theory such as PA or ZFC. Then there exists a Turing machine with two symbols M that does not stop when it is launched on a blank tape, but the fact that it does not stop is not provable in T.

• Proof of the theorem from the proposition. Let M be the Turing machine given by the proposition, let N be the number of states of M, and let L = S(N). Then, to prove that "S(N) = L", we have to prove that M does not stop. But, by the proposition, such a proof does not exist.

• Proof of the proposition. This proposition is well-known and a one line proof can be given, as follows.

  If all non-halting machines were provably non-halting, then an algorithm that gives simultaneously the computable enumeration of the halting machines and the computable enumeration of the provably non-halting machines would solve the halting problem on a blank tape.

  We give a detailed proof for nonspecialist readers.

  Let M₁, M₂, . . . be a computably enumerable sequence of all Turing machines with two symbols.
  Such a sequence can be obtained as follows: we list machines according to their number of states, and, inside the set of machines with n states, we list the machines according to the alphabetical order of their transition tables.
  

  Let T₁, T₂, . . . be a computably enumerable sequence of the theorems of the theory T.
  The existence of such a sequence is the main requirement that theory T has to satisfy in order that the proposition holds, and of course such a sequence exists for well-known mathematical theories such as PA or ZFC.

  Now consider the following algorithms A and B.

  Algorithm A. We launch the machines M_i on the blank tape as follows:

  • one step of computation of M₁,
  • 2 steps of computation of M₁, 2 steps of computation of M₂,
  • 3 steps of computation of M₁, 3 steps of computation of M₂, 3 steps of computation of M₃,
  • . . .

  When a machine M_i stops, we add it to a list of machines that stop when they are launched on a blank tape.

  Note that, given a machine M, by running Algorithm A we will know that M stops if M stops, but we will never know that M doesn't stop if M doesn't stop.

  Algorithm B. We launch the algorithm that provides the computably enumerable sequence of theorems of theory T, and each time we get a theorem T_i, we look and see if this is a theorem of the form "The Turing machine M does not stop when it is launched on a blank tape". If that is the case, we add M to a list of Turing machines that provably do not stop on a blank tape.

  Note that, given a machine M, by running Algorithm B we will know that M is provably non-halting if M is provably non-halting, but we will never know that M is not provably non-halting if M is not provably non-halting.

  Now we have two algorithms, A and B, and

  • Algorithm A gives us a computably enumerable list of the Turing machines that stop when they are launched on a blank tape.

  • Algorithm B gives us a computably enumerable list of the Turing machines that provably do not stop on a blank tape.

  We mix together these two algorithms, by a procedure called dovetailing, to get Algorithm C, as follows.

  Algorithm C.

  • one step of Algorithm A, one step of Algorithm B,
  • 2 steps of Algorithm A, 2 steps of Algorithm B,
  • 3 steps of Algorithm A, 3 steps of Algorithm B,
  • . . .

  Algorithm C gives us simultaneously both the computably enumerable lists provided by Algorithm A and Algorithm B.

  So Algorithm C gives us both the list of halting Turing machines and the list of provably non-halting Turing machines (on a blank tape).

  Now we are ready to prove the proposition.
  If all non-halting Turing machines were provably non-halting, then Algorithm C would give us the list of halting Turing machines and the list of non-halting Turing machines (on a blank tape). So, given a Turing machine M, by running Algorithm C, we would see M appearing in one of the lists, and we could settle the halting problem for machine M on a blank tape. So Algorithm C would give us a computable procedure to settle the halting problem on a blank tape. But it is known that such a computable procedure does not exist. Thus, there exists a non-halting Turing machine that is not provably non-halting on a blank tape.

• Consider the Turing machine M given by the proposition: M does not stop when it is launched on a blank tape, but this fact is not provable in theory T. We can get an idea of what such a machine M looks like, as follows.

  • For example, M can be a machine that enumerates the theorems of theory T, and stops when it finds a contradiction (such that 0 = 1 if T is Peano arithmetic).

    Then a proof within theory T that M does not stop would be a proof within theory T of the consistency of T, which is impossible by Gödel's Second Incompleteness Theorem (if theory T is consistent).

    This gives another proof of the proposition, a shorter one, but resting on a big theorem.

  • Another example can be given using Gödel's First Incompleteness Theorem. If T is PA or ZFC, supposed to be consistent, the proof of this theorem provides a formula F that asserts its own unprovability. Thus F is true, but unprovable within theory T.

    Consider the machine M that enumerates the theorems of theory T, and stops when it finds formula F.

    Machine M does not stop, since F is unprovable, but a proof that it does not stop would be a proof that F is unprovable, so, since F is "F is unprovable", a proof of F, which is impossible, since F is unprovable.

  • As a third example, consider the machine M that enumerates the theorems of theory T (PA or ZFC, supposed to be consistent), and stops when it finds a formula F that says that M itself does not stop. Such a machine can be proved to exist by applying the Recursion Theorem to the function f such that machine M_f(x) stops if it finds a proof that machine M_x does not stop.

    Then F is true, because, if F were false, then M would stop, so F would be a theorem of T, so F would be true. But F is unprovable, because since F is true, M does not stop, so F is not a theorem of theory T. So the fact that M does not stop is true and unprovable.

  Note that, in these three examples of Turing machines M, the watched formulas are more and more complicated, and the theorems used to prove that M suits are more and more elementary.

• Since May 2016, there are explicit constructions of Turing machines whose behaviors are independent of ZFC.

  • Adam Yedidia and Scott Aaronson gave, in May 2016, a Turing machine with 7910 states and two symbols such that it cannot be proved in ZFC that it never halts. They note that enumerating the theorems of ZFC would need a big number of states. They use a graph theoretic statement that Harvey Friedman proved to be equivalent to the consistency of a theory that implies the consistency of ZFC. By using a new high-level language that is easily compiled down to Turing machine description, they build a machine that would halt if it finds a counterexample to Friedman's statement.

    This is published in:

    Adam Yedidia, Scott Aaronson,
    A relatively small Turing machine whose behavior is independent of set theory,
    Complex Systems 25 (4), 2016, 297-327.
    Available on the Web.

  • S. O'Rear improved the number of states to 1919, in September 2016.
    He improved later the number of states to 748.
    His machines enumerate the theorems of a formal system which has the same power as ZFC.

  • See Scott Aaronson's blog for a general presentation.

• Note that, if "S(N) = L" is a true sentence unprovable in theory T, then, for all m > L, "S(N) < m" is also a true sentence unprovable in theory T.

• Note that the proposition is a special case of the following more general theorem.

  Theorem. Let A be a set of natural numbers that is computably enumerable but not computable, and let T be a well-known mathematical theory such as PA or ZFC. Then there exists a natural number n such that the sentence "n is not a member of A" is true but not provable in theory T.

  The proof of this theorem is the same as above: if all natural numbers not in A were provably not in A, then the simultaneous enumerations of A and of natural numbers provably not in A would give a procedure that decides membership in A, contradicting the fact that A is not computable.

  The proposition is gotten from this theorem by numbering the list of Turing machines, and by defining A as the set of numbers of Turing machines that stop on a blank tape.

• There is another proof of unprovability, based on Kolmogorov complexity.
  

  The Kolmogorov complexity of a number is the length of the shortest program from which a universal Turing machine can output this number.

  By Chaitin's Incompleteness Theorem, for any well-known mathematical theory T, there exists a number n(T) such that, for all numbers of complexity greater than n(T), the fact that they have complexity greater than n(T) is true but unprovable within theory T.

  Chaitin's theorem also applies to the complexity defined as follows: The complexity of a number k is the smallest number n of states of a Turing machine with n states and two symbols that outputs this number k, written as a string of k symbols 1, when the machine is launched on a blank tape.

  So there exists a number n(T) such that, for any number k of complexity greater than n(T), the sentence "the complexity of k is greater than n(T)" is true but unprovable within theory T. But "k > Sigma(n(T))" implies "the complexity of k is greater than n(T)", so, for any number k > Sigma(n(T)), "k > Sigma(n(T))" is true but unprovable within theory T.

  For more details, see the following papers and books:

  • Chaitin G. (1987)
    Computing the busy beaver function
    Open Problems in Communication and Computation, Springer, 1987, 108-112.
    Reprinted in: Information, Randomness and Incompleteness, World Scientifics, 2nd Ed., 1990.

  • Boolos G.S., Burgess J.P. and Jeffrey R.C. (2002)
    Computability and Logic, 4th Ed., Cambridge, 2002, pp. 40-44 and 227-230 (They note that n(T) < 10^10^10^10^10^10^10^10^10^10).

  • Lafitte G. (2009)
    Busy beavers gone wild
    in: The Complexity of Simple Programs 2008, EPTCS 1, 2009, 123-129.

Tables normalization

A permutation of states, or a permutation of symbols, does not change the behavior of a Turing machine.
Suppose you get two Turing machines, taking the same time to stop on an initially blank tape. How to know whether these machines are essentially different, or they are just the same machine up to a permutation of states or symbols?
To settle this problem, you can normalize the table, putting it in tree normal form (TNF).

Since we are interested by the behaviors of Turing machines on an initially blank tape, the simplest rule is the following one:

When the Turing machine is launched on a blank tape:

• it enters states in the following order: A, B, C, ...

• it writes symbols in the following order: 0, 1, 2, ...

As an example, we give below the tables of the Turing machines as found by Terry and Shawn Ligocki, and their normalized versions as given in the present web pages.

Turing machines with 2 states and 4 symbols

Turing machines with 2 states and 5 symbols

Turing machines with 2 states and 6 symbols

Turing machines with 3 states and 4 symbols

Turing machines with 4 states and 3 symbols

Link to the home page of Pascal Michel