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 tominimise it where we cannot. We describe our experiments for the n = 4 and n = 5 cases appropriate inductive conjectures.