Rohit's Blog

The last of three, following “The Countdown Problem” by Graham Hutton (JFP 2002). Part 1 built a correct brute force program; part 2 calculated a fused version that was about twenty times faster and generated exactly the 4,672,540 valid expressions.

This post takes that to 245,644 by changing four lines. And the reason I wanted to write this series is what happens to the proofs when it does: nothing.

🔗Valid is not the same as useful

Part 2 ended with a program that constructs exactly the expressions that evaluate. Sounds optimal. It isn’t, because the search space is full of different spellings of the same thing.

Hutton puts it in one sentence: the language of arithmetic expressions is not a free algebra. It’s subject to equational laws, and a generator that ignores them enumerates each value many times over.

Two families of law do almost all the damage.

Commutativity. x + y and y + x are different expressions and the same number. Ditto x × y and y × x. Every commutative node in a tree doubles the count of ways to spell it.

Identity. x × 1 is a longer way of writing x. So is x ÷ 1. These don’t just duplicate — they inflate, because having spent a source number to achieve nothing, the expression is strictly worse than the one it wraps while occupying a slot in the search.

🔗Four lines

The fix is not a new algorithm. It’s a stronger valid.

Recall part 1’s version, which asked only whether the arithmetic stays in the positive naturals:

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

Strengthen it to reject the redundant spellings as well — for the commutative operators, insist the arguments arrive in numerical order; for multiplication and division, refuse a unit argument:

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

That’s it. That’s the optimisation. Nothing else in the program changes — results, combineR, subbags, solutions all stay exactly as part 2 left them.

🔗What it buys

I ran both versions rather than taking the paper’s word for it:

	valid	valid2	remaining
valid expressions built	4,672,540	245,644	5.3%
solutions found for 765	780	49	6.3%

Nineteen out of every twenty expressions we were building were redundant.

And the solution count drops from 780 to 49 — which is not a loss. Those 780 were mostly the same handful of solutions written out in every possible commuted form. Forty-nine is closer to the number of genuinely distinct ways to make 765, and it’s a far more useful thing to hand a person.

The paper’s timings, on 2002 hardware:

	fused	+ arithmetic properties	speedup
first solution	0.08 s	0.04 s	2×
all solutions	5.76 s	0.86 s	~7×
target 831 (none)	5.40 s	0.80 s	~7×

Hutton adds the practical claim that matters: for any source and target from the television version, the final program typically returns all solutions in under a second, and he had yet to find a case needing more than three. The thirty-second time limit that constrains human contestants stopped being the binding constraint.

Cumulatively, from part 1: 113.74 seconds to 0.86 seconds, about 130×, from one derivation and one predicate.

🔗The part I actually wanted to write about

Here is the sentence in the paper that made me want to do this series.

Changing valid changes the specification — isSolution is defined in terms of eval, which is defined in terms of valid. So we have a new specification and a new implementation, and the honest question is whether all that proof work from part 1 has to be redone.

It does not. None of the proofs depend on the definition of valid.

Look back at what was actually proved: that split inverts append; that filtering distributes over membership; that nesplit returns strictly shorter pieces; that exprs inverts values; and, from those, that solutions agrees with isSolution. Every one of those is a statement about list structure. valid appears in the program as an opaque predicate that is either true or false, and no lemma ever asks what it computes.

So the correctness results carry over to the new predicate unchanged. The program got 130 times faster and the proof burden did not move.

That is not luck. It’s a consequence of where the abstraction boundary was drawn — valid was a parameter of the reasoning rather than part of it. And it generalises well past this paper: if your correctness argument is parameterised over the thing you expect to tune, you can tune it for free. The corollary is the useful one — when you find yourself unable to change something without redoing an argument, that’s a sign the argument was entangled with a detail it didn’t need.

I have made this mistake. Proofs are rare in my work, but tests have the same property, and a test suite that breaks whenever you change a heuristic is a suite that was testing the heuristic instead of the behaviour.

🔗Sound, and complete up to equivalence

One piece of care that’s easy to skip past. Strengthening valid changes what counts as a solution, so what exactly have we preserved?

The paper’s answer is a two-part claim:

Sound: anything the new specification calls a solution really is one under the original. We haven’t invented answers.
Complete up to equivalence: anything that was a solution under the original can be rewritten, using the exploited laws, into one the new version finds. We haven’t lost answers — only alternative spellings of answers we still find.

That second clause is doing the real work, and it’s the right shape for this kind of optimisation. We’re not claiming the same output; we’re claiming the same output modulo an equivalence we named. Which is only meaningful because the equivalence was written down — commutativity of + and ×, unit laws for × and ÷, and nothing else.

Anyone who read the algebra series will recognise this as observational equality wearing different clothes: two things are the same if you can’t tell them apart by the criterion you specified. Here the criterion is the arithmetic laws.

🔗What I’d take from the paper

Optimisation as a sequence of justified steps. Part 2’s fusion had no ideas in it — six transformations, five of them definition-unfoldings. Part 3’s had one idea, expressible in four lines. Neither required cleverness; both required knowing precisely what the program was meant to do before making it faster.

Where you draw the abstraction boundary determines what you can change later. valid being an opaque parameter is why a 130× speedup cost nothing in proof.

And a pearl should stay a pearl. Eight pages, one example, two optimisations, a real result. When I recommended this paper I said not to pad it into a long series, and having written three posts I’d say three is the ceiling — there’s a version of this that’s one post and loses very little.

🔗The Scala 3 postscript

Three things worth carrying:

Laziness is a decision here, not an ambience. The paper’s “first solution” timings only mean something in a lazy language. With List, first and all cost the same; you need LazyList to have the benchmark at all. That’s now the third time this has come up on this blog, and the pattern is consistent: Haskell’s laziness is a property of the setting, Scala’s is a property of the type you picked.

Memoisation is nearly free in Scala, and it’s the paper’s own future work. Hutton lists tabulation as a direction not taken. When I ran the counts I memoised results on the input list, and it’s a two-liner — List[Int] has structural equality and hashing, so a mutable.HashMap[List[Int], List[Result]] just works. That’s the same finding as the contracts series: a first-order ADT is a hashable one, and being hashable is what makes tabulation trivial. It matters more here than usual, because many different sub-bags produce the same list.

And the calculational style is available in Scala but not practised. for-comprehensions desugar by a specified rule, so part 2’s derivation is as sound here as in Haskell. What Scala lacks is the tradition, not the mechanism — which is a more interesting kind of gap than the ones this blog usually turns up, because it’s one that could close without any language changing.

🔗Sources

Hutton, Graham. The Countdown Problem. Journal of Functional Programming 12(6), 609–616, November 2002. The strengthened valid′ predicate, the soundness and completeness-up-to-equivalence claims, the observation that no proof depends on valid, the expression and solution counts, and all timings are his. Available from the author — eight pages, and better than my summary of it.

The Scala 3 translation is mine. I re-ran the algorithm to confirm the 4,672,540 / 780 and 245,644 / 49 figures before quoting them; the timings are the paper’s own, measured in 2002 on a 1GHz Pentium III, and are useful as ratios rather than absolutes.