Simple Recursion

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 SimpleRecursion
  ( simpleRec, _test_simplerec, main_simplerec
  ) where

import Testing
import Booleans
import Tuples
import DisjointUnions
import NaturalNumbers

So far we’ve defined the natural numbers as an iterative set with a special universal property, which was encapsulated in the existence of a simple recursion operator \(\natrec\). Anything we will wish to do with the natural numbers can be done using this operator alone. However, in practice, it will be handy to define synonyms for some more complicated recursive functions; the first of these is simple recursion with a parameter.

Suppose we have sets \(A\) and \(B\) and functions \(\varphi : A \rightarrow B\) and \(\mu : \nats \times A \times B \rightarrow B\). Then there is a unique function \(Θ : \nats \times A \rightarrow B\) such that, for all \(n \in \nats\) and \(a \in A\), \[Θ(\zero,a) = \varphi(a)\] and \[Θ(\next(n),a) = \mu(n,a,Θ(n,a)).\]

This function \(Θ\) will be denoted \(\simprec(\varphi)(\mu)\).

First we establish existence. Define \(\varepsilon : A \rightarrow \nats \times B\) by \[\varepsilon = \compose(\tup(\zero))(\varphi)\] and define \(\chi : A \rightarrow \nats \times B \rightarrow \nats \times B\) by \[\chi(a)(\tup(n)(b)) = \tup(\next(n))(\mu(n,a,b)).\] Thinking of \((\nats \times B, \varepsilon(a), \chi(a))\) as an inductive set, we define \(Ω : \nats \rightarrow A \rightarrow \nats \times B\) by \[Ω(n,a) = \natrec(\varepsilon(a))(\chi(a))(n)\] and \(Θ : \nats \times A \rightarrow B\) by \(Θ(n,a) = \snd(Ω(n,a))\).

Now note that \[\begin{eqnarray*} & & Θ(\zero,a) \\ & \let{Θ(n,a) = \snd(\natrec(\varepsilon(a))(\chi(a))(n))} = & \snd(\natrec(\varepsilon(a))(\chi(a))(\zero)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \snd(\varepsilon(a)) \\ & \hyp{\varepsilon(a) = \tup(\zero)(\varphi(a))} = & \snd(\tup(\zero)(\varphi(a))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \varphi(a) \end{eqnarray*}\] as claimed.

Next we show that \[Ω(\next(n),a) = \tup(\next(n))(\mu(n,a,Θ(n,a)))\] for all \(a \in A\) and \(n \in \nats\) by induction on \(n\). For the base case \(n = \zero\), we have \[\begin{eqnarray*} & & Ω(\next(\zero),a) \\ & \let{Ω(n,a) = \natrec(\varepsilon(a))(\chi(a))(n)} = & \natrec(\varepsilon(a))(\chi(a))(\next(\zero)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & \chi(a)(\natrec(\varepsilon(a))(\chi(a))(\zero)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \chi(a)(\varepsilon(a)) \\ & \hyp{\varepsilon(a) = \tup(\zero)(\varphi(a))} = & \chi(a)(\tup(\zero)(\varphi(a))) \\ & \hyp{\chi(a)(\tup(n)(b)) = \tup(\next(n))(\mu(n,a,b))} = & \tup(\next(\zero))(\mu(\zero,a,\varphi(a))) \\ & \hyp{Θ(\zero,a) = \varphi(a)} = & \tup(\next(\zero))(\mu(\zero,a,Θ(\zero,a))) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some \(n\). Now \[\begin{eqnarray*} & & Ω(\next(\next(n)),a) \\ & \let{Ω(n,a) = \natrec(\varepsilon(a))(\chi(a))(n)} = & \natrec(\varepsilon(a))(\chi(a))(\next(\next(n))) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & \chi(a)(\natrec(\varepsilon(a))(\chi(a))(\next(n))) \\ & \let{Ω(n,a) = \natrec(\varepsilon(a))(\chi(a))(n)} = & \chi(a)(Ω(\next(n),a)) \\ & \hyp{Ω(\next(n),a) = \tup(\next(n))(\mu(n,a,Θ(n,a)))} = & \chi(a)(\tup(\next(n))(\mu(n,a,Θ(n,a)))) \\ & \hyp{\chi(a)(\tup(n)(b)) = \tup(\next(n))(\mu(n,a,b))} = & \tup(\next(\next(n)))(\mu(\next(n),a,\mu(n,a,Θ(n,a)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \tup(\next(\next(n)))(\mu(\next(n),a,\snd(\tup(\next(n))(\mu(n,a,Θ(n,a)))))) \\ & \hyp{Ω(\next(n),a) = \tup(\next(n))(\mu(n,a,Θ(n,a)))} = & \tup(\next(\next(n)))(\mu(\next(n),a,\snd(Ω(\next(n),a)))) \\ & \hyp{Θ(n,a) = \snd(Ω(n,a))} = & \tup(\next(\next(n)))(\mu(\next(n),a,Θ(\next(n),a))) \end{eqnarray*}\] as needed. Thus for all \(a\) and \(n\) we have \[\begin{eqnarray*} & & Θ(\next(n),a) \\ & \hyp{Θ(n,a) = \snd(Ω(n,a))} = & \snd(Ω(\next(n),a)) \\ & \hyp{Ω(\next(n),a) = \tup(\next(n))(\mu(n,a,Θ(n,a)))} = & \snd(\tup(\next(n))(\mu(n,a,Θ(n,a)))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \mu(n,a,Θ(n,a)) \end{eqnarray*}\] as claimed.

To see that \(Θ\) is unique, we again use induction. Suppose \(\Psi : \nats \times A \rightarrow B\) is another mapping which satisfies the properties of \(Θ\). Then we have \[\begin{eqnarray*} & & \Psi(\zero,a) \\ & \hyp{\Psi(\zero,a) = \varphi(a)} = & \varphi(a) \\ & \hyp{Θ(\zero,a) = \varphi(a)} = & Θ(\zero,a) \end{eqnarray*}\] for all \(a \in A\), and if \(n \in \nats\) such that \(\Psi(n, a) = Θ(n, a)\) for all \(a \in A\), we have \[\begin{eqnarray*} & & \Psi(\next(n),a) \\ & \hyp{\Psi(\next(n),a) = \mu(n,a,\Psi(n,a))} = & \mu(n,a,\Psi(n,a)) \\ & \hyp{\Psi(n,a) = Θ(n,a)} = & \mu(n,a,Θ(n,a)) \\ & \hyp{Θ(\next(n),a) = \mu(n,a,Θ(n,a))} = & Θ(\next(n),a) \end{eqnarray*}\] as needed. Thus \(\Psi = Θ\).

That proof may look complicated, but structurally it’s very simple. We defined \(Θ\) and showed it has the claimed properties with induction, then we showed it is unique by induction.

Implementation

As we did with \(\natrec(\ast)(\ast)\), we’d like to implement \(\simprec(\ast)(\ast)\) in software. There are a couple of ways to go about this.

simpleRec'', simpleRec', simpleRec :: (Natural n)
  => (a -> b)
  -> (n -> a -> b -> b)
  -> n
  -> a
  -> b

There’s the naive way:

simpleRec'' phi mu n a = case unnext n of
  Left () -> phi a
  Right k -> mu k a $ simpleRec'' phi mu k a

There’s the definition from the proof:

simpleRec' phi mu n a = snd (naturalRec (epsilon a) (chi a) n)
  where
    epsilon b = tup zero (phi b)
    chi c (Pair m b) = tup (next m) (mu m c b)

And the tail recursive strategy:

simpleRec phi mu n a =
  let
    tau !x h m = case unnext m of
      Left () -> x
      Right k -> tau (mu h a x) (next h) k
  in tau (phi a) zero n

While we’re at it, we should test that these implementations are equivalent.

_test_simplerec_equiv_def :: (Natural n, Equal b)
  => n -> a -> b -> Test ((a -> b) -> (n -> a -> b -> b) -> n -> a -> Bool)
_test_simplerec_equiv_def _ _ _ =
  testName "simpleRec(phi,mu)(n,a) == simpleRec'(phi,mu)(n,a)" $
  \phi mu n a -> eq (simpleRec phi mu n a) (simpleRec' phi mu n a)

_test_simplerec_equiv_naive :: (Natural n, Equal b)
  => n -> a -> b -> Test ((a -> b) -> (n -> a -> b -> b) -> n -> a -> Bool)
_test_simplerec_equiv_naive _ _ _ =
  testName "simpleRec(phi,mu)(n,a) == simpleRec''(phi,mu)(n,a)" $
  \phi mu n a -> eq (simpleRec phi mu n a) (simpleRec'' phi mu n a)

Some simple testing again shows that the tail recursive form is more efficient – both of the other forms run out of space on medium-sized numbers. All we need to do is verify that the efficient simpRec is equivalent to the inefficient, but obviously correct, simpRec''. We will (eventually) do this by induction.

First, though, we need a lemma about tau. Note that in the definition of tau there are two implicit parameters, mu and a. With mu and phi fixed, we define supplementary functions mu' and phi' as follows:

mu' k a b = mu (N k) a b
phi' a = mu Z a (phi a)

We will denote by tau' the version of tau where mu' is in scope, and by tau the version with mu in scope. We claim that

tau' x h k == tau x (N h) k

for all x, h, and k, and prove it by induction on k. For the base case, note that

   tau' x h Z
== x
== tau x (N h) Z

For the inductive step, suppose the equation holds for k. Then we have

   tau' x h (N k)
== tau' (mu' h a x) (N h) k
== tau (mu' h a x) (N $ N h) k
== tau (mu (N h) a x) (N $ N h) k
== tau x (N h) (N k)

as needed.

Next we claim that

simpRec phi' mu' k a == simpRec phi mu (N k) a

for all phi, mu, k, and a. To see this, note that

   simpRec phi mu (N k) a
== tau (phi a) Z (N k)
== tau (mu Z a (phi a)) (N Z) k
== tau' (mu Z a (phi a)) Z k
== tau' (phi' a) Z k
== simpRec phi' mu' k a

as needed. Also, simpRec'' satisfies this equation, which we show by induction on k. For the base case, note that

   simpRec'' phi' mu' Z a
== phi' a
== mu Z a (phi a)
== mu Z a $ simpRec'' phi mu Z a
== simpRec'' phi mu (N Z) a

And if the equation holds for k, then we have

   simpRec'' phi' mu' (N k) a
== mu' k a $ simpRec'' phi' mu' k a
== mu' k a $ simpRec'' phi mu (N k) a
== mu (N k) a $ simpRec'' phi mu (N k) a
== simpRec'' phi mu (N $ N k) a

so that

simpRec'' phi' mu' k a == simpRec'' phi mu (N k) a

for all phi, mu, k, and a as claimed.

Finally we are prepared to show that simpRec == simpRec'', by induction on k. For the base case, we have

   simpRec'' phi mu Z a
== phi a
== tau (phi a) Z Z
== simpRec phi mu Z a

And if the result holds for k, we have

   simpRec'' phi mu (N k) a
== simpRec'' phi' mu' k a
== simpRec phi' mu' k a
== simpRec phi mu (N k) a

So our efficient simpRec is equivalent to simpRec''. (We will leave the equivalence of simpRec' and simpRec as an exercise.)

What it does

This page is already long enough, so I’ll save examples of simple recursion for another day. Just note what \(\simprec(\ast)(\ast)\) does: given some data \(\varphi\) and \(\mu\), it produces a recursive function with signature \(\nats \times A \rightarrow B\). So whenever we encounter (or want to construct) a function with this signature, it may be worthwhile to look for a definition in terms of \(\simprec(\ast)(\ast)\). The uniqueness of simple recursion makes such functions very nice to reason about.

As with natural recursion, the “uniqueness” part of simple recursion is also handy. To be a little more explicit, it says the following.

Let \(A\) and \(B\) be sets, with \(\varphi : \nats \times A \rightarrow B\) and \(\mu : \nats \times A \times B \rightarrow B\). Then \(\simprec(\varphi)(\mu)\) is the unique solution \(f : \nats \times A \rightarrow B\) to the following system of functional equations for all \(k \in \nats\), \(a \in A\), and \(b \in B\): \[\left\{\begin{array}{l} f(\zero,a) = \varphi(a) \\ f(\next(k),a) = \mu(k,a,f(k,a)) \end{array}\right.\]

Testing

Suite:

_test_simplerec
  :: (TypeName n, Natural n, Equal n, Show n, Arbitrary n
  , Equal b, Arbitrary a, CoArbitrary a, Arbitrary b, CoArbitrary b
  , Show a, Show b, TypeName a, TypeName b, CoArbitrary n)
  => Int -> Int -> n -> a -> b -> IO ()
_test_simplerec size cases n a b = do
  testLabel3 "simpleRec" n a b

  let args = testArgs size cases

  runTest args (_test_simplerec_equiv_def n a b)
  runTest args (_test_simplerec_equiv_naive n a b)

Main:

main_simplerec :: IO ()
main_simplerec = do
  _test_simplerec 100 200 (zero :: Unary) (true :: Bool)  (true :: Bool)
  _test_simplerec 100 200 (zero :: Unary) (zero :: Unary) (true :: Bool)
  _test_simplerec 100 200 (zero :: Unary) (true :: Bool)  (zero :: Unary)
  _test_simplerec 100 200 (zero :: Unary) (zero :: Unary) (zero :: Unary)