256 (machine squaring) Given a natural number, write a program to find its square using only addition, subtraction, doubling, halving, test for even, and test for zero, but not multiplication or division.
§ The question says we can double, but not multiply, so I’ll take that to mean that we can multiply by 2 but not by anything else. The question says we can halve, but not divide, so I’ll take that to mean that we can divide by 2 but not by anything else.
For a solution with linear time we could use a2 = (a–1)2 + 2×a – 1
For a solution with logarithmic time, use
if even a then a2 = 4×(a/2)2 else a2 = 4×((a–1)/2)2 + 2×a – 1 fi
Let all variables be natural.
x:= a2 ⇐ if a=0 then x:= 0
else if even a then a:= a/2. x:= a2. a:= a×2. x:= x×2×2
else a:= (a–1)/2. x:= a2. a:= a×2 + 1. x:= x×2×2 + a×2 – 1 fi fi
Note that in the solution, the occurrences of x:= a2 are recursive calls. Note also that in the usual binary representation of natural numbers, a×2 is just shift left, and both a/2 (for even a ) and (a–1)/2 (for odd a ) are just shift right. The refinement can be proven in 3 cases. First case:
a=0 ∧ (x:= 0)
= a=0 ∧ aʹ=a ∧ xʹ=0
= a=0 ∧ aʹ=a ∧ xʹ=a2
⇒ x:=a2 Middle case:
expand assignment context specialization
expand final assignment substitution law substitution law substitution law arithmetic specialization
arithmetic substitution law substitution law specialization
even a ∧ (a:= a/2. x:= a2. a:= a×2. x:=x×2×2)
even a ∧ (a:= a/2. x:= a2. a:= a×2. aʹ=a ∧ xʹ=x×2×2) even a ∧ (a:= a/2. x:= a2. aʹ=a×2 ∧ xʹ=x×2×2)
even a ∧ (a:= a/2. aʹ=a×2 ∧ xʹ=a2×2×2)
even a ∧ aʹ=a/2×2 ∧ xʹ=(a/2)2×2×2
even a ∧ aʹ=a ∧ xʹ=a2
a>0 ∧
= a>0 ∧
= a>0 ∧
= a>0 ∧
= a>0 ∧
= a>0 ∧
⇒ x:=a2
Last case:
odd a ∧ (a:= (a–1)/2.
= odd a ∧ (a:= (a–1)/2.
= odd a ∧ (a:= (a–1)/2.
= odd a ∧ (a:= (a–1)/2.
= odd a ∧ (a:= (a–1)/2.
= odd a ∧ aʹ=a ∧ xʹ=a2
⇒ x:=a2
x:= a2.
x:= a2.
x:= a2.
x:= x×2×2 + a×2 – 1)
expand final assignment
aʹ=a ∧ xʹ = x×4 + a×2 – 1)
substitution law
a:= a×2 + 1.
a:= a×2 + 1.
aʹ = a×2 + 1 ∧ xʹ = x×4 + (a×2 + 1)×2 – 1)
x:= a2.
aʹ = a×2 + 1 ∧ xʹ = (a2)×4 + a×4 + 1)
aʹ = a×2 + 1 ∧ xʹ = x×4 + a×4 + 1)
For the timing, replace x:= a2 by if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi , and put t:= t+1 in front of the recursive calls. The proof is by cases. First,
if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi ⇐ a=0 ∧ xʹ=x ∧ tʹ=t =⊤
The second case, right side, is
a⧧0 ∧ even a ∧ ( a:= a/2. t:= t+1.
if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi. a:= a×2. x:= x×2×2)
= a⧧0 ∧ even a ∧ if a/2=0 then tʹ=t+1 else tʹ ≤ t + 2 + log (a/2) fi
= a⧧0 ∧ even a ∧ tʹ ≤ t + 2 + log (a/2)
= a⧧0 ∧ even a ∧ tʹ ≤ t + 1 + log a
⇒ if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi
which is the left side. The third case, right side, is a⧧0 ∧ odd a ∧ ( a:= (a–1)/2. t:= t+1.
if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi.
a:= a×2 + 1. x:= x×2×2 + a×2 – 1)
= a⧧0 ∧ odd a ∧ if (a–1)/2=0 then tʹ=t+1 else tʹ ≤ t + 2 + log ((a–1)/2) fi
= a⧧0 ∧ odd a ∧ if a=1 then tʹ=t+1 else tʹ ≤ t + 1 + log (a–1) fi
⇒ if a=0 then tʹ=t else tʹ ≤ t + 1 + log a fi which is the left side.
Here’s the best solution. Define
P = yʹ = y + x×n ∧ if x=0 then tʹ=t else tʹ ≤ t + log x fi
Then the program is
yʹ=x2 ∧ if x=0 then tʹ=t else tʹ ≤ t + log x fi ⇐ y:= 0. n:= x. P P ⇐ if even x then even x ⇒ P else odd x ⇒ P fi
even x ⇒ P ⇐
odd x ⇒ P ⇐
even x ∧ x>0 ⇒ P ⇐ n:= 2×n. x:= x/2. t:= t+1. x>0 ⇒ P
x>0 ⇒ P ⇐ if even x then even x ∧ x>0 ⇒ P else odd x ⇒ P fi
if x=0 then ok else even x ∧ x>0 ⇒ P fi y:= y+n. x:= x–1. even x ⇒ P