Analysis of Busy Beaver Machines via Induction Proofs

Harland, J.

The busy beaver problem is to find the maximum number of 1's that can be printed by an n-state Turing machine of a particular type. A critical step in the evaluation of this value is to determine whether or not a given n-state Turing machine halts. Whilst this is undecidable in general, it is known to be decidable for n _ 3, and undecidable for n _ 19. In particular, the decidability question is still open for n = 4 and n = 5. In this paper we discuss our evaluation techniques for busy beaver machines based on induction methods to show the non-termination of particular classes of machines. These are centred around the generation of inductive conjectures about the execution of the machine and the evaluation of these conjectures on a particular evaluation engine. Unlike previous approaches, our aim is not limited to reducing the search space to a size that can be checked by hand; we wish to eliminate hand analysis entirely, if possible, and to minimise it where we cannot. We describe our experiments for the n = 4 and n = 5 cases appropriate inductive conjectures.

Cite as: Harland, J. (2007). Analysis of Busy Beaver Machines via Induction Proofs. In Proc. Thirteenth Computing: The Australasian Theory Symposium (CATS2007), Ballarat, Australia. CRPIT, 65. Gudmundsson, J. and Jay, B., Eds. ACS. 71-78.

(from crpit.com) (local if available)