Skelet #1: What I Know

Update (13 Mar 2023): Skelet #1 is infinite … we think

Note: Throughout this article I will use @username to refer to users of the bbchallenge.org Discord.

After my post proving Skelet #34 infinite, there was a lot of discussion on the bbchallenge.org Discord about which Skelet machines remained unproven. There is no objective answer, because “proofs” of these machines come in widely varying levels of rigor. But if you take the most liberal/optimistic approach, accepting any time anyone (or any program) claimed to have proven a machine (and accept for example, my hand-wavy “proof sketches” for Skelet #15, #26 and #33 and Dan Briggs’s annotation of Skelet #17 as “easy?”), then there was exactly one Skelet machine which nobody has claimed to have proven. Fittingly it is Skelet #1.¹

The feeling is that this may be the 5-state 2-symbol TM with the most complex behavior. Therefore several of us on Discord have been focussed on analyzing Skelet #1 specifically over the course of the last two weeks. In that time we’ve founds some interesting things about it’s behavior, but it still doesn’t feel like we’re that close to proving it infinite (or halting!). I have been holding off on writing up a post about this TM until I had something conclusive to say … but at this point that may never happen. So instead I will present here what I know, some tools I’ve been using to analyze Skelet #1 and my ideas for ways forward. I hope that this will (A) provide a common language for us to discuss analyzing this TM, (B) teach folks who haven’t understood the details of this TM about it’s behavioral struture, (C) inspire collaboration and innovation.

The Machine

The TM I will be discussing here is Skelet #1 which he describes with the notation C1L E1L H1L D1L D1R D0L A1L E1R B0L C0R. Converted into Tree Normal Form (TNF) and using Standard Text format this is:

1RB1RD_1LC0RC_1RA1LD_0RE0LB_---1RC

	0	1
A	1RB	1RD
B	1LC	0RC
C	1RA	1LD
D	0RE	0LB
E	—	1RC

It is TM #68,329,601 on bbchallenge.org.

For the rest of this article, I will use this TNF state naming.

Overview

I will present here:

1. A broad overview of the behavior of this TM.
2. A mid-level abstraction to help understand how to simulate this TM more easily.
3. A high-level (but incomplete) counter abstraction which explains how this TM operates “most” of the time but cannot fully explain intermittent “collision” behavior.
4. Backwards reasoning approaches I’ve tried so far.
5. Discussion about direct simulation.

Behavior Overview

Broadly, this TM is variation on a type of machine that Pavel Kropitz calls “structural counters”. A structural counter is a counter whose digits are not all adjacent. Instead the digits are spread out over the tape separated by some sort of innocuous “filler”.

This machine is a base 4 structural counter with a twist. In a “traditional” structural counter, the digits tend to drift away from each other over time. With Skelet #1, the digits actually shift towards each other. This digit movement eventually leads to “collisions” where two digits (or a digit and a “dot”) get too close and suddenly the TM behavior changes drastically before eventually re-establishing a structural counter configuration (often with new digits inserted).

This behavior is reminiscent of the behavior of Skelet #34 and other Shift Overflow Counters in so far as it has a relatively easy to explain “Counter Phase” interspersed with relatively complex “Reset Phases”. However, Skelet #1 is more complex even than these Shift Overflow Counters because it’s reset phase is much more chaotic (depending on precise details of the collision event) and I am nowhere near being able to describe in general the results of arbitrary Collision Resets nor to state a general “Reset Invariant” like I did for Skelet #34.

Basic Abstraction

In order to make any sense of this TMs behavior it helps to have an abstraction slightly higher level than the raw TM transition table. Consider any tape matching this RegEx:

^.* (<C10|A>) (10|110)*$

(In other words, the left half of the tape is unconstrained, the right half is made up only of an arbitrary sequence of blocks 10 or 110 and it is either in state A moving right or in state C moving left with a 10 immediately behind itself). Then the following rules completely describe the behavior of this TM:

  011 <C10  ->  <C10  110
   01 <C10  ->  <C10  10

  111 <C10  ->  01  A> 110
    0 <C10  ->   1  A> 10

A> 110 110  ->  011 011  A>
A> 110 10   ->  011 01   A>
A> 10  10   ->    1 011  A>

A> 10  110  ->    1 <C10  10
A> $        ->    1 <C10  $
A> 110 $    ->      <C10  110 $
A> 10 $     ->   **HALT**

This set of rules is exhaustive and unique meaning that for any configuration in the regular language ^.* (<C10|A>) (10|110)*$ exactly one of these rules apply.

This abstraction has effectively reduced the cognitive burden of analyzing this machine by reducing it to 2 states (only one moving each direction) and 3 blocks on the right (10, 110 and $).

Run-length Encoding

I have found a run-length encoding to be a useful way to summarize this TM. In this encoding we will replace 1n 0 with simply the number n on the right (and the mirror image 0 1n with n on the left). Additionally, I shorten A> to > and <C10 to < since these are the only right and left moving states respectively. Then the rules above look like:

    2 <  ->  < 2
    1 <  ->  < 1

  m+3 <  ->  m   1 > 2
m 0   <  ->  m+1   > 1

   > 22  ->     22 >
   > 21  ->     21 >
 m > 11  ->  m+1 2 >

 m > 12  ->  m+1 < 1
 m > $   ->  m+1 < $
   > 2$  ->      < 2$
   > 1$  ->  **HALT**

Note: Here I’m writing 22 to mean 2 followed by 2 (i.e. 110 110 on the raw tape) not “twenty-two”! I have not seen run-lengths of 10 or larger, if they come up, a notational variation will be necessary. Maybe something like (10)?

Counter Encoding

The TM is in Counter Configuration if it is of the form:

\[(x|D|C_0|C_1|C_2|C_3)^* \; (<|>) \; (x|D|C)^* \; R\]

Where:

Name	Counter Code	Run-length	Raw Tape (Left)	Raw Tape (Right)
Filler	\(x\)	22	011 011	110 110
Dot	\(D\)	21	011 01	110 10
Digit 0	\(C_0\)	232	011 0111 011
Digit 1	\(C_1\)	201	011 0 01
Digit 2	\(C_2\)	42	01111 011
Digit 3 (Clot)	\(C_3 = C\)	11	01 01	10 10
Right End	\(R\)	2$		110 $

And, as before < represents <C 10 and > represents A>. Note, I will use \(C_3\) and \(C\) interchangeably below.²

Low Level Counter Rules

This TM satisfies the following low level rules:

Left moving rules:

\[\begin{array}{l} x & < & \to & < & x \\ D & < & \to & < & D \\ C_3 & < & \to & < & C_3 \\ \end{array}\]

Increment rules:

\[\begin{array}{l} C_0 & < & \to & C_1 & x & > \\ C_1 & < & \to & C_2 & & > \\ C_2 & < & \to & C_3 & x & > \\ \end{array}\]

Right moving rules:

\[\begin{array}{l} > & & x & \to & x & > \\ > & & D & \to & D & > \\ > & x & C_3 & \to & C_0 & > \\ \end{array}\]

Right end rule:

\[\begin{array}{l} > & R & \to & < & R \end{array}\]

Note that these rules define behavior in all cases except for \(> DC\) and \(> CC\). These are “collisions” and when one occurs, the behavior becomes quite chaotic and hard to reason about.

Counter Behavior

Bringing all of these low-level rules together we get the basic counter increment rule (for \(k < 3\)):

\[\begin{array}{l} C_k & & w_0 & x & C_3 & ... & x & C_3 & w_n & < & R & \to \\ C_{k+1} & a & w_0 & & C_0 & ... & & C_0 & w_n & < & R & \\ \end{array}\]

Where all \(w_i \in (x|D)^*\). In other words, the \(w_i\) are all sequences of \(x\) and \(D\)s (Empty sequences are allowed). And where \(a = x\) if \(k \in \{0, 2\}\) (or is blank for \(k = 1\)).

This rule makes it clear how this TM operates as a base 4 counter. You can also see how every time one of the digits overflows (goes from \(C_3 \to C_0\)) it eats one \(x\) to the left. This continues until there is a \(C_3\) with no \(x\) to its left at which point there is a collision (either \(D C_3\) or \(C_k C_3\)).

Since digits to the right overflow 4x faster than those to their left, collisions are inevitable eventually.

Collisions analysis

Collisions are much harder to model and can be quite complex. Let’s look at some of the simpler examples. In order to talk about collisions I introduce a new symbol:

Name	Counter Symbol	Run-length Code	Raw Tape (Left)	Raw Tape (Right)
Parity Change	\(P\)	2	011	110

\[\begin{array}{l} > & DC & & \to & & xP & > \\ & P & < & \to & < & P & \\ >P & x & & \to & & x & >P \\ >P & R & & \to & < & CxR & \\ >P & Dx & & \to & & C_1 D & >P \\ >P & Cx & & \to & < & PDP & \\ >P & DP & & \to & & C_1 D & > \\ \end{array}\]

And so, for example, starting from the configuration:

\[\begin{array}{c} C_0 & x^a & D C & x^b & D & x^{c+2} & C & x^d & < R & \to \\ C_1 & x^{a+1} & > D C & x^b & D & x^{c+2} & C & x^d & R & \to \\ C_1 & x^{a+1} & x P > & x^b & D & x^{c+2} & C & x^d & R & \to \\ C_1 & x^{a+1} & x P < & x^b & D & x^{c+1} & C & x^{d+2} & R & \to \\ C_2 & x^{a+1} & > x P & x^b & D & x^{c+1} & C & x^{d+2} & R & \to \\ C_2 & x^{a+1} & x & x^b & >P Dx & x^c & C & x^{d+2} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_1 D & x^c & >P Cx & x^{d+1} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_1 D & x^c & < PDP & x^{d+1} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_1 < D & x^c & PDP & x^{d+1} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_2 x D & x^c & > PDP & x^{d+1} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_2 x D & x^c & C_1 D > & x^{d+1} & R & \to \\ C_2 & x^{a+1} & x & x^b & C_2 x D & x^c & C_1 D & x^{d+1} & < R & \\ \end{array}\]

Until finally we re-enter a standard counter configuration. But notice that the original digit that collided (\(DC\)) does not exist any more and a new digit was created to its right (\(C_2 x D\)). In general, collisions may remove and add digits like this.

Note: These rules are still not complete. For example, they do not explain what happens after a \(>CC\), \(>PDD\), \(>PDC\), \(>PDR\), \(>PCD\), \(>PCC\) or \(>PCR\) collision. Each of these has its own unique complex behavior. And this list of possible collisions is not even finite. For example \(> C^n x\) leads to a different collision with surprisingly different behavior for every different value of \(n\)!

But perhaps there is some finite way to describe all possible collisions. Such a theory could potentially lead to a proof of this TM being infinite by showing, say, that no possible collision leads to Halting. But note that \(>PCR\) and \(>PDDR\) both lead to Halt, so such a theory will have to be able to exclude collisions like that.

Accelerated Simulation

But perhaps we don’t need a “Grand Unified Theory” of collisions. Perhaps Skelet #1 ends up falling into a pattern after a huge number of steps. For example, @Yto is convinced that it will eventually be a translated cycler (aka Lin Recurrent), but with a gigantic starting step and/or period :) In order to investigate this, one approach would be custom-built acceleration for the specific behavior of this TM.

The @uni Cycle

Pavel Kropitz (@uni) wrote such a simulator and on 15 Feb 2023 he shared some very interesting repetitive behavior. Translated into my notation, the tape looked like:

\[\begin{array}{rl} & ... & \\ \{ & C_2 & x^{7640} & D & x^{10\,344} & \}^{1263} \\ & C_1 & x^{7640} & D & x^{10\,345} & \\ & C_3 & x^{7639} & D & x^{10\,347} & \\ & C_2 & x^{7634} & D & x^{10\,356} & \\ & C_0 & x^{7615} & D & x^{10\,394} & \\ & C_1 & x^{7540} & D & x^{10\,545} & \\ & C_2 & x^{7238} & D & x^{11\,149} & \\ & C_2 & x^{6032} & D & x^{13\,560} & \\ \\ & C_2 & x^{1208} & D & & D & x^{55} & D & x^{1303} & \\ & C_1 & x^{5060} & D & x^{38} & D & x^{530\,512\,281} & \\ & C_0 & x^{20\,395} & \\ \{ & D & x^{72\,142} & D & x^{3076} & D & x^{1538} & D & x^{300} & D & x^{30\,876} & \}^{1270} \\ & ... & \\ & D & x^{1\,037\,302\,028} & C_3 & x^{120\,874\,141} & < R & \\ \end{array}\]

In other words, there were two sections that were repeated >1200 times each:

\[\begin{array}{l} F & = & C_2 & x^{7640} & D & x^{10\,344} \\ L & = & D & x^{72\,142} & D & x^{3076} & D & x^{1538} & D & x^{300} & D & x^{30\,876} \\ \end{array}\]

And, in fact, there is a cycle here.

@uni Cycle Theorem:

\[\begin{array}{l} F^a & G & x^n & C & L^b & w & D & x^c & C & x^d & < R & \to \\ F^{a+1} & G & x^{n - p} & C & L^{b+1} & w & D & x^{c - 4p} & C & x^{d + 8p} & < R & \\ \end{array}\]

Where \(p = 53\,946\), \(n \ge p\), \(w \in (x|D)^*\) and \(G\) is roughly the part of the original configuration after the initial repeat and before \(x^{530\,512\,281}\).

However, the keen-eyed observer will note that this is not, in fact, an infinite cycle. Each iteration reduces the exponent \(n\) by \(p\) and so after \(\lfloor 530\,512\,281 / 53\,946 \rfloor = 9834\) more iterations the @uni cycle breaks down and the behavior becomes chaotic again.³

Counter-mode Acceleration

There is potential for accelerating the simulation exponentially as long as it remains in Counter Configuration (until a collision) by using the following rule:

\[\begin{array}{l} & > & w_0 & x & C & & w_1 & x^4 & C & & ... & w_n & x^{4^n} & C & & w_{n+1} & R & \to \\ & < & w_0 & & C & x^2 & w_1 & & C & x^8 & ... & w_n & & C & x^{2 \cdot 4^n} & w_{n+1} & R & \\ \end{array}\]

Where (once again) all \(w_i \in (x|D)^*\).

If someone implements this, I would be very interested to see some stats from it:

1. Distribution of times between collisions.
2. Frequency of different flavors of collisions \(>DCx\), \(>CCx\), \(>CCCx\), etc.

Backwards Reasoning

Another powerful approach to prove TMs infinite is by reasoning backwards from the Halting configurations to see what could have led there. Thinking this way, I started to wonder: How can this TM ever halt? There are a ton of different directions you could go with this but I explored one specifically that I’d like to write about:

Let me motivate this with a few things I noticed after analyzing Skelet #1 for a while:

1. It has a lot of 2s on it’s tape (which is why I named x = 22 as “filler”). So, a very common right side ending of the tape is \(x^n R\) aka 22 ... 22 22 2$. And this \(n\) can be quite large. For example, in the @uni cycle config I list above you can see that \(n > 100\,000\,000\).
2. The only way for this TM to halt is to eventually reach config >1$. In other words, we need to get a 1 all the way to the right end.
3. It is reasonably difficult to move 1s right or create them on the right.
4. If we force a specific alignment of the tape (for example 22 22 22 2$) then there are only 3 ways that the TM can approach this from the left:

	Run-length Code	Counter Code
Aligned	> 22 22 22 2$	\(> xxxR\)
Parity change	>2 22 22 22 2$	\(>P xxxR\)
Parity change (1)	>1 22 22 22 2$

Note: that the last option >1 doesn’t travel very far in practice. For example, whereas:

• For >: > 22 -> 22 > and > 21 -> 21 >
• For >2: >2 22 -> 22 >2 and >2 21 22 -> 201 21 >2
• But for >1: m >1 2a -> m+1 < 1a

So now, the question I have is: Starting from a configuration ending in a large number of 2s, how do we end up getting a 1 all the way to the right end using a sequence of > and >2.

There are an infinite number of such sequences. One way to convert this into a finite problem is to consider how each of the > and >2 act upon a fix-length suffix of the right-hand side. For example, let’s look at suffixes of size 7 starting from 22 22 22 2$ (Note: To make these slightly easier to distinguish, I have replaced 2 with . in the size 7 suffix):

ID	Config	Start	End	To ID
0	.. .. .. .$	> .. .. .. .$	< .. .. .. .$	0
		>2 .. .. .. .$	22 22 < .. 11 .. .$	24
24	.. 11 .. .$	> .. 11 .. .$	< 11 .. .. .$	96
		>2 .. 11 .. .$	< .. .. 1. .$	8
96	11 .. .. .$	2 > 11 .. .. .$	001 > .. .. .. .$	0
		>2 11 .. .. .$	22 22 < .. 11 .. .$	24
8	.. .. 1. .$	> .. .. 1. .$	22 < 11 .. .1 .$	98
		>2 .. .. 1. .$	22 22 < .1 11 .. .$	56
98	11 .. .1 .$	2 > 11 .. .1 .$	001 > .. .. .1 .$	2
		>2 11 .. .1 .$	< .. 1. .1 .$	18
56	.1 11 .. .$	2 > .1 11 .. .$	< .. .. .. .$	0
		>2 .1 11 .. .$	22 22 < .1 11 .. .$	24
2	.. .. .1 .$	> .. .. .1 .$	< .. .. .1 .$	2
		>2 .. .. .1 .$	22 22 11 > .. 11 .. .$	24
18	.. 1. .1 .$	> .. 1. .1 .$	< 11 .. .1 .1 .$	10
		>2 .. 1. .1 .$	22 21 11 > .. 11 .. .$	24
10	.. .1 .1 .$	> .. .1 .1 .$	< .. .1 .1 .$	10
		>2 .. .1 .1 .$	Halt

This table is a bit busy, but the punchline is that: Starting from config 22 22 22 2$ = .. .. .. .$ we can only reach Halt by the precise sequences:

  >2   .. .. .. .$   ->  22 22 <   .. 11 .. .$
  >2   .. 11 .. .$   ->        <   .. .. 1. .$
  >    .. .. 1. .$   ->     22 <   11 .. .1 .$
  >2   11 .. .1 .$   ->        <   .. 1. .1 .$
  >    .. 1. .1 .$   ->     < 11   .. .1 .1 .$
  >2   .. .1 .1 .$   ->      **Halt**

I call this the “signal sequence” PPaPaP where P represents >2 (parity change) and a represents > (aligned). This is a “halting signal sequence”.

So, if we can find some sort of left-side config that can produce this sequence PPaPaP, that would define a complete config that would lead to Halting. Or alternatively if we can show that this sequence is impossible from any valid left side, then we might be on the path to proving that this TM never halts.

Update (27 Feb 2023): See Skelet #1: A Halting Counter Config where I describe such a full halting configuration.

Ways Forward

Even with all the theory presented here, so much still remains a mystery about Skelet #1. Honestly, I still think there’s a chance that this TM halts! (My current feeling is ~10% chance.) But I do see a number of potential directions to make progress:

1. A complete theory of collisions. Is there some sort of abstraction that will allow us to think about collisions in a simpler way? Or can we enumerate all possible collisions using software? Are there certain collisions that can never happen?
2. A complete high-level encoding. Could we find an encoding which the TM never left (like the run-length encoding) but was also higher level and easier to reason about? Or (the dream) a closed encoding which had no way to lead to Halting (like a CTL proof).
3. Acceleration speed-up. The discovery of the @uni cycle was very exciting. It was “almost” an infinite cycle. It seems like it could be possible for a cycle like that to be infinite. Perhaps what we need most is a hyper-accelerated simulator that can get us out to \(10^{1000}\) steps at which point it will enter an infinite cycle? Or maybe it really does halt and a simulator will simply tell us that!
4. Can we find a collision which produces the halting signal sequence PPaPaP? Or prove that no left side config can ever produce a sequence like this? Can we find other halting signal sequences? Can we describe all halting signal sequences?

It’s an exciting world out here. If you’re interested in getting involved, come join us on our dedicated Skelet #1 Discord channel.

Related Articles

This article is part of a series studying Skelet TMs:

1. Skelet #34 is Infinite

2. Shift Overflow Counters

3. Skelet #1: What I Know

4. Skelet #1: A Halting Counter Config

5. Skelet #1 is infinite … we think

6. Skelet #10: Double Fibonacci Counter

Footnotes

1. Massive Caveat: You should not accept my proof sketches as fact. The reset invariants are subtle and a tiny hole in that proof could lead to them halting! Likewise, there has been a lot of chatter on Discord about how Skelet #17 may not (in fact) be easy to prove. See @bt’s Discord post discussing this optimistic approach on 8 Feb 2023. ↩

2. By the way, the “DCR” notation was introduced by @Yto on 14 Feb 2023 along with P for Parity Change which I use later in the article. ↩

3. You may be asking: Shawn, what about when \(c < 4p\), won’t that happen first … well yes, but that collision is much simpler and has almost no effect on the @uni cycle (just modifies \(c, d, w\) slightly). Try it out for yourself :) ↩