--- title: Find Smallest author: nbloomf date: 2017-12-29 tags: arithmetic-made-difficult, literate-haskell slug: findsmallest --- > {-# LANGUAGE NoImplicitPrelude #-} > module FindSmallest ( > findSmallest, _test_findSmallest, main_findSmallest > ) where > > import Testing > import Booleans > import And > import DisjointUnions > import NaturalNumbers > import BailoutRecursion > import Plus > import LessThanOrEqualTo The Well-Ordering Principle on $\nats$ gives a sufficient condition under which a natural number minimal with respect to a given property must exist; namely, that the set of all natural numbers with that property is not empty. WOP can come in really handy when we want to show that, say, the smallest number $k$ with property *foo* exists, and reason about it. Unfortunately, WOP alone is nonconstructive -- it tells us nothing about how to actually *find* anything. Today we'll establish a weak constructive form of WOP. More precisely, given a predicate $\sigma : \nats \rightarrow \bool$ and two natural numbers $k$ and $n$, we'll define an operator $\Theta$ such that $\Theta(\next(n),k)$ is the *smallest* number $t$ between $k$ and $\nplus(k,n)$ such that $\sigma(t) = \btrue$, if any such number exists, and $\ast$ otherwise. :::::: definition :: Let $\sigma : \nats \rightarrow \bool$. Define $\varphi : \nats \rightarrow 1 + \nats$ by $$\varphi(k) = \lft(\ast),$$ $\beta : \nats \times \nats \rightarrow \bool$ by $$\beta(n,k) = \sigma(k),$$ $\psi : \nats \times \nats \rightarrow 1 + \nats$ by $$\psi(n,k) = \rgt(k),$$ and $\omega : \nats \times \nats \rightarrow \nats$ by $$\omega(n,k) = \next(k).$$ We then define $$\findsmallest() : \bool^\nats \rightarrow \nats \times \nats \rightarrow 1 + \nats$$ by $$\findsmallest(\sigma)(n,k) = \bailrec(\varphi)(\beta)(\psi)(\omega)(n,k).$$ In Haskell: > findSmallest :: (Natural n) => (n -> Bool) -> n -> n -> Union () n > findSmallest sigma = bailoutRec phi beta psi omega > where > phi _ = lft () > beta _ k = sigma k > psi _ k = rgt k > omega _ k = next k :::::::::::::::::::: Because $\findsmallest(\sigma)$ is defined in terms of bailout recursion, it is the unique solution to a system of functional equations. :::::: corollary ::: Let $\sigma : \nats \rightarrow \bool$ be a map. Then $\findsmallest(\sigma) : \nats \times \nats \rightarrow 1 + \nats$ is the unique solution $f : \nats \times \nats \rightarrow 1 + \nats$ to the following system of equations for all $n,k \in \nats$. $$\left\{\begin{array}{l} f(\zero,k) = \lft(\ast) \\ f(\next(n),k) = \bif{\sigma(k)}{\rgt(k)}{f(n,\next(k))} \end{array}\right.$$ ::: test ::::::::::: > _test_findSmallest_zero_left :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> Bool) > _test_findSmallest_zero_left _ = > testName "findSmallest(sigma)(0,k) == lft(*)" $> \sigma k -> eq (findSmallest sigma zero k) (lft ()) > > > _test_findSmallest_next_left :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> Bool) > _test_findSmallest_next_left _ = > testName "findSmallest(sigma)(next(n),k) == if(sigma(k),rgt(k),findSmallest(sigma)(n,next(k)))"$ > \sigma n k -> eq > (findSmallest sigma (next n) k) > (if sigma k then rgt k else findSmallest sigma n (next k)) :::::::::::::::::::: :::::::::::::::::::: First, if $\findsmallest(\sigma)$ returns a result $\rgt(t)$, then $t$ satisfies $\sigma$. :::::: theorem ::::: Let $\sigma : \nats \rightarrow \bool$, with $n,k,t \in \nats$. If $\findsmallest(\sigma)(n,k) = \rgt(t)$, then $\sigma(t) = \btrue$. ::: proof :::::::::: We proceed by induction on $n$. For the base case $n = \zero$, note that $$\findsmallest(\sigma)(\zero,k) = \lft(\ast),$$ so the implication holds vacuously. For the inductive step, suppose we have $n$ such that for all $k$ and $t$, if $\findsmallest(\sigma)(n,k) = \rgt(t)$ then $\sigma(t) = \btrue$. Suppose further that $\findsmallest(\sigma)(\next(n),k) = \rgt(t)$. Now we have $$\findsmallest(\sigma)(\next(n),k) = \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(n,\next(k))}.$$ We have two possibilities. If $\sigma(k) = \btrue$, then $$\findsmallest(\sigma)(n,k) = \rgt(k),$$ with $\sigma(k) = \btrue$ as needed. If $\sigma(k) = \bfalse,$ we have $$\rgt(t) = \findsmallest(\sigma)(\next(n),k) = \findsmallest(\sigma)(n,\next(k)),$$ and by the inductive hypothesis, $\sigma(t) = \btrue$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_findSmallest_satisfies :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> Bool) > _test_findSmallest_satisfies _ = > testName "if findSmallest(sigma)(n,k) == rgt(t) then sigma(t) == true" $> \sigma n k -> case findSmallest sigma n k of > Right t -> eq (sigma t) true > Left () -> true :::::::::::::::::::: :::::::::::::::::::: Next, if$\findsmallest(\sigma)(\next(n),k)$returns a result$\rgt(t)$, then$t$is bounded; specifically,$\nleq(k,t)$and$\nleq(t,\nplus(n,k))$. :::::: theorem ::::: If$\findsmallest(\sigma)(\next(n),k) = \rgt(t)$, then$\nleq(k,t)$and$\nleq(t,\nplus(n,k))$. ::: proof :::::::::: We proceed by induction on$n$. For the base case$n = \zero$, if$\findsmallest(\sigma)(\next(n),k) = \rgt(t)$we have $$\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)}. \end{eqnarray*}$$ In particular, we must have$\sigma(k) = \btrue$and$t = k$. Thus$\nleq(k,t)$and$\nleq(t,\nplus(n,k))$as needed. For the inductive step, suppose the implication holds for all$k$and$t$for some$n$, and suppose further that$\findsmallest(\sigma)(\next(\next(n)),k) = \rgt(t)$. Now $$\begin{eqnarray*} & & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}$$ We have two possibilities. If$\sigma(k) = \btrue$, then$\rgt(t) = \rgt(k)$, so that$\nleq(k,t)$and$\nleq(t,\nplus(n,k))$as needed. If$\sigma(k) = \bfalse$, we have$\rgt(t) = \findsmallest(\sigma)(\next(n),\next(k))$. By the inductive hypothesis, we have$\nleq(\next(k),t)$and$\nleq(t,\nplus(\next(n),\next(k)))$. By transitivity we thus have$\nleq(k,t)$and$\nleq(t,\nplus(\next(\next(n)),k))$as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_findSmallest_bounded :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> Bool) > _test_findSmallest_bounded _ = > testName "if findSmallest(sigma)(next(n),k) == rgt(t) then leq(k,t) and leq(t,plus(n,k))"$ > \sigma n k -> case findSmallest sigma (next n) k of > Right t -> and (leq k t) (leq t (plus n k)) > Left () -> true :::::::::::::::::::: :::::::::::::::::::: $\findsmallest(\sigma)(\next(n),k)$ returns $\lft(\ast)$ if and only if $\sigma$ is false for all $u$ between $k$ and $\nplus(n,k)$. :::::: theorem ::::: Let $\sigma : \nats \rightarrow \bool$ and $n,k \in \nats$. Then $\findsmallest(\sigma)(\next(n),k) = \lft(\ast)$ if and only if $\sigma(t) = \bfalse$ for all $t$ with $\nleq(k,t)$ and $\nleq(t,\nplus(n,k))$. ::: proof :::::::::: We prove the "only if" direction by induction on $n$. For the base case $n = \zero$, suppose $\findsmallest(\sigma)(\next(\zero),k) = \lft(\ast)$. Expanding, we have $$\begin{eqnarray*} & & \lft(\ast) \\ & = & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \end{eqnarray*}$$ Thus $\sigma(k) = \bfalse$. Now if $\nleq(k,t)$ and $\nleq(t,\nplus(\zero,k))$, we have $t = k$ by antisymmetry, and thus $\sigma(t) = \bfalse$ for all $\nleq(k,t)$ and $\nleq(t,\nplus(n,k))$ as needed. For the inductive step, suppose the implication holds for all $k$ for some $n$, and suppose further that $\findsmallest(\sigma)(\next(\next(n)),k) = \lft(\ast)$. Expanding, we have $$\begin{eqnarray*} & & \lft(\ast) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}$$ Now we must have $\sigma(k) = \bfalse$, and moreover $\findsmallest(\sigma)(\next(n),\next(k)) = \lft(\ast)$. By the inductive hypothesis, we have $\sigma(t) = \bfalse$ whenever $\nleq(\next(k),t)$ and $\nleq(t,\nplus(\next(n),\next(k)))$; thus $\sigma(t) = \bfalse$ whenever $\nleq(k,t)$ and $\nleq(t,\nplus(\next(\next(n)),k))$ as needed. We also prove the "if" direction by induction on $n$. For the base case $n = \zero$, suppose $\sigma(t) = \bfalse$ when $\nleq(k,t)$ and $\nleq(t,\nplus(\zero,k))$; by antisymmetry, we have $\sigma(k) = \bfalse$, and thus $$\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\zero,k)} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \\ & = & \bif{\bfalse}{\rgt(k)}{\lft(\ast)} \\ & \href{@booleans@#cor-if-false} = & \lft(\ast) \end{eqnarray*}$$ as needed. For the inductive step, suppose the implication holds for all $k$ for some $n$, and suppose further that $\sigma(t) = \bfalse$ whenever $\nleq(k,t)$ and $\nleq(t,\nplus(\next(n),k))$. Then we have $\sigma(k) = \bfalse$, and we also have $\sigma(t) = \bfalse$ whenever $\nleq(\next(k),t)$ and $\nleq(t,\nplus(n,\next(k)))$, and by the inductive hypothesis, $\findsmallest(\sigma)(\next(n),\next(k)) = \lft(\ast)$. Now $$\begin{eqnarray*} & & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))} \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)} \\ & = & \bif{\bfalse}{\rgt(k)}{\lft(\ast)} \\ & \href{@booleans@#cor-if-false} = & \lft(\ast) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_findSmallest_return_lft :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> n -> Bool) > _test_findSmallest_return_lft _ = > testName "if eq(findSmallest(sigma)(next(n),k),lft(*)) and leq(k,t) and leq(t,plus(n,k)) then eq(sigma(t),false)" $> \sigma n k t -> if and (leq k t) (leq t (plus n k)) > then if eq (findSmallest sigma (next n) k) (lft ()) > then eq (sigma t) false > else true > else true :::::::::::::::::::: :::::::::::::::::::: If$\findsmallest(\sigma)(n,k)$returns a value, then$\findsmallest(\sigma)(t,k)$does not, where$t$is the difference between$k$and the returned value. :::::: theorem ::::: If$\findsmallest(\sigma)(n,k) = \rgt(\nplus(k,\next(t)))$, then$\findsmallest(\sigma)(t,k) = \lft(\ast)$. ::: proof :::::::::: We proceed by induction on$t$. For the base case$t = \zero$, note that $$\findsmallest(\sigma)(\zero,k) = \lft(\ast),$$ so the implication holds regardless of$n$and$k$. For the inductive step, suppose the implication holds for all$n$and$k$for some$t$, and suppose further that $$\findsmallest(\sigma)(n,k) = \rgt(\nplus(k,\next(\next(t)))).$$ Now we must have$n = \next(m)$for some$m$, and moreover $$\begin{eqnarray*} & & \rgt(\nplus(\next(k),\next(t))) \\ & = & \rgt(\nplus(k,\next(\next(t)))) \\ & = & \findsmallest(\sigma)(\next(m),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(m,\next(k))} \end{eqnarray*}$$ Note that$\sigma(k)$cannot be$\btrue$, as in this case we have$k = \nplus(k,\next(\next(t)))$. So we have$\sigma(k) = \bfalse$and $$\begin{eqnarray*} & & \rgt(\nplus(\next(k),\next(t))) \\ & = & \findsmallest(\sigma)(m,\next(k)). \end{eqnarray*}$$ By the inductive hypothesis, we have$\findsmallest(\sigma)(t,\next(k)) = \lft(\ast)$, and thus $$\begin{eqnarray*} & & \findsmallest(\sigma)(\next(t),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(t,\next(k))} \\ & = & \findsmallest(\sigma)(t,\next(k)) \\ & = & \lft(\ast) \end{eqnarray*}$$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_findSmallest_value_lft :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> n -> Bool) > _test_findSmallest_value_lft _ = > testName "if findSmallest(sigma)(n,k) == rgt(plus(k,next(t))) then findSmallest(sigma)(t,k) = lft(*)"$ > \sigma n k t -> if eq (findSmallest sigma n k) (rgt (plus k (next t))) > then eq (findSmallest sigma t k) (lft ()) > else true :::::::::::::::::::: :::::::::::::::::::: Finally, $\findsmallest(\sigma)$ returns a least value. :::::: theorem ::::: If $\findsmallest(\sigma)(\next(n),k) = \rgt(t)$, and if $u \in \nats$ such that $\sigma(u) = \btrue$, $\nleq(k,u)$, and $\nleq(u,\nplus(n,k))$, then $\nleq(t,u)$. ::: proof :::::::::: We proceed by induction on $n$. For the base case $n = \zero$, suppose $$\begin{eqnarray*} & & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\zero),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\lft(\ast)}. \end{eqnarray*}$$ We must have $\sigma(k) = \btrue$ and thus $k = t$. Then we have $\nleq(t,u)$ whenever $\nleq(k,u)$ as needed. For the inductive step, suppose the implication holds for all $k$, $t$, and $u$ for some $n$, and suppose further that $\findsmallest(\sigma)(\next(\next(n)),k) = \rgt(t)$. Now $t = \nplus(k,m)$ for some $m$ since $\nleq(k,t)$. We have $$\begin{eqnarray*} & & \rgt(\nplus(k,m)) \\ & = & \rgt(t) \\ & = & \findsmallest(\sigma)(\next(\next(n)),k) \\ & = & \bif{\sigma(k)}{\rgt(k)}{\findsmallest(\sigma)(\next(n),\next(k))}. \end{eqnarray*}$$ If $\sigma(k) = \btrue$, then $t = k$, and we again have $\nleq(t,u)$ as needed. If instead $\sigma(k) = \bfalse$, we have $$\rgt(t) = \findsmallest(\sigma)(\next(n),\next(k)).$$ By the inductive hypothesis, if $\sigma(u) = \btrue$ and $\nleq(\next(k),u)$ and $\nleq(u,\nplus(n,\next(k)))$, then $\nleq(t,u)$. Suppose $\sigma(u) = \btrue$, $\nleq(k,u)$, and $\nleq(u,\nplus(\next(n),k))$. Since $\sigma(k) = \bfalse$, we have $\nleq(\next(k),u)$, so by the inductive hypothesis, $\nleq(t,u)$ as needed. :::::::::::::::::::: ::: test ::::::::::: > _test_findSmallest_minimal :: (Natural n, Equal n) > => n -> Test ((n -> Bool) -> n -> n -> n -> n -> Bool) > _test_findSmallest_minimal _ = > testName "if findSmallest(sigma)(next(n),k) == rgt(t) and sigma(u) and leq(k,u) and leq(u,plus(n,k)) then leq(t,u)" $> \sigma n k _ u -> case findSmallest sigma (next n) k of > Right t -> if and (sigma u) (and (leq k u) (leq u (plus n k))) > then leq t u > else true > Left () -> true :::::::::::::::::::: :::::::::::::::::::: To summarize: :::::: corollary ::: Let$\sigma : \nats \rightarrow \bool$and$n,k \in \nats$. 1. If$\findsmallest(\sigma)(\next(n),k) = \rgt(t)$, then$\sigma(t)$,$\nleq(k,t)$, and$\nleq(t,\nplus(n,k))$, and if$u \in \nats$such that$\sigma(u)$,$\nleq(k,u)$, and$\nleq(u,\nplus(n,k))$, then$\nleq(t,u)$. 2. If$\findsmallest(\sigma)(\next(n),k) = \lft(\ast)$, then there does not exist$u \in \nats$such that$\sigma(u)$,$\nleq(k,u)$, and$\nleq(u,\nplus(n,k))\$. :::::::::::::::::::: Testing ------- Suite: > _test_findSmallest :: > ( TypeName n, Natural n, Equal n, Arbitrary n, CoArbitrary n, Show n > ) => Int -> Int -> n -> IO () > _test_findSmallest size cases n = do > testLabel1 "findSmallest" n > > let args = testArgs size cases > > runTest args (_test_findSmallest_zero_left n) > runTest args (_test_findSmallest_next_left n) > runTest args (_test_findSmallest_satisfies n) > runTest args (_test_findSmallest_bounded n) > runTest args (_test_findSmallest_return_lft n) > runTest args (_test_findSmallest_value_lft n) > runTest args (_test_findSmallest_minimal n) Main: > main_findSmallest :: IO () > main_findSmallest = do > _test_findSmallest 50 100 (zero :: Unary)