Computer Arithmetic and Formal Proofs

The coverage of this book is much broader than its title or subtitle (“Verifying Floating-point Algorithms with the Coq System”) suggest. About half of the book deals with the Coq system (a proof assistant) and the other half deals with the types of errors that can occur in floating-point calculations and how algorithms can be improved to avoid or reduce these. There are many examples. It is a very specialized book, but easy to follow, and would interest researchers in numerical analysis as well as in computer arithmetic.

The book is based on the free program Coq (French for “rooster”), which is described as a proof assistant, and on an addendum package for Coq called Flocq that formalizes floating point operations. Once a proof is in electronic form, Coq can verify its correctness. Coq is generally not able to devise entire proofs by itself, but it works interactively with the human to overcome gaps in proofs. Coq knows a large number of standard proof methods, but is generally not able to decide for itself which ones to use. The human studies each difficulty in the partial proof, thinks of a way it can probably be overcome, and tells Coq to apply a method or gives Coq additional information inferred from the problem. Thus the human provides the ingenuity and intuition and Coq provides the heavy lifting, as well as mechanically verifying the proof once it’s done. Because Coq is doing the systematic work, the human side of the proof process tends to have a very ad hoc flavor, with each proof looking very different from the others. Most of the methods are based in interval arithmetic.

Prior to 1985 the work in the present book probably would have been impossible, because floating point operations were different on each computer and each designer was vague about how accurate they were. In 1985 the IEEE 754 floating-point arithmetic standard was introduced, and today nearly all computers follow this standard. Among its innovations were a standard format for floating point numbers, and a requirement that all calculations be performed as if to infinite precision and then rounded to fit the number format; the rounding operations were also specified. Therefore any two machines that followed the IEEE 754 standard would (in theory) always produce exactly the same results. Much of the work in Flocq is in formalizing in Coq’s language the floating-point formats and the cases of underflow and overflow, and this is done at several levels of detail.

Another common source of numerical error is optimizing compilers that may rearrange the order of operations to make the program run faster. Operationally this is good, but numerically it can change the result. The book contains a chapter on compiler problems, including a discussion of CompCert, a verified C compiler.

Here’s a simple example of an unexpected source of error, from p. 166. If we are asked to find the area \(A\) of a triangle with sides \(a\), \(b\), \(c\), the obvious approach for humans and for computers is Heron’s formula \(A = \sqrt{s(s-a)(s-b)(s-c)}\) where \(s = (a + b + c)/2\) is called the semiperimeter. This usually works well. In 1986 William Kahan studied this more carefully and found the computer calculation can fail for “needle-like triangles”: those with two very long sides of almost the same length and one very short side. The problem is that because of round-off error the semiperimeter calculation may round off and loose accuracy, and in some cases the calculated semiperimeter is less than the longest side, leading us to calculate the area as the square root of a negative number. Kahan devised a new formula that is mathematically equivalent (but not numerically equivalent) to Heron’s formula. The book uses a combination of hand and computer proofs to prove this formula. This is in two parts: one to show that the square root will never fail, and one to show that the relative error from the calculation is small.

An interesting example of the limitations of the methods is on p. 134, using the auxiliary tool Gappa, that specializes in proving numerical properties such as inequalities. We are given a point \((x,y)\) in the plane lying in or on the triangle with vertices \((0,1)\), \((1,0)\), and \((0,-1)\). Prove that \((x,y)\) is on or inside the unit circle. Geometrically this is obvious, because the three vertices are on the unit circle. We describe the triangle to Gappa in terms of a system of linear inequalities. Gappa is able to prove \(x^2 + y^2 \le 1.1\), and in fact can prove \(x^2 + y^2 \le 1 + \epsilon\) for any given fixed \(\epsilon > 0\), but it can’t by itself conclude \(x^2 + y^2 \le 1\). One way to help Gappa is to provide the additional observation (essentially a change of variables) that \(x^2 + y^2 = \frac{1}{2}((x+y)^2 + (x-y)^2)\). The problem statement already includes inequalities for \(x+y\) and \(x-y\) (both are less than or equal 1 in absolute value), so with this additional observation Gappa is able to finish the proof.

The production quality is good. The authors are French, but the book is written in flawless and idiomatic English. I spotted a couple of typos: on p. 32 Zult should be Zmult (it’s correct in the index), and on p. 17 there’s a reference to a non-existent reference COQ 86. The index is weak. For example, none of the terms Kahan, Heron, or needle-like triangle are in the index.

Allen Stenger is a math hobbyist and retired software developer. He is an editor of the Missouri Journal of Mathematical Sciences. His personal web page is allenstenger.com. His mathematical interests are number theory and classical analysis.