Which games end at which level

The condition the recursion rests on is the ending condition every value on this site depends on: a game must end, or there is nothing for the recursion to bottom out at. Two ways to end with no bound compared the two games here that end and say nothing about when, and closed by naming the scale:

Between ends within a computable bound and ends, with no computable bound at all there are levels, each corresponding to a strength of induction, and knowing which level a game sits at is knowing exactly what a solver can promise about it. Placing this site’s games on that scale would be a piece of work with an answer for every one of them.

The scale has a concrete rung-ladder in it, and the reason this can be measured rather than argued is that a level is decided by an object.

A level is a measure #

To know a game ends, exhibit a termination measure: a quantity that every legal move strictly decreases, in an order with no infinite descending chain. There is nothing else to it. The measure is the proof, and the level a game sits at is the level of the order the measure lives in.

That turns a question about proof strength into a question about a function on positions, and a function on positions is something a sweep can check.

It is worth saying why the definition has two clauses and not one. Strictly decreases on its own is not enough: the rationals between 0 and 1 decrease strictly for ever, and so would a measure landing in them. What rules that out is the second clause — the order must have no infinite descending chain, which is what well-founded means — and the levels of the scale are exactly the well-founded orders of increasing strength. The naturals are the smallest one anybody uses; the ordinals below ε₀ are much larger and still well-founded; and what makes a level higher is that proving its order well-founded takes more.

Most of this site sits at the bottom of the scale.

Nim’s measure is the number of counters. Every move removes at least one.

Cutcake’s is the number of cells less the number of pieces. A cut leaves the cells alone and makes one more piece, so it goes down by one — which is a better measure than the obvious ones, since neither the cells nor the pieces move in the right direction on their own.

Toads and Frogs’ is the total distance the pieces still have to travel: for each toad, how far it is from the right end, and for each frog, how far from the left. A step moves one piece one square in its own direction and a hop moves it two, so the measure falls by one or two.

That last one is the interesting measure of the three, because Toads and Frogs is the game on this site with the least well-behaved values — the strip nobody has a formula for is the same game — and its termination is the simplest thing about it. A game can be at the bottom of this scale and impossible to solve, and Toads and Frogs is the standing example of both at once.

All three are natural numbers and all three are checked on every move of every position in range — several thousand moves, no exceptions. A measure into the naturals is ordinary induction, and a solver looking at one of these games can promise a bound before it starts.

Where the naturals run out #

Sylver Coinage’s natural measure is the set of numbers not yet expressible from the ones named. Every move names one of them, so the set shrinks, and the game must end when it is empty.

Except that it is not a number for most of the game. With nothing named, infinitely many numbers remain. With 5 named, infinitely many. With 4 and 6 named — two numbers sharing a factor — still infinitely many, because nothing odd will ever be expressible from them. Only once the named numbers have no common factor does the set become finite: 3 and 5 leave four gaps, 2 and 3 leave one.

So there is no natural number descending during the opening of the game, and the argument that Sylver Coinage ends is not a count. It is a well-quasi-ordering argument — the observation that a sequence of sets of this kind cannot decrease for ever, which is Dickson’s lemma — and that is a strictly stronger principle than induction on the naturals.

The failure is also not a technicality about the first move or two. {4, 6} is a perfectly ordinary position — two numbers named, the game well under way — and it has infinitely many numbers still nameable, because everything odd is out of reach for ever. A game that stays in the even numbers stays infinite, and the players decide when it stops doing so.

That is the property worth carrying: the position at which the measure becomes a number is chosen by the players. No function of the starting position says when it happens, because nothing has happened at the start.

That is the difference the rung below could see and not name. Sylver Coinage does have a computable bound once the numbers are coprime, and getting to coprime is the part with no bound on it.

Where the measure goes up #

The hydra is at the top, and what puts it there is not the size of the numbers.

Chop a head from a hydra and the hydra makes copies of a subtree. From a small starting hydra the node count rises on half the chops — so the obvious measure is not merely unbounded, it is going the wrong way, and no amount of patience will find a natural number that descends.

What does descend is an ordinal. Assign each hydra the ordinal its tree spells out and the sequence runs ω^ω + ω, then ω^ω + 2, then ω^ω + 1 — down, while the tree gets bigger. Ordinals below ε₀ have no infinite descending chain, so the game ends, and the principle that says so is transfinite induction to ε₀, which is exactly the principle Peano arithmetic does not have.

The second step of that sequence is the one to look at. Going from ω^ω + ω to ω^ω + 2 is a drop past infinitely many ordinals, and it happens on a chop that made the tree larger. So the ordinal is not a disguised size: it is reading the shape of the tree, and the shape is getting simpler in a sense the node count cannot express while the size is getting bigger.

That is the whole of why an ordinal is needed rather than merely convenient. A measure has to fall on every move, and no arithmetic function of a hydra falls on every chop.

That is the sharp end of the scale and it is where the anchor’s interest has always been. A game whose termination needs a principle stronger than arithmetic is a game about which arithmetic can prove nothing useful.

The one that does not end at all #

There is a fourth place on the scale and it is off the end of it.

A loopy game does not end, and no measure descends because there is nothing for a measure to do. That is not a fourth level of the same scale; it is the failure of the condition the whole scale is about, and it is why the loopy anchor has to build a theory out of outcomes rather than values.

Putting the two anchors side by side gives the honest picture of what the ending condition buys. A game with a measure into the naturals has values computed by a recursion that visibly stops. A game with a measure needing an ordinal has values computed by a recursion that stops for reasons the computation cannot state. A game with no measure has no recursion, and the theory starts again from who wins.

What the levels are not #

Three things this classification does not measure, and each of them is what a reader is likely to think it does.

It is not how long a game takes. A bounded game can take longer than anybody will wait — a Nim position with a googol counters is at the bottom of this scale — and the hydra from a small start finishes in a few dozen chops. What separates the levels is what a proof has to quantify over, not what a play costs.

It is not about who wins. A termination measure says the game stops and says nothing about how it stops or who is standing at the end. All three levels here are compatible with any outcome, and the hydra is not even a two-player game in the ordinary sense — it is a one-player process the anchor borrows because its termination is the extreme case.

It is not how hard the game is to solve. Sylver Coinage’s open problem is who wins after 16, which has nothing to do with termination and is unsolved for entirely different reasons; the games at the bottom of this scale include several nobody can solve either.

And it is not a property of the game so much as of the argument. A measure is exhibited, not derived: a cleverer measure could put a game lower, and the level a game is at is the lowest level any measure reaches. The three levels here are three measures that work, and nothing rules out a better one for Sylver Coinage. For the hydra something does — the Kirby–Paris theorem is precisely the statement that no arithmetic argument suffices — and that is why the hydra’s level is a fact and the others are ceilings.

What a solver can promise #

The point of the scale, as the rung below put it, is what a solver can promise.

At the bottom the promise is complete: a bound computable from the position, before the search starts. This site’s value machinery relies on that everywhere — every generator here walks a game tree and stops, and it stops because a measure it never mentions is descending.

At Sylver’s level the promise is conditional: no bound now, a bound once the game reaches a certain state, and no way to say how long that takes. A solver can be written and cannot be given a timeout.

At the hydra’s level there is no promise at all that arithmetic can state. The game ends, the proof is real, and nothing expressible in the language a program is written in gives a bound.

That is a genuinely practical distinction and it is the reason this rung is worth having as more than taxonomy. A search that will finish and a search that will finish for reasons the search cannot articulate behave the same until they do not.

It also says something about where a solver’s effort belongs. At the bottom level the useful engineering is a better bound — a tighter measure means a smaller search — and every optimisation this site’s generators make is of that kind. At Sylver’s level a better bound is not available and the useful work is a test: recognising the state at which the measure becomes finite, so that the solver knows when it has entered the part it can promise something about. At the hydra’s level there is nothing to engineer.

That is three different jobs for a programmer, decided by a fact about proof theory, which is not a connection anybody expects to be practical.

What is measured #

Four games and three levels. The site has many more games than four, and the ones checked here are the ones whose measures are short enough to state — the rest are at the bottom of the scale for the same reasons, by measures of the same kind.

The “same kind” is worth naming since it covers most of the site. Almost every game here removes something on every move — an edge, a domino, a stone, a counter — so the count of the removable thing is a measure and the game is at the bottom. The games that are not obviously of that shape are the ones where a move adds something: Cutcake adds a piece, Sprouts adds a spot, the hydra adds subtrees. Two of those three have a measure anyway and the third is the hydra.

The measures are exhibited, not searched for. Nothing here looked for the best measure; each is one that works, verified on every move in range.

And the sweeps are small. Nim to three heaps of six, Cutcake to six by six, Toads and Frogs to six squares — a few thousand moves. The measures are exact statements about the move rules and the sweep is a check on the statement rather than evidence for it, which is the opposite of most measurements on this site and is worth saying so it is not read the other way.

What the sweep is for is a measure stated wrongly, and the wrong statement it guards against is a specific one. A measure that counted only the toads’ distance would decrease on every Left move and rise on every Right one, and it would look like a measure to anybody who checked one player’s moves. A measure has to fall for both players — that is what makes it a measure of the game rather than of one player’s progress — and checking every move of both sides is the difference between a measure and a plausible quantity.

The same trap is available in Cutcake, where the number of pieces rises and the number of cells is constant, so either quantity alone is useless and their difference is the measure. Writing that one down correctly is the only part of this page that took any thought.

Why a level is exhibited rather than assigned #

Nothing here classifies a game by inspecting its rules. Each level is established by producing the ordinal that decreases, and a game sits at a level because somebody wrote that quantity down and checked it falls at every move.

That is why the classification has three levels rather than a spectrum: the levels are the strengths of induction anybody has needed, and a fourth would arrive with a game whose termination proof needs something stronger. It is a record of what has been proved, not a taxonomy waiting to be filled in.

Where the ladder goes next #

termination has four rungs: the condition the recursion needs, a game that ends with nothing saying when, two such games compared, and now the scale they sit on.

The rung above is the middle. Sylver Coinage is placed here by exhibiting a measure that needs Dickson’s lemma, and that places an upper bound on its level rather than pinning it: a measure into the naturals, if one exists, would move it down. The natural attempt is a measure combining the gap count with something that decreases while the gaps are infinite — the number of distinct prime factors the named numbers share, say, which falls to one exactly when the gaps become finite. Whether that combination descends on every move is a checkable question of the same shape as everything on this page, and it would either move Sylver Coinage to the bottom of the scale or say why nothing of that shape can.

Two neighbours are worth the trip. It ends, and nothing says when is the hydra taken on its own terms, where the ordinals are the subject rather than the top of a scale. And the condition the recursion rests on is what all of this is in aid of: every value on this site exists because a measure nobody wrote down is descending.