237 (bit sum) Write a program to find the number of ones in the binary representation of a given natural number.
§ Let f n be the number of ones in the binary representation of natural n , defined inductively as follows.
f0 = 0
f (2×n) = f n
f (2×n + 1) = f n + 1
Here’s one solution. Let n and c be natural variables. cʹ=fn ⇐ c:= 0. cʹ=c+fn
cʹ=c+fn ⇐ if n=0 then ok
else if even n then n:= n/2. cʹ=c+fn
Proof of first refinement: c:= 0. cʹ=c+fn
else n:= (n–1)/2. c:= c+1. cʹ=c+fn fi fi
substitution law, arithmetic
= cʹ=fn
The last refinement is proven by cases. First case:
n=0 ∧ ok
= n=0 ∧ cʹ=c ∧ nʹ=n
= n=0 ∧ cʹ = c + f 0 ∧ nʹ=n
= n=0 ∧ cʹ = c + f n ∧ nʹ=n
⇒ cʹ=c+fn Middle case:
expand ok f 0 = 0 context from left conjunct to change middle conjunct specialization
n>0 ∧ even n ∧ (n:= n/2. cʹ=c+fn)
= n>0 ∧ even n ∧ cʹ=c+f(n/2)
= n>0 ∧ even n ∧ cʹ=c+fn
⇒ cʹ=c+fn Last case:
odd n ∧ (n:= (n–1)/2. c:= c+1. cʹ=c+fn)
= odd n ∧ cʹ=c+1+f((n–1)/2)
= odd n ∧ cʹ=c+fn
⇒ cʹ=c+fn
The execution time is exactly
if n=0 then 0 else floor (1 + log n) fi or, for easier proof,
(n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n) Proof of first refinement:
c:= 0. (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n)
= (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n) The last refinement is proven by cases. First case:
n=0 ∧ ok = n=0 ∧ tʹ=t
expand ok and drop useless conjuncts discharge and identity
= n=0 ∧ (n=0 ⇒ tʹ=t) ∧ ⊤
= n=0 ∧ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n)
⇒ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n) Middle case:
n>0 ∧ even n ∧ (n:= n/2. t:= t+1. (n=0 ⇒ tʹ=t) ∧
use context n=0 specialization
(n>0 ⇒ tʹ ≤ t + 1 + log n)) substitution law twice
= n>0 ∧ even n ∧ (n/2=0 ⇒ tʹ=t+1) ∧ (n/2>0 ⇒ tʹ ≤ t + 2 + log (n/2))
context n>0 means n/2=0 is ⊥ and n/2>0 is n>0
= n>0 ∧ even n ∧ ⊤ ∧ (n>0 ⇒ tʹ ≤ t + 2 + log (n/2))
substitution law property of f for even arguments specialization
substitution law twice property of f for odd arguments specialization
substitution law
context n>0 means n=0 is ⊥
= n>0 ∧ even n ∧ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 2 + log (n/2))
1 + log (n/2) = log n
= n>0 ∧ even n ∧ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n) specialization
⇒ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n) Last case:
odd n ∧ (n:= (n–1)/2. c:= c+1. t:= t+1. (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n)) substitution law 3 times
= odd n ∧ ((n–1)/2=0 ⇒ tʹ=t+1) ∧ ((n–1)/2>0 ⇒ tʹ ≤ t + 2 + log ((n–1)/2))
= odd n ∧ (n=1 ⇒ tʹ=t+1) ∧ (n>1 ⇒ tʹ ≤ t + 1 + log (n–1))
various simplifications
⇒ odd n ∧ (n≥1 ⇒ tʹ ≤ t + 1 + log (n–1))
= odd n ∧ (n=0 ⇒ tʹ=t) ∧ (n≥1 ⇒ tʹ ≤ t + 1 + log (n–1)) ⇒ (n=0 ⇒ tʹ=t) ∧ (n>0 ⇒ tʹ ≤ t + 1 + log n)
Here’s another solution. Let n be a natural variable. nʹ=fn ⇐ if n=0 then ok
else if even n then n:= n/2. nʹ=fn
else n:= (n–1)/2. nʹ=fn. n:= n+1 fi fi
use context to conjoin ⊤ specialization
with the same execution time. First, we prove the result without the execution time. There’s only one variable, n , so nʹ=fn = n:= fn . Therefore
if n=0 then ok
else if even n then n:= n/2. nʹ=fn
else n:= (n–1)/2. nʹ=fn. n:= n+1 fi fi
= if n=0 then nʹ=n
else if even n then n:= n/2. nʹ=fn
else n:= (n–1)/2. n:= fn. nʹ = n+1 fi fi
= if n=0 then nʹ=0
else if even n then nʹ = f(n/2)
context, substitution law three times
else nʹ = f(((n–1)/2)+1) fi fi
Those are the same three cases as the definition of f . (This proof is slightly unfinished. The timing should also be proven.)
combine the middle and last conjunct