article · 2008

Derivation of a Fast Integer Square Root Algorithm

Christoph Kreitz

Cited by 0Abstract and details only

Abstract

In a constructive setting, the formula ∀n ∃r r2≤n ∧ n&lt;(r+1)2 specifies an algorithm for computing the integer square root r of a natural number x. A proof for this formula implicitly contains an integer square root algorithm that mirrors the way in which the formula was proven correct. In this note we describe the formal derivation of several integer square root algorithms within the Nuprl proof development system and show how efficient algorithms can be derived using advanced induction schemes. 1 Deriving a Linear Algorithm The standard approach to proving ∀n ∃r r2≤n ∧ n&lt;(r+1)2 is induction on n, which will lead to the following two proof goals Base Case: prove ∃r r2≤0 ∧ 0&lt;(r+1)2 Induction Step: prove ∃r r2≤n+1 ∧ n+1&lt;(r+1)2 assuming ∃rn r2≤n ∧ n&lt;(rn+1)2. The base case can be solved by choosing r = 0 and using standard arithmetical reasoning to prove the resulting proof obligation 02≤0 ∧ 0&lt;(0+1)2. In the induction step, one has to analyze the root rn. If (rn+1)2≤n+1, then choosing r = rn+1

Cite this paper

APA 7

Kreitz, C. (2008). Derivation of a Fast Integer Square Root Algorithm.

MLA 9

Kreitz, Christoph. “Derivation of a Fast Integer Square Root Algorithm.” 2008.

Chicago

Kreitz, Christoph. 2008. “Derivation of a Fast Integer Square Root Algorithm.”

Harvard

Kreitz, C. (2008) ‘Derivation of a Fast Integer Square Root Algorithm’.

BibTeX

@article{kreitz2008derivation,
  title = {{Derivation of a Fast Integer Square Root Algorithm}},
  author = {Kreitz, Christoph},
  year = {2008}
}

Made from the index record. Check names, capitalisation and page numbers against the paper. Need another style? AI for Research has over 10,000.