Differences
This shows you the differences between two versions of the page.
sav08:proof_of_first_lecture01_example [2008/02/20 14:53] vkuncak |
sav08:proof_of_first_lecture01_example [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Proving Correctness of Recursive Multiplication ====== | ||
- | |||
- | We prove that this function computes x*y: | ||
- | |||
- | <code> | ||
- | private static int f(int x, int y) | ||
- | { | ||
- | if (y == 0) { | ||
- | return 0; | ||
- | } else { | ||
- | if (y % 2 == 0) { | ||
- | int z = f(x, y / 2); | ||
- | return (2 * z); | ||
- | } else { | ||
- | return (x + f(x, y - 1)); | ||
- | } | ||
- | } | ||
- | } | ||
- | </code> | ||
- | |||
- | By translating Java code into math, we obtain the following mathematical definition of $f$: | ||
- | |||
- | \[ | ||
- | f(x,y) = \left\{\begin{array}{rl} | ||
- | 0, & \mbox{ if } y = 0 \\ | ||
- | 2 f(x,\lfloor\frac{y}{2}\rfloor), & \mbox{ if } y > 0, \mbox{ and } y=2k \mbox{ for some } k \\ | ||
- | x + f(x,y-1), & \mbox{ if } y > 0, \mbox{ and } y=2k+1 \mbox{ for some } k \\ | ||
- | \end{array}\right. | ||
- | \] | ||
- | |||
- | By induction on $y$ we then prove $f(x,y) = x \cdot y$. | ||
- | * **Base case.** Let $y=0$. Then $f(x,y) = 0 = x \cdot 0$ | ||
- | * **Inductive hypothesis.** Assume that the claim holds for all values less than $y$. | ||
- | * Goal: show that it holds for $y$ where $y > 0$. | ||
- | * **Case 1**: $y = 2k$. Note $k < y$. By definition and I.H. | ||
- | \[ | ||
- | f(x,y) = f(x,2k) = 2 f(x,k) = 2 (x k) = x (2 k) = x y | ||
- | \] | ||
- | * | ||
- | * **Case 2**: $y = 2k+1$. Note $y-1 < y$. By definition and I.H. | ||
- | \[ | ||
- | f(x,y) = f(x,2k+1) = x + f(x,2k) = x + x \cdot (2k) = x (2 k + 1) = x y | ||
- | \] | ||
- | This completes the proof. | ||