# 7  IEEE-Compliant Square Root

Most of the results listed in Chapters 1, 4, and 6 are propositions pertaining to real variables, which are formalized by ACL2 events in which these variables are restricted to the rational domain. Many of the lemmas of this chapter similarly apply to arbitrary real numbers, but in light of its focus, these results are formulated to correspond more closely with their formal versions. Apart from the informal discussion below, the lemmas themselves contain no references to the real numbers or the square root function.

Establishing IEEE compliance of a floating-point square root module entails proving that the final value computed for a given radicand , rounding mode , and precision satisfies

 (7.1)

We would like to formulate a proposition of rational arithmetic that is transparently equivalent to (7.1). This requirement is satisfied by the following criterion: For all positive rational numbers and ,

 (7.2)

Obviously, the monotonicity of rounding (Lemma 6.5.11) ensures that (7.1) implies (7.2). On the other hand, suppose that (7.2) holds. According to Lemma 6.5.16, either is -exact (and, in particular, rational) or for some , for all satisfying . In either case, there exist and such that and . Since ,

and hence .

We would also like to prove formally that (7.2) is satisfied by the value computed by any module of interest. For this purpose, it will be useful to have a function that computes, for given and , a rational number that satisfies

 (7.3)

We shall define a conceptually simple (albeit computationally horrendous) rational function qsqrt that serves this need. The definition is motivated by Lemma 6.5.17, which guarantees that if

 (7.4)

where , then (7.3) holds for . Of course, (7.4) will not be our formal definition of qsqrt, nor shall we prove any instance of (7.3). However, our definition will be motivated by this observation, and we shall prove the following (Lemma 7.3.5):

If , then for all positive rationals and and positive integers and ,

 and (7.5)

Thus, in order to prove that a computed value satisfies (7.2), it suffices to show that for some .

Among various other properties of qsqrt that are derived in this chapter is one that warrants some motivation. In practice, a typical implementation of a subtractive square root algorithm produces a final truncated approximation of and a remainder that provides a comparison between and . A final rounded result is derived from this approximation in accordance with a given rounding mode and precision . In order to apply (7.5), we would like to show that for some appropriate . This may be done by invoking Lemma 6.5.20 with and substituted for and , respectively. But this requires showing that and determining whether . Thus, we require a means of converting inequalities relating and to inequalities relating and . This is achieved by the following result (Lemma 7.3.6):

If and are positive rationals and is -exact, then

and

Subsections
David Russinoff 2017-08-01