Turing machines deciders, part I

TL;DR

This work surveys multiple non-halting deciders used in the Busy Beaver challenge for five-state Turing machines, culminating in a Coq-formalized proof of S(5) = 47,176,870. It introduces a spectrum of techniques—Cyclers, Translated Cyclers, Backward Reasoning, Halting Segment, Finite Automata Reduction (FAR), and Bouncers—to certify non-halting by deriving regular or finite-segment structures that preclude halting. Each method provides formal correctness arguments and practical implementations (often in Go, Rust, C++, or Dafny) with verifiers and certificates, illustrating both theoretical foundations and real-world scalability. The work lays a foundation for Part II, which documents the deciders that were actually used in the Coq proof, while Part I collects complementary techniques that broaden the toolkit for analyzing Turing machines beyond the specific BB(5) result.

Abstract

The Busy Beaver Challenge (or bbchallenge) aims at collaboratively solving the following conjecture: "$S(5) = 47{,}176{,}870$" [Radó, 1962], [Marxen and Buntrock, 1990], [Aaronson, 2020]. This conjecture says that if a 5-state Turing machine runs for more than 47,176,870 steps without halting, then it will never halt -- starting from the all-0 tape. Proving this conjecture amounts to deciding whether 181,385,789 Turing machines with 5 states halt or not -- starting from the all-0 tape [bbchallenge, 2025]. To do so, we write $\textit{deciders}$: programs that take as input a Turing machine and output either HALT, NONHALT, or UNKNOWN. Each decider is specialised in recognising a particular type of non-halting behavior. After two years of work, the Busy Beaver Challenge achieved its goal in July 2024 by delivering a proof of "$S(5) = 47{,}176{,}870$" formalised in Coq [bbchallenge, 2025]. In this document, we present deciders that were developed before the Coq proof and which were mainly not used in the proof; nonetheless, they are relevant techniques for analysing Turing machines. Part II of this work is the decider section of our paper showing "$S(5) = 47{,}176{,}870$" [bbchallenge, 2025], presenting the deciders that were used in the Coq proof.

Figures (10)

• Figure 1: Space-time diagrams of the 30 first steps of bbchallenge's machines #279,081 (left) and #4,239,083 (right) which are both "Cyclers": they eventually repeat the same configuration for ever. Access the machines at https://bbchallenge.org/279081 and https://bbchallenge.org/4239083.
• Figure 2: Example "Translated cycler": 45-step space-time diagram of bbchallenge's machine #44,394,115. See https://bbchallenge.org/44394115. The same bounded pattern is being translated to the right forever. The text annotations illustrate the main idea for recognising "Translated Cyclers": find two configurations that break a record (i.e. visit a memory cell that was never visited before) in the same state (here state D) such that the content of the memory tape at distance $L$ from the record positions is the same in both record configurations. Distance $L$ is defined as being the maximum distance to record position 1 that was visited between the configuration of record 1 and record 2.
• Figure 3: More complex "Translated cycler": 10,000-step space-time diagram (no state colours) of bbchallenge's machine #59,090,563. See https://bbchallenge.org/59090563.
• Figure 4: Applying backward reasoning on bbchallenge's machine #55,897,188. (a) 10,000-step space-time diagram of machine #55,897,188. The forward behavior of the machine looks very complex. (b) Transition table. (c) We are able to deduce that the machine will never halt thanks to only 3 backward reasoning steps: because a contradiction is met, it is impossible to reach the halting configuration in more than 3 steps -- and, by (a), the machine did not halt in 10,000 steps starting from all-0 tape.
• Figure 5: Halting Segment graph for the 3-state machine https://bbchallenge.org/1RB1RC_0LA0RA_0LB--- and segment size 2, see Definition \ref{['def:hs-graph']}. Nodes of this graph correspond to segment configurations (Definition \ref{['def:hs-conf']}), i.e. configurations of the machine on a finite segment (here, of size 2). In a node, the machine's head position is represented between brackets and the symbol - represents the outside of the segment (either to the left or to the right). Nodes where the machine's head is within the segment (circle shape) only one have child corresponding to the next step of the machine and nodes where the head is outside of the segment (diamond shape) may have multiple children corresponding to all the theoretically possible ways (deduced from the machine's transition table) that the machine can enter the segment back or continue to stay out of it. In order to improve readability, edges that revisit a node are dotted. The machine presented here does not halt because the halting nodes (red outline) that are reachable from the initial nodes (blue outline) do not cover all the positions of the segment (there is no halting node for any of the two internal positions of the segment), by contraposition of Theorem \ref{['th:hs']}.

Theorems & Definitions (73)

• Example 2.1
• Theorem 2.1
• proof
• Corollary 2.1
• proof
• Definition 3.1: record-breaking configurations
• Definition 3.2: Distance $L$ between record-breaking configurations
• Lemma 3.1
• proof
• Theorem 3.1