9 modules (0–8) · 12 to 15 minutes each
BB(6) learning guide
How it works
Each module is a few pictures of real runs, simulated in the page, with short notes. You step through them, then guess what a real run does before the page plays it.
The modules build on each other, from reading a machine string to reading one of our Coq kill files. W5-3, one of our kills, comes back in most of them.
The path
- 0Reading a machine and its pictures · 12 min Read a machine string as a table, follow a run step by step, and read directed-head notation and a space-time diagram.
- 1The easy fates · 12 min Recognise halt, cycler, translated cycler and bouncer, and see what the deciders catch and why holdouts are left.
- 2Compression: blocks, background, shift rules · 12 min Write a long tape as blocks with exponents, spot the background and its defects, and cross a block in one jump with a shift rule.
- 3Counters · 15 min See a binary counter on the tape, whether its digits are cells, 2-cell words, or blocks with fuel.
- 4Bells eating counters · 15 min Follow one round (count, count, …, eat) and predict the next eat configuration.
- 5Invariants · 15 min Say why simulating for a long time is not a proof, what "closed" means, and how an invariant holds or fails.
- 6Halting at astronomical times · 15 min See how a halt far beyond any simulation is proved, with rules for every size and a replay in giant jumps.
- 7Cryptids · 15 min Iterate Antihydra's rule by hand and see why such machines block an exact BB(6).
- 8From informal proof to Coq · 15 min Find each part of an informal proof inside a kill file, and know what our kill checks demand.
Which module answers my question?
| question | module |
|---|---|
What does a string like 1RB1LB_1LA1RZ mean, and what is ---? | 0 |
What do B> and <E mean in a tape string? | 0, 2 |
| Where do holdouts come from, and what are TNF and the holdout list? | 0, 1 |
| What are cyclers, translated cyclers and bouncers, and why do the deciders miss some machines? | 1 |
What does (10)^21 mean, and what is a shift rule? | 2 |
| What are the background (filler) and defects? | 2 |
| What is a counter on the tape, and what is a carry? | 3 |
| What is a bell, and what does "the bell eats the counter" mean? | 4 |
| Why is running a machine for 10^9 steps not a proof? | 5 |
| How can we know that a machine halts after far more steps than anyone can simulate? | 6 |
| What is a cryptid, and why does Antihydra block an exact BB(6)? | 7 |
What is inside one of our .v kill files? | 8 |