Skip to main content
PRL Project

A Fast Algorithm for the Integer Square Root

by Anne Trostle and Mark Bickford      June 2014
based on an original proof by Christoph Kreitz 1

1. Introduction

For a natural number x (i.e. x ∈ {0,1,2,3,...}), the integer square root of x is defined as the natural number r such that r2 ≤ x < (r + 1)2. It is the greatest r such that r2 ≤ x, or equivalently, the least r such that (r + 1)2 > x. The following chart is a visual representation of the integer square root over a portion of the natural numbers:


graph of the integer square root

The question is, given a natural number x, how do we systematically solve for its integer square root? In other words, can we write an algorithm that finds the solution for any x? Looking at the chart, we can see that the root of x is related to the root of (x - 1): sometimes it's the same, and sometimes it's one more. So we could write a recursive algorithm based on testing the root of (x - 1):


λx.letrec sqrt(x) = if x = 0 then 0 else let r2 := sqrt (x - 1) in let r3 := r2 + 1 in if (x) < (r3 * r3) then r2 else r3 in sqrt(x)

We can code this algorithm directly as a recursive definition in Nuprl. In this way, the Nuprl proof assistant can be used as a programming language. But recursive algorithms like this one go hand-in-hand with proofs by induction. Standard natural number induction says that to prove a statement P(x) for any natural number x, it is enough to prove the base case, P(0), and to prove that P(x) can be derived from assuming P(x - 1). In Nuprl, we can actually extract recursive algorithms from proofs by induction. The algorithm shown above is the result from proving the following theorem in Nuprl using standard natural number induction on x:


Theorem 1: Specification of the Integer Square Root ∀x:ℕ. (∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))})

When we prove this theorem in Nuprl, we prove it constructively, meaning that in order to show that the integer square root exists, we have to show how to construct it. And then we can extract a program from this constructive proof, and in doing so, we have actually proven that the program is correct—we know that the result will satisfy the specification of Theorem 1. We say that the program is correct by construction.

But although the algorithm is correct, it isn't the most efficient method. In order to solve the integer square root of x this way, you must first solve the root of (x - 1). Likewise, in order to solve the root of (x - 1), you must first find the root of (x - 2). This process of stepping down by 1 continues until you reach 0. So now we ask, is there another way to prove Theorem 1 that would produce a faster algorithm?


2. Fast Induction

To find a faster algorithm, we turn to the proof method of complete induction on the natural numbers. Complete induction says that to prove a statement P(x) for any natural number x, it is enough to prove that P(x) can be derived from assuming P(y) for all y less than x. This is a stronger assumption than before. Formally, it can be stated as the following theorem, where ℕx stands for the natural numbers less than x:

Theorem 2: Complete Natural Induction ∀[P:ℕ → ℙ]. ((∀x:ℕ. ((∀y:ℕx. P[y]) ⇒ P[x])) ⇒ (∀x:ℕ. P[x]))

Notice that the standard induction principle using (x - 1) is just a specific case of complete induction, since (x - 1) < x. Also note that although the base case isn't specifically mentioned in Theorem 2, it can still be required as a separate proof step. For example, when using complete induction with (x - 1), you still must consider the case of x = 0 separately, since (x - 1) is not a natural number when x = 0.

This stronger induction principle opens the door for decrementing x in larger jumps, rather than stepping down by only 1 each time. In fact, we can prove that for any integer b greater than 1, induction with (x ÷ b) is a valid method as well. Once again, we can think of this method as a specific case of complete induction. For this principle to hold, we need (x ÷ b) < x. Thus we state that b must be greater than 1 and that the base case P(0) must be proven separately.


Theorem 3: Division Natural Induction ∀b:{b:ℤ| 1 < b}. ∀[P:ℕ → ℙ]. (P[0] ⇒ (∀x:ℕ+. (P[x ÷ b] ⇒ P[x])) ⇒ (∀x:ℕ. P[x]))

So to improve the speed of the integer square root algorithm, perhaps we could step down to 0 using integer division rather than by subtracting 1 each time. But what number should we divide by? By using the induction principle in Theorem 3, we will be able to assume that there exists a root r0 for the number (x ÷ b) and then use r0 to construct a root for x. More specifically, the induction hypothesis will be that there exists a natural number r0 such that r02 ≤ (x ÷ b) < (r0 + 1)2, and we'll need to construct a new r such that r2 ≤ x < (r + 1)2. Ignoring remainders for the moment and just using some algebra, we can see that (√b ⋅ r0) might work as a root of x. Therefore, we should try using a perfect square for b, which is intuitive since we're dealing with square roots. As we show in the next section, if we use division by 4 in the induction step, the integer square root of x will be either 2r0 or (2r0 + 1), depending on whether or not x is less than (2r0 + 1)2. After we prove this result, we will be able to extract a more efficient algorithm:


λx.letrec sqrt(x) = if x = 0 then 0 else let z := x ÷ 4 in let r2 := 2 * (sqrt z) in let r3 := r2 + 1 in if (x) < (r3 * r3) then r2 else r3 in sqrt(x)

This result can be extended to the more general problem of finding the nth integer root of a natural number for any positive integer n, i.e. finding a natural number r such that rn ≤ x < (r + 1)n. The existence of this more general root can be proved by induction using Theorem 3 with division by 2n. The following algorithm can be extracted from the proof:


λn.let b := 2^n in λx.letrec nth_root(x) = if x = 0 then 0 else let z := x ÷ b in let r2 := 2 * (nth_root z) in let r3 := r2 + 1 in if (r3^n) < (x + 1) then r3 else r2 in nth_root(x)

In the next section we show the details of proving the existence of the integer square root, using division by 4 in the induction step. For a closer look at all theorems and proofs mentioned so far, we include projections from Nuprl at the end in Section 6.


3. Proof of the Integer Square Root using Fast Induction

We start the proof by using the division induction principle from Theorem 3, choosing 4 as our divisor. The first task in this method is to prove that the theorem holds for the base case, i.e. when x = 0. It is obvious that when x is 0, the integer square root will be 0.


⊢ ∀x:ℕ. (∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))}) | BY (DivNatInduction ⌈4⌉⋅ THEN Auto) | ⊢ ∃r:{ℕ| (((r * r) ≤ 0) ∧ 0 < (r + 1) * (r + 1))} | BY (With ⌈0⌉ (D 0)⋅ THEN Auto') Instantiate the conclusion with 0

For the induction step, we will now assume that x is greater than 0 and that we know that a root r exists for (x ÷ 4). Thus the induction hypothesis is that there exists a natural number r such that r2 ≤ (x ÷ 4) < (r + 1)2. We will be using this r to construct a root for x. But in order to prove that the constructed root meets the specification of the integer square root, we will need to use some additional properties about integer division and remainders, proven separately in Nuprl:


Lemma 1: div_rem_sum ∀[a:ℤ]. ∀[n:ℤ-0]. (a = (((a ÷ n) * n) + (a rem n))) Lemma 2: rem_bounds_1 ∀[a:ℕ]. ∀[n:ℕ+]. ((0 ≤ (a rem n)) ∧ a rem n < n)

We instantiate these lemmas now, for use by Nuprl later in the proof.


1. x: ℕ+ 2. ∃r:{ℕ| (((r * r) ≤ (x ÷ 4)) ∧ x ÷ 4 < (r + 1) * (r + 1))} ⊢ ∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))} | BY (D (-1) | THEN Auto | THEN (InstLemma `div_rem_sum` [⌈x⌉;⌈4⌉]⋅ THENA Auto) | THEN (InstLemma `rem_bounds_1` [⌈x⌉;⌈4⌉]⋅ THENA Auto)) | 2. r: ℕ from the induction [3]. ((r * r) ≤ (x ÷ 4)) ∧ x ÷ 4 < (r + 1) * (r + 1) hypothesis 4. x = (((x ÷ 4) * 4) + (x rem 4)) from Lemma 1 5. (0 ≤ (x rem 4)) ∧ x rem 4 < 4 from Lemma 2 ⊢ ∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))}

Our claim is that the integer square root of x is either (2r) or (2r + 1). If x < (2r + 1)2, then the root is (2r). Otherwise, the root is (2r + 1). For each case, we'll need to prove that the constructed root satisfies the specification of the integer square root.

Case 1: x < (2r + 1)2

We claim that the root is (2r) and therefore need to prove that (2r)2 ≤ x < (2r + 1)2. Since we are assuming that x < (2r + 1)2, the right inequality is trivial. Proving the left inequality requires just a bit of algebra. Here is an informal proof sketch of why (2r)2 ≤ x:

             r2 ≤ (x ÷ 4) by the induction hypothesis
         r2 * 4 ≤ (x ÷ 4) * 4  
          (2r)2 ≤ (x ÷ 4) * 4        
          (2r)2 ≤ (x - (x rem 4)) by Lemma 1 
(x - (x rem 4)) ≤  x by Lemma 2, since 0 ≤ (x rem 4)                       
          (2r)2 ≤  x

With Lemma 1 and Lemma 2 instantiated as hypotheses, Nuprl can handle this algebra automatically without any further guidance. Here is how the proof looks in Nuprl:


1. x: ℕ+ 2. r: ℕ [3]. ((r * r) ≤ (x ÷ 4)) ∧ x ÷ 4 < (r + 1) * (r + 1) 4. x = (((x ÷ 4) * 4) + (x rem 4)) 5. (0 ≤ (x rem 4)) ∧ x rem 4 < 4 ⊢ ∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))} | BY ((Evaluate ⌈r2 = (2 * r)⌉⋅ THENA Auto) | THEN (Evaluate ⌈r3 = (r2 + 1)⌉⋅ THENA Auto) | THEN (Decide ⌈x < r3 * r3⌉⋅ THENA Auto)) | 6. r2: ℤ 7. r2 = (2 * r) 8. r3: ℤ 9. r3 = (r2 + 1) 10. x < r3 * r3 Case 1: assume x < (2r + 1)2 ⊢ ∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))} | BY (With ⌈r2⌉ (D 0)⋅ THEN Auto')⋅ Instantiate the conclusion | with r2 = (2 * r) 3. (r * r) ≤ (x ÷ 4) 4. x ÷ 4 < (r + 1) * (r + 1) 5. x = (((x ÷ 4) * 4) + (x rem 4)) 6. 0 ≤ (x rem 4) 7. x rem 4 < 4 8. r2: ℤ 9. r2 = (2 * r) 10. r3: ℤ 11. r3 = (r2 + 1) 12. x < r3 * r3 ⊢ (r2 * r2) ≤ x | Nuprl takes care of BY (ElimVar `r3' THEN ElimVar `r2' THEN Auto') the rest of the proof

Case 2: x ≥ (2r + 1)2

We claim that the root is (2r + 1) and therefore need to prove that (2r + 1)2 ≤ x < (2r + 2)2. Since we are assuming that x ≥ (2r + 1)2, the left inequality is trivial. The right inequality requires algebra and is a bit trickier than the proof from the first case. Here is an informal proof sketch of why x < (2r + 2)2:

                    (x ÷ 4) < (r + 1)2 by the induction hypothesis
                (x ÷ 4) + 1 ≤ (r + 1)2 since we are working with integers
          ((x ÷ 4) * 4) + 4 ≤ (r + 1)2 * 4 
          ((x ÷ 4) * 4) + 4 ≤ (2r + 2)2
        (x - (x rem 4)) + 4 ≤ (2r + 2)2 by Lemma 1
                          x ≤ (2r + 2)2 + (x rem 4) - 4
  (2r + 2)2 + (x rem 4) - 4 < (2r + 2)2 by Lemma 2, since (x rem 4) < 4
                          x < (2r + 2)2

As with Case 1, Nuprl can handle this algebra automatically without any further guidance. Here is how the proof looks in Nuprl:


1. x: ℕ+ 2. r: ℕ [3]. ((r * r) ≤ (x ÷ 4)) ∧ x ÷ 4 < (r + 1) * (r + 1) 4. x = (((x ÷ 4) * 4) + (x rem 4)) 5. (0 ≤ (x rem 4)) ∧ x rem 4 < 4 6. r2: ℤ 7. r2 = (2 * r) 8. r3: ℤ 9. r3 = (r2 + 1) 10. ¬x < r3 * r3 Case 2: assume x ≥ (2r + 1)2 ⊢ ∃r:{ℕ| (((r * r) ≤ x) ∧ x < (r + 1) * (r + 1))} | BY (With ⌈r3⌉ (D 0)⋅ THEN Auto')⋅ Instantiate the conclusion | with r3 = (2r + 1) 3. (r * r) ≤ (x ÷ 4) 4. x ÷ 4 < (r + 1) * (r + 1) 5. x = (((x ÷ 4) * 4) + (x rem 4)) 6. 0 ≤ (x rem 4) 7. x rem 4 < 4 8. r2: ℤ 9. r2 = (2 * r) 10. r3: ℤ 11. r3 = (r2 + 1) 12. ¬x < r3 * r3 13. (r3 * r3) ≤ x ⊢ x < (r3 + 1) * (r3 + 1) | Nuprl takes care of BY (ElimVar `r3' THEN ElimVar `r2' THEN Auto')⋅ the rest of the proof

From this proof, we can see how the induction method directly corresponds to the recursive algorithm, shown again below. The base case of the induction matches the first line of the algorithm, for when x = 0. Then for the induction step, we assume that we know the result for (x ÷ 4). This matches the recursive call to (sqrt z) in the algorithm. In the proof we then consider two cases separately by testing whether or not x is less than (2r + 1)2. This matches the inner if-then-else expression in the algorithm.


λx.letrec sqrt(x) = if x = 0 then 0 else let z := x ÷ 4 in let r2 := 2 * (sqrt z) in let r3 := r2 + 1 in if (x) < (r3 * r3) then r2 else r3 in sqrt(x)


4. Other Methods of Finding the Integer Square Root

If we were to approach any typical person on the street and ask him or her to find the integer square root of a number (and explain what we mean by the integer square root), how do we think that person would solve it?

For numbers less than 100, chances are that person would use a simple guess-and-check method to find the solution. For example, if prompted to find the root of 56, we might think to ourselves, 72 = 49 and 82 = 64, so the answer must be 7.

This guess-and-check method is an abbreviated version of a search algorithm that we could write formally. To find the root r of a number x, we could start with r = 0 and then increment r by 1 until we find that (r + 1)2 > x. Or we could write a binary search algorithm: start by testing (x ÷ 2) as a root and then only search above or below based on the result. Then continue by testing the midpoint of the search area each time. In general, search algorithms involve testing an output r as a potential solution. In contrast, all of the methods described earlier involved recursion on the input variable, x.

Now how about larger numbers, beyond what we memorize or would be willing to test? Well, we would probably just get out a calculator to find the decimal answer and then round down to the nearest integer. This idea prompted us to explore the method of using the real number, decimal square root to find the integer square root. This method would involve two main steps: (1) finding the real square root and (2) truncating the result to an integer. Supposing we find an algorithm to calculate the real square root, we might run into problems in the second step. Intuitively, 4.000000001 and 3.999999999 might be equivalent real numbers, but truncation clearly results in two different integers.

While investigating this situation, we realized that it might be more interesting to approach the connection between the integer square root and the real square root in the opposite direction. That is, instead of using the real square root to find the integer square root, we realized that the integer square root is important for calculating the real square root. This direction offers insight to a question you might be asking yourself by now, what purpose does the integer square root serve?

What we discovered is that the integer square root can be used to improve efficiency when calculating the real square root. In the next section we introduce a few concepts of the real numbers, ℝ, and discuss the real number square root.


5. The Real Square Root

To start, by real numbers we mean the continuum of decimal numbers on a number line, which includes the integers, rationals, and all possible points between such as the decimal 8.58697958483 or the irrational number √2. By rational numbers we mean fractions.

How do we represent the real numbers and analyze them constructively in mathematics? Errett Bishop and Douglas Bridges explore this topic in Chapter 2 of their book, Constructive Analysis 2. In this chapter, they define a real number as a regular sequence of rational numbers (pg 18):


Definition. A sequence (xn) of rational numbers is regular if |xm - xn| ≤ m-1 + n-1 (m,n ∈ ℤ+). A real number is a regular sequence of rational numbers. Two real numbers x ≡ (xn) and y ≡ (yn) are equal if |xn - yn| ≤ 2n-1 (n ∈ ℤ+).

To illustrate this defintion, consider the following two sequences of rational numbers:


x ≡ (4 + n-1) ≡ (5, 4 1/2, 4 1/3, 4 1/4, ... ) y ≡ (4 - n-1) ≡ (3, 3 1/2, 3 2/3, 3 3/4, ... )

Based on the definition provided by Bishop and Bridges, these sequences are considered equal in the real numbers. We can see this intuitively, since both sequences are approaching the number 4, x from above and y from below. We might say that both of these sequences are real number representations of the number 4.

Mark Bickford has been formalizing the definitions from Chapter 2, using Nuprl. In doing so he discovered some serious problems with efficiency when trying to compute with these real numbers. So now he has been developing a new way to formalize real numbers in Nuprl by focusing on the numerators in the rational sequences and representing real numbers as sequences of integers rather than rationals. This new method has provided much greater efficiency when computing with the real numbers.

Now we turn our attention back to the square root problem. Using this new method of defining real numbers, Mark has proven the existence of the real square root in Nuprl and extracted an algorithm for finding it. Furthermore, since the real numbers are represented as sequences of integers, he has found a simple and efficient algorithm which actually uses the integer square root to approximate the real square root. So here we see a direct use of the integer square root.

As a side note, we can calculate the decimal square root of a number by hand, following a manual procedure such as the one shown here. In this algorithm, the first step is actually to find the integer square root of the left-most pair of digits. So once again, we see that the integer square root can be used in solving for the real square root.


6. Projections from Nuprl


View PDFs of selected proofs


View selected proofs in the frame below





References

  1. Christoph Kreitz. Derivation of a Fast Integer Square Root Algorithm. In Information-Intensive Proof Technology Marktoberdorf NATO Summer School 2003, Appendix A, pp 45-49.

  2. Errett Bishop and Douglas Bridges. Constructive Analysis. Springer-Verlag, 1985. Chapter 2: Calculus and the Real Numbers, pp 14-66.