Halting at astronomical times

1Simulation runs out of time

Start with a machine whose halt is within reach. Guess first, then reveal: the page runs it.

Our C simulator does about 254 million steps per second, so BB(5) takes it a fifth of a second. Three of our holdouts were still running at 10⁹ steps, and all three turned out to halt.

On a scale of powers of ten, the gap looks like this. Each step along the axis is ten times more steps.

2Find the rhythm: W5-5's rounds and eats

To prove anything about a run that long, we first need its rhythm. Here is W5-5 at step 8,600, at the start of one round. Press play.

The brackets under the first row name the parts. Left of the head is a counter of 3-cell digits, with its lowest digit next to the head; each bracket shows a digit's value. Then comes one boundary cell, a 0, and the head, in state E, on the 101 cap.

Right of the cap is a bell: b blocks 001, one defect 0001, and c more blocks 001. Here b = 13 and c = 2.

In the round, the head dips left into the counter and adds 1: the low digit 000 becomes 101. Then it walks right to the defect and back, and moves the defect one block to the left. After 182 steps the tape has the same shape again: the counter is one higher, b went from 13 to 12, and c from 2 to 3.

How the digits count

Here is the counter at five round starts in a row of the real run (steps 1,956 to 2,182, simulated in your browser). The bracket of a digit that just changed is blue.

Adding 1 to 001 gives 000, so 001 is worth −1. Adding 1 to 100 (worth 2) gives 001 and a carry of 1 into the next digit: 2 + 1 = 3 = 4 − 1. So the digits are base 4 with values −1, 0, 1, 2 (balanced base 4). These four are the clean digits; a digit whose middle cell is 1 is dirty.

The strip also shows what a round costs: 12b + 22 steps, plus 14 for each 100 the carry passes, plus 4 if it stops on a 000. The round you played above is 12·13 + 26 = 182 steps.

The proof does not run rounds one by one. It proves the round once, for a bell of any size. The box below runs the same round for b = 1 … 13 and checks each one live (its 12n + 26 is the cost for a carry that stops on 000). The lemma in the .v covers every b, every c and every counter of clean digits.

Now one row per round, from the blank tape. Watch b count down and c count up while the counter climbs.

When b reaches 0 the next round is an eat: the bell bites a few cells off the low end of the counter, and the defect restarts near the far end (b becomes about the old c). An eat plus its rounds is a cycle. You can see it at step 1,402 (b = 0, c = 7), which is followed by b = 6.

Cycles get longer: c grows by about 2 per cycle, and a whole cycle costs about 6c² steps. The halt comes in cycle 611,577, where c = 1,218,828. The machine halts only 7,435 rounds into that cycle (out of about 1.2 million), after 108,456,557,258 steps.

3Coq replays the run in giant jumps

Coq's proof walks this same run, but as a checker that makes one move at a time. Each move is one of three kinds:

• eat: simulated cell by cell (long stretches of bell are crossed with proved shift rules);
• jump n rounds: one lemma does n rounds at once: the counter goes up by n, b down by n, c up by n;
• 1 round, simulated: when the next carry would reach a dirty digit (like 011), which the jump lemma does not cover.

The checker's moves over these rows (tap one to see where it starts):

In these early rows, most rows are never visited: the checker lands on a round start, jumps over the rest of the cycle, simulates the eat, and jumps again. Later cycles need more moves (the averages are under the replay below).

Who picks n? A small program, the proposer, suggests each jump size. Decide first:

Be the proposer. Here is a real moment of the run: the counter 001 010 001 has a dirty digit 010 just above its low digit. Pick a jump size.

That is the whole proof for W5-5, start to finish:

On average a move covers about 3.7·10¹¹ steps. Coq checks the moves in 751 chunks of about 400,000 macro steps each (a macro step is one machine step, or one proved jump across a run of repeated blocks). It never runs the 1.82·10¹⁸ machine steps themselves.

4The last round, and who counts the steps

This is the round where W5-5 ends: round 7,435 of cycle 611,577. The six low digits are all 100 (worth 2), so the carry runs through all six and reaches 110. Two eats made a 111 there by regrouping cells, and the carry of round 3,339 turned it into 110.

At step 32 C reads the 0 of 110, at step 33 D reads its middle 1, at step 34 E reads its first 1, and at step 35 F reads the last cell of 101 above it, a 1. F reading 1 has no rule (---, lit in the table), so the machine halts there. The head never reaches the bell in this round, which is why cutting the bell changes nothing.

busycoq counts one step fewer than our simulator. busycoq stops at this configuration, where F reads 1 and finds no rule: "halts in 35 steps" here, and 1,816,824,067,232,869,944 for the whole run. Our simulator runs --- as one more step (write 1, move right, stop) and says 36 here and 1,816,824,067,232,869,945 for the run. This page quotes our simulator's count.

Step counts are computed, not proved. A script adds up the cost of every move of the same run: 288 for the opening, the steps of every eat, and for every round the cost formula of beat 2 (a round whose carry reaches a dirty digit has its own formula). Each formula was checked against direct simulation. The Coq theorem is only halts tm c0, so the total sits outside the proof.

5Two more of ours: a fuel race, and no clock at all

C2-552: digits that burn fuel

C2-552 also counts. Look at it each time the head, in state A, reaches new ground on the right. The run from one such moment to the next is one increment. (The head also reaches new ground in other states, one step before or after; only the moments in A count.)

Read the tape left of the head as walls, runs of 2 or more equal cells, with gaps between them. Walls of 2, 5, 8, … ones (11, 11111, …) are boundaries: they separate the digits. Each digit starts with its bit (the wall after its boundary: 00 = 0, 1111 = 1) and ends with its fuel, the gap at its right end. The gap after the last boundary is the tail.

Step through and watch the fuel numbers. Every carry that touches a digit burns some of its fuel. A digit with spare walls survives running low: it hands its last wall to its right neighbour and takes the gap next to that wall as its new fuel. A digit with no spare wall (orange outline) can only burn down, and one with bit 0 and no fuel halts the machine at the next carry.

New digits come from the tail. At a reset, which takes two increments, the tail becomes a new lowest digit with fuel 2a_n − 1. Here a_n + 1 is the number of increments since the previous reset. The panel shows resets at rows 0–1, 3–4 and 8–9.

The new digit lives roughly as long as the next reset comes within twice the time: a_n+1 / a_n < 2. The ratio swings, and the swings grow:

After reset 82 the next reset would need about twice as long, and it never comes. The second-lowest digit has no spare wall, and neither does its left neighbour, so it burns its last fuel. The next carry into it halts the machine, during increment 11,631,266,794,472,450,654,093, about 1.77·10⁴⁴ steps in.

The proof is the same recipe as W5-5's: each kind of carry is a lemma for all sizes, long runs of increments are applied in closed form, and Coq replays the run from step 342 in 107,781 checked moves (22 chunks).

W5-7: no step count at all

W5-7 keeps a binary counter on the left and a register on the right. Each bounce of the head adds 1 to the counter and one block 011 to the register. A fill is the run of bounces that makes every digit 1. Then comes an overflow: the head walks out to the far (left) end of the counter and back, and the register becomes new low digits. Here is the first fill, 5 bounces from step 847, and its overflow:

The counter is made of words 001 (W0) and 111 (W1). Read from the head, W1 W0 is a digit 0, W1 W1 a digit 1, and a lone W0 is a separator (the brackets). The row label says how many bounces are left until the counter is full.

An overflow after c bounces turns the register into (c − 1)/2 new low digits, all 0, so the next fill takes at least 2^(c−1)/2 − 1 bounces. The fills take 5, then 51, then 1,308,622,847 bounces, then at least 2^654,311,423 − 1. Each count is roughly 2 to the power of the one before.

So this proof never counts. The 38,573-step opening simulates the first 2 cycles directly. Coq then checks 192 more abstractly, with lower bounds instead of sizes ("a block of at least 256 pairs"). That makes 194 cycles, and the halt comes in the 195th overflow: a tower of exponents about 195 high.

In that overflow the far end of the counter is doomed: once the head walks out to it, the machine halts, whatever is to its right. The head gets there one token at a time:

A W1 W1 pair takes 12 steps (the rule walk1) and a W0 takes 19 (walk0). Each turns its token into cells right of the head (010101 or 011) and reads nothing outside its own cells. At the far end the head meets this fixed run:

At step 1,368 F reads 1: no rule, so the machine halts. That is busycoq's count, as in the write-up; our simulator would call the halting move step 1,369. The head never goes more than one cell right of where it starts, so whatever follows 010 1 (the walked-over tokens and the register) is never read.