Prove algorithm correctness

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.

---

I'm extremely sorry for my mistake.. I've just edited the code (first else)..

Answer 1

Hint $\ $ By Kummer, $\rm\displaystyle\:{n \choose k}\:$ is odd iff there are no carries when adding $\rm\:n\:$ and $\rm\:n-k\:$ in base $2$.

Alternatively, here's a direct parity proof, split into cases based on the values of $\rm\:n,k\ mod\ 2\!:$

$\rm\displaystyle \begin{matrix}n\equiv 0:\\ \rm k\equiv 1:\end{matrix}\ \ {n\choose k}\ =\ \frac{n}k {n-1 \choose k-1 } \equiv\: 0$

$\rm\displaystyle\begin{matrix}n\equiv 0:\\ \rm k\equiv 0:\end{matrix}\ \ {n\choose k}\equiv \frac{n(n-2)(n-4)\:\cdots\:(n-k+2)}{2\cdot 4\cdot 6\:\cdots\:k}\equiv\frac{\frac{n}{2}(\frac{n}2-1)\:\cdots(\frac{n}2-\frac{k}2+1)}{1\cdot 2\cdot 3\:\cdots\:\frac{k}2}\equiv {n/2\choose k/2}$

$\rm\displaystyle \begin{matrix}n\equiv 1:\\ \rm k\equiv 1:\end{matrix} \ \ {n\choose k}\: =\: \frac{n}k {n-1 \choose k-1 }\:\equiv\:{n-1\choose k-1}\equiv {(n-1)/2\choose (k-1)/2}\equiv{\lfloor n/2\rfloor\choose \lfloor k/2\rfloor}$

$\rm\displaystyle\begin{matrix}n\equiv 1:\\ \rm k\equiv 0:\end{matrix} \ \ {n\choose k}\ \ \:=\:\ \ {n-1 \choose k-1 }\: +\: {n-1\choose k}\equiv {(n-1)/2\choose k/2}\equiv{\lfloor n/2\rfloor\choose \lfloor k/2\rfloor}$

Answer 2

The program is incorrect as written (in that the function it calculates is not the function $F(n,k)$).

For $n=k$, $\binom{n}{k}=\binom{n}{n}=1$, so $F(n,k) = 1$. However, if you input $n=k$ both odd, then $k=0$ is false, and $(n\bmod 2 = 1)$ and $(k\bmod 2 = 1)$ are both true, so your program will return $0$ instead. It will also return $0$ incorrectly with $n$ odd and $k=1$.

---

As corrected, the program is now correct.

This can be seen by invoking the theorem of Kummer mentioned by Bill Dubuque:

Theorem. (Kummer) Let $p$ be a prime, and let $m$ and $n$ be integers, $0\leq n\leq m$. The exact power of $p$ that divides $\binom{m}{n}$ is the number of carries when adding $n$ and $m-n$ in base $p$.

Thus, $F(n,k)=1$ if and only if there are no carries, and $F(n,k)=0$ if and only if there is at least one carry, when adding $k$ and $n-k$ in base $2$.

If $k$ is odd and $n$ is even, then both $k$ and $n-k$ are odd, so you will have a carry in the units. Thus, if $n\equiv 0\pmod{2}$ and $k\equiv 1\pmod{2}$, then $F(n,k)=0$.

If $k$ and $n$ are both even, then so are $k$ and $n-k$; there will be a carry if and only if there is a carry after the left-most digit; i.e., if and only if there is a carry when adding $\frac{k}{2}$ and $\frac{n-k}{2}$ in base $2$. Thus, $$\binom{n}{k}\equiv \binom{\frac{n}{2}}{\frac{k}{2}}\text{ if }n\equiv k\equiv 0\pmod{2}.$$

Similarly, if $k$ is even and $n$ is odd, then there is no carry in the units when adding $k$ and $n-k$; so there will be a carry if and only if there is one when adding $\frac{k}{2}$ and $\frac{n-k-1}{2} = \frac{(n-1)-k}{2}$. Thus, $$\binom{n}{k}\equiv\binom{\frac{n-1}{2}}{\frac{k}{2}}\text{ if }n\equiv 1\pmod{2}\text{ and }k\equiv 0\pmod{2}.$$

Finally, if both $n$ and $k$ are odd, then you need to check if there is a carry when adding $\frac{k-1}{2}$ and $\frac{n-k}{2} = \frac{(n-1)-(k-1)}{2}$; this amounts to checking the parity of $$\binom{\frac{n-1}{2}}{\frac{k-1}{2}}.$$ This is what your program is doing, so the program returns the correct answer.

Answer 3

I posted this a few minutes ago on the duplicate that was then closed. Perhaps it is of interest.

Use a double induction. First prove that $F[0,0]$ is correct. Then, assuming $F[n,0]$ is correct, that $F[n+1,0]$ is correct. These are both trivial for the given algorithm. And finally, if $F[j,k ]$ is correct for all $[j,k]$ lexicographically less than or equal to $[n,k]$, that $F[n,k+1]$ is correct. For this you will need to take cases. But they're easy, and the call on $F[n \mbox{ div } 2, k \mbox{ div }2]$ is "automatically" correct by the induction hypothesis.

The double induction works because if $F$ fails to return the correct value, then there is some $[a,b]$ least in the lexicographic order on $\mathbb{N}\times \mathbb{N}$ for which it fails. If $b=0$, then $a>0$ and one could use the first "inductive step" to get a contradiction. If $b>0$, then one could use the second "inductive step" to get a contradiction.