It ends, and nothing says when
Assumes: The condition the recursion rests on · The game that is a number system
The condition the recursion rests on is that a game ends. Every line of play reaches a position with no moves, and without that there is nothing for the recursion to stand on and no value to compute.
The condition is usually met by something obvious. Counters go away, squares fill up, edges are cut, coins fall off a cliff. There is a quantity that decreases at every move and cannot decrease for ever, and the game is over in at most that many moves.
This essay is about what happens when the condition is met and there is no such quantity.
The hydra
A hydra is a rooted tree. Hercules removes one leaf. If that leaf had a grandparent, the whole subtree hanging from its parent is then copied several times over alongside itself — times on the -th move, in the standard rule.
So a chop removes one node and adds a great many, and the tree grows almost every time.
Hercules wins anyway. Whatever leaf is chosen, however fast the copies multiply, the hydra dies in finitely many moves. That is Kirby and Paris’s theorem, from 1982, and the proof is three lines long.
The proof, and why nothing shorter works
Assign each hydra an ordinal. A leaf is ; a node with children whose ordinals are is , which is Cantor normal form. The hydras of finite height get ordinals below .
Then: every chop strictly decreases the ordinal. Removing a leaf reduces one exponent; the copies that grow back are copies of something strictly smaller than what was there, and adding any finite number of strictly smaller terms leaves the total below where it was. A strictly decreasing sequence of ordinals is finite. The fight ends.
The reason nothing simpler works is the same reason the theorem is famous. The length of the fight, as a function of the starting hydra, grows faster than every function Peano arithmetic can prove total. So there is no ordinary induction that establishes it: the statement “Hercules always wins” is true and unprovable in Peano arithmetic, and the induction the proof runs is an induction up to , which is exactly the strength arithmetic does not have.
That is Kirby and Paris’s actual result, and the hydra was constructed to demonstrate it.
Twenty chops, and then nothing
The counts in the first figure are the practical face of it.
A single head is one chop. A head on a neck is three. Two heads on a neck is ten. A head two levels deep — four nodes, a tree a reader can draw without thinking — is twenty.
Add one more level. A head three levels deep is five nodes, and 279 chops take it to forty thousand nodes, at which point the computation stops because the tree no longer fits in a sensible amount of memory. Two heads two levels deep is six nodes and does the same in 282.
That is the whole essay in two rows. The step from four nodes to five is the step from a number a reader can hold to a number no machine here will ever print, and there is no warning anywhere in the picture.
Three chops is where a drawing stops being readable, and the claim is about all twenty. So the same fight is worth having as a ledger, with the two quantities in columns and nothing drawn at all — because the interesting thing about it is not what the tree looks like but what happens to the ordinal beside it.
That last transition is the whole of the essay’s subject caught in one row. The moment the ordinal becomes finite, it becomes a bound: the fight is at fifteen after five chops, and there are exactly fifteen chops left. Nothing is left to be surprised by from there — the tree only shrinks, one node a move, and a reader can count to the end.
The first five chops are the ones with no such promise in them. The tree goes from four nodes to sixteen while the ordinal comes down through three transfinite values, and at no point during them is there a number saying how much longer the descent will take. A rank that is an ordinal past is not a bound; a rank that is a natural number is one; and this fight passes from the first to the second on move five, which is as close as a single picture comes to showing what the difference is.
The three quantities, and which one is doing the work
Watching a fight, three numbers are available and it is worth saying what each one does.
The node count goes up and down without pattern. In the ten-chop fight tabulated above it rises on three moves and falls on seven, and nothing about the sequence suggests a bound.
The number of chops so far goes up by one each time, which is not information.
The ordinal goes down, strictly, every single time. Ten of ten in that fight, and the theorem says it in general.
That third quantity is not a count of anything visible. is the ordinal of a hydra with two heads on a neck, and there is no collection of two things in the picture that is counting. What it does is order the possible hydras in a way that every legal move respects — and ordering is all a termination proof needs.
What this has to do with a game
Two things, and it is worth separating them from what it does not.
The hydra is not a partizan game in the sense of this site. There are two participants and only one of them has choices that matter — the hydra’s growth is forced, and the theorem holds for every choice Hercules makes — so it has no outcome class and no value, and nothing in the site’s evaluator will evaluate it. What it is, exactly, is a termination argument with a game’s clothes on.
The first connection is that a real game on this site has the same shape. Sylver Coinage is a genuine two-player impartial game: players name positive integers that are not sums of multiples of earlier ones, and whoever names loses. It must end, because the set of unnameable numbers only grows and a numerical semigroup’s complement is finite — but the length of a game is not bounded by any function of the first move, and no strategy is known for a great many openings.
The second is that the same distinction between “ends” and “ends by a known time” runs through the whole subject. A game that ends within moves is a game a solver can search. A game that merely ends is a game a solver may run on for ever without being wrong.
A finite rank bounds the game; an ordinal one does not
The ordinal is described above as an ordering that every move respects, and that is exactly what every termination argument on this site is — a rank, a function from positions into a well-ordered set that strictly decreases along every move. What the hydra supplies is the case where the well-ordered set has to be bigger than the numbers.
The difference between the two cases is one line, and it is the whole of “ends” against “ends by a known time”.
If the rank is a natural number, the game is bounded by it. A position of rank has every play descending through strictly smaller naturals, so the play is over in at most moves. Nim’s rank is the counter total and a game of Nim lasts at most that many moves; Domineering’s is the free-square count; Hackenbush’s is the edge count. In every one of those the rank is a bound, automatically, with no further argument.
If the rank is an ordinal past , nothing follows about the length. A hydra of rank descends through ordinals below , and there are infinitely many of those, so the descent is finite and its length is not determined by the rank at all. The chops each choose which smaller ordinal comes next, and the choices can be extravagant.
So the two clauses a reader runs together — there is a decreasing quantity and there is a bound — are the same clause exactly when the quantity is finite, and come apart the moment it is not. The hydra is not a game with an unusually large bound. It is a game with a rank and no bound, and those are different situations.
Which is the boundary a solver actually meets
That is worth stating in the solver’s terms, because it decides which of two very different tools applies.
A finite rank licenses depth-limited search. Compute the rank, search to that depth, and the search is complete — anything not found by then does not exist. Every exhaustive census on this site works that way, and the depth limit is not a heuristic cut-off but a theorem.
An ordinal rank licenses nothing of the kind. There is no depth at which “not found yet” means anything, because the rank gives no depth. A solver can run correctly and for ever, and the difference between this fight is still going and this fight will never end is invisible from inside it — even though the second is known to be impossible.
That is the uncomfortable position, and it is worth naming as the shape it is: the theorem guarantees termination and refuses to say when, so the guarantee is of no use to the one thing a solver needs. Knowing a search will finish is not knowing when to stop looking.
And it explains the two rows the essay makes so much of. Four nodes and twenty chops is a fight inside every bound; five nodes is a fight past every bound this machine has. Nothing about the pictures separates them because nothing about the rank separates them either — and are both ordinals with no finite content, and reading a size out of either is the mistake the caption warns against.
The game on this site with the same problem
Sylver Coinage deserves a paragraph of its own, because it is a real two-player impartial game with genuinely unbounded fights.
Players alternately name a positive integer that is not a non-negative combination of the numbers already named. Naming loses, because after nothing is left. The set of nameable numbers shrinks and the game ends — Dickson’s lemma, or the fact that a numerical semigroup’s complement is finite — and nothing bounds how long it takes: a player can name an enormous prime and extend the game by an enormous amount.
So the site already carries a game whose termination is a theorem rather than a count, and whose analysis is stuck for reasons that include it. What the hydra adds is the extreme case, where the length is not merely unbounded but not bounded by anything writable.
What a solver needs, and what it gets
This site’s recursion memoises on the position and terminates because the positions form a well-founded order. That is a stronger property than “every line of play is finite” and it is the property that matters computationally.
For a hydra there is no memoisation to be done — every position is visited once, because the tree never repeats — and no bound on the depth. The recursion is a loop rather than a search, and it runs until it runs out.
That also puts the hydra off the chart that what an exact evaluator reaches draws. Every family on it has a size on the horizontal axis and a count of positions on the vertical, and both are properties of a position a solver can read before it starts. A hydra has a node count and the node count predicts nothing: four nodes is twenty chops and five nodes is either seven, twenty-one, or a number this machine has not reached. There is no axis to put it on.
So the practical statement is not that the hydra is hard. Hardness is a statement about a growth rate and there is a growth rate here, in the sense that the number of chops is a definite finite number for every hydra. The statement is that the growth rate is not a function anybody can write down with the usual apparatus, and a bound that cannot be written cannot be planned against.
Three grades of ending
The games on this site sort into three grades and the sorting is worth having, because the grade decides what a solver can promise.
Bounded by the position. A Nim heap of ends within moves; a Domineering board of squares within ; a Hackenbush string of edges within . The bound is read off the picture, and a solver can allocate for it in advance. Almost everything here is in this grade.
Bounded, but not obviously. Sprouts ends within moves for spots, and the bound needs Euler’s formula rather than a count of anything visible. The rule that makes Go finite is a repetition ban, and without it the game does not end at all. Both are bounded and neither is bounded by inspection.
Unbounded and finite. Sylver Coinage. The hydra. A game where every line ends and no function of the starting position says when.
The middle grade is the one worth holding onto, because it is the grade a reader is likely to confuse with the third. Brussels Sprouts from three crosses lasts the same number of moves however it is played, and nothing on the paper says so — the length comes out of Euler’s formula, applied to a quantity that is conserved rather than one that decreases. A bound obtained from a theorem is still a bound, and the whole difference from a hydra is that the theorem produces a number. The hydra’s theorem produces an ordinal, and an ordinal past is not a number of anything.
The recursion this site runs works in all three, because well-foundedness rather than a bound is what it needs. What changes with the grade is whether it finishes — and in the third grade there is no answer to that question in advance.
What the picture cannot show
The ordinal is not a size. and are drawn beside four-node and five-node trees and there is nothing in either symbol that says the second fight is astronomically longer. Ordinals order the fights correctly and measure nothing.
Growth is not the enemy. A reader watching the tree explode will conclude that the growth is what makes the fight long, and it is the wrong reading: the growth is what makes it look endless, and the ordinal falling is what makes it end. The two facts are simultaneous and only one of them is about the outcome.
The rule is a choice. “Copy the subtree times on move ” is the standard rule and the theorem holds for any growth function whatever — copy it a googol times, or a number of times given by the current tree size, and Hercules still wins. What changes is only how long. That the theorem is indifferent to the growth rule is the clearest possible statement that the growth is not the point.
Who found it, and when
Kirby and Paris published the hydra in 1982, in a paper whose purpose was to exhibit a natural statement of arithmetic that is true and unprovable in Peano arithmetic. Gödel’s sentences had been known since 1931 and were widely regarded as artificial; the Paris–Harrington theorem of 1977 was the first natural example, and the hydra is the most vivid.
The reason it is a game rather than a process is presentational: a fight between a hero and a monster is a memorable way to display a decreasing ordinal, and Kirby and Paris knew it. The first theorem in this subject is also a statement about who wins that names no move, and the two have the same relation to the games they are about — both are results about determinacy rather than about play.
The Goodstein sequences are the other standard example and are the same phenomenon in a different costume: a sequence of integers that grows astronomically and provably reaches zero, by an ordinal argument, with no proof available in arithmetic.
The reason all three examples look like games or puzzles is not decoration. A statement that is true and unprovable has to be one whose truth is establishable by some argument, and the arguments available are transfinite inductions; a process that visibly terminates by an ordinal argument and visibly explodes otherwise is the clearest way to display the gap.
What the ordinal buys a reader
A last word on why the ordinal is worth learning rather than treating as machinery.
The two hydras the table gives up on differ from the ones it finishes by one level of nesting, and the ordinals record that exactly: for the one that dies in twenty chops, for the one that does not finish. One extra tower of exponentiation.
That is a compression of the situation that nothing else supplies. The node counts do not distinguish them — four against five — and the chop counts distinguish them only after the fact, by one of them being unavailable. The ordinal says the difference in advance, in two symbols, and it says it in the currency the theorem is stated in.
The sharpest form of it is inside the five-node hydras alone. There are three of them in the table and their fights are seven chops, twenty-one chops, and a number past two hundred and seventy-nine that this machine does not reach. Same node count, three answers, and the shortest of the three is short enough to draw entire.
Set that beside the other two five-node trees and the ordinals do the whole of the sorting. is seven chops, is twenty-one, and is past every number here — and those three ordinals are in that order, while the node counts are all five and say nothing.
The same holds across the whole table. Put the nine hydras in ordinal order and they come out in fight-length order too, on all seven of them whose fights finish: 1, 2, 3, 7, 10, 20, 21, with and above them and unreached. That is not a theorem and it is a fact about the table a reader can check, and it is the only column in the table that has the property.
So the ordinal is not merely the thing that makes the proof work. It is the only description of a hydra that predicts anything about the fight, and a reader who wants to know which of two trees is going to be worse has no other instrument.
Where the ladder goes next
The first rung out is the game version proper. Sylver Coinage is on this site already and its termination is a Dickson’s-lemma argument rather than an ordinal one; the interesting comparison is between the two kinds of unbounded-but-finite and what each costs a solver.
The second is the boundary. Between “ends in at most moves for a computable ” and “ends, with no computable bound” there is a hierarchy, and every level of it corresponds to a strength of induction. This site’s games are almost all at the bottom of it, which is why the recursion works, and knowing where a game sits is knowing what a solver can promise.
And the third is what a value would even mean for such a game. The recursion here computes a value by induction on the position, and the induction needs well-foundedness rather than a bound — so a game that terminates by an ordinal argument has values, in principle, defined by transfinite recursion. The recursion this site cannot run is the essay about where a finite interner stops, and this is the same wall from the other side: not a value too large to write, but a computation too long to reach it.
Part 2 of 4
One argument about Termination. The parts either side of it:
What links here
Essays that reach for this one mid-argument — the half of a link its own author cannot write down.
The objects named here
The third axis, after the field and the series: the games, values and theorems themselves, and every essay that touches each one.
Backward inductionCertificateComplexityEnding conditionExhaustive searchFixed length gameInductionIntractableNormal playOrdinalRecursionSurrealSylver CoinageTerminationUnsolved game
- A conjecture from hand play certificate, complexity, exhaustive search, intractable, termination
- A parity with a first exception exhaustive search, intractable, normal play, sylver coinage, unsolved game
- Proving a loss means answering everything certificate, complexity, exhaustive search, induction, normal play
- A point with three neighbours certificate, complexity, exhaustive search, intractable
- A puzzle asks once, a game asks alternately certificate, complexity, exhaustive search, intractable
- Every play ends and no round settles backward induction, induction, ordinal, termination