The game the algorithm was playing

The game that decides what a sentence can say is a template, not a fact about first-order logic. Spoiler picks a point in one structure, Duplicator answers in the other, and after $k$ rounds the chosen points must induce the same pattern. Change any rule of that and the game measures a different language.

Two changes matter. Limit the pebbles — give the players a fixed supply that has to be lifted and reused — and the game measures the logic with a fixed number of variables. Change Duplicator’s move from picking one point to offering a whole bijection, from which Spoiler then chooses, and the game measures counting logic.

The second change is the one this rung is about, because the game it produces is not a curiosity. It is an algorithm that was already in use, under a different name, for a different purpose.

What colour refinement is #

Anybody wanting to test whether two graphs are the same starts by computing an invariant, and the standard first invariant is this.

Give every point the same colour. Then repeatedly recolour: a point’s new colour records its old colour together with the multiset of its neighbours’ colours. Stop when the partition into colours stops changing. Two graphs with different colour multisets are certainly different.

The algorithm is called one-dimensional Weisfeiler–Leman, or colour refinement, and it is fast, standard, and the first thing every practical isomorphism test runs. It is also incomplete: some non-isomorphic graphs come out with identical colourings.

The same thing, as a game #

Here is the bijective game. Duplicator must offer a bijection between the two vertex sets; Spoiler picks a vertex in one graph and the corresponding one is pebbled in the other; and with a fixed supply of $k$ pebbles, the oldest is lifted when a new one is needed.

To see why a bijection is the right move, consider what a single-element answer would allow. In the ordinary game Duplicator may inspect Spoiler’s choice before replying, which is a considerable advantage; it is what makes the ordinary game measure a logic with no counting in it. Requiring the bijection to be committed before Spoiler chooses removes exactly that advantage, and what it adds is counting: a bijection between the two vertex sets exists only when the sets are the same size, and a bijection respecting the pebbled structure exists only when the corresponding parts are the same size.

Duplicator survives the $(k+1)$-pebble bijective game for $r$ rounds exactly when $k$-dimensional refinement fails to separate the graphs within $r$ rounds. That is the Cai–Fürer–Immerman correspondence, and the figures check it on the pair above: two pebbles and Duplicator survives, three and Spoiler wins, matching one-dimensional refinement failing and two-dimensional refinement succeeding.

Read one way, the correspondence explains the algorithm. Colour refinement computes exactly what a two-variable counting sentence can express about a graph, and its incompleteness is the expressive limit of that logic. Read the other way, it explains the logic: a question about what a sentence can say has an answer that is a linear-time algorithm.

Neither field found this. It was found by noticing that two things were the same. The algorithm dates from 1968 and the logical characterisation from 1992.

The gap of twenty-four years is worth a sentence, because the two communities were not far apart. Refinement was published as a heuristic and analysed as a heuristic: papers about it asked how often it worked and how fast it ran, and answered both. What nobody asked was what it computed — what property of a graph its output is a complete record of — and that question has an exact answer which the heuristic framing makes invisible.

An algorithm described as “a fast way to try X” invites questions about speed and success rate. The same algorithm described as “the complete invariant for property Y” invites questions about Y, and Y here is a logic with its own theory. The relabelling did the work, which is a recurring pattern rather than an accident: the correspondence between the two views was not difficult once stated, and stating it required somebody who held both.

Why a cycle defeats it #

The failing pair is worth understanding, because the mechanism is the whole story of what refinement can and cannot see.

It is also worth running the algorithm by hand on the pair once, because it takes three lines. Every point starts colour 0. At the first round each point of both graphs reports “colour 0, with two neighbours of colour 0” — identical, so nothing splits. At the second round the report is the same sentence one level deeper, and it is identical again. The partition has stabilised at one class in both graphs after a single round, and no further round can change that, because refinement is a fixed-point computation and a fixed point that has been reached stays reached.

Refinement only ever looks at a point’s neighbourhood, then at neighbourhoods of neighbourhoods, and so on. Every point of a cycle has two neighbours, each of which has two neighbours, for as long as one looks. A cycle of six and two triangles are locally identical at every radius, and refinement is local by construction.

That is the same limitation locality states for first-order logic, arriving from a different direction. The connection is exact: a graph in which refinement never splits anything is a regular graph, and regular graphs are precisely the ones on which a two-variable counting sentence can say nothing beyond the degree and the size.

What refinement is really computing #

There is a third description of the same invariant, from linear algebra, and having all three makes the object hard to mistake for an accident.

Two graphs have the same colour refinement result exactly when their adjacency matrices $A$ and $B$ satisfy $AX = XB$ for some doubly stochastic matrix $X$ — a square matrix of non-negative entries whose rows and columns each sum to one. That is called fractional isomorphism, and the equivalence with refinement is a theorem of Ramana, Scheinerman and Ullman.

Read it beside the corners of the doubly stochastic polytope and the shape of the statement is clear. An actual isomorphism is a permutation matrix satisfying $AX = XB$; permutation matrices are exactly the corners of the doubly stochastic polytope; so fractional isomorphism is the relaxation of isomorphism obtained by allowing any point of the polytope rather than only a corner.

Colour refinement is a linear-programming relaxation of graph isomorphism, computed by an algorithm that mentions no linear programming at all. And the higher dimensions of refinement correspond to tighter relaxations, in the way a hierarchy of linear programmes tightens towards an integer answer.

Three descriptions: an algorithm that recolours, a game with a bijection, and a relaxation of a matrix equation. They agree exactly, which is the strongest evidence available that the object is natural rather than invented.

Going up a dimension #

The repair is to colour pairs of points rather than points. A pair’s colour records the colours of the two paths through every third vertex, and the resulting invariant is strictly stronger — it separates the cycle from the two triangles at once.

The two-dimensional version separates the failing pair for a reason that is easy to state. In a cycle of six there are pairs at distance three; in two triangles there are none, because nothing is more than one step from anything in its own triangle and pairs across the two components are at no distance at all. Colouring pairs notices the difference at the first round, and colouring points never can, because distance is not a property of a point.

The general version colours $k$-tuples and is called $k$-dimensional Weisfeiler–Leman, and it corresponds to the $(k+1)$-pebble game. Each dimension is strictly stronger than the last, so there is an infinite hierarchy of invariants, each computable in time about $n^{k+1}$.

The obvious hope is that some fixed dimension is complete — that $k$-dimensional refinement separates every pair of non-isomorphic graphs for some $k$ that does not grow. It is false, and the counterexamples are the reason the correspondence became famous: Cai, Fürer and Immerman built, for every $k$, a pair of graphs on a bounded number of points that $k$-dimensional refinement cannot separate. So no fixed-dimensional refinement decides isomorphism, and — by the correspondence — no fixed-variable counting logic expresses it.

That is a lower bound for an algorithm, obtained entirely by a logical argument. It is the clearest case on this ladder of the game paying for itself.

It is worth being precise about what the counterexamples do and do not rule out. They say no fixed dimension suffices. They do not say the required dimension grows quickly — and in fact for the constructed pairs it grows linearly in the number of points, which is as slow as a counterexample can manage while still being one. Nor do they say anything about the running time of any other method; isomorphism has a quasi-polynomial algorithm, found in 2015, which does not proceed by refinement at all.

So the correct summary is narrow and useful. Refinement, at any dimension one is willing to pay for, is a fast and incomplete invariant; the hierarchy it generates is strictly increasing; and the graphs that defeat it are constructed rather than encountered.

What a fixed number of variables buys #

The pebble version deserves a paragraph of its own, because it is the change with the most consequences elsewhere.

A sentence with $k$ variables can nest quantifiers arbitrarily deep, reusing the same variable names, so it can express things a $k$-round game would not permit. What it cannot do is refer to more than $k$ points at once. The pebble game captures that exactly: pebbles are variables, lifting a pebble is reusing a variable name, and the number of rounds is the depth.

Two-variable first-order logic is decidable, which is unusual and useful — most fragments are not — and the pebble game is how its properties are proved. Three variables and the decidability is gone.

The distinction between depth and variables is easy to lose and is worth one example. The sentence saying “there is a path of length three” can be written with four variables and depth four, or with two variables and depth four by reusing names: there is an x with a neighbour y, which has a neighbour x, which has a neighbour y. Reading that aloud is confusing and it is a legal sentence, and the pebble game is the machinery that says exactly which sentences can be compressed that way and which cannot.

So the number of variables is a resource with a sharp boundary, and the game measures it exactly. That is the same style of statement as the ones about quantifier depth on the rungs below, and it is worth noticing that the game adapted to a new resource without any change to its structure: the same alternation of moves, the same winning condition, a different accounting for what the players may keep.

What the correspondence does not settle #

Graph isomorphism is not known to be solvable in polynomial time, and nothing here changes that.

What the correspondence gives is a precise account of one family of methods. Refinement of every fixed dimension is a polynomial-time invariant and none of them is complete, so the whole family is ruled out — and every practical isomorphism program uses refinement anyway, as a fast first pass that succeeds on nearly every graph and is backed by a search when it fails.

The gap between “fails on some pairs” and “fails often” is worth stating. Refinement separates almost every pair of random graphs after one round, and the graphs it cannot handle are highly structured — regular graphs, strongly regular graphs, and the constructed counterexamples. An invariant that is incomplete in theory and nearly always sufficient in practice is the normal situation, and knowing exactly where it fails is what the game supplies.

A fourth field arrives at the same place #

The most recent identification is worth recording because it happened in a field that had never heard of any of this.

A message-passing neural network on a graph works by giving every vertex a vector, then repeatedly replacing each vector by a function of itself and the multiset of its neighbours’ vectors, and finally reading off a summary of all of them. That description is colour refinement with the colours replaced by vectors and the recolouring rule learned rather than fixed.

The consequence, proved in 2019, is exact: no message-passing network can distinguish two graphs that one-dimensional refinement fails to distinguish. The architecture’s expressive ceiling is the algorithm from 1968, which is the logic from 1992, which is the relaxation from 1994.

So a network of any size and any training cannot tell a cycle of six from two triangles, and the figure at the top of this rung is a complete account of why. That is an unusually sharp statement about a class of learned models, and the reason it could be proved at all is that the models’ update rule was already a well-understood object under three other names.

The practical response has been to add what refinement lacks — random identifiers on the vertices, or a higher-dimensional message passing that corresponds to the next level of the hierarchy — and each repair moves the ceiling to exactly the place the correspondence predicts.

What the pictures cannot show #

The bijective game is played out on graphs of six points and to a depth of three. The correspondence is a theorem about all graphs and all dimensions, and the figures verify one instance of it.

The Cai–Fürer–Immerman construction is described and not drawn. Its graphs are built from a gadget substituted at every vertex of an expander, and the smallest interesting case is already too large for a figure.

And two-dimensional refinement is computed as a colouring of pairs, with the multiset of colours reported. The colouring itself is a table of thirty-six entries per graph, which the figure summarises rather than shows.

Where the ladder goes next #

Named here as debts. The Cai–Fürer–Immerman graphs, which are the reason the hierarchy is strict and which would need a rung about the gadget. And two-variable logic’s decidability, proved by the pebble game and worth its own account.

Sideways, the game in its original form is the first rung, the locality that explains refinement’s blindness is the third, the random graphs refinement succeeds on almost always are the zero-one law’s, and a graph drawn as the map of a group is a Cayley graph, which is regular and therefore invisible to one-dimensional refinement.

What is worth carrying away #

When two fields have a hard problem each and one of them has a fast algorithm, it is worth asking what the algorithm computes rather than what it is for.

Colour refinement was written to test graphs for isomorphism and it computes the expressive power of a two-variable counting logic. Nobody designed it to do that, and the identification was made a quarter of a century later by somebody looking at both.

The habit worth taking is to ask what an algorithm’s output is an invariant of. An incomplete invariant is incomplete for a reason, the reason is usually a statement about what it can see, and a statement about what something can see is a logic.

The corollary is about the value of a negative result of this shape. Knowing that no fixed-dimensional refinement is complete is worth more than another dimension would be: it stops the search along that line and redirects it, and it does so with a construction rather than an intuition. A theorem that closes an approach is a service to everyone still working on it.