Skelet: Difference between revisions
(→Translated Cycler Periods: Add caveat about there potentially being other TCs.) |
m (fix sort) |
||
| (2 intermediate revisions by 2 users not shown) | |||
| Line 243: | Line 243: | ||
!Offset | !Offset | ||
|- | |- | ||
| 1 || <math>\approx 5.42 \times 10^{51}</math> || 8468569863 || -107917 | | 1 ||data-sort-value="5.42e51"| <math>\approx 5.42 \times 10^{51}</math> || 8468569863 || -107917 | ||
|- | |- | ||
| 2 || 15055 || 4328 || 74 | | 2 || 15055 || 4328 || 74 | ||
| Line 259: | Line 259: | ||
| 25 || 6354 || 589 || 23 | | 25 || 6354 || 589 || 23 | ||
|} | |} | ||
While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by | While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by direct simulation. | ||
This list is not necessarily exhaustive, it is possible that some of the other Skelet machines are also Translated Cyclers with very large start step or periods, but were proven infinite using a [[Closed Set]] method. | This list is not necessarily exhaustive, it is possible that some of the other Skelet machines are also Translated Cyclers with very large start step or periods, but were proven infinite using a [[Closed Set]] method. | ||
| Line 265: | Line 265: | ||
== References == | == References == | ||
<references/> | <references/> | ||
Latest revision as of 03:07, 9 July 2025
Georgi Ivanov Georgiev (aka Skelet) was a Busy Beaver hunter who attempted to prove BB(5) in the early 2000s.
bbfind
In 2003, he announced his results on his webpage in which he shared his code bbfind (a 6000 line Pascal program) which he claimed enumerated 150M 5-state TMs and reduced them down to 164 holdouts (he called them "nonregular machines"). After manually analyzing these 164 nonregular machines he reduced it to 43 holdouts which he called "hardly nonregular" (HNR) which were not solvable by his program nor by hand. These 43 HNR TMs became famous examples of hard TMs to prove and these TMs began to be named by their place on this list (such as Skelet 1 and Skelet 17).
Due to the length and lack of comments in bbfind's source code, Skelet's work is not believed to have been independently verified.[1] It is now known that all 43 of these holdouts do not halt. Other work done in bbfind includes computing the correct value of BB(4) and for "RTM(5)" (the set of all "Reversal Turing Machines").
Skelet's 43 HNR TMs
- Skelet's original list: https://skelet.ludost.net/bb/nreg.html
- bbchallenge.org list: https://bbchallenge.org/skelet (canonically numbers the TMs)
- More info on some of Skelet's 43 TMs: https://discuss.bbchallenge.org/t/proving-bb-5-in-coq/225/6
| Skelet # | Skelet machine code | Zoology | Proof by Coq-BB5 |
|---|---|---|---|
| 1 | 1LC1LE_---1LD_1RD0LD_1LA1RE_0LB0RC (bbch)
|
Translated cycler[2] | TABLE_BASED_SPORADIC |
| 2 | 1LC0RE_---0RC_1RD0LA_1RA1RD_1LA0RB (bbch)
|
Translated cycler[3] | TABLE_BASED_NG_3_6 |
| 3 | 1LC0RA_---1LE_1RD0LB_1RA1RC_0LC1LD (bbch)
|
TABLE_BASED_NG_3_6 | |
| 4 | 1LC0RD_---0LE_1RD1LC_1LE1RA_1LB0LD (bbch)
|
TABLE_BASED_NG_3_2 | |
| 5 | 1LC1LA_---0LD_1RD0LE_1LA0RC_1RC0LB (bbch)
|
Translated cycler[3] | TABLE_BASED_NG_3_6 |
| 6 | 1LC0RB_---0RD_1LD0RA_1RE0LC_1RC1RE (bbch)
|
Translated cycler[3] | TABLE_BASED_NG_3_6 |
| 7 | 1LC0RB_---1RE_1LD1LA_1RA0LD_0RA1RC (bbch)
|
TABLE_BASED_NG_3_6 | |
| 8 | 1LC0RB_---0RC_1LD0LC_0RE1LC_0RA1RE (bbch)
|
TABLE_BASED_RWL_15_2 | |
| 9 | 1LC1RD_---0LC_1RA1LC_1RE0RA_1LB0LE (bbch)
|
TABLE_BASED_DNV_12 | |
| 10 | 1LC0LA_---0LC_0RD1LA_1LB1RE_1RD0RE (bbch)
|
Double Fibonacci counter[4] | TABLE_BASED_SPORADIC |
| 11 | 1LC0LA_---0RA_0RD1LA_0RE1RD_1LA0RB (bbch)
|
TABLE_BASED_RWL_15_2 | |
| 12 | 1LC0LE_---1LE_0RD1LA_0LA1RC_1RC0LB (bbch)
|
NGRAM_CPS_IMPL1_params_6_2_2_3200 | |
| 13 | 1LC0RB_---1RA_0LD1RE_0RE1LC_1RC0RA (bbch)
|
NGRAM_CPS_IMPL1_params_6_2_2_3200 | |
| 14 | 1LB---_1RC0RE_1LD0RB_0LD1LA_0RC0LA (bbch)
|
Translated cycler[3] | TABLE_BASED_Lp1 |
| 15 | 1LB---_1LC1RB_1RD1LE_1RB0RD_1LA0LC (bbch)
|
Shift overflow counter[5] | TABLE_BASED_SPORADIC |
| 16 | 1LB---_0RC1LD_1RD1RC_1LE0LE_0LA0RB (bbch)
|
TABLE_BASED_DNV_11 | |
| 17 | 1LB---_0RC1LE_0RD1RC_1LA1RB_0LB0LA (bbch)
|
Dekaheptoid | TABLE_BASED_SPORADIC |
| 18 | 1LB---_0LC0RD_1LD0RE_1LE0LA_1RC0RD (bbch)
|
Translated cycler[3] | TABLE_BASED_RWL_19_2 |
| 19 | 1LB---_0LC0LB_1RC0RD_1LA0RE_0RA0RE (bbch)
|
TABLE_BASED_DNV_10 | |
| 20 | 1LB---_0LC1LD_0RD1LC_1RE0LA_1LA0RE (bbch)
|
Bouncer[6] | TABLE_BASED_RWL_20_2 |
| 21 | 1LC1LE_1LA---_1RD0RE_1RB1RE_1RC0LA (bbch)
|
Bouncer[6] | TABLE_BASED_RWL_10_3 |
| 22 | 1LC0LE_1RA---_1RD0LA_0RD1RB_0LC0RB (bbch)
|
Translated cycler[3] | TABLE_BASED_Lp1 |
| 23 | 1LC0RC_0LD---_1RD0LE_1LC0RE_1RA1LB (bbch)
|
NGRAM_CPS_IMPL1_params_6_2_2_3200 | |
| 24 | 1LC1LA_1RE---_1RD0RD_0RB0LE_0LA1RC (bbch)
|
TABLE_BASED_DNV_10 | |
| 25 | 1LC0RA_1LA---_1RD1LE_1RA0RD_0LE0RB (bbch)
|
Translated cycler[3] | NGRAM_CPS_IMPL1_params_2_2_2_1600 |
| 26 | 1LC1RE_1RD---_1LD0LC_1RA1LD_1RB0RA (bbch)
|
Shift overflow counter[5] | TABLE_BASED_SPORADIC |
| 27 | 1LC0RE_0LE---_1LD0LB_1RA0LA_0RA1RE (bbch)
|
NGRAM_CPS_IMPL1_params_2_3_3_1600 | |
| 28 | 1LC0LE_1RD---_1LB1LE_1RA1RE_1LA0RD (bbch)
|
Bouncer[6] | TABLE_BASED_RWL_10_3 |
| 29 | 1LC0RD_0LA---_1RA0LD_1RE1LB_1LC0RC (bbch)
|
NGRAM_CPS_IMPL1_params_6_2_2_3200 | |
| 30 | 1LC0LE_1RC---_0RD1LA_1RA0RE_1RB0LE (bbch)
|
TABLE_BASED_NG_6_11 | |
| 31 | 1LC0RB_0RE---_0LD1LC_1LE0LC_1RA0RC (bbch)
|
TABLE_BASED_RWL_17_2 | |
| 32 | 1LC0RE_0LC---_0LD0LB_1RD0RA_1RA1LD (bbch)
|
NGRAM_CPS_IMPL1_params_2_2_2_1600 | |
| 33 | 1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LE (bbch)
|
Shift overflow counter[5] | TABLE_BASED_SPORADIC |
| 34 | 1LC1RD_1RE---_0LD0LC_1RB0RA_1RA1LA (bbch)
|
Shift overflow counter[5] | TABLE_BASED_SPORADIC |
| 35 | 1LC1RD_1RE---_0LD0LC_1RB0RA_1RA0RA (bbch)
|
Shift overflow counter[5] | TABLE_BASED_SPORADIC |
| 36 | 1LC1RE_1RD---_0LD0LC_1RB1LA_1LD0RA (bbch)
|
TABLE_BASED_NG_2_2 | |
| 37 | 1LC0RB_1RC---_0LD0RD_1RA0LE_1LD1LE (bbch)
|
NGRAM_CPS_IMPL1_params_2_2_2_1600 | |
| 38 | 1LC0LC_1LD---_0LB0RD_0RE1LA_1RA1RE (bbch)
|
TABLE_BASED_DNV_10 | |
| 39 | 1LB1LD_1RC---_1RE1RD_1LE0RC_1LA0LD (bbch)
|
Bouncer[6] | TABLE_BASED_RWL_10_3 |
| 40 | 1LB0LA_1RC---_0RC0RD_1LE0LB_0LE1LA (bbch)
|
TABLE_BASED_DNV_3 | |
| 41 | 1LB0RA_1LC---_0LD1RE_1LE0LA_1RC0RA (bbch)
|
TABLE_BASED_NG_6_11 | |
| 42 | 1LB0RE_1LC---_0LD0LC_1RD0RA_0RB0RE (bbch)
|
TABLE_BASED_DNV_9 | |
| 43 | 1LB0RA_0LC---_1RC1LD_1LE1RA_0LB0RD (bbch)
|
TABLE_BASED_NG_7_10 |
Translated Cycler Periods
Several of Skelet's holdouts were translated cyclers, here are the parameters for them. Start step is the earliest step that the cycle starts at. Period is the step count per cycle. Offset is the translation shift along tape each period (positive to the right, negative to the left).
| Skelet # | Start Step | Period | Offset |
|---|---|---|---|
| 1 | 8468569863 | -107917 | |
| 2 | 15055 | 4328 | 74 |
| 5 | 15063 | 4328 | -74 |
| 6 | 24149 | 4328 | 74 |
| 14 | 4265 | 91995 | 543 |
| 18 | 6102 | 1143 | -19 |
| 22 | 4663 | 91995 | -543 |
| 25 | 6354 | 589 | 23 |
While Skelet #1 is technically a Translated Cycler, it requires specialized acceleration to prove this. Whereas all the other cyclers can be demonstrated by direct simulation.
This list is not necessarily exhaustive, it is possible that some of the other Skelet machines are also Translated Cyclers with very large start step or periods, but were proven infinite using a Closed Set method.
References
- ↑ "Story" (section "Skelet's 43 undecided machines").
- ↑ https://www.sligocki.com/2023/03/13/skelet-1-infinite.html
- ↑ 3.0 3.1 3.2 3.3 3.4 3.5 3.6 https://discuss.bbchallenge.org/t/skelet-machines-that-are-translated-cyclers/58
- ↑ https://www.sligocki.com/2023/03/14/skelet-10.html
- ↑ 5.0 5.1 5.2 5.3 5.4 https://www.sligocki.com/2023/02/05/shift-overflow.html
- ↑ 6.0 6.1 6.2 6.3 https://discuss.bbchallenge.org/t/the-30-to-34-ctl-holdouts-from-bb-5/141