# Lookback Fold

Posted on 2018-07-17 by nbloomf

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 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)$$.

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 ()