Choose

Posted on 2017-04-15 by nbloomf

Tags: arithmetic-made-difficult, literate-haskell

\(\newcommand{\hyp}[2]{\stackrel{\tiny\text{hyp}}{#2}}\) \(\newcommand{\let}[2]{\stackrel{\tiny\text{let}}{#2}}\) \(\newcommand{\a}{a}\) \(\newcommand{\b}{b}\) \(\newcommand{\c}{c}\) \(\newcommand{\p}{p}\) \(\newcommand{\q}{q}\) \(\newcommand{\r}{r}\) \(\newcommand{\s}{s}\) \(\newcommand{\x}{x}\) \(\newcommand{\y}{y}\) \(\newcommand{\z}{z}\) \(\newcommand{\bool}{\mathbb{B}}\) \(\newcommand{\btrue}{\mathsf{true}}\) \(\newcommand{\bfalse}{\mathsf{false}}\) \(\newcommand{\bnot}{\mathsf{not}}\) \(\newcommand{\band}{\mathbin{\mathsf{and}}}\) \(\newcommand{\bor}{\mathbin{\mathsf{or}}}\) \(\newcommand{\bimpl}{\mathbin{\mathsf{impl}}}\) \(\newcommand{\beq}{\mathsf{eq}}\) \(\newcommand{\bif}[3]{\mathsf{if}\left(#1,#2,#3\right)}\) \(\newcommand{\id}{\mathsf{id}}\) \(\newcommand{\compose}{\mathsf{compose}}\) \(\newcommand{\const}{\mathsf{const}}\) \(\newcommand{\apply}{\mathsf{apply}}\) \(\newcommand{\flip}{\mathsf{flip}}\) \(\newcommand{\flipB}{\mathsf{flip2}}\) \(\newcommand{\flipC}{\mathsf{flip3}}\) \(\newcommand{\flipD}{\mathsf{flip4}}\) \(\newcommand{\flipE}{\mathsf{flip5}}\) \(\newcommand{\clone}{\mathsf{clone}}\) \(\newcommand{\cloneC}{\mathsf{clone3}}\) \(\newcommand{\composeAonB}{\mathsf{compose1on2}}\) \(\newcommand{\composeAonC}{\mathsf{compose1on3}}\) \(\newcommand{\composeAonD}{\mathsf{compose1on4}}\) \(\newcommand{\composeBonA}{\mathsf{compose2on1}}\) \(\newcommand{\composeBonB}{\mathsf{compose2on2}}\) \(\newcommand{\composeConA}{\mathsf{compose3on1}}\) \(\newcommand{\ptrue}{\mathsf{ptrue}}\) \(\newcommand{\pfalse}{\mathsf{pfalse}}\) \(\newcommand{\pnot}{\mathsf{pnot}}\) \(\newcommand{\pand}{\mathbin{\mathsf{pand}}}\) \(\newcommand{\por}{\mathbin{\mathsf{por}}}\) \(\newcommand{\pimpl}{\mathbin{\mathsf{pimpl}}}\) \(\newcommand{\fst}{\mathsf{first}}\) \(\newcommand{\snd}{\mathsf{second}}\) \(\newcommand{\dup}{\mathsf{dup}}\) \(\newcommand{\tup}{\mathsf{tup}}\) \(\newcommand{\tSwap}{\mathsf{swap}_{\times}}\) \(\newcommand{\tPair}{\mathsf{pair}_{\times}}\) \(\newcommand{\tAssocL}{\mathsf{assocL}_{\times}}\) \(\newcommand{\tAssocR}{\mathsf{assocR}_{\times}}\) \(\newcommand{\tupL}{\mathsf{tupL}}\) \(\newcommand{\tupR}{\mathsf{tupR}}\) \(\newcommand{\uncurry}{\mathsf{uncurry}}\) \(\newcommand{\curry}{\mathsf{curry}}\) \(\newcommand{\lft}{\mathsf{left}}\) \(\newcommand{\rgt}{\mathsf{right}}\) \(\newcommand{\either}{\mathsf{either}}\) \(\newcommand{\uSwap}{\mathsf{swap}_{+}}\) \(\newcommand{\uPair}{\mathsf{pair}_{+}}\) \(\newcommand{\uAssocL}{\mathsf{assocL}_{+}}\) \(\newcommand{\uAssocR}{\mathsf{assocR}_{+}}\) \(\newcommand{\isLft}{\mathsf{isLeft}}\) \(\newcommand{\isRgt}{\mathsf{isRight}}\) \(\newcommand{\nats}{\mathbb{N}}\) \(\newcommand{\zero}{\mathsf{0}}\) \(\newcommand{\next}{\mathsf{next}}\) \(\newcommand{\unnext}{\mathsf{unnext}}\) \(\newcommand{\iszero}{\mathsf{isZero}}\) \(\newcommand{\prev}{\mathsf{prev}}\) \(\newcommand{\natrec}{\mathsf{natrec}}\) \(\newcommand{\simprec}{\mathsf{simprec}}\) \(\newcommand{\bailrec}{\mathsf{bailrec}}\) \(\newcommand{\mutrec}{\mathsf{mutrec}}\) \(\newcommand{\dnatrec}{\mathsf{dnatrec}}\) \(\newcommand{\normrec}{\mathsf{normrec}}\) \(\newcommand{\findsmallest}{\mathsf{findsmallest}}\) \(\newcommand{\mnormrec}{\mathsf{mnormrec}}\) \(\newcommand{\nequal}{\mathsf{eq}}\) \(\newcommand{\nplus}{\mathsf{plus}}\) \(\newcommand{\ntimes}{\mathsf{times}}\) \(\newcommand{\nleq}{\mathsf{leq}}\) \(\newcommand{\ngeq}{\mathsf{geq}}\) \(\newcommand{\nminus}{\mathsf{minus}}\) \(\newcommand{\nmax}{\mathsf{max}}\) \(\newcommand{\nmin}{\mathsf{min}}\) \(\newcommand{\ndivalg}{\mathsf{divalg}}\) \(\newcommand{\nquo}{\mathsf{quo}}\) \(\newcommand{\nrem}{\mathsf{rem}}\) \(\newcommand{\ndiv}{\mathsf{div}}\) \(\newcommand{\ngcd}{\mathsf{gcd}}\) \(\newcommand{\ncoprime}{\mathsf{coprime}}\) \(\newcommand{\nlcm}{\mathsf{lcm}}\) \(\newcommand{\nmindiv}{\mathsf{mindiv}}\) \(\newcommand{\nisprime}{\mathsf{isPrime}}\) \(\newcommand{\npower}{\mathsf{power}}\) \(\newcommand{\nchoose}{\mathsf{choose}}\) \(\newcommand{\dom}{\mathsf{dom}}\) \(\newcommand{\cod}{\mathsf{cod}}\) \(\newcommand{\lists}[1]{\mathsf{List}(#1)}\) \(\newcommand{\nil}{\mathsf{nil}}\) \(\newcommand{\cons}{\mathsf{cons}}\) \(\newcommand{\uncons}{\mathsf{uncons}}\) \(\newcommand{\isnil}{\mathsf{isNil}}\) \(\newcommand{\tail}{\mathsf{tail}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\foldr}{\mathsf{foldr}}\) \(\newcommand{\foldl}{\mathsf{foldl}}\) \(\newcommand{\tacunfoldN}{\mathsf{tacunfoldN}}\) \(\newcommand{\unfoldN}{\mathsf{unfoldN}}\) \(\newcommand{\dfoldr}{\mathsf{dfoldr}}\) \(\newcommand{\cfoldr}{\mathsf{cfoldr}}\) \(\newcommand{\bfoldr}{\mathsf{bfoldr}}\) \(\newcommand{\dbfoldr}{\mathsf{dbfoldr}}\) \(\newcommand{\lfoldr}{\mathsf{lfoldr}}\) \(\newcommand{\snoc}{\mathsf{snoc}}\) \(\newcommand{\revcat}{\mathsf{revcat}}\) \(\newcommand{\rev}{\mathsf{rev}}\) \(\newcommand{\last}{\mathsf{last}}\) \(\newcommand{\cat}{\mathsf{cat}}\) \(\newcommand{\addlength}{\mathsf{addlength}}\) \(\newcommand{\length}{\mathsf{length}}\) \(\newcommand{\head}{\mathsf{head}}\) \(\newcommand{\at}{\mathsf{at}}\) \(\newcommand{\map}{\mathsf{map}}\) \(\newcommand{\range}{\mathsf{range}}\) \(\newcommand{\zip}{\mathsf{zip}}\) \(\newcommand{\zipPad}{\mathsf{zipPad}}\) \(\newcommand{\unzip}{\mathsf{unzip}}\) \(\newcommand{\prefix}{\mathsf{prefix}}\) \(\newcommand{\suffix}{\mathsf{suffix}}\) \(\newcommand{\lcp}{\mathsf{lcp}}\) \(\newcommand{\lcs}{\mathsf{lcs}}\) \(\newcommand{\all}{\mathsf{all}}\) \(\newcommand{\any}{\mathsf{any}}\) \(\newcommand{\tails}{\mathsf{tails}}\) \(\newcommand{\inits}{\mathsf{inits}}\) \(\newcommand{\filter}{\mathsf{filter}}\) \(\newcommand{\elt}{\mathsf{elt}}\) \(\newcommand{\addcount}{\mathsf{addcount}}\) \(\newcommand{\count}{\mathsf{count}}\) \(\newcommand{\repeat}{\mathsf{repeat}}\) \(\newcommand{\sublist}{\mathsf{sublist}}\) \(\newcommand{\infix}{\mathsf{infix}}\) \(\newcommand{\select}{\mathsf{select}}\) \(\newcommand{\unique}{\mathsf{unique}}\) \(\newcommand{\delete}{\mathsf{delete}}\) \(\newcommand{\dedupeL}{\mathsf{dedupeL}}\) \(\newcommand{\dedupeR}{\mathsf{dedupeR}}\) \(\newcommand{\common}{\mathsf{common}}\) \(\newcommand{\disjoint}{\mathsf{disjoint}}\) \(\newcommand{\sublists}{\mathsf{sublists}}\) \(\newcommand{\take}{\mathsf{take}}\) \(\newcommand{\drop}{\mathsf{drop}}\) \(\newcommand{\takeBut}{\mathsf{takeBut}}\) \(\newcommand{\dropBut}{\mathsf{dropBut}}\) \(\newcommand{\takeWhile}{\mathsf{takeWhile}}\) \(\newcommand{\dropWhile}{\mathsf{dropWhile}}\)

This page is part of a series on Arithmetic Made Difficult.

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

In Haskell:

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.

\(\nchoose(n,\zero) = \next(\zero)\).
\(\nchoose(n,n) = \next(\zero)\).

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