--- title: From Arrows to Programs author: nbloomf date: 2014-05-07 tags: arithmetic-made-difficult, literate-haskell slug: unary --- > {-# LANGUAGE NoImplicitPrelude, BangPatterns #-} > module Unary > ( Unary(Z,N), mkUnary, natRec, _test_unary, main_unary > ) where > > import Prelude (Integer, (-), (<=)) > import Test.QuickCheck.Modifiers (NonNegative(..)) > import Testing > import Booleans > import Tuples > import DisjointUnions A nice consequence of wrapping up recursion in the $\natrec$ function is that it allows us to write programs, independent of any implementation, and prove things about them. We'll see lots of examples of this, but first we need to establish some structural results. :::::: definition :: []{#def-unnext} Let $1 = \{\ast\}$, and define $\varphi : 1 + \nats \rightarrow 1 + \nats$ by $$\varphi = \compose(\rgt)(\either(\const(\zero),\id)).$$ In this post we consider $$(1 + \nats, \lft(\ast), \varphi)$$ as an inductive set, and denote the natural recursion map $\nats \rightarrow 1 + \nats$ by $\unnext$. :::::::::::::::::::: We can evaluate $\unnext$ directly. :::::: theorem ::::: []{#thm-unnext-zero}[]{#thm-unnext-next} If $n \in \nats$, we have the following. 1. $\unnext(\zero) = \lft(\ast)$. 2. $\unnext(\next(n)) = \rgt(n)$. ::: proof :::::::::: 1. Note that $$\begin{eqnarray*} & & \unnext(\zero) \\ & \href{@unary@#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\zero) \\ & \href{@peano@#cor-natrec-zero} = & \lft(\ast) \end{eqnarray*}$$ as claimed. 2. We proceed by induction on $n$. For the base case $n = \zero$, note that $$\begin{eqnarray*} & & \unnext(\next(\zero)) \\ & \href{@unary@#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(\zero)) \\ & \href{@peano@#cor-natrec-next} = & \compose(\rgt)(\either(\const(\zero),\next))(\natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\zero)) \\ & \href{@peano@#cor-natrec-zero} = & \compose(\rgt)(\either(\const(\zero),\next))(\lft(\ast)) \\ & \href{@functions@#def-compose} = & \rgt(\either(\const(\zero),\next)(\lft(\ast))) \\ & \href{@disjoint-unions@#def-either-lft} = & \rgt(\const(\zero)(\ast)) \\ & \href{@functions@#def-const} = & \rgt(\zero) \end{eqnarray*}$$ as needed. For the inductive step, suppose the equality holds for some $n$. Now we have $$\begin{eqnarray*} & & \unnext(\next(\next(n))) \\ & \href{@unary@#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(\next(n))) \\ & \href{@peano@#cor-natrec-next} = & \compose(\rgt)(\either(\const(\zero),\next))(\natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(n))) \\ & \href{@unary@#def-unnext} = & \compose(\rgt)(\either(\const(\zero),\next))(\unnext(\next(n))) \\ & \hyp{\unnext(\next(n)) = \rgt(n)} = & \compose(\rgt)(\either(\const(\zero),\next))(\rgt(n)) \\ & \href{@functions@#def-compose} = & \rgt(\either(\const(\zero),\next)(\rgt(n))) \\ & \href{@disjoint-unions@#def-either-rgt} = & \rgt(\next(n)) \end{eqnarray*}$$ as needed. :::::::::::::::::::: :::::::::::::::::::: It turns out that $1 + \nats$ is isomorphic to $\nats$, and the map that achieves this is useful. :::::: theorem ::::: []{#thm-unnext-inverse} The map $\unnext : \nats \rightarrow 1 + \nats$ is an isomorphism; in particular, the inverse of $\unnext$ is $$Ω = \either(\const(\zero),\next).$$ ::: proof :::::::::: We need to show two results: first that $Ω$ is an inductive set homomorphism, and second that $Ω$ and $\Theta$ are mutual inverses. To the first point, note that $$\begin{eqnarray*} & & Ω(\lft(\ast)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\lft(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \const(\zero)(\ast) \\ & \href{@functions@#def-const} = & \zero \end{eqnarray*}$$ and if $x \in 1 + \nats$, we have two possibilities. If $x = \lft(\ast)$, we have $$\begin{eqnarray*} & & Ω(\compose(\rgt)(\either(\const(\zero),\next))(\lft(\ast))) \\ & \href{@functions@#def-compose} = & Ω(\rgt(\either(\const(\zero),\next)(\lft(\ast)))) \\ & \href{@disjoint-unions@#def-either-lft} = & Ω(\rgt(\const(\zero)(\ast))) \\ & \href{@functions@#def-const} = & Ω(\rgt(\zero)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(\zero)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \next(\zero) \\ & \href{@functions@#def-const} = & \next(\const(\zero)(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \next(\either(\const(\zero),\next)(\lft(\ast))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \next(Ω(\lft(\ast))) \end{eqnarray*}$$ and if $x = \rgt(n)$, with $n \in \nats$, we have $$\begin{eqnarray*} & & Ω(\compose(\rgt)(\either(\const(\zero),\next))(\rgt(n))) \\ & \href{@functions@#def-compose} = & Ω(\rgt(\either(\const(\zero),\next)(\rgt(n)))) \\ & \href{@disjoint-unions@#def-either-rgt} = & Ω(\rgt(\next(n))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(\next(n))) \\ & \href{@disjoint-unions@#def-either-rgt} = & \next(\next(n)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \next(\either(\const(\zero),\next)(\rgt(n))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \next(Ω(\rgt(n))) \end{eqnarray*}$$ as needed. Next to see that $Ω$ and $\Theta$ are mutual inverses. First we show that $\compose(Ω)(\unnext)(n) = \id(n)$ for all $n \in \nats$, proceeding by induction. For the base case $n = \zero$ we have $$\begin{eqnarray*} & & \compose(Ω)(\unnext)(\zero) \\ & \href{@functions@#def-compose} = & Ω(\unnext(\zero)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\unnext(\zero)) \\ & \href{@unary@#thm-unnext-zero} = & \either(\const(\zero),\next)(\lft(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \const(\zero)(\ast) \\ & \href{@functions@#def-const} = & \zero \end{eqnarray*}$$ and if the equality holds for $n$, we have $$\begin{eqnarray*} & & \compose(Ω)(\unnext)(\next(n)) \\ & \href{@functions@#def-compose} = & Ω(\unnext(\next(n))) \\ & \href{@unary@#thm-unnext-next} = & Ω(\rgt(n)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(n)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \next(n) \end{eqnarray*}$$ as needed. Now to see that $\Theta \circ Ω = \id$, we consider two possibilities. First note that $$\begin{eqnarray*} & & \compose(\unnext)(Ω)(\lft(\ast)) \\ & \href{@functions@#def-compose} = & \unnext(Ω(\lft(\ast))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\lft(\ast))) \\ & \href{@disjoint-unions@#def-either-lft} = & \unnext(\const(\zero)(\ast)) \\ & \href{@functions@#def-const} = & \unnext(\zero) \\ & \href{@unary@#thm-unnext-zero} = & \lft(\ast) \end{eqnarray*}$$ To see that $(\Theta \circ Ω)(\rgt(n)) = \rgt(n)$ for all $n \in \nats$, we proceed by induction. For the base case $n = \zero$ we have $$\begin{eqnarray*} & & \compose(\unnext)(Ω)(\rgt(\zero)) \\ & \href{@functions@#def-compose} = & \unnext(Ω(\rgt(\zero))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\rgt(\zero))) \\ & \href{@disjoint-unions@#def-either-rgt} = & \unnext(\next(\zero)) \\ & \href{@unary@#thm-unnext-next} = & \rgt(\zero) \end{eqnarray*}$$ as needed. For the inductive step, if the equality holds for some $n$, we have $$\begin{eqnarray*} & & \compose(\unnext)(Ω)(\rgt(\next(n))) \\ & \href{@functions@#def-compose} = & \unnext(Ω(\rgt(\next(n)))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\rgt(\next(n)))) \\ & \href{@disjoint-unions@#def-either-rgt} = & \unnext(\next(\next(n))) \\ & \href{@unary@#thm-unnext-next} = & \rgt(\next(n)) \end{eqnarray*}$$ as needed. :::::::::::::::::::: :::::::::::::::::::: From $\unnext$ we define two helper functions. :::::: definition :: []{#def-prev}[]{#def-iszero} We define $\prev : \nats \rightarrow \nats$ by $$\prev = \compose(\either(\const(\zero),\id))(\unnext)$$ and $\iszero : \nats \rightarrow \bool$ by $$\iszero = \compose(\either(\const(\btrue),\const(\bfalse)))(\unnext).$$ :::::::::::::::::::: Now $\prev$, and $\iszero$ have some useful properties. :::::: theorem ::::: []{#thm-prev-zero}[]{#thm-prev-next}[]{#thm-iszero-zero}[]{#thm-iszero-next} 1. $\prev(\zero) = \zero$. 2. $\prev(\next(n)) = n$. 3. $\iszero(\zero) = \btrue$. 4. $\iszero(\next(n)) = \bfalse$. ::: proof :::::::::: 1. We have $$\begin{eqnarray*} & & \prev(\zero) \\ & \href{@unary@#def-prev} = & \compose(\either(\const(\zero),\id))(\unnext)(\zero) \\ & \href{@functions@#def-compose} = & \either(\const(\zero),\id)(\unnext(\zero)) \\ & \href{@unary@#thm-unnext-zero} = & \either(\const(\zero),\id)(\lft(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \const(\zero)(\ast) \\ & \href{@functions@#def-const} = & \zero \end{eqnarray*}$$ as claimed. 2. We have $$\begin{eqnarray*} & & \prev(\next(n)) \\ & \href{@unary@#def-prev} = & \compose(\either(\const(\zero),\id))(\unnext)(\next(n)) \\ & \href{@functions@#def-compose} = & \either(\const(\zero),\id)(\unnext(\next(n))) \\ & \href{@unary@#thm-unnext-next} = & \either(\const(\zero),\id)(\rgt(n)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \id(n) \\ & \href{@functions@#def-id} = & n \end{eqnarray*}$$ as claimed. 3. We have $$\begin{eqnarray*} & & \iszero(\zero) \\ & \href{@unary@#def-iszero} = & \compose(\either(\const(\btrue),\const(\bfalse)))(\unnext)(\zero) \\ & \href{@functions@#def-compose} = & \either(\const(\btrue),\const(\bfalse))(\unnext(\zero)) \\ & \href{@unary@#thm-unnext-zero} = & \either(\const(\btrue),\const(\bfalse))(\lft(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \const(\btrue)(\ast) \\ & \href{@functions@#def-const} = & \btrue \end{eqnarray*}$$ as claimed. 4. We have $$\begin{eqnarray*} & & \iszero(\next(n)) \\ & \href{@unary@#def-iszero} = & \compose(\either(\const(\btrue),\const(\bfalse)))(\unnext)(\next(n)) \\ & \href{@functions@#def-compose} = & \either(\const(\btrue),\const(\bfalse))(\unnext(\next(n))) \\ & \href{@unary@#thm-unnext-next} = & \either(\const(\btrue),\const(\bfalse))(\rgt(n)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \const(\bfalse)(n) \\ & \href{@functions@#def-const} = & \bfalse \end{eqnarray*}$$ as claimed. :::::::::::::::::::: :::::::::::::::::::: We're now ready to finish off the Peano axioms. :::::: theorem ::::: []{#thm-next-injective} 1. Every natural number is either $\zero$ or of the form $\next(m)$ for some natural number $m$, 2. No natural number is both $\zero$ and $\next(m)$ for some $m$, and 3. $\next(n) = \next(m)$ if and only if $n = m$. ::: proof :::::::::: 1. Let $n \in \nats$. Consider $\unnext(n) \in 1 + \nats$; we have either $\unnext(n) = \lft(\ast)$ or $\unnext(n) = \rgt(m)$ for some $m \in \nats$. In the first case we have $$\begin{eqnarray*} & & n \\ & \href{@functions@#def-id} = & \id(n) \\ & \href{@unary@#thm-unnext-inverse-left} = & \compose(\either(\const(\zero),\next))(\unnext)(n) \\ & \href{@functions@#def-compose} = & \either(\const(\zero),\next)(\unnext(n)) \\ & \hyp{\unnext(n) = \lft(\ast)} = & \either(\const(\zero),\next)(\lft(\ast)) \\ & \href{@disjoint-unions@#def-either-lft} = & \const(\zero)(\ast) \\ & \href{@functions@#def-const} = & \zero \end{eqnarray*}$$ and in the second case we have $$\begin{eqnarray*} & & n \\ & \href{@functions@#def-id} = & \id(n) \\ & \compose(\either(\const(\zero),\next))(\unnext)(n) = & \either(\const(\zero),\next)(\unnext(n)) \\ & \hyp{\unnext(n) = \rgt(m)} = & \either(\const(\zero),\next)(\rgt(m)) \\ & \href{@disjoint-unions@#def-either-rgt} = & \next(m) \end{eqnarray*}$$ as claimed. 2. If $\zero = \next(n)$, we have $$\begin{eqnarray*} & & \btrue \\ & \href{@unary@#thm-iszero-zero} = & \iszero(\zero) \\ & \hyp{\next(n) = \zero} = & \iszero(\next(n)) \\ & \href{@unary@#thm-iszero-next} = & \bfalse \end{eqnarray*}$$ which is absurd. 3. The "if" part is trivial. To see the "only if" part, suppose we have $\next(n) = \next(m)$; then $$\begin{eqnarray*} & & n \\ & \href{@unary@#thm-prev-next} = & \prev(\next(n)) \\ & \hyp{\next(n) = \next(m)} = & \prev(\next(m)) \\ & \href{@unary@#thm-prev-next} = & m \end{eqnarray*}$$ as claimed. :::::::::::::::::::: :::::::::::::::::::: Establishing that every natural number is either $\zero$ or of the form $\next(m)$ for some $m$ also justifies our use of the following Haskell type to model the natural numbers. > data Unary > = Z | N Unary > > instance Show Unary where > show Z = "O" > show (N k) = 'I' : show k > > instance TypeName Unary where > typeName _ = "Unary" > > instance Equal Unary where > eq Z Z = true > eq Z (N _) = false > eq (N _) Z = false > eq (N x) (N y) = eq x y (That show instance is so we can display elements of Nat without too many parentheses.) We also define a helper function to convert integers into Nats as follows. > mkUnary :: Integer -> Unary > mkUnary k = if k <= 0 > then Z > else N (mkUnary (k-1)) So calling mkUnary 7 in ghci, for instance, prints NNNNNNNZ And we can also give a straightforward implementation of $\natrec(\ast)(\ast)$. > natRec' :: a -> (a -> a) -> Unary -> a > natRec' e _ Z = e > natRec' e phi (N n) = phi (natRec' e phi n) For example: let theta' = natRec' true not and we can test out this map by evaluating it on several natural numbers: > theta' $mkUnary 10 true > theta'$ mkUnary 11 false Now this theta' is pretty silly (though not *that* silly, it detects the parity of a natural number, which we haven't defined yet). But in the next section we'll define a more interesting recursive function. But... ------ There is a practical problem with this implementation of natRec'. If we evaluate on a natural number like NNNZ, the "stack" of function calls expands to something like this: natRec' e phi (N $N$ N Z) == phi $natRec' e phi (N$ N Z) == phi $phi$ natRec' e phi (N Z) == phi $phi$ phi $natRec' e phi Z == phi$ phi $phi$ e == phi $phi$ e' == phi $e'' == e''' So we generate a tower of unevaluated calls to phi,$n$tall, before collapsing it down again. In the meantime all those unevaluated phis are sitting in memory. It is not difficult to see that if we evaluate natRec' on a "larger" number (whatever that means) we will quickly run out of actual memory. To help with this, we can try rewriting natRec in so-called "tail call" recursive form like so. > natRec :: a -> (a -> a) -> Unary -> a > natRec e phi n = > let > tau !x k = case k of > Z -> x > N m -> tau (phi x) m > in tau e n Now natRec does not leave a bunch of unevaluated functions in memory. It is effectively a loop, iterating "up" from 0 (again with the scare quotes because we don't have an order on$\nats$yet but of course you know what it means) rather than "down" from$n$. So this version expands to something like this: natRec e phi (N$ N $N Z) == tau e (N$ N $N Z) == tau e' (N$ N Z) == tau e'' (N Z) == tau e''' Z == e''' It deconstructs its natural number argument and evaluates phi strictly at each step. (That is what the bang pattern and $! are for.) At least I think that's what it does; my simple testing shows that natRec' easily falls down while natRec does not. But profiling Haskell seems like a bit of dark art to me still. I am open to being wrong here. We can see that natRec has better performance than natRec', but there is a hitch. natRec' is obviously an implementation of$\natrec(\ast)(\ast)$. But it is **not** obvious that natRec and natRec' are the same function! This is where the universal property of natural recursion comes in: if we can show that both functions satisfy the universal property, then *they must be the same*. And we can do this using induction. First, we claim that for all n :: Nat, natRec' (phi e) phi n == phi$ natRec' e phi n Using induction, it suffices to note that natRec' (phi e) phi Z == phi e == phi $natRec' e phi Z and that if the equation holds for n, then natRec' (phi e) phi (N n) == phi$ natRec' (phi e) phi n == phi $phi$ natRec' e phi n == phi $natRec' e phi (N n) Now, again using induction, we have natRec e phi Z == tau e Z == e == natRec' e phi Z and if natRec e phi n == natRec' e phi n, then natRec e phi (N n) == tau e (N n) == tau (phi e) n == natRec (phi e) phi n == natRec' (phi e) phi n == phi$ natRec' e phi n == natRec' e phi (N n) Since natRec e phi and natRec' e phi are both functions with signature Unary -> a which satisfy the universal property of $\nats$, they must be the same function: equal on all inputs. This is a powerful idea. We've effectively written a slow but obviously correct program, and then proven it is equivalent to a more efficient one. We'll be doing more of this later. Testing ------- Along the way we'll be writing some proofs involving Nats, but it is also useful to do some automated testing. I'll toss in an Arbitrary instance here. > instance Arbitrary Unary where > arbitrary = do > NonNegative k <- arbitrary > return (mkUnary k) > > shrink Z = [] > shrink (N k) = [k] > > instance CoArbitrary Unary where > coarbitrary Z = variant (0 :: Integer) > coarbitrary (N x) = variant (1 :: Integer) . coarbitrary x We can try out this instance with the following command. haskell $> generate (arbitrary :: Gen Unary)  While we're here, we can test that natRec and natRec' aren't _not_ equivalent. > _test_natRec_equiv :: (Equal a) => a -> Test (a -> (a -> a) -> Unary -> Bool) > _test_natRec_equiv _ = > testName "natRec(e)(f)(n) == natRec'(e)(f)(n)"$ > \e f n -> eq (natRec e f n) (natRec' e f n) > > _test_unary :: > ( Equal a, Show a, Arbitrary a, CoArbitrary a, TypeName a > ) => Int -> Int -> a -> IO () > _test_unary size cases a = do > testLabel1 "unary" a > let args = testArgs size cases > > runTest args (_test_natRec_equiv a) > > main_unary :: IO () > main_unary = do > _test_unary 30 300 () > _test_unary 30 300 (true :: Bool) > _test_unary 30 300 (tup true true :: Pair Bool Bool) > _test_unary 30 300 (lft true :: Union Bool Bool)