Finned 3

1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA (bbch), also called Finned #3, is a non-halting irregular BB(5) TM. It belongs to a group of 5 sporadic machines, called finned machines, which had to be individually proven as non-halting in Coq-BB5. It was proven to be irregular in March 2023 by lijil.

Analysis by lijil

With the CTL-deciders proving to be very strong there is the question which machines cannot be proven by it. 10756090 is an example of such a machine. We can prove that there is no regular language that includes all configuration the TM reaches, but rejects all configurations that lead to halting:

Write C(n,m) for (10)^n A0 1^m

Then the TM follows these rules:

C(n,m) → halt, if n+m is odd
C(n,m) → C(((n+m)/2)+1,n+1), if n+m is even
I’ll leave the proof as an exercise for the reader.
We start in C(0,0) and C(n,n) → C(n+1,n+1) for all n, so the machine is infinite and visits C(n,n) for all n.

To see how it behaves with n != m we consider the difference n-m after applying rule 2:
((n+m)/2)+1-(n+1) = (n+m-2n)/2 = -(n-m)/2

So the TM divides the difference of the exponents by 2 (and flips the sign) until the difference becomes odd. Then it halts. This can only go on forever if the difference is 0 to begin with.

Thus C(n,m) → halt, if n!=m

It is impossible for a regular language to separate {C(n,n) for all n} and {C(n,m) for all n!=m}

To finish it off with an argument by savask:
“If there was a regular language containing all non-halting configs of your machine, then we could intersect it with a language (10)* A0 1* and obtain that (10)^n A0 1^n is regular”