172 (combinations) Write a program to find the number of ways to partition a+b things into a things in the left part and b things in the right part. Include recursive time.
§ The number of ways to partition a+b things into a things and b things is (a+b)! / (a!×b!) where ! is the factorial function. First without time.
x:= (a+b)! / (a!×b!) ⇐
if a=0 then x:= 1
else a:= a–1. x:= (a+b)! / (a!×b!). a:= a+1. x:= x×(a+b)/a fi
The assignment x:= (a+b)! / (a! b!) means xʹ = (a+b)! / (a! b!)) ∧ aʹ=a ∧ bʹ=b . On the right side it is a recursive call. Stating it as an assignment makes the proof easy: just
use the substitution law and simplify. The proof is by cases. First case:
a=0 ∧ (x:= 1) ⇒ (x:= (a+b)! / (a!×b!)) definition of assignment
= a=0 ∧ xʹ=1 ∧ aʹ=a ∧ bʹ=b ⇒ xʹ = (a+b)! / (a! b!)) ∧ aʹ=a ∧ bʹ=b =⊤
Second case, starting with the right side:
use 0!=1
a⧧0 ∧ (a:= a–1. x:= (a+b)! / (a!×b!). a:= a+1. x:= x×(a+b)/a)
= a⧧0 ∧ (a:= a–1. x:= (a+b)! / (a!×b!). a:= a+1. xʹ=x×(a+b)/a ∧ aʹ=a ∧ bʹ=b)
= a⧧0 ∧ xʹ = (a–1+b)!/((a–1)!×b!)×(a+b)/a ∧ aʹ=a ∧ bʹ=b
= a⧧0 ∧ xʹ = (a+b)! / (a!×b!) ∧ aʹ=a ∧ bʹ=b
⇒ x:= (a+b)! / (a!×b!) Now the time.
assignment
substitution law 3 times simplify specialization
tʹ = t+a ⇐ if a=0 then x:= 1
else a:= a–1. t:= t+1. tʹ = t+a. a:= a+1. x:= x×(a+b)/a fi
Proof by cases. First case: a=0 ∧ (x:= 1) ⇒ tʹ = t+a
= a=0∧xʹ=1 ∧ aʹ=a ∧ bʹ=b ∧ tʹ=t ⇒ tʹ=t+a =⊤
Second case, starting with the right side:
definition of assignment
a⧧0 ∧ (a:= a–1. t:= t+1. tʹ = t+a. a:= a+1. x:= x×(a+b)/a)
= a⧧0 ∧ (a:= a–1. t:= t+1. tʹ = t+a. a:= a+1. xʹ=x×(a+b)/a ∧ aʹ=a ∧ bʹ=b ∧ tʹ=t)
= a⧧0 ∧ (tʹ = t+a. xʹ=x×(a+1+b)/(a+1) ∧ aʹ=a+1 ∧ bʹ=b ∧ tʹ=t)
= a⧧0 ∧ (∃xʹʹ, aʹʹ, bʹʹ, tʹʹ· tʹʹ=t+a ∧ xʹ=xʹʹ×(aʹʹ+1+bʹʹ)/(aʹʹ+1)
dependent comp
one point 4 times specialization
= a⧧0 ∧ tʹ = t+a ⇒ tʹ=t+a
∧ aʹ=aʹʹ+1 ∧ bʹ=bʹʹ ∧ tʹ=tʹʹ)
When refining x:= (a+b)! / (a!×b!) , there was no time variable.
variable, we cannot write this as an assignment, because that would mean tʹ=t . We can put the result and the timing together as
xʹ = (a+b)! / (a! b!)) ∧ aʹ=a ∧ bʹ=b ∧ tʹ=t+a or as
x:= (a+b)! / (a!×b!). t:= t+a
Here is a solution that is symmetric in a and b . x:= (a+b)! / (a!×b!) ⇐
if a=0 ∨ b=0 then x:= 1
else a:= a–1. b:= b–1. x:= (a+b)! / (a!×b!).
a:= a+1. b:= b+1. x:= x/a/b×(a+b–1)×(a+b) fi And its execution time is smaller: min a b .
assignment substitution law 3 times
Adding the time
Here is a solution with the same execution time and its recursion does not require a stack.
xʹ = (a+b)! / (a!×b!) ∧ tʹ = t + min a b ⇐ x:= 1. xʹ = x × (a+b)! / (a!×b!) ∧ tʹ =
t + min a b xʹ = x × (a+b)! / (a!×b!) ∧ tʹ = t + min a b ⇐
if a=0 ∨ b=0 then ok
else x:= x/a/b×(a+b–1)×(a+b). a:= a–1. b:= b–1. t:= t+1.
xʹ = x × (a+b)! / (a!×b!) ∧ tʹ = t + min a b fi
Now, here is a for-loop solution. Define Ik = x = (a+k)! / (a!×k!)
Then
xʹ = (a+b)! / (a!×b!) ⇐ x:= 1. I0⇒Iʹb I0⇒Iʹb ⇐ for k:= 0;..b do Ik⇒Iʹ(k+1) od Ik⇒Iʹ(k+1) ⇐ x:= x×(a+k+1)/(k+1)
with timing tʹ = t+b .
Finally, here are two functional solutions. Define f = 〈a, b: nat → (a+b)! / (a!×b!)〉
Then
f a b = if a=0 then 1 else f (a–1) b × (a+b) with execution time a . For execution time min a b
/ a fi
f a b = if a=0 ∨ b=0 then 1 else f (a–1) (b–1) × (a+b–1) ×
(a+b) / a / b fi