Skelet 10

1LC0LA_---0LC_0RD1LA_1LB1RE_1RD0RE (bbch), called Skelet #10, was one of Skelet's 43 holdouts and one of the last holdouts in BB(5). It is a double fibonacci counter. It is one of the few TMs to have required an individual proof of non-halting in Coq-BB5.

Behavior

Skelet 10 implements two base fibonacci counters, one on the right tape side and one on the left tape side. The TM halts if these counters become desynchronised. The right side counter can be described by the following rules:

A>  0 10^k 0 --> <D 0^2k   10
B> 10 10^k 0 --> <D 0^2k+1 10

These rules are equivalent to the Zeckendorf increment rules:

Z(n) = 0  10^k 0 w ==> Z(n+1) = 0^2k   10 w
Z(n) = 10 10^k 0 w =0> Z(n+1) = 0^2k+1 10 w
Where Z(n) represents n in the little-endian (least significant digit is on the left) representation of Zeckendorf notation.

and can be restated as:

Z(n) = 0 w ==> A> Z(n) --> <D Z(n+1)
Z(n) = 1 w ==> B> Z(n) --> <D Z(n+1)
Where Z(n) = 0 w means that the least-significant bit in Z(n) is 0.

The left side counter encodes base fibonacci differently and is also reversed to big-endian (least significant digit is on the right). The two least-significant symbols are also omitted. These differences can be described using the following definitions:

T(0w)    = T(w)00
T(10w)   = T(w)1010
T(empty) = empty
where w is any valid Zeckendorf expression.
--> This encodes the Zeckendorf representations in a way consistent with the left fibonacci counter by encoding 10 as 1010 and 0 as 00. This also reverses the order of the Zeckendorf representation to big-endian.

L(n) is defined in the following way:
T(Z(n)) = v ab ==> L(n) = v
where v is any valid Zeckendorf expression.
--> This removes the two least-significant tape symbols.

There are now 3 possible cases for 3 possible values of the two least-significant digits of the left counter:

Z(n) = 00 w            --> T(Z(n)) = T(w) 00 00                 --> L(n) = T(w) 00
Z(n) = 0 10^k+1 0 w    --> T(Z(n)) = T(w) 00 10 1010^k+1 00     --> L(n) = T(w) 00 10^2k+1 10
Z(n) = 10 10^k 0 w     --> T(Z(n)) = T(w) 00 1010^k+1           --> L(n) = T(w) 00 10^2k 10

These are affected by incrementing in the following way:

Z(n) = 00 w            --> L(n) = T(w) 00                       ==> Z(n+1) = 10 w            --> L(n+1) = T(w) 10
Z(n) = 0 10^k+1 0 w    --> L(n) = T(w) 00 10^2k+1 10            ==> Z(n+1) = 0^2k+2 10 w     --> L(n+1) = T(w) 10 10 10^2k+1
Z(n) = 10 10^k 0 w     --> L(n) = T(w) 00 10^2k 10              ==> Z(n+1) = 0^2k+1 10 w     --> L(n+1) = T(w) 10 10 00^2k

The TM follows these rules on the left:

        00 <D -->         10 B>
00 10^k 00 <D --> 10 10 00^k A>

These can be rewritten as:

Z(n) = 00 w ==> L(n) <D --> L(n+1) B>
Z(n) ≠ 00 w ==> L(n) <D --> L(n+1) A>

For a proof of this TM not halting, see https://www.sligocki.com/2023/03/14/skelet-10.html

See also

• Skelet 1
• Skelet 17
• Finned 3