General proof strategies to show correctness of recursive functions?

Question

I'm wondering if there exists any rule/scheme of proceeding with proving algorithm correctness? For example we have a function $F$ defined on the natural numbers and defined below:

function F(n,k)
begin
  if k=0 then return 1
  else if (n mod 2 = 0) and (k mod 2 = 1) then return 0
  else return F(n div 2, k div 2);
end;

where $n \ \text{div}\ 2 = \left\lfloor\frac{n}{2}\right\rfloor$

the task is to prove that $F(n,k)= \begin{cases} 1 \Leftrightarrow {n \choose k} \ \text{mod} \ 2 = 1 \ 0 \text{ otherwise } \end{cases} $

It does not look very complicated (am I wrong?), but I don't know how does this kind of proof should be structured. I would be very grateful for help.

Sergey Kalinichenko · Accepted Answer · 2012-03-03T17:30:16.173

6

Correctness of recursive algorithms is often proven by mathematical induction. This method consists of two parts: first, you establish the basis, and then you use an inductive step.

In your case, the basis is all cases when k=0, or when k is odd but n is even.

The inductive step requires proving that when f(n,k) is correct, f(2*n,2*k), f(2*n+1,2*k), f(2*n,2*k+1) and f(2*n+1,2*k+1) are all correct.

edited Mar 03 '12 at 17:30

answered Mar 02 '12 at 18:45

Sergey Kalinichenko

714,442
84
1,110
1,523

I like this one better than my answer. It would probably be good to add a proof that the 4 derived cases cover NxN, to justify the inductive conclusion. – Jean-Bernard Pellerin Mar 02 '12 at 19:00
I like this approach the most. But it is still not simple for me, how to use induction base to show these implications.. – xan Mar 03 '12 at 17:13
Is there a typo in f(2*n+1,k)? It should be f(2*n+1, 2*k) ? – xan Mar 03 '12 at 17:28
@xan Yes, absolutely! I fixed it n the answer. – Sergey Kalinichenko Mar 03 '12 at 17:31
I can't move on with this proof :( and I'm afraid I don't understand why the base in form of: {all cases when k=0, or when k is odd but n is even} is sufficient to show that when f(n,k) is correct then f(2n, 2k); f(2n+1, 2k); f(2n, 2k+1); f(2n+1,2k+1) are correct.. I'm very sorry but I lost the way. – xan Mar 03 '12 at 18:21
1

@xan The base has to be proven by itself, separately from the step. It should be reasonably easy. The four formulas of the step need to be proved separately: you need to show that `f(n,k)` being correct is *sufficient* for the `f(2*n,2*k)` to be correct; then you do the other three. – Sergey Kalinichenko Mar 03 '12 at 19:53
Why are there 4 cases to consider in the inductive step? – rasen58 Feb 27 '16 at 15:42

score 6 · Answer 2 · answered Mar 02 '12 at 18:45

Outside of proving your logic mathematically (example: inductive proof), there are some results in computing science related to this.

You can start here for an outline of the subject: Correctness
For your particular case, you'd be interested in partial correctness to show that the answer is the intended one. Then total correctness to show that the program terminates.

Hoare logic can solve your partial correctness.

As for the termination for this particular problem:

If (n%2==0 and k%1==1) or (k==0) the program terminates, otherwise it recurses to the n/2, k/2 case.
Using strong induction on k, we can show that the program always reaches one of the terminal nodes where k==0. (It may terminate earlier on the first clause but we only needed to show that it terminates at all, which this does)

So I've left the proof of partial correctness to you (because I don't know that stuff)

score 2 · Answer 3 · answered Mar 02 '12 at 18:40

Generally speaking, you would attempt a proof by induction to show correctness. This works very well when proving correctness of recursive functions, since you can prove the base case directly, and then can use the fact that the function works for "smaller" inputs in order to prove that it works for the next largest input.

In this case, I'd attempt a proof by well-founded induction. Specifically, I'd prove that

The function is correct for all inputs of the form (n, 0).
Assuming that for all inputs (n', k') such that (n', k') is lexicographically less than (n, k), the function is correct, prove that it is correct for (n, k).

The specifics of this proof would need to leverage the specifics of your function and the bahvaior of binomial coefficients, but the general template is as above.

Hope this helps!

General proof strategies to show correctness of recursive functions?

3 Answers3