Rohit's Blog

Occasional writing on software engineering.

The Countdown Problem, Part 2: Calculating a Faster Program

scalaprogram-derivation

Following “The Countdown Problem” by Graham Hutton (JFP 2002). Part 1 formalised the game, wrote a brute force program, and established that it generates 33,665,406 expressions of which only 4,672,540 — under 14% — are valid at all.

This post fixes that. What I find worth writing about isn’t the speedup; it’s that the faster program is not designed. It’s calculated from a specification, mechanically, and the process is one most of us have never seen applied to code we’d actually ship.

🔗The waste, precisely

solutions does two things in sequence: generate every expression, then evaluate each one and keep those hitting the target.

The trouble is that generation doesn’t know what evaluation is about to discover. We build a complete expression tree, hand it to eval, and learn that a subtraction three levels down went negative — at which point the entire tree is garbage, along with every larger tree we were about to build on top of it.

Six sevenths of the work is spent constructing objects that are dead on arrival.

The fix, stated informally, is obvious: evaluate as you generate, so an invalid sub-expression is discarded before anything is built on top of it. Anyone would guess that.

The interesting part is what happens if, instead of guessing, you derive it.

🔗Specify the fused function

Give a name to what we want: a function returning valid expressions paired with their values.

type Result = (Expr, Int)

def results(ns: List[Int]): List[Result] =
  for
    e <- exprs(ns)
    n <- eval(e)
  yield (e, n)

That is not an implementation — it calls exprs, so it does all the work we’re trying to avoid. It’s a specification: a statement of what results must return, written in terms of things we already understand.

Now we calculate an implementation, by induction on the length of ns.

🔗The base cases

For the empty list, exprs gives nothing, so results gives nothing.

For a single number, exprs gives one expression and eval succeeds exactly when the number is positive:

def results(ns: List[Int]): List[Result] = ns match
  case Nil      => Nil
  case n :: Nil => if n > 0 then List((Expr.Val(n), n)) else Nil
  case _        => ???

🔗The inductive case

This is the heart of the paper. We start from the specification and rewrite, and I’ll label each step with its justification — the same discipline as the derivations in the tile algebra, except here it’s producing a program rather than a proof.

Start — the specification:

pairs (e, n) where e comes from exprs(ns) and n from eval(e)

Step 1 — unfold exprs. Replace exprs(ns) with its definition and flatten the nested comprehension:

pairs (e, n) where (ls, rs) comes from nesplit(ns), l from exprs(ls), r from exprs(rs), e from combine(l, r), and n from eval(e)

Step 2 — unfold combine. Its only job is to apply each of the four operators, so e is always App(o, l, r) for some o:

pairs (App(o, l, r), n) where … o comes from the four operators, and n from eval(App(o, l, r))

Step 3 — unfold eval. By definition, evaluating an application evaluates both sides and applies the operator when valid:

pairs (App(o, l, r), apply(o, x, y)) where … x comes from eval(l), y from eval(r), and valid(o, x, y)

Step 4 — move the generators. This is the only step requiring any thought, and it’s the one that does all the work. x depends only on l; y only on r. So the generator for x can slide left to sit immediately after l, and likewise y after r:

(ls, rs) from nesplit(ns), l from exprs(ls), x from eval(l), r from exprs(rs), y from eval(r), o from the operators, where valid(o, x, y)

Legitimate because reordering independent generators in a comprehension doesn’t change the result — a law about the list monad, not about Countdown.

Step 5 — spot the induction hypothesis. Look at what those adjacent pairs now say. “l from exprs(ls), x from eval(l)” is precisely the specification of results(ls). Same for rs. Fold them:

(ls, rs) from nesplit(ns), (l, x) from results(ls), (r, y) from results(rs), o from the operators, where valid(o, x, y)

The recursive calls appeared. We did not put them there; they emerged because step 4 arranged the generators into the shape of the thing we were defining.

Step 6 — name the inner part. The tail is “combine two results with each operator, keeping valid ones”, which wants a name:

def combineR(lx: Result, ry: Result): List[Result] =
  val (l, x) = lx
  val (r, y) = ry
  for
    o <- Op.values.toList
    if valid(o, x, y)
  yield (Expr.App(o, l, r), apply(o, x, y))

And we’re done:

def results(ns: List[Int]): List[Result] = ns match
  case Nil      => Nil
  case n :: Nil => if n > 0 then List((Expr.Val(n), n)) else Nil
  case _        =>
    for
      (ls, rs) <- nesplit(ns)
      lx       <- results(ls)
      ry       <- results(rs)
      res      <- combineR(lx, ry)
    yield res

def solutions2(ns: List[Int], n: Int): List[Expr] =
  for
    ns2     <- subbags(ns)
    (e, m)  <- results(ns2)
    if m == n
  yield e

Compare with exprs from part 1: the shape is identical, and the single difference is that combineR checks valid before constructing the node. An invalid combination is now never built, and nothing is ever built on top of it.

🔗Why this matters more than the speedup

I want to dwell on what just happened, because I think it’s the actual content of the paper.

We did not have an idea. We wrote down what we wanted in terms of what we had, and then applied six transformations, of which five were “unfold a definition” and one was “reorder independent generators”. At no point was there a creative leap. The recursion in the final program appeared in step 5 because step 4 put the pieces next to each other.

And correctness comes free. Since every step preserves meaning, the derived program equals the specification by construction. The paper’s proof that the fused version agrees with the brute force one is four lines, and it works by unfolding the specification of results back out again.

That’s a different relationship to correctness than testing. In the tile series I built an obviously-correct implementation, generated thousands of property tests from it, and used those to guard a rewrite. That works, and it’s what I’d do at work. But it establishes “we couldn’t find a difference”, whereas this establishes “there is no difference” — and it does so as a byproduct of writing the program, not as extra work afterwards.

The catch, and it’s a real one: this only scales to programs small enough to hold in your head. Countdown fits in eight pages. I have never calculated a program at work and I don’t expect to. What I have taken from it is narrower and still useful — when you optimise, try to find the sequence of meaning-preserving steps rather than the destination. If you can’t write down the steps, you don’t yet know why your optimisation is correct.

🔗How much faster?

The paper’s measurements, on 2002 hardware — the ratios are what matter:

brute forcefusedspeedup
first solution0.89 s0.08 s~10×
all 780 solutions113.74 s5.76 s~20×
target 831 (no solutions)104.10 s5.40 s~20×

Twenty times faster, from a transformation with no ideas in it.

The counts explain the number. We’ve gone from constructing 33,665,406 expressions to constructing 4,672,540 — exactly the valid ones and nothing else. That’s a factor of 7.2 in allocations, and the rest comes from not walking dead trees.

🔗Scala notes

The calculation is available in Scala, and nobody does it. Scala’s for-comprehensions desugar to flatMap/map/withFilter by a specified rule, so every step above is as justifiable here as in Haskell. Step 4 in particular — reordering independent generators — is sound for List in exactly the same way.

What’s missing isn’t a language feature; it’s the practice. Haskell has a calculational tradition going back to Bird and Meertens, and Scala doesn’t, so the tooling and the reflexes aren’t there. That’s a cultural gap rather than a technical one, which I find more interesting than if it had been the reverse.

One place Scala is genuinely worse. In combineR I wrote:

    for
      o <- Op.values.toList
      if valid(o, x, y)
    yield (Expr.App(o, l, r), apply(o, x, y))

The guard desugars to withFilter. On List that allocates an intermediate structure that Haskell’s list comprehension doesn’t. It won’t change the asymptotics, but on a hot path generating four and a half million results it’s the kind of thing that shows up in a profile, and the direct version is barely less readable:

    Op.values.toList.collect {
      case o if valid(o, x, y) => (Expr.App(o, l, r), apply(o, x, y))
    }

And the laziness point from part 1 still stands. These are Lists, so “first solution” and “all solutions” cost the same. To get the paper’s 0.08-second figure you need LazyList throughout, and the ratio in the table’s first row exists only in a lazy setting.

🔗Still 4.6 million

We now build exactly the valid expressions and nothing more, which sounds optimal.

It isn’t, because valid is not the same as useful. Among those 4,672,540 expressions, (1 + 50) and (50 + 1) both appear. So do x × 1 and x ÷ 1, which are elaborate ways of writing x. We are enumerating a search space in which enormous numbers of entries are different spellings of the same thing.

Arithmetic has laws. The next post uses them, and takes the search space down by another factor of nineteen.

Next: Part 3 — Exploiting arithmetic properties.

🔗Sources

  • Hutton, Graham. The Countdown Problem. JFP 12(6), 609–616, 2002. The specification of results, the six-step calculation, combine′, the fused solutions′, the equivalence theorem, and all timing figures are his. Available from the author.
  • Bird, Richard & Lambert Meertens — the calculational programming tradition this derivation belongs to.

The Scala 3 translation, the verified expression counts, the withFilter observation, and the note about the calculational practice being absent from Scala culture are mine.