Recursion and Induction: Reasoning AboutRecursive ProgramsGreg PlaxtonTheory in Programming Practice, Spring 2005Department of Computer ScienceUniversity of Texas at AustinProving Properties of power2• Recall the recursive program power2 presented last timepower2 0 = 1power2 (n+1) = 2 * (power2 n)• Claim: For all nonnegative integers n, the value of the power2 functionapplied to n is 2n• While this claim may seem relatively obvious, how can we formallyprove it?Theory in Programming Practice, Plaxton, Spring 2005Proving Properties of count• Recall the recursive program count we presented last timecount 0 = 0count n| even n = count (n ‘div‘ 2)| odd n = count (n ‘div‘ 2) + 1• For any nonnegative integer n, let C(n) denote the value returned bythe count function applied to argument n• Claim 1: For all nonnegative integers n, C(n) equals the number of 1sin the binary representation of nTheory in Programming Practice, Plaxton, Spring 2005Proving Properties of count• Claim 2: For all nonnegative integers m and n,C(m + n) ≤ C(m) + C(n)• Hint: Use induction over pairs (m, n) (ordered lexicographically, say),and consider cases depending on the parity of m and nTheory in Programming Practice, Plaxton, Spring 2005Proving Properties of fib• Recall the recursive program we presented last time for computing theFibonacci numbersfib 0 = 0fib 1 = 1fib (n + 2) = (fib n) + (fib (n+1))• For any nonnegative integer n, let F (n) denote the value returned bythe fib function applied to argument n• Claim: For all integers m and n such that m > 0 and n ≥ 0F (m + n) = F (m − 1) · F (n) + F (m) · F (n + 1)– Hint: Fix m arbitrarily and use induction on n aloneTheory in Programming Practice, Plaxton, Spring 2005Proving Properties of fib and gcd• Recall Euclid’s gcd algorithmgcd m n| m == n = m| m > n = gcd (m - n) n| n > m = gcd m (n - m)• For any nonnegative integers m and n, let g(m, n) denote the valuereturned by the gcd function applied to arguments m and n• Claim: For all positive integers ng(F (n), F (n + 1)) = 1Theory in Programming Practice, Plaxton, Spring
View Full Document
Unlocking...