@Frans_Faase proved that https://bbchallenge.org/5807483 is infinite by CTL (see: SymbolicTM/BB5807483.txt at main · FransFaase/SymbolicTM · GitHub ) I worked through that machine-generated proof certificate by hand to try to understand more about it, here’s my human-readable summary of the behavior:
Consider the Regex: .* (<D | C> | 0 A> | 01 B>) (0|11)*
This is a Closed Tape Language (CTL) in a general sense. Specifically, we can prove directly that all configs in this set return to the set within a fixed number of steps (max is 10).
The proof, by case analysis mostly comes down to noting the following transitions and seeing how the right sides fit into the CTL Regex. (Note here that X -(n)-> Y means that any config with X at its core transitions to the same config with Y replacing X in n steps):
0 <D --(1)-> 1 C>
1 <D --(1)-> <D 0
C> 0 --(1)-> 0 A>
C> 11 --(1)-> <D 11
0 A> 0 --(1)-> 01 B>
0 A> 11 --(2)-> 001 C>
01 B> 0 --(5)-> <D 011
01 B> 11 -(10)-> 1011 C>
Most of these transitions are trivial (one step), but the last one is a bit more complicated. You can expand all of these multi-step rules into many one-step rules and if you do you roughly get Frans’s original proof.
Finally, note that the starting config is actually a member of this CTL Regex and we can see that no halting configs are in this CTL, so that completes the proof that this TM will never halt!
