research!rsc: Pulling a New Proof from Knuth’s Fixed-Point Printer

In a tribute to Donald Knuth's 88th birthday, Russ Cox revisits a classic problem from Knuth's 1989 paper, "A Simple Program Whose Proof Isn’t." The problem is to convert a 16-bit fixed-point binary fraction into its shortest, correctly rounded decimal representation. Knuth's original program, P2, was effective but notoriously difficult to prove correct in a simple, insightful way. Cox's post offers a new proof, not by tackling P2 head-on, but by starting with a much simpler program and transforming it into P2, proving the correctness of each step along the way.

The Problem and a Trivial Starting Point

The core task is to find the shortest decimal d (e.g., 0.39999) for a 16-bit binary fraction f = n / 2^16 that, when converted back to binary, yields the original f. This requires the decimal to be both accurate (rounding back to f) and correctly rounded (the best possible representation for its number of digits).

Cox begins by defining the "accuracy interval" for f, which is [f - 2^-17, f + 2^-17). Any decimal within this interval is accurate. He then establishes a crucial lemma: for up to 4 decimal places, this interval is narrow enough to contain at most one such decimal. This means that for shorter outputs, finding any decimal in the interval is sufficient.

This insight leads to a simple, provably correct algorithm:

1. Start with 1-digit decimals.
2. Check if the correctly rounded decimal for f lies within the accuracy interval.
3. If it does, return it.
4. If not, increment the number of digits and repeat.

Because the accuracy interval has a fixed width while decimal spacing shrinks, a solution is guaranteed by the 5th decimal place. This program is straightforward to prove correct because its logic directly mirrors the mathematical definitions.

The Path of Transformation

The heart of the article is the series of verified transformations that turn this simple program into Knuth's P2. Each step is a logical optimization that can be proven correct in isolation:

1. Walking the Digits: Instead of re-calculating the rounded decimal at each step, the algorithm can be seen as "walking" along the decimal representations of the interval's endpoints (min and max). The digits of the final answer are simply the digits where min and max first diverge. This allows the program to collect digits one by one.

2. Premultiplication: To avoid expensive repeated divisions by powers of ten, the algorithm can premultiply f, min, and max by 10 at the start of each iteration. This simplifies the arithmetic significantly.

3. Change of Basis: Knuth's P2 uses a clever basis to reduce the number of variables. Instead of tracking f, min, and max, it tracks s (which corresponds to the scaled max) and t (the width of the interval). This change simplifies the loop's arithmetic to just a few operations.

4. Scaling and Integer Arithmetic: The final step is to scale all values by 2^16 to work entirely with integers, eliminating the need for rational arithmetic. This makes the algorithm efficient on machines without hardware floating-point support.

By proving each of these transformations preserves the program's correctness, Cox arrives at Knuth's P2, having provided a clear, comprehensible proof along the way.

Context: Other Solutions and Historical Notes

The article doesn't stop at P2. Cox explores several other approaches:

• A Simpler Modern Version: He shows a slightly different formulation that is arguably clearer and avoids the need for collecting digits one at a time, making its proof even simpler. This version, however, might require 64-bit integers, which were not readily available when Knuth first wrote the code.

• The Schubfach Algorithm: He briefly mentions this highly efficient algorithm, which avoids iteration by calculating the range of valid decimals directly. It's a more advanced solution for modern systems.

• The Textbook Solution: Cox uncovers a fascinating historical puzzle. The algorithm is very similar to one presented in exercise 4.4-3 of Knuth's own The Art of Computer Programming, Volume 2. However, the textbook version, while finding the shortest decimal, does not guarantee correct rounding. A later correction by Steele and White fixed this, and Knuth included it in later editions. Cox speculates on why Knuth might have re-invented a variant in 1984 rather than using the one from his book—perhaps a simple case of forgetting to check his own work, or perhaps the textbook version seemed too complex at the time.

Conclusion: The Role of Tools in Thought

Ultimately, Cox argues that the tools we use fundamentally shape our programs and our ability to reason about them. Knuth's original P2 was a brilliant piece of engineering for the constrained 32-bit systems of the 1980s, where operations like division were costly. A modern language like Ivy, with its arbitrary-precision rationals and concise notation, makes it possible to start with a conceptually simple program and then apply optimizations as a separate, provable step.

This approach allows the proof to follow the structure of the ideas, rather than being a monolithic, after-the-fact justification. It demonstrates that a good proof can be built incrementally, making a difficult problem comprehensible and educational, which was Knuth's original goal all along.