# Find Smallest

Posted on 2017-12-29 by nbloomf

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

{-# 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.

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

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.

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_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$$.

Let $$\sigma : \nats \rightarrow \bool$$, with $$n,k,t \in \nats$$. If $$\findsmallest(\sigma)(n,k) = \rgt(t)$$, then $$\sigma(t) = \btrue$$.

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_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))$$. If $$\findsmallest(\sigma)(\next(n),k) = \rgt(t)$$, then $$\nleq(k,t)$$ and $$\nleq(t,\nplus(n,k))$$. 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_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)$$.

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

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{/posts/arithmetic-made-difficult/Booleans.html#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{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \lft(\ast) \end{eqnarray*}$ as needed.

_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. If $$\findsmallest(\sigma)(n,k) = \rgt(\nplus(k,\next(t)))$$, then $$\findsmallest(\sigma)(t,k) = \lft(\ast)$$. 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_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.

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

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_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:

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)