= Left-fold fusion law
{title2=$f\circ\operatorname{foldl}(g,a)=\operatorname{foldl}(h,f(a))$}
If $f$ is a <strict function> and $f(g(a,x))=h(f(a),x)$ for every $a,x$, then `f (foldl g a xs) = foldl h (f a) xs`. Prove the equation simultaneously for all accumulators by <structural induction> on the <list>. The empty case is immediate; at a cons, apply the hypothesis with accumulator `g a x` and then rewrite its image using the assumed equation. At the <bottom value>, strictness supplies the required equality. For pure definable <functions>, equality on finite <partial lists> extends to infinite <lazy lists> by finite approximations. For finite terminating spines alone, strictness is unnecessary.
Back to article page
