Left Fold
Posted on 2018-01-04 by nbloomf
\(\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.
Our goal today is to get as close as possible to a tail-recursive implementation of \(\foldr(\ast)(\ast)\).
Let \(A\) and \(B\) be sets, with \(f : B \times A \rightarrow B\). There is a unique map \(\Theta : B \times \lists{A} \rightarrow B\) such that \[\Theta(e,\nil) = e\] and \[\Theta(e,\cons(a,x)) = \Theta(f(e,a),x).\] We denote this map by \(\foldl(f)\).
First we show existence. Define \(\psi : A \times \lists{A}^B \rightarrow \lists{A}^B\) by \[\psi(a,g)(b) = g(f(b,a)),\] and define \(\Theta : B \times \lists{A} \rightarrow B\) by \[\Theta(b,x) = \foldr(\id)(\psi)(x)(b).\] Now \[\begin{eqnarray*}
& & \Theta(e,\nil) \\
& = & \foldr(\id)(\psi)(\nil)(e) \\
& \href{/posts/arithmetic-made-difficult/Lists.html#def-foldr-nil}
= & \id(e) \\
& \href{/posts/arithmetic-made-difficult/Functions.html#def-id}
= & e
\end{eqnarray*}\] and \[\begin{eqnarray*}
& & \Theta(e,\cons(a,x)) \\
& = & \foldr(\id)(\psi)(\cons(a,x))(e) \\
& = & \psi(a,\foldr(\id)(\psi))(x)(e) \\
& = & \foldr(\id)(\psi)(x)(f(e,a)) \\
& = & \Theta(f(e,a),x)
\end{eqnarray*}\] as claimed.
Now we show that \(\Theta\) is unique with this property; to that end, suppose we have a map \(\Omega : B \times \lists{A} \rightarrow B\) such that \(\Omega(e,\nil) = e\) and \(\Omega(e,\cons(a,x)) = \Omega(f(e,a),x)\) for all \(e \in B\), \(a \in A\), and \(x \in \lists{A}\). We show that \(\Omega(e,x) = \Theta(e,x)\) by list induction on \(x\). For the base case \(x = \nil\), we have \[\begin{eqnarray*}
& & \Omega(e,\nil) \\
& = & e \\
& = & \Theta(e,\nil).
\end{eqnarray*}\] For the inductive step, suppose \(\Omega(e,x) = \Theta(e,x)\), for all \(e \in B\) and some \(x \in \lists{A}\), and let \(a \in A\). Now \[\begin{eqnarray*}
& & \Omega(e,\cons(a,x)) \\
& = & \Omega(f(e,a),x) \\
& = & \Theta(f(e,a),x) \\
& = & \Theta(e,\cons(a,x))
\end{eqnarray*}\] as needed.
Implementation
We have a few options for implementing \(\foldl(\ast)\).
There’s the definition from the proof:
\(\psi : A \times \lists{A}^B \rightarrow \lists{A}^B\) by \[\psi(a,g)(b) = g(f(a,b)),\] and define \(\Theta : B \times \lists{A} \rightarrow B\) by \[\Theta(b,x) = \foldr(\id)(\psi)(x)(b).\]
And there’s the definition from the universal property:
We should verify that the two implementations are not not equivalent.
Testing
Suite:
Main: