We discuss a new tool that is successfully used in an ongoing project to compute : an automated symbolic induction prover (SIP). The SIP tool is written in Mathematica and provides a unified way to prove that large sets of Turing machines are nonhalters. In a way, an SIP enables certain Turing machines to provide their own proof of being a nonhalter.

Introduction

It is a classic result of computability theory that there exist uncomputable functions. A prime example is Tibor Rado’s [1] function (or the busy beaver function) that measures the productivity of -state, binary Turing machines. Despite being uncomputable, we know [2] exact values of for and a high lower bound for : [3].

To compute the exact value of we have to decide the halting question for -state binary Turing machines. Fortunately, this huge number can be reduced by applying well-known techniques such as tree normalization, backtracking, and simple loop detection [2].

With few undecided Turing machines, we now have strong evidence that indeed . Final results will be reported in a forthcoming report [4].

Rado’s Uncomputable Sigma Function

There are far too many functions from the positive integers to the positive integers for them all to be (Turing) computable. A Cantor diagonalization argument [5] shows that the set of all such functions is not enumerable, whereas the set of all Turing machines is denumerable [5]. Hence, there must exist functions that are uncomputable.

In 1962, Tibor Rado [1] presented the uncomputable function (also known as the busy beaver function). Roughly speaking, is the largest number of 1s left on the tape by a halting binary -state Turing machine when started on an initially all 0 tape. The function is uncomputable because otherwise it would solve the halting problem, which is known to be undecidable [5]. Even more, Rado [1] proved that grows faster than any computable function for large enough values of , that is, for any computable function , it holds that .

In 1964 Green [6] established general lower bounds for the function for larger values of by explicitly constructing so-called class M Turing machines that generate long blocks of 1s. Julstrom [7] showed that Green’s class M Turing machines are related to the Ackermann function [5], a function that is computable but not primitive recursive.

Various computationally based approaches to make progress on the function have been taken: brute force searches, genetic algorithms, heuristic behavior analysis, and many more [8]. The function has become a classic topic in the theory of computing [8]. For a comprehensive list of references on Rado’s function, see [9].

However, so far, exact values of have only been computed for (see [2, 8]): , , , . These values are the first elements of the A028444 sequence of integers in The On-Line Encyclopedia of Integers [10].

In 1990 Marxen and Buntrock [3] established the lower bound , by publishing a record-holding binary 5-state Turing machine that halts after 47,176,870 steps and leaves 4098 1s on the tape.

Michel [11] shows a connection of most of the known low record-holding Turing machines and the Collatz problem.

There are three other related uncomputable functions associated with binary -state Turing machines:

• : The maximum number of moves of a halting binary -state Turing machine started on an all 0 tape.
• : The largest unary number that can be created by a halting binary -state Turing machine started on an all 0 tape.
• : The largest number of different tape cells scanned by a halting binary -state Turing machine started on an all 0 tape.

Ben-Amram et al. [12] prove that , .

Why Compute Values of Sigma?

Chaitin argues that the function is of considerable meta-mathematical interest. According to Chaitin [13], let be a computable predicate of a positive integer so that for any specific it is possible to compute if is true or false. The Goldbach conjecture is an example for . The function provides a crucial upper bound, for if has algorithmic information content , it suffices to examine the first natural numbers to decide whether is true or false for all natural numbers [13]. Hence, the function enables converting a large but finite number of calculations into a mathematical proof. Calculating for specific values of thus amounts to a systematic effort to settle all finitely refutable mathematical conjectures; that is, to determine all constructive mathematical truth [13].

Minds, Machines, and Sigma

There is an ongoing philosophical discussion as to whether the human mind can surpass the Turing limit or can be understood as a Turing machine. The famous logician Kurt Gödel discusses his point of view that the mind can indeed surpass the Turing limit in conjunction with his well-known incompleteness theorem. Gödel states in [14], that “although at each stage the number and precision of the abstract terms at our disposal may be finite, both may converge toward infinity in the course of the application of the procedure”. Computing values of for increasing serves as a quantitative example for the situation Gödel is referring to. Indeed, Bringsjord et al. [15] present a “new Gödelian argument for hypercomputing minds” that is based on the function. In their argument, the function provides a discrete way to measure the achievement of the human mind, surpassing the Turing limit and establishing new constructive mathematical truth. In [15] the core assumption is that if the human mind can compute it also can compute , although that advance might take quite a long time.

Experience from our ongoing project of computing for 5-state binary Turing machines shows that the halting question of large subsets of Turing machines can be decided in a unified way. By using data mining to identify patterns and by the subsequent use of an SIP, we can prove that these machines are in fact nonhalters once they reach a certain pattern when started on an all 0 tape. If we succeed in identifying an induction base (i.e., some pattern), we then can use the SIP to operate as a kind of meta-Turing machine, enabling the underlying Turing machine to create its own proof of being a nonhalter. Nothing in that process is restricted to 5-state Turing machines. Hence we can imagine climbing beyond . The main challenge becomes the data mining part of identifying suitable induction base steps for the increasingly complex and “erratic” behavior of Turing machines.

We now turn in more detail to the computation of and to our main computational tool for that task—the SIP for nonhalting Turing machines.

The Computation of Sigma for 5-State, Binary Turing Machines

Notations and Definitions

Binary -state Turing machines conform to these conditions:

• The tape is infinite in both directions.
• The tape alphabet is .
• The all 0 tape is called the blank tape .
• The Turing machine has states, labeled , and a halt state, labeled 0.
• At each step the machine reads/writes the cell scanned by the Turing head and moves the Turing head one cell to the left/right.

Definition: The instruction table of a 5-state binary Turing machine is a 52 table such that , with , , , , .

We call the current state of and the read symbol in the tape cell positioned under the Turing head . The triple is called a Turing instruction, with the write symbol being written into the tape cell positioned under the Turing head , the move direction of the Turing head , and the next state of . If , stops; otherwise, it continues executing instructions.

Without loss of generality, we assume the halt instruction to be .

That leaves us with possible binary 5-state Turing machines. We call this finite set .

Let . means Turing machine is started in state 1 on tape .

We define

Here is an example of a a 5-state Turing machine first published by Marxen and Buntrock [3]:

halts after 47,176,870 steps and leaves 4098 1s on the tape; that is, :

Hence, and we have to solve the halting question for a finite, but large number of Turing machines to compute the value of .

Configurations

Let denote the set of finite words from the alphabet . For and let x || y ^* denote the concatenated word.

A machine configuration is an expression

where denotes the left/right infinite blank portion of the tape. In this notation .

We use for all to define symbolic configurations with multipliers , as in . For example, . That is, is in state 3, the Turing head scans a 0 cell, and the subtape occurs times.

General Approach: Discover and Prove

By using well-known techniques [2], such as tree normalization, backtracking, or simple loop detection, the halting question can be decided for many of the 5-state binary Turing machines.

If we apply such techniques to the possible 5-state binary Turing machines, we find approximately 1,000,000 undecided machines (holdouts).

For each of the remaining undecided Turing machines:

• Iterate the holdout machine a “number of times”, starting on the blank tape .
• Save the configuration after each step.
• Try to discover recurring patterns and store them as machine configurations.

Here are some examples with and the multiplier satisfying a recurrence relation :

where .
Here are some actual examples of configurations.

A simple linear configuration:

A simple exponential configuration:

A more complicated configuration:

Once we have identified a reliable hypothesis for a recurring configuration of a Turing machine , we try to create an induction proof showing that does indeed not halt.

The general scheme is as follows:

Step 4 involves the handling of symbolic configurations. This cannot be done by using the Turing machine’s instruction table as it is, because the Turing instructions are defined for numeric tape configurations only, not for symbolic configurations. For this we need the SIP, a kind of meta-interpreter that enables the Turing machine to produce its own induction proof of being a nonhalter.

If the induction proof is successful, we know that the Turing machine does not halt; hence, . The induction proof might fail because of the following.

• The hypothesis is wrong (it is just based on a finite amount of tape data).
• The proof does not terminate within the prespecified amount of CPU time (i.e., it might go through if we allow more CPU time).
• A situation is encountered beyond the implemented induction logic (we need to enhance the prover).
• A generalized Collatz () problem is encountered (see below).

We now turn to a more detailed discussion of the SIP.

The Symbolic Induction Prover

Meta-Instructions

The underlying idea is a unified and simple principle: analyze the Turing machine’s instruction table and extract rules which describe meta-transactions on maximal invariant subtapes.

For example, let

Here is an example of a first-order meta-instruction:

where gl is the symbol for a general left tape and gr is the symbol for a general right tape.

If at time , has configuration

for some , , we can apply the meta-instruction to get

Here is an example of a second-order meta-instruction:

Note that a meta-instruction modifies an arbitrarily large countable portion of the tape.

Induction Schemes

The SIP has a built-in library to support several induction proof schemes. Induction schemes are used in conjunction with meta-instructions to produce an induction proof for a nonhalting Turing machine. If necessary, the library can be enhanced with new induction schemes. We now discuss some of the implemented schemes.

Scheme: Commutation Relations at the Tape Boundary

Assume Turing machine exhibits the symbolic machine configuration

for some , .

If true, does not halt; hence, .

Induction Proof:
Let be in the configuration

The SIP searches for maximal invariant boundary conditions and commutation relations.

Check If:

If true, check further if for some ; if this is also true, modify the induction assumption to read:

Extended Induction Hypothesis:

The SIP proves this extended induction assumption as follows:

Hence , and does not halt, meaning that .

Scheme: Cyclic Conditions at the Tape Boundary

Assume Turing machine exhibits the symbolic machine configuration

for some , .

Induction Base:
Verify .

Induction Assumption:
.

Assume further that the instruction table of results in meta-instructions:

where are the cyclic boundary conditions, with

Induction Proof:

Scheme: Decreasing Cell Sequence at the Tape Boundary

Assume Turing machine exhibits:

Induction Base:
Verify that for some function :

Verify the swap meta-instruction:

Induction Assumption:

Induction Proof:

Now, require that

and hence .

Similar schema are also supported:

and

Modular Arithmetic

Often meta-instructions are subject to some modular condition.

Here is an example:

If possible, the SIP calculates explicitly by using information about .

If the variable is of the form and , then .

In general, the SIP uses modular arithmetic in the finite ring , including Fermat’s little theorem:

and Euler’s generalization:

(Euler’s phi function gives the number of positive integers less than or equal to that are relatively prime to .)

If nothing specific can be computed, the SIP picks a value and generates subproofs, one for each of the possible values at each decision point in the general induction proof.

The Symbolic Induction Prover Package

The SIP includes the following major functional packages to support meta-instructions and symbolic induction proofs for Turing machine configurations.

Create and execute meta-instructions.

Handling of induction proofs.

Modulo arithmetic for symbolic variables.

Handling boundary conditions.

Technical services.

Results

Start with , .

Applying well-known [2] and fast techniques, such as tree normal form, backtracking, and simple loop detection, leaves about 1,000,000 Turing machines undecided.

• 850,000 Turing machines are of a linear type, for example, for some , or slightly more complex and are proved by the SIP to not halt.
• 143,000 Turing machines are of polynomial or exponential configurations and are proved by the SIP to not halt.
• 1,000 Turing machines are currently too complex for the SIP.
• 900 have been manually proven to not halt.
• 100 cases are still holdouts and are currently under consideration, but there is strong evidence that they do not halt.
• 6,000 Turing machines halt within 50 × .

Given that, we find that for the number of 1s () left on the tape, the number of cells scanned (Space), and the number of moves (Shift), the Marxen and Buntrock [3] machine is the champion

with:

The largest unary number (i.e., empty tape with a single block of consecutive 1s) produced by any halting binary 5-state Turing machine is .

The Num champion is:

The possibility exists that the halting question for one or more of the remaining holdouts is linked to the Collatz problem (see also [11]). This is currently under investigation, and the final results will be reported in a forthcoming paper [4].

References

[1]	T. Rado, “On Non-Computable Functions,” Bell System Technical Journal, 41, 1962 pp. 877-884.
[2]	R. Machlin and Q. Strout, “The Complex Behavior of Simple Machines,” Physica D: Nonlinear Phenomena, 42, 1990 pp. 85-98, and references therein. www.eecs.umich.edu/~qstout/abs/busyb.html
[3]	H. Marxen and J. Buntrock, “Attacking the Busy Beaver 5,” Bulletin of the European Association for Theoretical Computer Science, 40, 1990 pp. 247-251.
[4]	J. Hertel, “The Computation of the Value of Rado’s Non-Computable Function for 5-State Turing Machines,” work in progress.
[5]	G. S. Boolos and R. C. Jeffrey, Computability and Logic, New York: Cambridge University Press, 1989.
[6]	M. W. Green, “A Lower Bound on Rado’s Sigma Function for Binary Turing Machines,” in Proceedings of the Fifth IEEE Annual Symposium on Switching Circuit Theory and Logical Design, Princeton, NJ, 1964 pp. 91-94.
[7]	B. A. Julstrom, “A Bound on the Shift Function in Terms of the Busy Beaver Function,” ACM Special Interest Group on Algorithms and Computation Theory, 23(3), 1992 pp. 100-106.
[8]	E. W. Weisstein, “Busy Beaver” from Wolfram MathWorld—A Wolfram Web Resource. mathworld.wolfram.com/BusyBeaver.html
[9]	H. J. M. Wijers, “Bibliography on the Busy Beaver Problem,” 2004. www.win.tue.nl/~wijers/bbbibl.pdf
[10]	N. J. A. Sloane. “The On-Line Encyclopedia of Integer Sequences, Sequence Id=A028444.” oeis.org/search?q=A028444&language=english&go=Search
[11]	P. Michel, “Busy Beaver Competition and Collatz-Like Problems,” Archive for Mathematical Logic, 32(5), 1993 pp. 351-367.
[12]	A. M. Ben-Amrein, B. A. Julstrom, and K. Zwick, “A Note on Busy Beavers and Other Creatures,” Mathematical Systems Theory, 29(4), 1996 pp. 375-386.
[13]	G. J. Chaitin, “Computing the Busy Beaver Function,” Open Problems in Communication and Computation (T. M. Cover and B. Gopinath, eds.), New York: Springer-Verlag, 1987 pp. 108-112.
[14]	K. Gödel, “Some Remarks on the Undecidability Results,” Collected Works Volume II, Publications 1938-1974(S. Fefferman, J. W. Dawson, Jr., S. C. Kleene, G. H. Moore, and R. M. Soloway, eds.), New York: Oxford University Press, 1972/1990 pp. 305-306.
[15]	S. Bringsjord, O. Kellett, A. Shilliday, J. Taylor, Bram van Heuvein, Y. Yang, J. Baumes, and K. Ross, “A New Gödelian Argument for Hypercomputing Minds Based on the Busy Beaver Problem,” Applied Mathematics and Computation, 176(2), 2006 pp. 516-530. DOI Link: dx.doi.org/10.1016/j.amc.2005.09.071
J. Hertel, “Computing the Uncomputable Rado Sigma Function,” The Mathematica Journal, 2011. dx.doi.org/doi:10.3888/tmj.11.2-8.

About the Author

Joachim Hertel’s main area of research includes quantum computation and the theory of computability. Hertel’s special interest is in the general topic “Minds and Machines”, particularly the question of what role Rado’s function and Chaitin’s number play in this context.

Joachim Hertel
50 Main St, STE 1000
White Plains, NY,10606
jhertel@h-star.com