The 30 to 34 CTL holdouts from BB(5)

I’ve been building a library of Finite Automata Reduction proofs for 5-state TMs: in this repo with complete automta and some more info, and in the original shorter Decider Verification File format on Dropbox (index/DVF).

A remarkable finding has been that nearly all infinite 5-state TMs have proofs in this format. In fact, this proof library covers the entire undecided index with just 34 exceptions. (I plan to expand it to cover all previously decided machines too. The bbchallenge community is still working on a way to find all of these proofs from scratch, quickly, using accepted deciders.)

4 of these are bouncers of the form decided by Tony’s decider – thus they’re known to be provable by CTL, and there’s just some computation needed to find acceptably small proofs. It’s possible some of these will hit limitations of the binary DVF format. They are these three things and Skelet 20.

Those aren’t so interesting, but for the rest, I’ve compiled a holdout-zoology.zip file (945.9 KB) classifying them, with seed IDs and diagrams and links to analyses. There’s also a catalog showing my classification maps onto Skelet’s.

(The two "pointy-wide’ machines in this zip file are now historical. I wrote more about them here.)

The rest are holdouts for Skelet’s program and all of the community’s deciders to date. Most have proofs or strong heuristic arguments that CTL solutions (specifically, finding a regular language separating the set of reachable configurations from the set of halting configurations) are impossible

Skelet 1 is believed to be a translated cycler, thus theoretically CTLable, but with a preposterously long period and little hope of having a solution in this proof format.

Skelet 10 is manually proven by Dan Briggs and with a neat interpretation by Shawn Ligocki. There’s a heuristic argument that finite-state classifiers are insufficient – to analyze a configuration requires some counting.

5 more Skelet machines are classified as shift-overflow counters by Shawn, and believed to be proven. There’s similarly a heuristic argument about these.

Skelet 17 is being analyzed on Discord – it looks like the case is nearly cracked.

The “counter-balanced” class maps onto a subset of what Skelet calls “Shift Recursive” machines. Konrad Deka has analyzed one on Discord, giving a quick proof that it’s infinite and a strong heuristic argument that it’s not CTLable (also due to a need to count).

The “counter-inverted” class also maps into Skelet’s “Shift Recursive” class. Skelet wrote a non-halting argument for one.

The “cubic-finned” class effectively operates on a pair of unary numbers. @Iijil analyzed one and provided the first known proof that a naturally occurring TM has reachable and halting configuration sets which no regular language can separate.

The “cubic-helix” class is expected to have a similar obstacle (and easy proof of infinitude), though this hasn’t been done yet.

If interested, check out the zip file. In addition, here are the machine strings:

1RB---_0LC1LC_1LD1LB_1RE1RD_0LA0RE
1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA
1RB0LD_1RC0RA_0RD0RB_1LE---_1LB0LC
1RB0LE_1RC1RB_1RD1LC_0LE0RB_---1LA
1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB
1RB---_0RC1LB_1RD1RC_1LE1LD_0RA0LE
1RB0RC_1LC0LE_0LD0LB_1RA---_1LB0RD
1RB---_0RC1LC_1RD1RC_1LE1LD_0RA0LE
1RB---_0RC1LD_1RD1RC_1LE1LB_0RA0LE
1RB---_0RC1RC_1RD1RB_1LE1LD_0RA0LE
1RB---_0RC1RC_1RD1RC_1LE1LD_0RA0LE
1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE
1RB0RE_0RC0RA_1LD---_1LA0LB_1RA0LC
1RB0RE_1RC1RE_1LD---_1LA1LE_1RA0LD
1RB1LA_0LC0RE_---1LD_1LA0LC_1RA1RE
1RB1LA_0LC0RE_---1LD_1RA0LC_1RA1RE
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA
1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE
1RB1LC_1LB1RA_0LE0LD_0RA1RD_---0LC
1RB1LC_1LC1RA_0LE0LD_0RA1RD_---0LC
1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LA
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1LE
1RB1RA_1LC1LB_0RD0LC_1RE---_0RA1RA
1RB1RA_1LC1LE_0RD0LC_1RE---_0RA1LB
1RB1RA_1RC1LB_0LD0RA_1RA1LE_---0LD
1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC
1RB1RD_1LC0LD_1LE1LD_1LB0RA_1RA---
1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC
1RB1RD_1LC---_1LE1LD_1RE0LC_1RA0RD
1RB1RE_1LC1LB_0RD0LC_1LE---_0RA1RA
1RB1RE_1LC1LB_0RD0LC_1RE---_0RA1RA
1RB1RE_1LC1RB_0RA0LD_1LB1LD_---0RA
5 Likes

Commenting specifically to call out other decider authors whose work was used in the CTL library construction: @Iijil (GitHub - Iijil1/Bruteforce-CTL: An attempt to proof that a turing machine doesn't halt by finding a closed tape language using bruteforce), @Nathan-Fenner (GitHub - Nathan-Fenner/bb-simple-n-gram-cps), @TonyG (bbchallenge/Bouncers at main · TonyGuil/bbchallenge · GitHub), savask (The closed position set decider, reverse-engineered from Skelet's program · GitHub).
Update: Skelet too, now.
Indirectly, also @Frans_Faase (GitHub - FransFaase/SymbolicTM: Symbolic Turing Machine for Busy Beaver problems).
You are coauthors of this proof library.
I plan to release polished conversion utilities at some point, at least for most of these. (n-gram CPS has to be modified before it can emit convertible proof data – but the conversion is very smooth after that.)

1 Like

As of February 2024, here is the current situation:

Of the 32632 remaining machines, @UncombedCoconut has undocumented code that produces easy to verify certificates for all but 34 of them. These certificates have been verified by multiple independent sources, and you can find the repository containing all 32598 certificates here. The only reason why they are not counted as official is because there is not yet formal documentation of how to reproduce these certificates - otherwise, we can safely say that they’re counted.

Of the 34 remaining machines, 31 of them can be placed into six specific categories. Five of the six categories, as well as two of the three holdouts, have deciders and/or formal proofs:

This leaves the “cubic finned” category as well as Skelet #17 which have yet to be verified. For Skelet #17 I have a proof, but preferable would be for it to be formalized or automated.

4 Likes

Possibly slightly off topic, it would be good to give a clear Skelet status list here. UncombedCoconut pointed me on discord to his list: https://cdn.discordapp.com/attachments/960643023530762341/1073801475291099207/skelet_annotated_v2.txt and apparently all undecideds have been since decided, #1 and #17 manually and #3 and #7 by automata as mentioned by Justin on Discord. The list is reproduced here:

1	1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC	** UNDECIDED **
2	1RB0LD_1LC0RA_1LA1LC_1RA0LE_---0LB	Decided by: bbchallenge.org
3	1RB0LA_1LC0RD_1LA1LB_---1RE_0RB1RC	** UNDECIDED ** ~7
4	1RB0LC_1LC1RB_1RD1LA_1RE0RC_---0RD	Decided by: Justin, [CPS untested]
5	1RB1RA_1LC0RD_1RA0LB_1LB0RE_---0RC	Decided by: bbchallenge.org
6	1RB0LE_1RC0LA_1LD0RB_1LB1LD_---0LC	Decided by: bbchallenge.org
7	1RB0LD_1RC1RA_1LA0RC_---1LE_0LA1LB	** UNDECIDED ** ~3
8	1RB0LE_1RC0RB_0LD1RB_0LA1LD_---0LB	Decided by: Justin, bouncers, shawn_oct3, [CPS untested]
9	1RB1LC_1LA1RB_1LD0LA_1RE0RD_---0RB	Decided by: Justin, [CPS untested]
10	1RB0RA_0LC1RA_1RE1LD_1LC0LD_---0RB	[manual: D. Briggs]
11	1RB0RA_0LC1RA_0LD1LC_1RA0LE_---0LA	Decided by: Justin, bouncers, shawn_oct3, [CPS untested]
12	1RB0RD_0LC1RA_0RA1LB_1LB0RE_---1RD	Decided by: Justin, [CPS untested]
13	1RB0LE_0RC1LD_0LD1RB_1LB0LA_---1LA	Decided by: Justin, [CPS untested]
14	1RB---_1LC0LE_1RD0LB_0RD1RA_0LC0RA	Decided by: bbchallenge.org
15	1RB---_1RC1LB_1LD1RE_1LB0LD_1RA0RC	[manual: S. Ligocki]
16	1RB---_0LC1RD_1LD1LC_1RE0RE_0RA0LB	Decided by: Justin, [CPS untested]
17	1RB---_0LC1RE_0LD1LC_1RA1LB_0RB0RA	** UNDECIDED **
18	1RB---_0RC0LD_1RD0LE_1RE0RA_1LC0LD	Decided by: bbchallenge.org
19	1RB---_0RC0RB_1LC0LD_1RA0LE_0LA0LE	Decided by: Justin, [CPS untested]
20	1RB---_0RC1RD_0LD1RC_1LE0RA_1RA0LE	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
21	1RB1RD_1LC0LD_1LE1LD_1LB0RA_1RA---	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
22	1RB0RE_1LC0RA_0LC1LD_1LA---_0RB0LD	Decided by: bbchallenge.org
23	1RB0LB_1LC0RD_1RB0LD_1LA1RE_0RC---	Decided by: Justin, [CPS untested]
24	1RB1RA_1LC0LC_0LE0RD_0RA1LB_1LD---	Decided by: Justin, [CPS untested]
25	1RB0LA_1LC1RD_1LA0LC_0RD0LE_1RA---	Decided by: bbchallenge.org
26	1RB1LD_1RC0RB_1LA1RC_1LE0LA_1LC---	[manual: S. Ligocki]
27	1RB0LD_1RC0RE_1LA0RA_0LA1LD_0RD---	Decided by: Justin, [CPS untested]
28	1RB0RE_1RC1RE_1LD---_1LA1LE_1RA0LD	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
29	1RB0LC_1LA0RC_1LD1RE_1RB0LB_0RA---	Decided by: Justin, [CPS untested]
30	1RB0RD_0LC1RA_1LA0LD_1LE0RD_1LB---	Decided by: CPS:(w,s)≤(54,27)
31	1RB0LE_0RC1RB_1RD0RB_1LA0LB_0LD---	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
32	1RB0LD_0RC0RE_1LC0LA_1LA1RC_0RB---	Decided by: Justin, [CPS untested]
33	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RE	[manual: S. Ligocki]
34	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA1RA	[manual: S. Ligocki]
35	1RB1LC_0RC0RB_1LD0LA_1LE---_1LA0LA	[manual: S. Ligocki]
36	1RB1LE_0RC0RB_1LD1RA_1LC---_1RC0LA	Decided by: Justin, [CPS untested]
37	1RB0LE_0RC0LC_1LA0RD_1RC1RD_1LB---	Decided by: Justin, [CPS untested]
38	1RB0RB_0RC0LD_1RD---_0LE1RA_1LA1LE	Decided by: Justin, [CPS untested]
39	1RB1RD_1LC---_1LE1LD_1RE0LC_1RA0RD	Decided by: bouncers, CPS:(w,s)≤(54,27), shawn_oct3
40	1RB0RA_1LC---_0LC0LD_1RE0RB_0RE1RA	Decided by: Justin, [CPS untested]
41	1RB0LA_1RC---_0RD1LE_1RE0RA_1LC0LA	Decided by: CPS:(w,s)≤(54,27)
42	1RB0LE_1RC---_0RD0RC_1LD0LA_0LB0LE	Decided by: Justin, [CPS untested]
43	1RB0LA_0RC---_1LC1RD_1RE1LA_0RB0LD	Decided by: CPS:(w,s)≤(54,27)

I was curious about some things of the list:

  • what is Justin, [CPS untested]? Is there a database or paintext list somewhere of all the machines that were proven by that decider, possibly with the DFA or DFA size?
  • what is CPS:(w,s)≤(54,27)
  • what is shawn_oct3. Presumably some work by Sligoki.

The rest I understand.

It is also interesting that some of the machines that were not caught by deciders as mentioned at: The 30 to 34 CTL holdouts from BB(5) - #3 by chxu were decided by Skelet apparently. It would be interesting to find out if this was a bug on his side, of if he had some specialized deciders for those cases.

I also started to compile a more direct HTML Skelet list with links for copy paste at: halting problem - What is the smallest Turing machine where it is unknown if it halts or not? - Theoretical Computer Science Stack Exchange and I’ll update that as I understand things a bit more clearly.

| # | #BBC | proofs | comments |
|-|-|-|-|-|
| 1 | 68329601 | TC: Coq, manual | |
| 2 | 55767995 | TC: BBC decider | |
| 3 | 5950405 | FAR: decider | |
| 4 | 6897876 | FAR: BBC decider | |
| 5 | 60581745 | TC: BBC decider | |
| 6 | 58211439 | TC: BBC decider | |
| 7 | 7196989 | FAR: decider | |
| 8 | 7728246 | FAR: decider, manual | |
| 9 | 12554268 | FAR: decider, manual | |
| 10 | 3810716 | manual by D. Briggs | interpretation |
| 11 | 3810169 | FAR: decider, manual | |
| 12 | 4982511 | FAR: decider, manual | |
| 13 | 7566785 | FAR: decider, manual | |
| 14 | 31357173 | TC: BBC decider | |
| 15 | 2204428 | SOC: manual | |
| 16 | 20569060 | FAR: decider | |
| 17 | 1365166 | manual by C. Xu | |
| 18 | 15439451 | TC: BBC decider | |
| 19 | 14536286 | FAR: decider | |
| 20 | 347505 | BNC | |
| 21 | 9980689 | BNC, manual by D. Briggs | |
| 22 | 45615747 | TC: BBC decider | |
| 23 | 6237150 | FAR: BBC decider |
| 24 | 60658955 | FAR: decider | |
| 25 | 47260245 | TC: BBC decider | |
| 26 | 13134219 | SOC: manual by S. Ligocki | |
| 27 | 7163434 | FAR: decider | |
| 28 | 5657318 | BNC, manual by D. Briggs | |
| 29 | 6626162 | FAR: BBC decider | |
| 30 | 4986661 | FAR: decider | =41 |
| 31 | 56967673 | manual by D. Briggs | |
| 32 | 6957734 | FAR: BBC decider, manual | |
| 33 | 11896833 | SOC: manual by S. Sligocki | |
| 34 | 11896832 | SOC: manual by S. Sligocki, Coq | |
| 35 | 11896831 | SOC: manual by S. Sligocki, Coq | |
| 36 | 13609549 | FAR: BBC decider | |
| 37 | 7512832 | FAR: BBC decider | |
| 38 | 35771936 | ? | |
| 39 | 9914965 | BNC, manual by D. Briggs | |
| 40 | 3841616 | FAR: BBC decider | |
| 41 | 5915217 | FAR: decider | =30 |
| 42 | 57874080 | FAR: decider | |
| 43 | 5878998 | FAR: decider |

1 Like

Thanks for compiling all that.
Here’s a refreshed picture of which known deciders (or verifiers, in case of large numbers in the “FAR” columns) can get the various Skelet machines.
In this version, I’ll leave out the above shawn_oct3 category (which referred to results sligocki shared here). @sligocki and @univerz both have strong rule-proving programs which get some of the Skelet machines.

CPS refers to closed-position-set. At this point, the state of the art is what’s implemented in savask’s and univerz’s versions. The triplet of numbers specifies left/central/right segment sizes which work; the former program details in its comments what this means.

In the FAR column, I give the number of DFA states needed and show which way the DFA reads the tape. (In some cases I only have bounds on the solution size. If you see that, FAR is not the best method to use anyway!)

The FAR-MitM column gives the common left- and right-DFA size for a “meet-in-the-middle DFA” solution.
This is explained in my decider readme; the bbchallenge-proofs repo also has a draft write-up (but it’s commented out). Again, sometimes I only have bounds.

# Seed TranslatedCyclers Bouncers CPS FAR FAR-MitM
1 68329601
2 55767995 :smiley_cat: ≤12 12
3 5950405 17 ← 18
4 6897876 no? 5 → 10
5 60581745 :smiley_cat: ≤12 12
6 58211439 :smiley_cat: ≤12 12
7 7196989 17 → 18
8 7728246 :smiley_cat: 10 → 11
9 12554268 no? 13 → <∞
10 3810716
11 3810169 :smiley_cat: 10 → 10
12 4982511 7 → 13
13 7566785 7 ← 13
14 31357173 :smiley_cat: <∞ <∞
15 2204428
16 20569060 11 → 12
17 1365166
18 15439451 :smiley_cat: 1-18-20 <∞ <∞
19 14536286 9 → 11
20 347505 :smiley_cat: 8-24-7 <∞ <∞
21 9980689 :smiley_cat: 12-16-14 <∞ <∞
22 45615747 :smiley_cat: <∞ <∞
23 6237150 18-24-17 6 → 9
24 60658955 11 → 11
25 47260245 :smiley_cat: 16-5-4 2 5
26 13134219
27 7163434 7-7-7 7 → 9
28 5657318 :smiley_cat: 16-16-17 <∞ <∞
29 6626162 18-24-17 6 → 9
30 4986661 20-20-19 41 ← <∞
31 56967673 :smiley_cat: 1-17-9 195 ← <∞
32 6957734 no? 1 → 3
33 11896833
34 11896832
35 11896831
36 13609549 5 → 7
37 7512832 5 ← 8
38 35771936 11 → 11
39 9914965 :smiley_cat: 16-12-24 <∞ <∞
40 3841616 4 → 4
41 5915217 20-20-20 40 → <∞
42 57874080 9 → 11
43 5878998 14-14-14 50 → <∞
1 Like

Skelet got his “bbfind” program to solve most of the BB(5) problem space. He classified the remaining TMs on his nonregular machines page. This includes not only the numbered Skelet machines, but also various machines he considered easy to prove by hand. In this thread’s first post, I mention how Skelet’s categories map onto the informal zoology I used (“cubic helix” etc.). Does that clarify?

Belated realization: “these three things” are Skelet #28, #39, and #21, respectively. They’re still very annoying CTL-library gaps, because they’re both bouncers and CPS-able. (This is also true of Skelet #20, but it’s much harder for both of these deciders than the other three.)

Thank you very much for your message and contribution!

You are right, Skelet - bbchallenge is not up to date with the most recents proofs and it’s because it is only updated after each official release (approx twice a year), and most new proofs happened after the last release (April 23) :smiley:

I also started to compile a more direct HTML Skelet list with links for copy paste at: halting problem - What is the smallest Turing machine where it is unknown if it halts or not? - Theoretical Computer Science Stack Exchange and I’ll update that as I understand things a bit more clearly.

Thank you very much for making bbchallenge visible with your very detailed answer to that thread!

Hi there! I found myself needing something to do to pass some time on the train, and so I formalized the proof of Skelet #10 in Coq, following Shawn’s exposition. I find that this one in particular is nicely succinct and readable, especially compared to the other individual machines I’ve formalized.

@cirosantilli, you’ll probaby want to update your post.

Also, I’d like to caution against counting machines like Skelet #26 or #33 as proven. The linked post is merely a proof sketch, and Shawn himself calls attention to the gaping hole that is the reset invariant inequality for each of those. I don’t think anyone has ever looked at how hard these particular ones are to prove.

2 Likes

It would be cool if there was a way to attach metadata to specific machines via pull requests that would show up under https://bbchallenge.org/4637626 (e.g. unreviewed informal proof, reviewed informal proof, formal proof). The current review barrier are high, which is good, but on the other hand makes it hard to know the state of the leading edge without searching a bunch of forums. Maybe for bb(6)!

Yes, this is a good idea! I have been considering implementing it for a while, let’s see once we are done with bouncers!

I have updated this post to account for recent efforts. We only have six more machines to verify non-halting!

2 Likes