How to prove correctness of recursive programs?

Question

We consider the Russian farmer multiplication for calculating a product x · k with x ∈ R and k ∈ N.

def prod(x,k):
    if k == 0:
        return 0
    elif k % 2 == 0: # k is straight and greater than 0
         return prod(2*x, k//2) # k//2 corresponds to the integer division
    else: # k is odd
        return prod(2*x, k//2) + x

Here it is used that a doubling of x (or a half of k) with binary representation is relatively simple: a bit shift is sufficient. Now we want to convince ourselves of the correctness of the method.

a) Calculate prod(17,7) with the above algorithm. Specify the recursive calls.

b) Show with full induction to k: For all k ∈ N and all x ∈ R the call prod(x,k) returns the return value x · k

please help solve this, i don't know where to even start.

Answer 1

As an example, I'll show how to prove a different recursive program correct. I leave it to you to apply this technique to your exact problem. I'll write in Python, which hopefully everyone speaks.

---

def fact(n):

if n == 0: return 1

else: return n * fact(n-1)

We can prove that fact(n) evaluates to $n!$ by induction on $n$ as follows:

Base case:

If n = 0, then fact(n) = 1 = $0!$

Inductive case:

We now assume that fact(k) evaluates to $k!$ for every k less than or equal to some n, and show that fact(n+1) also evaluates to $(n+1)!$. If this method of proof is unfamiliar, I recommend googling "strong induction proof", there are lots of helpful guides around! It is a very important proof technique to be familiar with.

That said, we now see fact(n+1) = n * fact(n), by definition. But by assumption, fact(n) = $n!$. So fact (n+1) = (n+1) * fact(n) = (n+1) * $n!$ = $(n+1)!$

This completes the proof.

---

In general, you want to leverage the fact that you KNOW (by induction) that your recursive calls do the correct thing. Then you want to show that no matter what branch of the if statement you enter, your code correctly uses the recursive call to get the new result.

Good luck! Comment here if you're still confused, and I'll clarify what I can.

---

I hope this helps ^_^

Answer 2

Apply strong induction over k. Suppose prod(x, k) == x*k holds for all k < k'. We prove it will hold for k = k' in 3 cases:

Suppose k' = 0.

By definition, prod(x, 0) = 0 = x*0, so it holds for k = k' when k' = 0.

Suppose k' = 2*j > 0 is even and greater than 0.

By definition, prod(x, k') = prod(x*2, j). Since k = j < k', we know that prod(x*2, j) = (x*2)*j. Can you see how this equals x*k'?

Suppose k' = 2*j+1 is odd.

By definition, prod(x, k') = prod(x*2, j) + x. Since k = j < k', we know that prod(x*2, j) = (x*2)*j. Can you see how this equals x*k'?

Every k' falls into one of the above 3 cases, and thus it holds for all k' by induction.