From Arrows to Programs

Posted on 2014-05-07 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, 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.

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.

If $n \in \nats$, we have the following.

$\unnext(\zero) = \lft(\ast)$.
$\unnext(\next(n)) = \rgt(n)$.

Note that \[\begin{eqnarray*} & & \unnext(\zero) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\zero) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \lft(\ast) \end{eqnarray*}\] as claimed.
We proceed by induction on $n$. For the base case $n = \zero$, note that \[\begin{eqnarray*} & & \unnext(\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & \compose(\rgt)(\either(\const(\zero),\next))(\natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\zero)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \compose(\rgt)(\either(\const(\zero),\next))(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(\either(\const(\zero),\next)(\lft(\ast))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \rgt(\const(\zero)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#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{/posts/arithmetic-made-difficult/Unary.html#def-unnext} = & \natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & \compose(\rgt)(\either(\const(\zero),\next))(\natrec(\lft(\ast))(\compose(\rgt)(\either(\const(\zero),\next)))(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \rgt(\either(\const(\zero),\next)(\rgt(n))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#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.

The map $\unnext : \nats \rightarrow 1 + \nats$ is an isomorphism; in particular, the inverse of $\unnext$ is \[Ω = \either(\const(\zero),\next).\]

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{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\zero)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & Ω(\rgt(\either(\const(\zero),\next)(\lft(\ast)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & Ω(\rgt(\const(\zero)(\ast))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & Ω(\rgt(\zero)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(\zero)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \next(\zero) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \next(\const(\zero)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & Ω(\rgt(\either(\const(\zero),\next)(\rgt(n)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & Ω(\rgt(\next(n))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \next(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & Ω(\unnext(\zero)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\unnext(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-zero} = & \either(\const(\zero),\next)(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\zero)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \zero \end{eqnarray*}\] and if the equality holds for $n$, we have \[\begin{eqnarray*} & & \compose(Ω)(\unnext)(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & Ω(\unnext(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-next} = & Ω(\rgt(n)) \\ & \let{Ω = \either(\const(\zero),\next)} = & \either(\const(\zero),\next)(\rgt(n)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \unnext(Ω(\lft(\ast))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\lft(\ast))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \unnext(\const(\zero)(\ast)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \unnext(\zero) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \unnext(Ω(\rgt(\zero))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\rgt(\zero))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \unnext(\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#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{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \unnext(Ω(\rgt(\next(n)))) \\ & \let{Ω = \either(\const(\zero),\next)} = & \unnext(\either(\const(\zero),\next)(\rgt(\next(n)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \unnext(\next(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-next} = & \rgt(\next(n)) \end{eqnarray*}\] as needed.

From $\unnext$ we define two helper functions.

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.

1. $\prev(\zero) = \zero$. 2. $\prev(\next(n)) = n$. 3. $\iszero(\zero) = \btrue$. 4. $\iszero(\next(n)) = \bfalse$.

We have \[\begin{eqnarray*} & & \prev(\zero) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-prev} = & \compose(\either(\const(\zero),\id))(\unnext)(\zero) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\zero),\id)(\unnext(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-zero} = & \either(\const(\zero),\id)(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\zero)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \zero \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \prev(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-prev} = & \compose(\either(\const(\zero),\id))(\unnext)(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\zero),\id)(\unnext(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-next} = & \either(\const(\zero),\id)(\rgt(n)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \id(n) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-id} = & n \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \iszero(\zero) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-iszero} = & \compose(\either(\const(\btrue),\const(\bfalse)))(\unnext)(\zero) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\btrue),\const(\bfalse))(\unnext(\zero)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-zero} = & \either(\const(\btrue),\const(\bfalse))(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\btrue)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \btrue \end{eqnarray*}\] as claimed.
We have \[\begin{eqnarray*} & & \iszero(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#def-iszero} = & \compose(\either(\const(\btrue),\const(\bfalse)))(\unnext)(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\btrue),\const(\bfalse))(\unnext(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-next} = & \either(\const(\btrue),\const(\bfalse))(\rgt(n)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \const(\bfalse)(n) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \bfalse \end{eqnarray*}\] as claimed.

We’re now ready to finish off the Peano axioms.

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

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{/posts/arithmetic-made-difficult/Functions.html#def-id} = & \id(n) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-unnext-inverse-left} = & \compose(\either(\const(\zero),\next))(\unnext)(n) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-compose} = & \either(\const(\zero),\next)(\unnext(n)) \\ & \hyp{\unnext(n) = \lft(\ast)} = & \either(\const(\zero),\next)(\lft(\ast)) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \const(\zero)(\ast) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \zero \end{eqnarray*}\] and in the second case we have \[\begin{eqnarray*} & & n \\ & \href{/posts/arithmetic-made-difficult/Functions.html#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{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \next(m) \end{eqnarray*}\] as claimed.
If $\zero = \next(n)$, we have \[\begin{eqnarray*} & & \btrue \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-zero} = & \iszero(\zero) \\ & \hyp{\next(n) = \zero} = & \iszero(\next(n)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-next} = & \bfalse \end{eqnarray*}\] which is absurd.
The “if” part is trivial. To see the “only if” part, suppose we have $\next(n) = \next(m)$; then \[\begin{eqnarray*} & & n \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-prev-next} = & \prev(\next(n)) \\ & \hyp{\next(n) = \next(m)} = & \prev(\next(m)) \\ & \href{/posts/arithmetic-made-difficult/Unary.html#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.

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