Mutating Norm Recursion

Posted on 2018-01-19 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 MutatingNormRecursion (
  mnormrec
) where

import Testing
import Booleans
import DisjointUnions
import Unary
import NaturalNumbers
import MutatingRecursion

Just as mutating recursion generalizes bailout recursion at the expense of losing the tail recursive evaluation strategy, it will be handy to have a generalization of norm recursion that sacrifices tail recursion. We’ll call this mutating norm recursion.

Let $(A,\varepsilon,\varphi)$ be an inductive set, and let $\eta : A \rightarrow \nats$ be an inductive norm. Now suppose we have mappings $\delta : A \rightarrow B$ and $\sigma : A \times B \rightarrow B$. Then there is a unique map $\Theta : A \rightarrow B$ such that. \[\Theta(a) = \left\{\begin{array}{l} \delta(a) & \mathrm{if}\ \iszero(\eta(a)) \\ \sigma(a,\Theta(\varphi(a))) & \mathrm{otherwise} \end{array}\right.\] We denote this unique map by $\mnormrec(\varphi)(\eta)(\delta)(\sigma)$.

We define maps $\beta : \nats \times A \rightarrow \bool$ by \[\beta(n,a) = \iszero(\eta(a)),\] $\psi : \nats \times A \rightarrow B$ by \[\psi(n,a) = \delta(a),\] $\chi : \nats \times A \times B \rightarrow B$ by \[\chi(n,a,b) = \sigma(a,b),\] and $\omega : \nats \times A \rightarrow A$ by \[\omega(n,a) = \varphi(a).\] Now we define $\Omega : \nats \times A \rightarrow B$ by \[\Omega = \mutrec(\delta)(\beta)(\psi)(\chi)(\omega).\]

We first need the following intermediate result: for all $a \in A$ and $k \in \nats$, we claim that \[\Omega(\nplus(\eta(\varphi(a)),k),\varphi(a)) = \Omega(\eta(\varphi(a)),\varphi(a)).\] To see this, we proceed by strong induction on $\eta(\varphi(a))$. For the base case, suppose $\eta(\varphi(a)) = \zero$; we show the equality holds by induction on $k$. For the base case $k = \zero$, we have \[\begin{eqnarray*} & & \Omega(\nplus(\eta(\varphi(a)),k),\varphi(a)) \\ & = & \Omega(\nplus(\zero,\zero),\varphi(a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#cor-plus-up-zero} = & \Omega(\zero,\varphi(a)) \\ & = & \Omega(\eta(\varphi(a)),\varphi(a)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $k$ when $\eta(\varphi(a)) = \zero$. Now \[\begin{eqnarray*} & & \Omega(\nplus(\eta(\varphi(a)),\next(k)),\varphi(a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \Omega(\next(\nplus(\eta(\varphi(a)),k)),\varphi(a)) \\ & = & \bif{\iszero(\eta(\varphi(a)))}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a))))} \\ & = & \bif{\btrue}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a))))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \delta(\varphi(a)) \\ & = & \bif{\btrue}{\delta(\varphi(a))}{} \\ & = & \bif{\iszero(\eta(\varphi(a)))}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(\eta(\varphi(a)),\varphi(\varphi(a))))} \\ & = & \Omega(\eta(\varphi(a)),\varphi(a)) \end{eqnarray*}\] as needed.

For the strong inductive step, suppose the equality holds for all $k$ whenever $\nleq(\eta(\varphi(a)),m)$ for some $m$, and suppose further that $\eta(\varphi(a)) = \next(m)$. We proceed by induction on $k$. For the base case $k = \zero$, of course we have \[\begin{eqnarray*} & & \Omega(\nplus(\eta(\varphi(a)),k),\varphi(a)) \\ & = & \Omega(\nplus(\eta(\varphi(a)),\zero),\varphi(a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-zero-right} = & \Omega(\eta(\varphi(a)),\varphi(a)) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for some $k$. Now \[\begin{eqnarray*} & & \Omega(\nplus(\eta(\varphi(a)),\next(k)),\varphi(a)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-next-right} = & \Omega(\next(\nplus(\eta(\varphi(a)),k)),\varphi(a)) \\ & = & \bif{\iszero(\varphi(a))}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a))))} \\ & = & \sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a)))) \\ & = & Q. \end{eqnarray*}\] Note that $\eta(\varphi(a)) = \next(m)$, so that ((((a))),m)$, and thus $\nplus(\eta(\varphi(\varphi(a))),u) = m$ for some $u$. Now \[\begin{eqnarray*} & & \nplus(\eta(\varphi(a)),k) \\ & = & \nplus(\next(m),k) \\ & = & \nplus(m,\next(k)) \\ & = & \nplus(\nplus(\eta(\varphi(\varphi(a))),u),\next(k)) \\ & \href{/posts/arithmetic-made-difficult/Plus.html#thm-plus-associative} = & \nplus(\eta(\varphi(\varphi(a))),\nplus(u,\next(k))) \end{eqnarray*}\] Using the strong induction hypothesis, we have \[\begin{eqnarray*} & & Q \\ & = & \sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(\varphi(a))),\nplus(u,\next(k))),\varphi(\varphi(a)))) \\ & = & \sigma(\varphi(a),\Omega(\eta(\varphi(\varphi(a))),\varphi(\varphi(a)))) \\ & = & \sigma(\varphi(a),\Omega(\nplus(\eta(\varphi(\varphi(a))),u),\varphi(\varphi(a)))) \\ & = & \sigma(\varphi(a),\Omega(m,\varphi(\varphi(a)))) \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \bif{\bfalse}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(m,\varphi(\varphi(a))))} \\ & = & \bif{\iszero(\eta(\varphi(a)))}{\delta(\varphi(a))}{\sigma(\varphi(a),\Omega(m,\varphi(\varphi(a))))} \\ & = & \Omega(\next(m),\varphi(a)) \\ & = & \Omega(\eta(\varphi(a)),\varphi(a)) \end{eqnarray*}\] as needed.

Now we define $\Theta : A \rightarrow B$ by \[\Theta(a) = \Omega(\eta(a),a).\] To see that $\Theta$ has the claimed properties, note that if $\eta(a) = \zero$, we have \[\begin{eqnarray*} & & \Theta(a) \\ & = & \Omega(\eta(a),a) \\ & = & \Omega(\zero,a) \\ & = & \delta(a). \end{eqnarray*}\] If $\eta(a) = \next(m)$, then $\nleq(eta(\varphi(a)),m)$, so that $\nplus(\eta(\varphi(a)),u) = m$ for some $u$. Now \[\begin{eqnarray*} & & \Theta(a) \\ & = & \Omega(\eta(a),a) \\ & = & \Omega(\next(m),a) \\ & = & \bif{\iszero(\eta(a))}{\delta(a)}{\sigma(a,\Omega(m,\varphi(a)))} \\ & = & \bif{\iszero(\next(m))}{\delta(a)}{\sigma(a,\Omega(m,\varphi(a)))} \\ & \href{/posts/arithmetic-made-difficult/Unary.html#thm-iszero-next} = & \bif{\bfalse}{\delta(a)}{\sigma(a,\Omega(m,\varphi(a)))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-false} = & \sigma(a,\Omega(m,\varphi(a))) \\ & = & \sigma(a,\Omega(\nplus(\eta(\varphi(a)),u),\varphi(a))) \\ & = & \sigma(a,\Omega(\eta(\varphi(a)),\varphi(a))) \\ & = & \sigma(a,\Theta(\varphi(a))) \end{eqnarray*}\] as needed.

Finally we show that $\Theta$ is unique. To this end, suppose $\Psi : A \rightarrow B$ is a map such that $\Psi(a) = \delta(a)$ if $\eta(a) = \zero$ and $\Psi(a) = \sigma(a,\Psi(\varphi(a)))$ otherwise. We show that $\Psi(a) = \Theta(a)$ for all $a$ by strong induction on $\eta(a)$. For the base case $\eta(a) = \zero$, we have \[\begin{eqnarray*} & & \Psi(a) \\ & = & \delta(a) \\ & = & \Theta(a) \end{eqnarray*}\] as needed. For the inductive step suppose the equality holds for all $a$ such that $\nleq(\eta(a),m)$ for some $m$, and suppose further that $\eta(a) = \next(m)$. Now $\nleq(\eta(\varphi(a)),m)$, so we have \[\begin{eqnarray*} & & \Psi(a) \\ & = & \sigma(a,\Psi(\varphi(a))) \\ & = & \sigma(a,\Theta(\varphi(a))) \\ & = & \Theta(a) \end{eqnarray*}\] as needed.

Implementation

We have a couple of ways to implement $\mnormrec$.

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

There’s the universal property:

mnormrec phi eta delta sigma a =
  case unnext (eta a) of
    Left () -> delta a
    Right _ -> sigma a (mnormrec phi eta delta sigma (phi a))

And there’s the definition from the proof.

mnormrec' phi eta delta sigma a =
  mutatingRec delta beta psi chi omega (eta a) a
  where
    beta _ a = isZero (eta a)
    psi _ a = delta a
    chi _ a b = sigma a b
    omega _ a = phi a