Double Natural Recursion

Posted on 2018-01-01 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 #-}
module DoubleNaturalRecursion (
  dnaturalRec, _test_dnaturalRec, main_dnaturalRec
) where

import Testing
import Booleans
import DisjointUnions
import NaturalNumbers

Today we’ll implement a slight generalization of natural recursion that allows recursion on two arguments.

[]{@#thm-dnatrec-zero-nat} Let $A$ be a set. Let $\delta : \nats \rightarrow A$, $\psi : A \rightarrow A$, and $\chi : \nats \times A \times A \rightarrow A$. Then there is a unique map $Θ : \nats \times \nats \rightarrow A$ such that \[Θ(\zero,k) = \delta(k),\] \[Θ(\next(n),\zero) = \psi(Θ(n,\zero)),\] and \[Θ(\next(n),\next(k)) = \chi(k,Θ(n,k),Θ(n,\next(k))).\] We denote this map by $\dnatrec(\delta)(\psi)(\chi).$$

Define $φ : A^\nats \rightarrow A^\nats$ casewise by \[\begin{eqnarray*} φ(g)(\zero) & = & \psi(g(\zero)) \\ φ(g)(\next(k)) & = & \chi(k,g(k),g(\next(k))). \end{eqnarray*}\] We then define $Θ : \nats \times \nats \rightarrow A$ by \[Θ(n,k) = \natrec(\delta)(φ)(n)(k).\]

First we show that $Θ$ satisfies the claimed equations. To this end, note that \[\begin{eqnarray*} & & Θ(\zero,k) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\zero)(k) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-zero} = & \delta(k) \end{eqnarray*}\] that \[\begin{eqnarray*} & & Θ(\next(n),\zero) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\next(n))(\zero) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & φ(\natrec(\delta)(φ)(n))(\zero) \\ & \hyp{φ(g)(\zero) = \psi(g(\zero))} = & \psi(\natrec(\delta)(φ)(n)(\zero)) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \psi(Θ(n,\zero)) \end{eqnarray*}\] and that \[\begin{eqnarray*} & & Θ(\next(n),\next(k)) \\ & \let{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \natrec(\delta)(φ)(\next(n))(\next(k)) \\ & \href{/posts/arithmetic-made-difficult/natural-numbers.html#cor-natrec-next} = & φ(\natrec(\delta)(φ)(n))(\next(k)) \\ & \hyp{φ(g)(\next(k)) = \chi(k,g(k),g(\next(k)))} = & \chi(k,\natrec(\delta)(φ)(n)(k),\natrec(\delta)(φ)(n)(\next(k))) \\ & \hyp{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \chi(k,Θ(n,k),\natrec(\delta)(φ)(n)(\next(k))) \\ & \hyp{Θ(n,k) = \natrec(\delta)(φ)(n)(k)} = & \chi(k,Θ(n,k),Θ(n,\next(k))) \end{eqnarray*}\] as claimed.

Next suppose $\Psi : \nats \times \nats \rightarrow A$ also satisfies these equations. We show that $\Psi = Θ$ by induction on $n$. For the base case $n = \zero$ for all $k$ we have \[\begin{eqnarray*} & & \Psi(\zero,k) \\ & \hyp{\Psi(\zero,k) = \delta(k)} = & \delta(k) \\ & \hyp{Θ(\zero,k) = \delta(k)} = & Θ(\zero,k) \end{eqnarray*}\] as needed. For the inductive step, suppose $\Psi(n,k) = Θ(n,k)$ for all $k$ for some $n$. Now let $k \in \nats$. We have two possibilities; if $k = \zero$, then \[\begin{eqnarray*} & & \Psi(\next(n),\zero) \\ & \hyp{\Psi(\next(n),\zero) = \psi(\Psi(n,\zero))} = & \psi(\Psi(n,\zero)) \\ & \hyp{Θ(n,\zero) = \Psi(n,\zero)} = & \psi(Θ(n,\zero)) \\ & \hyp{Θ(\next(n),\zero) = \psi(Θ(n,\zero))} = & Θ(\next(n),\zero) \end{eqnarray*}\] and if $k = \next(m)$, we have \[\begin{eqnarray*} & & \Psi(\next(n),\next(m)) \\ & \hyp{\Psi(\next(n),\next(m)) = \chi(\next(m),\Psi(n,m),\Psi(n,\next(m)))} = & \chi(\next(m),\Psi(n,m),\Psi(n,\next(m))) \\ & \let{Θ(n,m) = \Psi(n,m)} = & \chi(\next(m),Θ(n,m),Θ(n,\next(m))) \\ & \hyp{Θ(\next(n),\next(m)) = \chi(\next(m),Θ(n,m),Θ(n,\next(m)))} = & Θ(\next(n),\next(m)) \end{eqnarray*}\] as needed.

Implementation

There’s a couple of ways to implement $\dnatrec$.

dnaturalRec, dnaturalRec' :: (Natural n)
  => (n -> a)
  -> (a -> a)
  -> (n -> a -> a -> a)
  -> n -> n -> a

We can use the definition in the theorem:

dnaturalRec' delta psi chi = naturalRec delta phi
  where
    phi g k = case unnext k of
      Left () -> psi (g zero)
      Right m -> chi m (g m) (g (next m))

And there’s the definition from the universal property:

dnaturalRec delta psi chi n k = case unnext n of
  Left () -> delta k
  Right m -> case unnext k of
    Left () -> psi (dnaturalRec delta psi chi m zero)
    Right t -> chi t
      (dnaturalRec delta psi chi m t)
      (dnaturalRec delta psi chi m (next t))

While we’re here, we should test that these two implementations aren’t not equivalent.

_test_dnaturalRec_equiv
  :: (Natural n, Equal a)
  => n -> a
  -> Test ((n -> a) -> (a -> a) -> (n -> a -> a -> a) -> n -> n -> Bool)
_test_dnaturalRec_equiv _ _ =
  testName "dnaturalRec == dnaturalRec'" $
  \delta psi chi n k -> eq
    (dnaturalRec delta psi chi n k)
    (dnaturalRec' delta psi chi n k)

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

Let $A$ be a set, with $\delta : \nats \rightarrow A$, and $\psi : A \rightarrow A$, and $\chi : \nats \times A \times A \rightarrow A$. Then $\dnatrec(\delta)(\psi)(\chi)$ is the unique solution $f : \nats \times \nats \rightarrow A$ to the following system of functional equations for all $n,k \in \nats$: \[\left\{\begin{array}{l} f(\zero,k) = \delta(k) \\ f(\next(n),\zero) = \psi(f(n,\zero)) \\ f(\next(n),\next(k)) = \chi(k,f(n,k),f(n,\next(k))) \end{array}\right.\]

Testing

Suite:

_test_dnaturalRec ::
  ( TypeName n, Show n, Equal n, Arbitrary n, CoArbitrary n, Natural n
  , CoArbitrary a, Arbitrary a, Show a, Equal a, TypeName a
  ) => Int -> Int -> n -> a -> IO ()
_test_dnaturalRec size cases n a = do
  testLabel2 "dnaturalRec" n a

  let args = testArgs size cases

  runTest args (_test_dnaturalRec_equiv n a)

Main:

main_dnaturalRec :: IO ()
main_dnaturalRec = do
  _test_dnaturalRec 10 50 (zero :: Unary) (zero :: Unary)
  _test_dnaturalRec 10 50 (zero :: Unary) (zero :: Unary)
  _test_dnaturalRec 10 50 (zero :: Unary) (true :: Bool)
  _test_dnaturalRec 10 50 (zero :: Unary) (true :: Bool)