Norm Recursion

Posted on 2017-12-25 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 NormRecursion (
  normRec
) where

import DisjointUnions
import NaturalNumbers
import BailoutRecursion

The essence of recursion is to solve problems by combining solutions to smaller instances of the same problem. The recursion patterns we’ve identified so far take a specific and limited view of what “smaller instance” means; the instance smaller than \(\next(n)\) is just \(n\). We can think of this as the recursion embodied in the induction principle, where we prove theorems about all natural numbers by assuming they hold for \(n\) and showing they also hold for \(\next(n)\).

We’ve seen an alternative induction principle – strong induction – which allows us to prove theorems by assuming they hold for all \(k\) with \(\nleq(k,n)\) and showing they hold for \(\next(n)\). Logically, strong induction is equivalent to “ordinary” induction, and so is redundant. But as we’ve seen, the stronger induction hypothesis of strong induction can make some proofs more convenient.

Today we’ll establish a recursion pattern analogous to strong induction.

Let \((A,\varepsilon,\varphi)\) be an iterative set. A map \(\eta : A \rightarrow \nats\) is called an iterative norm if the following hold for all \(a \in A\).

If \(\eta(a) = \zero\), then \(\eta(\varphi(a)) = \zero\).
If \(\eta(a) = \next(n)\), then \(\nleq(\eta(\varphi(a)),n)\).

Roughly speaking, an iterative norm is a measure of “size” on \(A\) with the property that this size is strictly decreasing under the action of \(\varphi\).

Let \((A,\varepsilon,\varphi)\) be an iterative set, with \(\eta : A \rightarrow \nats\) an iterative norm. Let \(B\) be a set, with \(\chi : A \rightarrow B\). Then there is a unique map \(\Theta : A \rightarrow B\) such that, for all \(a \in A\), \[\Theta(a) = \bif{\iszero(\eta(a))}{\chi(a)}{\Theta(\varphi(a))}.\] This \(\Theta\) will be denoted \(\normrec(\varphi)(\eta)(\chi)\).

We define \(\beta : \nats \times A \rightarrow \bool\) by \[\beta(k,a) = \iszero(\eta(a)),\] define \(\psi : \nats \times A \rightarrow B\) by \[\psi(k,a) = \chi(a),\] and define \(\omega : \nats \times A \rightarrow A\) by \[\omega(k,a) = \varphi(a),\] and \(\Omega : \nats \times A \rightarrow B\) by \[\Omega = \bailrec(\chi)(\beta)(\psi)(\omega).\] As a lemma, we need the following intermediate result: for all \(a \in A\) and \(k \in \nats\), we have \[\Omega(\nplus(\eta(\varphi(a)),k),\varphi(a)) = \Omega(\eta(\varphi(a)),\varphi(a)).\] We proceed by double induction, starting with strong induction on \(\eta(\varphi(a))\). For the base case \(\eta(\varphi(a)) = \zero\), we proceed 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*}\] 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(\eta(\varphi(a)))}{\chi(\varphi(a))}{\Omega(\nplus(\eta(\varphi(\varphi(a))),k))} \\ & = & \bif{\btrue}{\chi(\varphi(a))}{\Omega(\nplus(\eta(\varphi(\varphi(a))),k))} \\ & \href{/posts/arithmetic-made-difficult/Booleans.html#cor-if-true} = & \chi(\varphi(a)) \\ & = & \Omega(\zero,\varphi(a)) \\ & = & \Omega(\eta(\varphi(a)),\varphi(a)). \end{eqnarray*}\] So if \(\eta(\varphi(a)) = \zero\), we have \[\Omega(\nplus(\eta(\varphi(a)),k),\varphi(a)) = \Omega(\eta(\varphi(a)),\varphi(a)).\] For the strong induction step, suppose we have \(m \in \nats\) such that the equality holds for all \(k \in \nats\) and all \(a \in A\) such that \(\nleq(\eta(\varphi(a)),m)\). Suppose further that \(a \in A\) such that \(\eta(\varphi(a)) = \next(m)\). We proceed by induction on \(k\). If \(k = \zero\), we have \[\Omega(\nplus(\eta(\varphi(a)),\zero),\varphi(a)) = \Omega(\eta(\varphi(a)),\varphi(a)).\] 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(\eta(\varphi(a)))}{\chi(\varphi(a))}{\Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a)))} \\ & = & \Omega(\nplus(\eta(\varphi(a)),k),\varphi(\varphi(a))) \\ & = & Q. \end{eqnarray*}\] Now note that \(\eta(\varphi(a)) = \next(m)\), so \(\nleq(\eta(\varphi(\varphi(a))),m)\), and thus \(\nplus(\eta(\varphi(\varphi(a))),u) = m\) for some \(u\). Then \[\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*}\] and by the strong induction hypothesis, we have \[\begin{eqnarray*} & & Q \\ & = & \Omega(\nplus(\eta(\varphi(\varphi(a))),\nplus(u,\next(k))),\varphi(\varphi(a))) \\ & = & \Omega(\eta(\varphi(\varphi(a))),\varphi(\varphi(a))) \\ & = & \Omega(\nplus(\eta(\varphi(\varphi(a))),u),\varphi(\varphi(a))) \\ & = & \Omega(m,\varphi(\varphi(a))) \\ & = & \bif{\iszero(\eta(\varphi(a)))}{\chi(\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, we consider two possibilities for \(\eta(a)\). If \(\eta(a) = \zero\), we have \[\begin{eqnarray*} & & \Theta(a) \\ & = & \Omega(\eta(a),a) \\ & = & \Omega(\zero,a) \\ & = & \chi(a). \end{eqnarray*}\] If \(\eta(a) = \next(m)\), we have \(\nleq(\eta(\varphi(a)),m)\), so that \(\nplus(\eta(\varphi(a)),u) = m\) for some \(u\). Then \[\begin{eqnarray*} & & \Theta(a) \\ & = & \Omega(\eta(a),a) \\ & = & \Omega(\next(m),a) \\ & = & \bif{\iszero(\eta(a))}{\chi(a)}{\Omega(m,\varphi(a))} \\ & = & \bif{\next(m)}{\chi(a)}{\Omega(m,\varphi(a))} \\ & = & \Omega(m,\varphi(a)) \\ & = & \Omega(\nplus(\eta(\varphi(a)),u),\varphi(a)) \\ & = & \Omega(\eta(\varphi(a)),\varphi(a)) \\ & = & \Theta(\varphi(a)) \end{eqnarray*}\] as claimed.

We show that \(\Theta\) is unique by strong induction. Suppose \(\Pi\) is another function \(A \rightarrow B\) such that \(\Pi(a) = \chi(a)\) if \(\eta(a) = \zero\) and \(\Pi(a) = \Pi(\varphi(a))\) otherwise. For the base case, if \(\eta(a) = \zero\), we have \[\Pi(a) = \chi(a) = \Theta(a).\] For the inductive step, suppose \(\Pi(a) = \Theta(a)\) whenever \(\nleq(\eta(a),m)\) for some \(m\), and suppose \(\eta(a) = \next(m)\). Then \(\nleq(\eta(\varphi(a)),m)\) and \[\Pi(a) = \Pi(\varphi(a)) = \Theta(\varphi(a)) = \Theta(a)\] as needed.

Implementation

We can implement \(\normrec\) using the definition from the theorem…

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

normRec' phi eta chi a = bailoutRec chi beta psi omega (eta a) a
  where
    beta _ c = isZero (eta c)
    psi _ c = chi c
    omega _ c = phi c

Or by pattern matching, using the universal property.

normRec phi eta chi a = case unnext (eta a) of
  Left () -> chi a
  Right _ -> normRec phi eta chi (phi a)

As with our other recursion operators, \(\normrec(\varphi)(\eta)(\chi)\) is the unique solution to a system of functional equations. Specifically, we have the following.

Let \(A\) and \(B\) be sets, with \(\varphi : A \rightarrow A\), \(\eta : A \rightarrow \nats\) an iterative norm on \((A,\varepsilon,\varphi)\) for some \(\varepsilon\), and \(\chi : A \rightarrow B\). Then \(\normrec(\varphi)(\eta)(\chi)\) is the unique solution \(f : A \rightarrow B\) to the following functional equation for all \(a \in A\): \[f(a) = \bif{\iszero(\eta(a))}{\chi(a)}{f(\varphi(a))}.\]