# Prove algorithm correctness

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)..

-
Are you interested in your specific example, or in the general question in the first sentence? – Aryabhata Mar 2 '12 at 17:32
Recursive algorithms are often a candidate for induction. – Listing Mar 2 '12 at 17:42
Is the third line supposed to return $1$ instead of $0$? – Arturo Magidin Mar 2 '12 at 17:56
@Arturo There's a typo: it should say: n mod 2 = 0 – Bill Dubuque Mar 2 '12 at 17:59
@This: You'd better check your own link. The Collatz conjecture is about the $3n + 1$ function, and there's no multiplication by $3$ to be seen here. – TMM Mar 2 '12 at 19:31

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}$

-
Actually oddBinomial = (k & (n - k)) == 0, NOT (n & (n - k)) == 0 – cohadar Dec 30 '15 at 9:27

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.

-

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.

-
I like this approach the most. It seems to be nice and not difficult. I understand the whole structure of this proof but have problems with implication $F[n,k]$ correct $\rightarrow$ F[n,k+1]. How many cases there will be to consider, and how to approach them? – xan Mar 3 '12 at 21:41
Use the facts that: if $m$ is even, then $m!$ has $m/2$ even "parts", and if $m$ is odd, then $m!$ has $(m-1)/2$ even "parts". The only nontrivial case is when $n$ is even and $k+1$ is odd. In this case $F[n,k+1]] = 0$, so prove that $n$ choose $k+1$ is even by looking at the number of even "parts" of numerator and denonimator. It's not hard. – Patrick Mar 4 '12 at 15:32
done, thanks :-) – xan Mar 4 '12 at 17:23