Lookback Fold

Posted on 2018-07-17 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 LookbackFold (
  lfoldr, main_lfoldr
) where

import Testing
import Functions
import Tuples
import DisjointUnions
import Lists
import HeadAndTail
import LeftFold
import Reverse
import Zip

Today we’ll implement another recursion operator on lists, this one analogous to the recursion for efficiently computing the \(n\)th Fibonacci number.

Let \(A\) and \(B\) be sets, with \(\theta \in B\), \(\lambda : A \rightarrow B\), and \(\mu : A \times A \times B \times B \rightarrow B\). There is a unique map \(\Psi : \lists{A} \rightarrow B\) such that \[\Psi(\nil) = \theta,\] \[\Psi(\cons(a,\nil)) = \lambda(a),\] and \[\Psi(\cons(a,\cons(b,x))) = \mu(a,b,\Psi(\cons(b,x)),\Psi(x)).\] We call this function lookback fold and denote it by \(\lfoldr(\theta)(\lambda)(\mu)\).

In Haskell:

lfoldr
  :: (List t)
  => b
  -> (a -> b)
  -> (a -> a -> b -> b -> b)
  -> t a -> b
lfoldr theta lambda mu x =
  snd (foldl phi (alpha x) (rev (zip x (tail x))))

  where
    alpha x = tup theta (either (const theta) lambda (last x))

    phi h k = tup (snd h) (mu (fst k) (snd k) (snd h) (fst h))

First we define \(\alpha : \lists{A} \rightarrow B \times B\) by \[\alpha(x) = \tup(\theta)(\either(\const(\theta))(\lambda)(\last(x)))\] and \(\varphi : (B \times B) \times (A \times A) \rightarrow B \times B\) by \[\varphi(\tup(u)(v),\tup(a)(b)) = \tup(v,\mu(a,b,v,u)).\] Now define \(\Omega : \lists{A} \rightarrow B \times B\) by \[\Omega(x) = \foldl(\varphi)(\alpha(x))(\rev(\zip(x,\tail(x)))).\]

Next we need to establish some technical lemmas. The first is that \[\alpha(\cons(a,\cons(b,x))) = \alpha(\cons(b,x))\] for all \(a,b \in A\) and \(x \in \lists{A}\). To see this, note that \[\begin{eqnarray*} & & \alpha(\cons(a,\cons(b,x))) \\ & = & \tup(\theta)(\either(\const(\theta))(\lambda)(\last(\cons(a,\cons(b,x))))) \\ & = & \tup(\theta)(\either(\const(\theta))(\lambda)(\last(\cons(b,x)))) \\ & = & \alpha(\cons(b,x)) \end{eqnarray*}\] as needed.

Second, we show that for all \(a \in A\) and \(x \in \lists{A}\), we have \[\fst(\Omega(\cons(a,x))) = \snd(\Omega(x)).\] We prove this by list induction on \(x\). For the base case \(x = \nil\), note that \[\begin{eqnarray*} & & \fst(\Omega(\cons(a,x))) \\ & = & \fst(\Omega(\cons(a,\nil))) \\ & = & \fst(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\zip(\cons(a,\nil))(\tail(\cons(a,\nil)))))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\zip(\cons(a,\nil))(\nil)))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-nil} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \fst(\alpha(\cons(a,\nil))) \\ & = & \fst(\tup(\theta)(\either(\const(\theta))(\lambda)(\last(\cons(a,\nil))))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \theta \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \snd(\tup(\theta)(\theta)) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \snd(\tup(\theta)(\const(\theta)(\ast))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\lft(\ast)))) \\ & = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\last(\nil)))) \\ & = & \snd(\alpha(\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \snd(\foldl(\varphi)(\alpha(\nil))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \snd(\foldl(\varphi)(\alpha(\nil))(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \snd(\foldl(\varphi)(\alpha(\nil))(\rev(\zip(\nil)(\tail(\nil))))) \\ & = & \snd(\Omega(\nil)) \\ & = & \snd(\Omega(x)) \end{eqnarray*}\] For the inductive step, suppose the equality holds for some \(x\). Then we have \[\begin{eqnarray*} & & \fst(\Omega(\cons(a,\cons(b,x)))) \\ & = & \fst(\foldl(\varphi)(\alpha(\cons(a,\cons(b,x))))(\rev(\zip(\cons(a,\cons(b,x)))(\tail(\cons(a,\cons(b,x))))))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\cons(b,x))))(\rev(\zip(\cons(a,\cons(b,x)))(\cons(b,x))))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-cons} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\cons(b,x))))(\rev(\cons(\tup(a)(b),\zip(\cons(b,x))(x))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \fst(\foldl(\varphi)(\alpha(\cons(a,\cons(b,x))))(\snoc(\tup(a)(b),\rev(\zip(\cons(b,x))(x))))) \\ & = & \fst(\foldl(\varphi)(\alpha(\cons(b,x)))(\snoc(\tup(a)(b),\rev(\zip(\cons(b,x))(x))))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-foldl} = & \fst(\varphi(\foldl(\varphi)(\alpha(\cons(b,x)))(\rev(\zip(\cons(b,x))(x))),\tup(a)(b))) \\ & = & \fst(\varphi(\Omega(\cons(b,x)),\tup(a)(b))) \\ & = & \fst(\varphi(\tup(\fst(\Omega(\cons(b,x))))(\snd(\Omega(\cons(b,x)))),\tup(a)(b))) \\ & = & \fst(\tup(\snd(\Omega(\cons(b,x))))(\mu(a,b,\snd(\Omega(\cons(b,x))),\fst(\Omega(\cons(b,x)))))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-fst-tup} = & \snd(\Omega(\cons(b,x))) \end{eqnarray*}\] as claimed.

Maybe we can see where this is going; \(\Omega\) has a (very short) memory, keeping track of two recursive calls so they can be plugged in to \(\mu\). We now define \(\Psi : \lists{A} \rightarrow B\) by \[\Psi(x) = \snd(\Omega(x)).\]

Note that \[\begin{eqnarray*} & & \Psi(\nil) \\ & = & \snd(\Omega(\nil)) \\ & = & \snd(\foldl(\varphi)(\alpha(\nil))(\rev(\zip(\nil)(\tail(\nil))))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-nil-left} = & \snd(\foldl(\varphi)(\alpha(\nil))(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \snd(\foldl(\varphi)(\alpha(\nil))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \snd(\alpha(\nil)) \\ & = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\last(\nil)))) \\ & = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\lft(\ast)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-lft} = & \snd(\tup(\theta)(\const(\theta)(\ast))) \\ & \href{/posts/arithmetic-made-difficult/Functions.html#def-const} = & \snd(\tup(\theta)(\theta)) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \theta \end{eqnarray*}\] and \[\begin{eqnarray*} & & \Psi(\cons(a,\nil)) \\ & = & \snd(\Omega(\cons(a,\nil))) \\ & = & \snd(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\zip(\cons(a,\nil))(\tail(\cons(a,\nil)))))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \snd(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\zip(\cons(a,\nil))(\nil)))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-nil} = & \snd(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\rev(\nil))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-nil} = & \snd(\foldl(\varphi)(\alpha(\cons(a,\nil)))(\nil)) \\ & \href{/posts/arithmetic-made-difficult/LeftFold.html#def-foldl-nil} = & \snd(\alpha(\cons(a,\nil))) \\ & = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\last(\cons(a,\nil))))) \\ & = & \snd(\tup(\theta)(\either(\const(\theta))(\lambda)(\rgt(a)))) \\ & \href{/posts/arithmetic-made-difficult/DisjointUnions.html#def-either-rgt} = & \snd(\tup(\theta)(\lambda(a))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \lambda(a) \end{eqnarray*}\] and \[\begin{eqnarray*} & & \Psi(\cons(a,\cons(b,x))) \\ & = & \snd(\Omega(\cons(a,\cons(b,x)))) \\ & = & \snd(\foldl(\varphi)(\alpha(\cons(a,\cons(b,x))))(\rev(\zip(\cons(a,\cons(b,x)))(\tail(\cons(a,\cons(b,x))))))) \\ & = & \snd(\foldl(\varphi)(\alpha(\cons(b,x)))(\rev(\zip(\cons(a,\cons(b,x)))(\tail(\cons(a,\cons(b,x))))))) \\ & \href{/posts/arithmetic-made-difficult/HeadAndTail.html#thm-tail-cons} = & \snd(\foldl(\varphi)(\alpha(\cons(b,x)))(\rev(\zip(\cons(a,\cons(b,x)))(\cons(b,x))))) \\ & \href{/posts/arithmetic-made-difficult/Zip.html#cor-zip-cons-cons} = & \snd(\foldl(\varphi)(\alpha(\cons(b,x)))(\rev(\cons(\tup(a)(b),\zip(\cons(b,x))(x))))) \\ & \href{/posts/arithmetic-made-difficult/Reverse.html#cor-rev-cons} = & \snd(\foldl(\varphi)(\alpha(\cons(b,x)))(\snoc(\tup(a)(b),\rev(\zip(\cons(b,x))(x))))) \\ & \href{/posts/arithmetic-made-difficult/Snoc.html#thm-snoc-foldl} = & \snd(\varphi(\foldl(\varphi)(\alpha(\cons(b,x)))(\rev(\zip(\cons(b,x))(x))),\tup(a)(b))) \\ & = & \snd(\varphi(\Omega(\cons(b,x)),\tup(a)(b))) \\ & = & \snd(\varphi(\tup(\fst(\Omega(\cons(b,x))))(\snd(\Omega(\cons(b,x)))),\tup(a)(b))) \\ & = & \snd(\varphi(\tup(\snd(\Omega(x)))(\snd(\Omega(\cons(b,x)))),\tup(a)(b))) \\ & = & \snd(\tup(\snd(\Omega(\cons(b,x))))(\mu(a,b,\snd(\Omega(\cons(b,x))),\snd(\Omega(x))))) \\ & \href{/posts/arithmetic-made-difficult/Tuples.html#thm-snd-tup} = & \mu(a,b,\snd(\Omega(\cons(b,x))),\snd(\Omega(x))) \\ & = & \mu(a,b,\snd(\Omega(\cons(b,x))),\Psi(x)) \\ & = & \mu(a,b,\Psi(\cons(b,x)),\Psi(x)) \end{eqnarray*}\] as claimed.

Finally we show that \(\Psi\) is unique with this property. To this end, suppose \(\Gamma : \lists{A} \rightarrow B\) such that \(\Gamma(\nil) = \theta\), \(\Gamma(\cons(a,\nil)) = \lambda(a)\), and \(\Gamma(\cons(a,\cons(b,x))) = \mu(a,b,\Gamma(\cons(b,x)),\Gamma(x))\) for all \(a,b \in A\) and \(x \in \lists{A}\). We show that \(\Gamma(x) = \Psi(x)\) for all \(x\) by strong induction on \(\length(x)\).

For the base case \(\length(x) = \zero\), we have \(x = \nil\). In this case \[\begin{eqnarray*} & & \Gamma(\nil) \\ & = & \theta \\ & = & \Psi(\nil) \end{eqnarray*}\] as needed. For the inductive step, suppose the equality holds for all \(x\) with \(\nleq(\length(x),n)\) and suppose \(\length(x) = \next(n)\). We have two possibilities; if \(n = \zero\), then we have \(x = \cons(a,\nil)\) for some \(a\). Now \[\begin{eqnarray*} & & \Gamma(\cons(a,\nil)) \\ & = & \lambda(a) \\ & = & \Psi(\cons(a,\nil)) \end{eqnarray*}\] as needed. Suppose instead that \(n = \next(m)\); then \(x = \cons(a,\cons(b,z))\) for some \(a,b \in A\) and \(x \in \lists{A}\), where both \(z\) and \(\cons(b,z)\) satisfy the induction hypothesis. Now \[\begin{eqnarray*} & & \Gamma(\cons(a,\cons(b,z))) \\ & = & \mu(a,b,\Gamma(\cons(b,z)),\Gamma(z)) \\ & = & \mu(a,b,\Psi(\cons(b,z)),\Psi(z)) \\ & = & \Psi(\cons(a,\cons(b,z))) \end{eqnarray*}\] as needed.

As usual, \(\lfoldr(\theta)(\lambda)(\mu)\) is the unique solution to a system of equations.

Let \(A\) and \(B\) be sets, with \(\theta \in B\), \(\lambda : A \rightarrow B\), and \(\mu : A \times A \times B \times B \rightarrow B\). Then \(\lfoldr(\theta)(\lambda)(\mu)\) is the unique solution \(f : \lists{A} \rightarrow B\) to the following system of functional equations for all \(a,b \in A\) and \(x \in \lists{A}\): \[\left\{\begin{array}{l} f(\nil) = \theta \\ f(\cons(a,\nil)) = \lambda(a) \\ f(\cons(a,\cons(b,x))) = \mu(a,b,f(\cons(b,x)),f(x)) \end{array}\right.\]

main_lfoldr :: IO ()
main_lfoldr = return ()