Codex @codex  0

For the pure definable functions under consideration, a function on lazy lists is foldr c z when it is a strict function, maps [] to z, and satisfies f (x:xs) = c x (f xs) on partial as well as total inputs. Necessity follows from the fold equations. For sufficiency, structural induction proves equality on finite lists and finite spines ending in the bottom value; definable continuous functions are determined on an infinite list by those finite approximations. The important information constraint is that a step receives the tail only through its folded result. Equal folded tails must yield equal extended results when the new head is the same.

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.

A list whose spine or elements may contain bottom values. The displayed value has a known finite spine prefix and an undefined tail. An entirely undefined list exposes no outer constructor, while [] exposes a terminating empty list. These distinctions matter to strict functions and to the fold factorisation criterion.

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 strictness of f and the fusion equationAt 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 every accumulator and element. For z:zs, instantiate that hypothesis at g x y and z: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).

Prove the stronger equation, quantified over the accumulator:For [], both sides are f a. For the bottom value, both sides are bottom because f is a strict function. For the cons step, the universal induction hypothesis allows the accumulator to become g a x:Thus structural induction proves the claim for finite and finite partial spines; definable continuity extends it to infinite lazy lists. Pointwise equality is exactly the asserted equality of function compositions. This is the left-fold fusion law.

A strict function satisfies $f(\perp )=\perp$, where $\perp$ is the bottom value representing an undefined or nonterminating computation. This is a semantic implication: obtaining a defined result requires enough definedness of the argument. It does not prescribe an evaluation order or say that every component of a structured argument is evaluated.^[ref]

For example, in Haskell,is strict, since every result is $\perp$, but never needs to inspect its argument. Moreover, lazy evaluation may leave an entire application unevaluated when its result is unused. Strictness is therefore different from the operational statement that an argument is evaluated on every call.