= Solution
The <list fold> criterion is: there must be a value `z` and a definable combining function `c` such that
$$
f(\bot)=\bot,\qquad f([])=z,\qquad f(x:xs)=c\ x\ (f\ xs).
$$
The last equality says that all information needed about the tail factors through `f xs`; the combining function receives no other access to `xs`. These conditions give \b[`f = foldr c z`].
Necessity follows from the defining equations of `foldr`, including its case distinction on the input <list>. Sufficiency follows by <structural induction> for finite lists and finite partial-list approximations. For infinite or partial <lazy lists>, the usual continuous semantics of these definable functions extends equality from the approximations to their limit. The strictness condition matters: agreement only on finite total lists does not establish agreement at $\bot$. This is the <fold factorisation criterion>.
Back to article page
