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 The middle rewrite uses the fusion equation at
z:zs, instantiate that hypothesis at g x y and z:f (foldl g (g x y) (z:zs))
= f (foldl g (g (g x y) z) zs)
= foldl h (h (f (g x y)) z) zs
= foldl h (h (h (f x) y) z) zs
= foldl h (h (f x) y) (z:zs).x,y. For pure computable functions, equality on infinite spines follows from finite approximations as in part (a). Articles by others on the same topic
There are currently no matching articles.