List fold (foldr :: (a -> b -> b) -> b -> [a] -> b)

The structural recursion that replaces an empty list by a chosen value and a cons constructor by a combining function applied to the head and folded tail. A direct list fold is strict in the list spine at its outermost constructor, even when the combining function does not demand the folded tail. Its algebraic recognition rule is the fold factorisation criterion.

Splitting a list into its longest initially accepted list prefix and the remaining list suffix. On finite total lists with terminating predicate tests, the pair is a direct right fold: the true branch prepends to the first component; the false branch reconstructs the original tail by concatenating the two tail components and puts the current head before it. The richer pair result retains information that a direct dropped-list suffix list fold loses. Conventional recursive span is strict in the input spine; a literal pair of its two projections can expose an outer pair even on bottom, so partial-value equations require care.

Suppose a predicate accepts some $u$ and rejects some $v$. Dropping its initial accepted list prefix maps both the empty list and the singleton $u$ to the empty list, but maps the extensions by $v$ to different lists. A direct list fold cannot do this: its combining function receives the same head and the same folded-tail summary in both cases. This is an instance of the fold factorisation criterion. An auxiliary list fold retaining more information followed by projection is not ruled out.

If $f$ is strict, $f(a)=b$, and $f(g(x,y))=h(x,f(y))$, then $f\circ \mathrm{foldr}(g,a)=\mathrm{foldr}(h,b)$. The empty case uses the base image and the cons case uses compatibility followed by structural induction. Strictness handles a bottom-valued spine. For pure definable continuous functions, equality on finite partial lists extends to infinite lists by finite approximation. For finite total inputs alone, induction does not require the strictness hypothesis.