Compression: blocks, background, shift rules
A long tape is mostly one short word repeated. Write each repeat as a block with an exponent, like (10)^21 (the word 10, 21 times), and the whole tape fits on one line.
A shift rule says what the head does when it crosses a block, for every size of block at once. So a proof can jump the head across the block in one move.
1One tape, written two ways
W5-3 (1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC) at step 165. Two stretches repeat a 2-cell word, 10 10 and 00 00, so the tape can be written 0^inf (10)^2 0 11 B> 0 (00)^2 11 0^inf. Here (10)^2 means "10 twice", 0^inf is the endless blank on each side, and B> marks the head: state B, reading the cell right after it.
The two lines under the tape compress in different ways. as text only merges runs of one symbol (0^5 = five 0s). as blocks groups 2-cell words such as 10, which is what the rules below need.
Now the same machine each time its tape has this shape again, up to step 3,097. The raw tape grows from 15 to 52 cells, but the blocks line stays one short line. Press ▶ play, then switch the history between cells and blocks.
The exponent of (10) goes 2, 5, 8, 11, 14: up 3 per row. Then it jumps to 21, at a big eat: the machine bites the low digits of the counter written right of the head (the 00 and 11 pairs), and the counter drops from 22 to 6. Counters are module 3, eats module 4.
2Crossing a block: a shift rule
Step 3,103 of W5-3's real run, 6 steps after the last row above. E stands on the right end of (10)^21, moving left. <E is the mirror image of B>: state E reads the cell just left of the arrow (here the last 0 of the block).
Step through: every 2 steps the head passes one 10 and leaves it exactly as it was.
The two rules that do it: E reads 0 → write 0, move left, go to B; B reads 1 → write 1, move left, go to E. After 42 steps (2 × 21) E reads the blank cell left of the block. In the blocks view the exponent simply moves from the left of the head to the right (it ends at (10)^22 because the 10 that already stood right of the head joins the block).
That is W5-3's shift rule EB: (10)^n <E → <E (10)^n in 2n steps. Pick n: the page runs that case and checks the end tape, the step count, and every cell the head reads. The head reads only the block's cells and ends on the cell just left of it; the 1 1 on each side is only an edge for the picture.
Because the head reads nothing outside the block, the rule holds wherever the block sits on a tape, for every n. The page checks n = 1 … 10; W5-3’s Coq file proves it for every n, inside each lemma that crosses a block (module 8).
3Not every crossing is a straight walk
W5-3’s head also crosses (10)^n to the right, in state A. Guess first: the answer is not what the last section suggests.
That is rule AS: A> (10)^n 1 → (10)^n A> 1 in 4n steps. The head steps back once per copy, and on the last copy B reads the 1 just after the block. It never goes past that 1, which is why the 1 is part of the rule.
A shift rule may also rewrite the block it crosses. You met one in module 1: W5-8’s rule R1, where the head in state C crosses (11)^n.
4Background and defects
W4-3 (1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---), our 20th kill. Each picture is its whole visited tape, wrapped into lines like text (100 cells per line, 50 on a narrow screen). Almost every cell continues the pattern 0101…: that word is the background (also called the filler).
A defect is a place where two neighbouring cells are equal, so the pattern breaks; each one is boxed in red. An empty box is a 00 defect and a dark box an 11 defect. After a defect the stripes shift by one column, because the 0101 pattern starts again one cell later.
| after step | cells visited | defects |
|---|
Between two defects the cells alternate, so each stretch is one block: (10)^k, or (01)^k, which is the same background starting one cell later. A lone 0 or 1 between blocks, or a switch from (01) to (10) (…0 1 | 1 0…), is a defect; (100)^3 at the left end is three 00 defects in 9 cells.
That is why the blocks line is short: at step 1,000,000 the tape has 1,945 cells but only 16 defects.
5A sweep flips the background and leaves the defects
W4-3 from step 10,000,591: here are 38 cells of one long sweep to the right (the head turns only at cell 3,888, at step 10,003,345). Every step writes the opposite of what it reads (B0, C1, A0, B1, again and again), so 0101 becomes 1010: still background, faded here.
The defect at cell 1,151 is still there after the head has passed: B reads 1 twice in a row there, and the cycle goes on one beat later. The red pair that travels with the head is the seam between the part already flipped and the part not yet flipped.
Away from the defects the head only flips the background. The defects change only when the head reaches one (W4-3’s write-up lists 8 cases: pass, turn, wiggle). That is why its proof tracks only the defects, 18 at step 10,000,000 plus the seam next to the head, instead of 6,104 cells.
The explorer can fade the background over a long run too. Its k-block view cuts the tape into 2-cell blocks that start on even cells, fades 10 and 01, and paints the other blocks orange. So it shows a defect only when its two equal cells start on an even cell (6 of the 19 at step 10,000,000); phase 1 (key Shift+B, or the second link) cuts at odd cells and shows the other 13.
W4-3 to step 10^7, background faded, phase 0the same, phase 1
The preset p17-walls-time shows the same view for pilot machine #17 (1RB0LF_0RC0RB_1LC1LD_1RE0RD_---0RA_1LA0LF, line 628 of the 740 holdout list), which has the same 10/01 background.
- W4-3
1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---: our 20th kill, submitted upstream (busycoq pull request 17, open). Its write-up describes the tape by its defects alone: 8 rules say what happens when the head meets one, and most defects belong to counters (a left word that counts to 81 and a base-3 chain, module 3). - W5-3
1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC: our 24th kill. EB and AS are two of its low-level rules; in the Coq file busycoq’sestactic proves them inside each lemma that crosses a block (module 8). - W5-8
1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF: the bouncer from module 1, whose C rewrites(11)^ninto(10)^n.
- A block
(w)^nis a word repeated n times; a long tape is a few big blocks. - A shift rule crosses a whole block for every n at once (EB: 2n steps, AS: 4n), because the head treats each copy the same and reads no cell outside the ones the rule names.
- When one word fills almost the whole tape (the background), only the defects matter: a sweep flips the background and leaves them in place.