= Solution
Take compatible <function types> `f :: b -> c`, `g :: b -> a -> b`, and `h :: c -> a -> c`. The necessary conditions obtained from the two <induction base cases> are \b[strictness of `f` and the fusion equation]
$$
f(\bot)=\bot,\qquad f(g\ x\ y)=h\ (f\ x)\ y\quad\text{for all }x,y.
$$
At `zs = []`, the desired equation is exactly the displayed fusion equation. At `zs = undefined`, both <left folds> diverge because their <list> argument has no outer constructor; the equation therefore requires `f undefined = undefined`. This is the <strict function> condition. If only finite total spines were considered, the first condition would not be necessary.
These conditions also support the step. The <induction hypothesis> must hold for \i[every] accumulator and element. For `z:zs`, instantiate that hypothesis at `g x y` and `z`:
``
f (foldl g (g x y) (z:zs))
= f (foldl g (g (g x y) z) zs)
= foldl h (h (f (g x y)) z) zs
= foldl h (h (h (f x) y) z) zs
= foldl h (h (f x) y) (z:zs).
``
The middle rewrite uses the fusion equation at `x,y`. For pure <computable functions>, equality on infinite spines follows from finite approximations as in part (a).
Back to article page
