Here is an argument of why the algorithm works. This has in mind the go implementation, as opposed to the above python, seeing as the go code is more relevant. Not much is changed besides that a stack is used instead of a queue, making it depth first, and some of the variable names have changed. Let me know if this is not what you asked for; I’m happy to try and shorten it, or fill in other details that I breezed over.
The algorithm works backwards from all halting states to see if there is no possible way to reach a halting state. Abstractly, we are exploring a digraph where each node is a local configuration, that is a small section of the tape where no assumptions are made about the rest of the tape (put another way, each node represents all possible extensions of the local section of the tape). This differs from the usual notation wherein the rest of the unseen tape is assumed to be zeroes. The goal of the algorithm is to show that this digraph of predecessor configurations is self-contained finite by exploring it entirely. Technically we also need to show that the digraph does not contain a local configuration of state A and only zeroes on the tape, however I do not imagine that we will run the decider for 47 million steps on every undecided machine, and we already know that the digraph doesn’t contain a local configuration of the starting state if it has size less than 47 million.
Concretely, the algorithm implements a depth first search on the digraph (limited by a search depth). stack
contains the current leaves of our search. seenStates
stores the configurations we’ve seen already so that we don’t repeat unnecessary computation. That is, once we’ve found all of the predecessors of a configuration, we don’t need to look at it again.
To start the search, we add all of the local configurations consisting of a state s along with a single cell of exposed tape with bit b, where (s b) is an undefined transition. Next, as long as there are possible local configurations that we haven’t checked yet, we take the next one from the stack, and find all of the predecessor configurations. We do that by looking at all state + bit combinations (s’, b’) that transition to the current state s, and for each one checking that the place where that transition moved from (i.e. if (s’ b’) moves right then we look at the cell to the left of the current head), has the same bit as what the transition (s’ b’) writes. If the current head is at the far left (respectively right) and (s’ b’) moves right (respectively left) then the local configuration expands in scope; this is always acceptable as we made no assumptions about the tape outside of the scope of the local configuration.
For example, if we are in state A with tape 000[1]101, then we want any transition rules that transition to A and either
1. move right and write 0, or
2. move left and write 1
Then, for each pair (s’ b’) satisfying this, we add
1. s’: 00[b’]1101 or
2. s’: 0001[b]01
to stack
respectively, if it is not in seenStates
.
If this process terminates in 47 million steps or fewer, we know that the halting states are in a different connected component in the configuration graph than the starting configuration (A with all 0s), and so it is not possible for the machine to halt.