Sciweavers

CATS
2007

Analysis of Busy Beaver Machines via Induction Proofs

13 years 6 months ago
Analysis of Busy Beaver Machines via Induction Proofs
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 desc...
James Harland
Added 29 Oct 2010
Updated 29 Oct 2010
Type Conference
Year 2007
Where CATS
Authors James Harland
Comments (0)