research!rsc: Pulling a New Proof from Knuth’s Fixed-Point Printer (Floating Point Formatting, Part 2)

research!rsc

Thoughts and links about programming,<br>by Russ Cox

RSS

Pulling a New Proof from Knuth’s Fixed-Point Printer

(Floating Point Formatting, Part 2)

Russ Cox

January 10, 2026

research.swtch.com/fp-knuth

Posted on Saturday, January 10, 2026.

PDF

Introduction

Donald Knuth wrote his 1989 paper “A Simple Program Whose Proof Isn’t”<br>as part of a tribute to Edsger Dijkstra on the occasion of Dijkstra’s 60th birthday.<br>Today’s post is a reply to Knuth’s paper on the occasion of Knuth’s 88th birthday.

In his paper, Knuth posed the problem<br>of converting 16-bit fixed-point binary fractions to decimal fractions,<br>aiming for the shortest decimal that converts back to the original 16-bit binary fraction.<br>Knuth gives a program named P2 that leaves digits in the array d and a digit count in k:

P2:

j := 0; s := 10 * n + 5; t := 10;

repeat if t > 65536 then s := s + 32768 − (t div 2);

j := j + 1; d[j] = s div 65536;

s := 10 * (s mod 65536); t := 10 * t;

until s ≤ t;

k := j.

Knuth’s goal was to prove P2 correct without exhaustive testing,<br>and he did, but he didn’t consider the proof ‘simple’.<br>(Since there are only a small finite number of inputs,<br>Knuth notes that this problem is a counterexample to Djikstra’s remark that<br>“testing can reveal the presence of errors but not their absence.”<br>Exhaustive testing would technically prove the program correct,<br>but Knuth wants a proof that reveals why it works.)

At the end of the paper, Knuth wrote, “So. Is there a better program, or a better proof,<br>or a better way to solve the problem?”<br>This post presents what is, in my opinion, a better proof of the correctness of P2.<br>It starts with a simpler program with a trivial direct proof of correctness.<br>Then it transforms that simpler program into P2, step by step,<br>proving the correctness of each transformation.<br>The post then considers a few other ways to solve the problem,<br>including one from a textbook that Knuth probably had within easy reach.<br>Finally, it concludes with<br>some reflections on the role of language in shaping our programs and proofs.<br>Problem Statement

Let’s start with a precise definition of the problem.<br>The input is a fraction f of the form n/216 for some integer n∈[0,216).<br>We want to convert f to the shortest accurate correctly rounded decimal form.

By ‘correctly rounded’ we mean that the decimal is d=⌊f·10p+½⌋/10p—that is, d is f rounded to p digits—for some p.

By ‘accurate’ we mean that the decimal rounds back exactly:<br>⌊d·216+½⌋/216=f.

By ‘shortest’ we mean that any shorter correctly rounded decimal ⌊f·10q+½⌋/10q for qp is not accurate.

(For this problem, Knuth assumes “round half up” behavior,<br>as opposed to IEEE 754 “round half to even”,<br>and the rounding equations reflect this.<br>The answer does not change significantly if we use IEEE rounding instead.)<br>Notation

Next, let’s define some convenient notation.<br>As usual we will write the fractional part of x<br>as {x}<br>and rounding as [x]=⌊x+½⌋.<br>We will also define {x}p, ⌊x⌋p, ⌈x⌉p, and [x]p<br>to be the fractional part, floor, ceiling, and rounding<br>of x relative to decimal fractions with p digits:{x}p={x·10p}/10p⌊x⌋p=⌊x·10p⌋/10p⌈x⌉p=⌈x·10p⌉/10p[x]p=[x·10p]/10p

Using the new notation, the correctly rounded p-digit decimal for f is [f]p.

Following Knuth’s paper, this post also uses the notation<br>[x..y] for the interval from x to y, including x and y;<br>[x..y) is the half-open interval, which excludes y.<br>Initial Solution

The definitions of ‘accurate’ and ‘correctly rounded’ imply two simple observations,<br>which we will prove as lemmas.<br>(In my attempt to avoid accusations of imprecision,<br>I may well be too pedantic.<br>Skip the proof of any lemma you think is obviously true.)

Accuracy Lemma . The accurate decimals are those in the accuracy interval [f−2−17..f+2−17).

Proof. This follows immediately from the definition of accurate.⌊d·216+½⌋/216=f[definitionofaccurate]⌊d·216+½⌋=f·216[multiplyby216]d·216+½∈f·216+[0..1)[domainoffloor;f·216isaninteger]d·216∈f·216+[−½..½)[subtract½]d∈f+[−2−17..2−17)[divideby216]

We have shown that d being accurate is equivalent to d∈f+[−2−17..2−17)=[f−2−17..f+2−17).

Five-Digit Lemma . The correctly rounded 5-digit decimal d=[f]5<br>sits inside the accuracy interval.

Proof.<br>Intuitively, the accuracy interval has width 2−16 while 5-digit decimals occur at<br>the narrower spacing 10−5, so at least one such decimal appears inside each accuracy interval.

More precisely,d=⌊f·105+½⌋/105[definitionofd]∈(f·105+½−[0..1))/105[rangeoffloor]=(f−½·10−5..f+½·10−5][simplifying]⊂[f−2−17..f+2−17][½·10−52−17]

We have shown that the 5-digit correctly-rounded decimal for f is in the accuracy interval.

The problem statement and these two lemmas<br>lead to a trivial direct solution:<br>compute correctly rounded p-digit decimals<br>for increasing p and return the first accurate one.

We will implement that solution in<br>Ivy, an APL-like calculator language.<br>Ivy has...