= Fold factorisation criterion
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.
Back to article page
