= Solution
Again use <structural induction> on the finite <list>. At `[]`, both the <right fold> and the <left fold> return the seed $a$. If they agree on `zs`, then
$$
\begin{aligned}
\operatorname{foldr}(\oplus)\,a\,(z:\mathrm{zs})
&=z\oplus\operatorname{foldr}(\oplus)\,a\,\mathrm{zs}\\
&=z\oplus\operatorname{foldl}(\otimes)\,a\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,(z\oplus a)\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,(a\otimes z)\,\mathrm{zs}\\
&=\operatorname{foldl}(\otimes)\,a\,(z:\mathrm{zs}).
\end{aligned}
$$
The third line uses part (a); the fourth uses equation (2). Thus the <left-right fold equivalence> is
$$
\boxed{\operatorname{foldr}(\oplus)\,a\,\mathrm{xs}=\operatorname{foldl}(\otimes)\,a\,\mathrm{xs}.}
$$
This is a statement about values on finite, total inputs. It does not assert equal evaluation costs or equal behaviour on infinite <lists>.
Back to article page
