#5807483 infinite by CTL

@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!

1 Like

@cosmo has placed a bet that this TM is a Translated Cycler (Discord) but only after running for a very long time. So the next challenge is, can anyone prove that that is true or false based on this (much simplified) description of behavior?

1 Like

Playing around a little more, we can simplify this CTL further into .* C> (0|11)* if we allow unbounded (but finite) numbers of steps between elements of the CTL. Specifically:

   00 A> 00    -(  7)->     1 C> 011
0 1^n C> 11    -(n+2)->     1 C> 0^n 11
      C> 011   -(  3)->   001 C>
      C> 0011  -( 10)->  1011 C>
0 1^n C> 000   -(n+8)->     1 C> 0^n 011

(Where n is any non-negative integer).

1 Like

Really interesting work, thank you @sligocki and @Frans_Faase :pray:

Can’t wait to be proven wrong on my bet ahah