Rohit's Blog

Occasional writing on software engineering.

The Countdown Problem, Part 1: A Specification and a Program Too Slow to Run

scalaprogram-derivation

This series works through “The Countdown Problem” by Graham Hutton (JFP 12(6), 2002) — a functional pearl that starts from a formal specification of a numbers game, derives a brute force program, proves it correct, and then calculates two successive optimisations that between them make it about 130 times faster.

It’s eight pages. It is the tidiest demonstration I know of a discipline I keep circling on this blog: specify first, derive second, optimise by algebra third. The Scala 3 is mine.

🔗The game

Countdown is a British television programme that has been running since 1982. In the numbers round, contestants are given six source numbers and a three-digit target, and have thirty seconds to build an arithmetic expression hitting the target.

The rules, stated precisely:

  • Use each source number at most once — you don’t have to use them all.
  • Only +, −, ×, ÷.
  • Every intermediate result must be a positive whole number. No negatives, no zero, no fractions.

That last constraint is the one that makes the problem interesting rather than routine. Subtraction and division aren’t closed over the positive naturals, so most of the expressions you can write down don’t mean anything.

The paper’s running example: source numbers 1, 3, 7, 10, 25, 50 and target 765. One solution is (1 + 50) × (25 − 10) = 51 × 15 = 765. There are, as we’ll confirm shortly, 779 others.

Hutton is explicit about one modelling decision that matters: he does not generalise the positive naturals to integers or rationals, because doing so would fundamentally change the computational complexity. The awkward domain is the problem.

🔗Formalising it

Operators, and a predicate saying when applying one is legal:

enum Op:
  case Add, Sub, Mul, Div

def valid(o: Op, x: Int, y: Int): Boolean = o match
  case Add => true
  case Sub => x > y
  case Mul => true
  case Div => y != 0 && x % y == 0

def apply(o: Op, x: Int, y: Int): Int = o match
  case Add => x + y
  case Sub => x - y
  case Mul => x * y
  case Div => x / y

Then expressions, the numbers they use, and their value:

enum Expr:
  case Val(n: Int)
  case App(o: Op, l: Expr, r: Expr)

def values(e: Expr): List[Int] = e match
  case Val(n)       => List(n)
  case App(_, l, r) => values(l) ++ values(r)

def eval(e: Expr): List[Int] = e match
  case Val(n) => if n > 0 then List(n) else Nil
  case App(o, l, r) =>
    for
      x <- eval(l)
      y <- eval(r)
      if valid(o, x, y)
    yield apply(o, x, y)

eval returning a list deserves a note, because it looks odd. The convention is that a singleton list means success and the empty list means failure — so it’s Option wearing a different hat.

Hutton says why he chose it: failure could equally be handled with Maybe and do-notation, but restricting himself to the list monad and comprehension notation leads to simpler proofs. Since the whole paper is proofs and calculations, that’s the deciding factor.

In Scala the same choice is available and the code is nearly identical either way — for-comprehensions work over Option too, because Option has withFilter and so the guard desugars fine. I’ve kept List to stay close to the paper, and because part 2’s calculation reads better when everything is one monad.

🔗The specification

Now the part that makes this a derivation rather than a program. Before writing anything that searches, write down what it would mean to have succeeded.

Source numbers may be used at most once and in any order, so the numbers appearing in a solution must form a sub-bag of the source list — some sub-sequence, in some order:

def subbags[A](xs: List[A]): List[List[A]] =
  for
    ys <- subsequences(xs)
    zs <- ys.permutations.toList
  yield zs

And then:

def isSolution(e: Expr, ns: List[Int], n: Int): Boolean =
  subbags(ns).contains(values(e)) && eval(e) == List(n)

That’s the whole specification. An expression solves the problem if its numbers are a sub-bag of the sources, and it evaluates to the target.

Note what it isn’t: it isn’t executable in any useful sense — it tells you how to check a candidate, not how to find one. It’s a predicate, and the rest of the paper is about finding a program that agrees with it.

Anyone who has followed the algebra-driven design series will recognise the move. Write down the observation that defines correctness; only then go looking for something fast.

🔗Brute force

The obvious program: generate every expression over every sub-bag, keep the ones that hit the target.

First, splitting a list every possible way, keeping only splits where neither side is empty:

def split[A](xs: List[A]): List[(List[A], List[A])] =
  (0 to xs.length).toList.map(i => xs.splitAt(i))

def nesplit[A](xs: List[A]): List[(List[A], List[A])] =
  split(xs).filter((l, r) => l.nonEmpty && r.nonEmpty)

Then the key function — every expression whose values are precisely a given list:

def exprs(ns: List[Int]): List[Expr] = ns match
  case Nil      => Nil
  case n :: Nil => List(Expr.Val(n))
  case _        =>
    for
      (ls, rs) <- nesplit(ns)
      l        <- exprs(ls)
      r        <- exprs(rs)
      e        <- combine(l, r)
    yield e

def combine(l: Expr, r: Expr): List[Expr] =
  Op.values.toList.map(Expr.App(_, l, r))

Split the numbers every way, build every expression over each side, join them with each of the four operators. And finally:

def solutions(ns: List[Int], n: Int): List[Expr] =
  for
    ns2 <- subbags(ns)
    e   <- exprs(ns2)
    if eval(e) == List(n)
  yield e

Generate everything; keep what works. Fifteen lines, obviously correct, and — as we’re about to see — hopeless.

🔗How bad is it?

Bad in a way you can compute exactly, which I rather enjoy.

Let E(k) be the number of expressions over a list of length k. There’s one expression over a single number, and for longer lists you split at each of the k−1 interior points, build everything on both sides, and join with any of 4 operators:

E(1) = 1
E(k) = 4 · Σ E(i) · E(k−i)     for i = 1 … k−1

Which gives 1, 4, 32, 320, 3584, 43008 for lengths one to six.

The number of sub-bags of a six-element list is Σ C(6,k) · k! = 1957. Weight each by the expression count for its length and the total is:

33,665,406 expressions.

Of those, how many are valid — how many evaluate at all, given that subtraction must not go negative and division must be exact? I ran this rather than trusting my arithmetic:

4,672,540, which is just under 14%.

Over 86% of the work is wasted. We construct thirty million expression trees and throw almost all of them away, and we only discover a tree is worthless after building it.

And the answer we wanted: for target 765, there are 780 solutions. Change the target to 831 and there are none at all.

I verified the 4,672,540 and 780 figures by running the algorithm, and derived the 33,665,406 from the recurrence above. They match the paper. Where I quote timings later in this series they’re the paper’s own, measured in 2002 on a 1GHz Pentium III — useful for ratios, meaningless as absolute numbers today.

🔗Proving it correct

Here’s where a pearl differs from a blog post. Having written a program, Hutton proves it agrees with the specification, and the proof is a chain of small lemmas, each by induction:

  • split is an inverse to append: (xs, ys) is in split zs exactly when xs ++ ys == zs.
  • Membership of a filtered list is membership plus the predicate.
  • Therefore nesplit is an inverse to append for non-empty lists.
  • Therefore the pieces nesplit returns are strictly shorter than the original — which is what makes the recursion in exprs terminate.
  • Therefore exprs is an inverse to values: e is in exprs ns exactly when values e == ns.

And that last one, plus a few lines of equational reasoning, gives the theorem: e is in solutions ns n exactly when isSolution(e, ns, n).

I’m summarising rather than reproducing, but I want to flag the shape, because it’s the thing worth stealing. Each lemma is small and provable by induction; each is used to establish the next; the top-level theorem is then four lines of substitution. Nobody proves “the program is correct” in one go — they prove that exprs inverts values, and correctness falls out.

The Scala equivalent would be property tests, and they’d be good ones — forAll { e => exprs(values(e)).contains(e) } is a strong property that would catch real bugs. But it’s worth being honest that a property test is a different thing from a proof, and this paper is a reminder of what the stronger thing looks like when the program is small enough to admit it.

🔗One thing that doesn’t survive the port

The paper reports that the brute force version returns the first solution in 0.89 seconds, and all solutions in 113.74 seconds.

That gap only exists because Haskell is lazy. solutions describes a list; asking for its head does a small fraction of the work of asking for all of it.

The Scala above returns List, which is strict. Ask for the first solution and you have already computed all 780. There is no 0.89-second case; there’s only the 113-second one.

The fix is to be explicit, as it always is in Scala:

def solutions(ns: List[Int], n: Int): LazyList[Expr] =
  for
    ns2 <- subbags(ns).to(LazyList)
    e   <- exprs(ns2).to(LazyList)
    if eval(e) == List(n)
  yield e

This is the third time laziness has come up on this blog as a porting concern — it made an infinite tree representable in the music series, and it was a memory hazard in the contracts series. Here it’s neither: it’s the difference between a headline benchmark existing and not existing.

The general lesson I’m converging on is that laziness in Haskell is ambient — it shapes what the published numbers even mean — whereas in Scala it’s a decision you make per data structure, and if you don’t make it deliberately you get a different program with the same type.

🔗Where we’re going

We have a specification, a correct program, and a program that is unusable.

The interesting thing about the 14% figure is when we learn it. We build a full expression tree and only then discover that a subtraction went negative three levels down. The fix is to find out earlier — to interleave generation and evaluation so that invalid expressions are killed as they’re built.

The pearl’s move is that this is not invented. It’s calculated: you write down a specification of the fused function and grind out an implementation by induction, and each step is a definition unfolded or a law applied.

Next: Part 2 — Fusing generation and evaluation.

🔗Sources

  • Hutton, Graham. The Countdown Problem. Journal of Functional Programming 12(6), pages 609–616, November 2002. The formalisation, the split/nesplit/exprs/solutions program, the lemma chain, the correctness theorem, and all the timing figures are his. Freely available from the author’s page — it’s eight pages and worth reading directly.
  • Bird, Richard & Philip Wadler. An Introduction to Functional Programming. Prentice Hall, 1988 — the source of subs and perms.

The Scala 3 translation, the expression-count derivation, and the note on strict List versus LazyList changing what the paper’s benchmark means are mine.