Reading a machine and its pictures

1The string is a table

This is W5-3, one of our kills. Tap any piece of the string and its transition lights up in the table, with the rule written out in words.

Cut the string at each _ and you get one piece per state, A to F. Each piece holds two transitions of three characters: the first for reading 0, the second for reading 1. This format is the community's Standard Text Format (STF).

1RB means: write 1, move Right, go to state B. --- means the transition is undefined: if the run ever needs it, the machine halts. W5-3's only --- is F0, so W5-3 halts exactly when it reads a 0 in state F.

2One run, every step

The BB(2) champion 1RB1LB_1LA1RZ: no halting 2-state machine runs longer or leaves more 1s. Unless a widget says otherwise, a run starts on a blank tape (all 0s), with the head on cell 0 in state A, the start state.

The round badge sits on the cell the machine reads now, and its letter and colour are the state. The yellow flash marks the cell just written.

Each step looks up (state, symbol read) in the table, which lights the transition used. Then it writes, moves one cell, and changes state. When the rule line adds new record, the head has just reached a cell further left or right than ever before.

The Z in 1RZ is not a state: it means halt. The run above stops at step 2 on purpose, and the next two drills ask what comes after.

3The same run, as text

Proofs and tools write each tape on one line, in directed-head notation. B> means the head is in state B and reads the cell just to its right. <B means it reads the cell just to its left. 1^2 is two 1s, and 0^inf is blank tape forever.

The underlined piece is the cell being read. The arrow also shows which way the head last moved: <B after a move left, B> after a move right (step 0 uses A> by convention). Step 6 says Z>, because the run halted there.

4Zoom out: the space-time diagram

Now draw each step's tape as one thin row, with time going down. This is W5-3 from the blank tape, steps 0 to 165. Solid cells are 1s, and the coloured cell in each row is the head, in its state's colour. Tap a row, or press ▶▶, to see that step in the big strip.

The last row, step 165, is 0^inf 1 0 1 0^2 1^2 B> 0^5 1^2 0^inf. Up close:

Read it in three parts: two copies of 10, a fixed separator 0 11 B> 0 (the head reads its last 0), and the number 4. The number is in binary, each digit written as two cells (11 = 1, 00 = 0), lowest digit first: 00 00 11 is 0, 0, 1, so 100 in binary, which is 4. Module 4 calls this tape E(2,4), and W5-3's proof starts from it.

10 word: the striped band. It grows left each round. ◀ counter: the staircase

W5-3 in the explorer (10⁵ steps, state colours)

5Where machines and holdouts come from

Nobody writes machines by hand: TNF (Tree Normal Form) builds them while running them. Start with every transition --- and run from the blank tape. Each time the run needs a transition that is still empty, branch: one copy halts there, and the others each try a move.

Three rules keep each machine listed once:

• Permutation. A new state always gets the next unused letter, so machines that differ only by renaming states are built once.
• Mirror. Swapping every L and R gives the same run, mirrored, so only machines whose first move goes right are kept. The lists go further and fix A0 = 1RB.
• Unused transitions. A transition the run never needs stays ---, so machines that differ only there are built once too.

W5-3 was built the same way

Each transition below shows the step at which W5-3's run first needed it. The run reaches the states in the order A, B, C, D, E, F: the permutation rule at work. F0 was never needed, so it is still ---.

Whether a run ever needs its --- transition is the whole question. W5-3 does not reach F0 in 10⁹ simulated steps, but that proves nothing (module 5 shows machines that halt far later). Our Coq proof shows it never does.

The holdout lists

Deciders are programs that each prove one kind of behaviour (module 1), and they settle almost every machine TNF produces. The machines that every decider failed on form the holdout list. The community publishes a new one as proofs land:

Bars: a selection of the lists in data/holdouts/, one machine per line. Dates are wiki upload dates, except 778 (Discord post) and 740 (the day we received it). Right column: the line W5-3 is on.

A machine leaves the list when its proof is merged into busycoq, or when it is shown to behave exactly like another holdout, which stays on the list as the representative (nothing is solved by this). Of the 38 machines that left between the 778 and the 740 lists, one was our #2 (our first kill) and 31 left by equivalence. W5-3 has been on every list since June 2024, and will leave once its proof is accepted.