= Natural-number fold fusion law
{title2=$f\circ\operatorname{foldNat}(g,a)=\operatorname{foldNat}(h,b)$}
Suppose $f$ is a <strict function>, $f(a)=b$ and $f\circ g=h\circ f$. The zero case of the asserted equation is the base identity; the successor case rewrites $f(g(z))$ as $h(f(z))$ and applies <structural induction>. At an undefined argument, the <strict function> premise makes both sides the <bottom value>. For pure definable <Haskell> functions, equality on finite partial approximations extends to infinite constructor chains by continuity in the information order. For finite total arguments alone, the zero and successor proof does not require strictness.
Back to article page
