1RB0LD_1RC0RC_1LA0RD_1RC1LE_0LF---_1LA0RC

From BusyBeaverWiki
Jump to navigation Jump to search

1RB0LD_1RC0RC_1LA0RD_1RC1LE_0LF---_1LA0RC (bbch) is a non-halting BB(6) TM. It is equivalent to 1RB0RC_1RC1LE_1LD0RB_1RA0LB_0LF---_1LD0RF (bbch).

Analysis by @nerdyjoe

These two machines are non-halting. After a brief stabilization period, it works as a ternary counter with some fun behavior. The head sweeps left and right. Each bounce off the left side extends the meta-tape by one, each pass to the right "adds one" and encodes the result, bounces off the right side, then re-encodes the result.

The state of the counter can be read off most easily when the meta-tape is mostly ...111010111010..., instead of when it's mostly ...001001001...

The tail end looks something like ...010111010101101, which i would read as 131121. Subtracting the baseline ...131313 from these gives -2 1 -2. Renormalizing signs gives 212. These are the first several numbers, the first after 115 steps: 2 100 101 102 200 201 202 212 222 10000 10001 10002 10100 10101 10102 10200 10201 10202 10212 10222 20000 20001

Formalizing the details is a little annoying, but it should be relatively straightforward to pick out about 6 modules of tape and state to characterize the full behavior.

I have reposted my original message above, with the specific machines in question.

In general, this thread can be for machines with similar behavior, where a left-right sweeping head increments some sort of counter on one side, and extends the tape on which the counter is written on the other side.

Analysis by mxdys

On Jun 16 2025, mxdys gave a Rocq proof that this TM does not halt: https://github.com/ccz181078/busycoq/blame/c0724b3706d96fddb5c253ee2301e9efeb18f5aa/verify/BTCv1.v#L479-L497

The equivalent TM was proved non-halting in lines 455-473.