Hi! The bbchallenge.org front page currently names Machine #7,410,754 first among the “scary undecided machines”.

I’ve observed that it doesn’t halt; I’d like to sketch a proof and ask any ideas here might be new and fit into the overall program.

I’m now seeing “Closed Tape Language”, and the idea here is similar (sadly with some notation differences).

As a TM steps through many intermediate states, whose description would clutter a closed language, let’s analyze equivalent String Rewriting Systems.

We model a TM’s state TM as a word in the language `[01]*[a-eA-E][01]*`

.

Lower-case a-e represent the TM head in state A-E on top of a 0 bit.

Upper-case A-E represent the TM head in state A-E on top of a 1 bit.

A “Word” is just a string (with designated left/state/right components).

The TM states are Words modulo leading/trailing zeros.

Words (NOT modulo leading/trailing zeros) can also represent TM-state infixes.

Our little friend’s machine code is thus expressible as these rewrite rules:

a0→1b, a1→1B, 0A→d0, 1A→D0, 0b→c1, 1b→C1, B0→1c, B1→1C, 0c→a1, 1c→A1, C0→0c, C1→0C, 0D→e0, 1D→E0, e0→0b, e1→0B, 0E→d1, 1E→D1

The benefit is that we can compose rules and obtain a system with the same behavior (transform a TM state into a future state) with intermediate steps/states bypassed.

I found it convenient to formalize these rewrite (not exactly Semi-Thue) systems as follows:

- Binary → relation on words (modulo leading/trailing zeros) generated from finitely many infix substitutions.
- Designated
*halt words*({`d`

} here): if one appears as an infix, the machine will halt. - Designated
*start state*(`a`

here). - The system is
*deterministic*: every TM state matches exactly one rewrite or halt-word.

Determinism helps us prove certain transformations are sound.

A designated start state helps us *prune* unreachable rules. (Formally: mark them halting, and declare the system equivalent when the start state’s trajectory is.)

Imagine you diagrammed the system: vertex per rewrite rule, directed edge between rules which (partially) compose. The first rewrite applied to the start state serves as a root. Only vertices reachable from the root matter; furthermore, we can advance the start-state until this root belongs to a cycle.

So #7410754 simplifies as follows. (Messy but doable with heuristics.)

- Compose rewrites, where possible: a0→0C, a1→1B, 1A→D0, 0b→c1, 1b→0C, B0→A1, B1→1C, 0c→1B, 1c→A1, C0→1B, C1→0C, 0D→c1, 1D→E0, e0→c1, e1→0B, 1E→D1; start at a; halt on 0A|d|0E
- Advance start & prune a0→0C, a1,0b,1b,e0,e1 rules: 1A→D0, B0→A1, B1→1C, 0c→1B, 1c→A1, C0→1B, C1→0C, 0D→c1, 1D→E0, 1E→D1; start at C; halt on a|0A|b|d|e|0E
- Split rules whose targets overlap with halt-words 0A, 0E: 1A→D0, 1B0→1A1→D01, B1→1C, 0c→1B, 11c→1A1→D01, C0→1B, C1→0C, 0D→c1, 11D→1E0→D10, 1E→D1; start at C; halt on a|0A|b|0B0|01c|d|01D|e|0E
- Prune 1A→D0, 1E→D1: 1B0→D01, B1→1C, 0c→1B, 11c→D01, C0→1B, C1→0C, 0D→c1, 11D→D10; start at C; halt on a|0A|1A|b|0B0|01c|d|01D|e|0E|1E = a|A|b|0B0|01c|d|01D|e|E
- Split on halt-word 01c, compose: 1B0→D01, B1→1C, 0c→1B, 11c→D01, C0→1B, C1→0C, 00D→0c1→11C, 110D→11c1→D011, 11D→D10; start at C; halt on a|A|b|0B0|01c|d|01D|010D|e|E
- Prune: 1B0→D01, B1→1C, C0→1B, C1→0C, 00D→11C, 110D→D011, 11D→D10; start at C; halt on a|A|b|0B0|c|d|01D|010D|e|E
- Split on substitutable 1B0, compose, prune: C00→D01, C01→11C, C1→0C, 00D→11C, 110D→D011, 11D→D10; start at C; halt on a|A|b|B|c|d|01D|010D|e|E

By inspection, the modified system only inserts 1’s on the left in pairs, so the halt-words are unreachable!

That is, the regular language `(0|11)*[CD].*`

separates reachable states from halting states.

One thing that has me concerned about the approach: the simplifications helped *me* find a “closed tape language”, but what’s the algorithm, and could it have tackled the original TM just as easily? (By unwinding the above construction, we see that a CTL for the original TM exists.)

The RewriteSystem simplification is mostly implemented in Python. Needs work before it’s obviously correct, readable, and able to choose “split” steps automatically. If the approach doesn’t sound like a dead end, I’ll get it polished and shared.