# Choose

Posted on 2017-04-15 by nbloomf

This post is literate Haskell; you can load the source into GHCi and play along.

{-# LANGUAGE NoImplicitPrelude #-}
module Choose
( choose, _test_choose, main_choose
) where

import Testing
import Functions
import Booleans
import NaturalNumbers
import DoubleNaturalRecursion
import Plus
import LessThanOrEqualTo

Today we’ll define the binomial coefficient operator, $$\nchoose$$.

Define $$\delta : \nats \rightarrow \nats$$ by $\delta(k) = \bif{\iszero(k)}{\next(\zero)}{\zero},$ $$\psi : \nats \rightarrow \nats$$ by $\psi(m) = \next(\zero),$ and $$\chi : \nats \times \nats \times \nats$$ by $\chi(t,a,b) = \nplus(a,b).$ Now define $$\nchoose : \nats \times \nats \rightarrow \nats$$ by $\nchoose = \dnatrec(\delta)(\psi)(\chi).$

choose :: (Natural n) => n -> n -> n
choose = dnaturalRec delta (const (next zero)) chi
where
delta k = if isZero k then next zero else zero
chi _ a b = plus a b

Because $$\nchoose$$ is implemented in terms of double natural recursion, it is the unique solution to a system of equations.

$$\nchoose$$ is the unique solution $$f : \nats \times \nats \rightarrow \nats$$ to the following system of functional equations for all $$n,k \in \nats$$. $\left\{\begin{array}{l} f(\zero,k) = \bif{\iszero(k)}{\next(\zero)}{\zero} \\ f(\next(n),\zero) = \next(\zero) \\ f(\next(n),\next(k)) = \nplus(f(n,k),f(n,\next(k))). \end{array}\right.$

_test_choose_zero_nat :: (Natural n, Equal n)
=> n -> Test (n -> Bool)
_test_choose_zero_nat _ =
testName "choose(0,k) == if(isZero(k),next(zero),zero)" $\k -> if isZero k then eq (choose zero k) (next zero) else eq (choose zero k) zero _test_choose_next_zero :: (Natural n, Equal n) => n -> Test (n -> Bool) _test_choose_next_zero _ = testName "choose(next(n),0) == 1"$
\n -> eq (choose (next n) zero) (next zero)

_test_choose_next_next :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_choose_next_next _ =
testName "choose(next(n),next(k)) == plus(choose(n,next(k)),choose(n,k))" $\n k -> eq (choose (next n) (next k)) (plus (choose n (next k)) (choose n k)) We can show that $$\nchoose$$ satisfies the usual properties of binomial coefficients. First, if $$k$$ is large enough then $$\nchoose(n,k) = \zero$$. Let $$n,k \in \nats$$. If $$\nleq(\next(n),k) = \btrue$$, then $$\nchoose(n,k) = \zero$$. We proceed by induction on $$n$$. For the base case $$n = \zero$$, note that if $$\nleq(\next(n),k) = \btrue$$ then $$k \neq \zero$$. Then we have $\begin{eqnarray*} & & \nchoose(n,k) \\ & = & \nchoose(\zero,k) \\ & = & \bif{\iszero(k)}{\next(\zero)}{\zero} \\ & = & \zero \end{eqnarray*}$ as needed. For the inductive step, suppose the implication holds for some $$n$$. Suppose further that we have $$\nleq(\next(\next(n)),k) = \btrue$$. Now $k = \nplus(\next(\next(n)),u) = \next(\nplus(\next(n),u))$ for some $$u \in \nats$$. Letting $$m = \nplus(\next(n),u)$$, note that $$k = \next(m)$$ and $\begin{eqnarray*} & & \btrue \\ & = & \nleq(\next(\next(n)),k) \\ & = & \nleq(\next(\next(n)),\next(m)) \\ & \href{/posts/arithmetic-made-difficult/LessThanOrEqualTo.html#thm-leq-next-cancel} = & \nleq(\next(n),m) \end{eqnarray*}$ Using the inductive hypothesis, we have $\begin{eqnarray*} & & \nchoose(\next(\next(n)),k) \\ & = & \nchoose(\next(\next(n)),\next(m)) \\ & = & \nplus(\nchoose(\next(n),m),\nchoose(\next(n),\next(m))) \\ & = & \nplus(\zero,\zero) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \zero \end{eqnarray*}$ as claimed. _test_choose_big_k :: (Natural n, Equal n) => n -> Test (n -> n -> Bool) _test_choose_big_k _ = testName "leq(next(n),k) ==> choose(n,k) == 0"$
\n k -> if leq (next n) k
then eq (choose n k) zero
else true

The special cases:

For all $$n \in \nats$$, we have the following.

1. $$\nchoose(n,\zero) = \next(\zero)$$.
2. $$\nchoose(n,n) = \next(\zero)$$.
1. We have two possibilities for $$n$$. If $$n = \zero$$, we have $\begin{eqnarray*} & & \nchoose(n,\zero) \\ & = & \nchoose(\zero,\zero) \\ & = & \bif{\iszero(\zero)}{\next(\zero)}{\zero} \\ & = & \next(\zero) \end{eqnarray*}$ as claimed. If $$n = \next(m)$$ for some $$m$$, we have $\begin{eqnarray*} & & \nchoose(n,\zero) \\ & = & \nchoose(\next(m),\zero) \\ & = & \next(\zero) \end{eqnarray*}$ as claimed.
2. We proceed by induction on $$n$$. For the base case $$n = \zero$$, we have $\begin{eqnarray*} & & \nchoose(n,n) \\ & = & \nchoose(\zero,\zero) \\ & = & \next(\zero) \end{eqnarray*}$ as needed. For the inductive step, suppose the equality holds for some $$n \in \nats$$. Note that $$\nleq(\next(n),\next(n)) = \btrue$$. Using the inductive hypothesis, we have $\begin{eqnarray*} & & \nchoose(\next(n),\next(n)) \\ & = & \nplus(\nchoose(n,n),\nchoose(n,\next(n))) \\ & = & \nplus(\next(\zero),\zero) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \next(\zero) \end{eqnarray*}$ as needed.
_test_choose_nat_zero :: (Natural n, Equal n)
=> n -> Test (n -> Bool)
_test_choose_nat_zero _ =
testName "choose(n,zero) == 1" $\n -> eq (choose n zero) (next zero) _test_choose_equal_args :: (Natural n, Equal n) => n -> Test (n -> Bool) _test_choose_equal_args _ = testName "choose(n,n) == 1"$
\n -> eq (choose n n) (next zero)

$$\nchoose$$ is kind of symmetric:

Let $$n \in \nats$$, and suppose $$n = \nplus(k,m)$$. Then $\nchoose(n,k) = \nchoose(n,m).$

We proceed by induction on $$n$$. For the base case $$n = \zero$$, note that $$k = m = \zero$$. Then we have $$\nchoose(n,k) = \nchoose(n,m)$$ as needed. For the inductive step, suppose the equality holds for some $$n$$. Say $$\next(n) = \nplus(k,m)$$. We now consider two possibilities for $$k$$. If $$k = \zero$$, we have $$m = \next(n)$$, so that $\begin{eqnarray*} & & \nchoose(\next(n),k) \\ & = & \nchoose(\next(n),\zero) \\ & = & \next(\zero) \\ & = & \nchoose(\next(n),\next(n)) \\ & = & \nchoose(\next(n),m) \end{eqnarray*}$ as needed. Suppose then that $$k = \next(v)$$. We now consider two possibilities for $$m$$. If $$m = \zero$$, then $$\next(n) = k$$ and we have $\begin{eqnarray*} & & \nchoose(\next(n),k) \\ & = & \nchoose(\next(n),\next(n)) \\ & = & \next(\zero) \\ & = & \nchoose(\next(n),\zero) \\ & = & \nchoose(\next(n),m) \end{eqnarray*}$ as needed. Suppose then that $$m = \next(u)$$. Note that $\begin{eqnarray*} & & \next(n) \\ & = & \nplus(k,m) \\ & = & \nplus(\next(v),m) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-next} = & \next(\nplus(v,m)) \end{eqnarray*}$ so that $$n = \nplus(v,m)$$, and similarly $\begin{eqnarray*} & & \next(n) \\ & = & \nplus(k,m) \\ & = & \nplus(k,\next(u)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \next(\nplus(k,u)) \end{eqnarray*}$ so that $$n = \nplus(k,u)$$. Using the inductive hypothesis, we have $\begin{eqnarray*} & & \nchoose(\next(n),k) \\ & = & \nchoose(\next(n),\next(v)) \\ & = & \nplus(\nchoose(n,v),\nchoose(n,\next(v))) \\ & = & \nplus(\nchoose(n,m),\nchoose(n,k)) \\ & = & \nplus(\nchoose(n,\next(u)),\nchoose(n,u)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-commutative} = & \nplus(\nchoose(n,u),\nchoose(n,\next(u))) \\ & = & \nplus(\next(n),\next(u)) \\ & = & \nplus(\next(n),m) \end{eqnarray*}$ as needed.

_test_choose_plus :: (Natural n, Equal n)
=> n -> Test (n -> n -> Bool)
_test_choose_plus _ =
testName "choose(plus(a,b),a) == choose(plus(a,b),b)" \$
\a b -> eq (choose (plus a b) a) (choose (plus a b) b)

## Testing

Suite:

_test_choose ::
( TypeName n, Natural n, Equal n, Arbitrary n, Show n
) => Int -> Int -> n -> IO ()
_test_choose size cases n = do
testLabel1 "choose" n

let args = testArgs size cases

runTest args (_test_choose_zero_nat n)
runTest args (_test_choose_next_zero n)
runTest args (_test_choose_next_next n)
runTest args (_test_choose_big_k n)
runTest args (_test_choose_nat_zero n)
runTest args (_test_choose_equal_args n)
runTest args (_test_choose_plus n)

Main:

main_choose :: IO ()
main_choose = do
_test_choose 10 50 (zero :: Unary)