Prove the stronger equation, quantified over the accumulator:For 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.
[], 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:f (foldl g a (x:xs))
= f (foldl g (g a x) xs)
= foldl h (f (g a x)) xs
= foldl h (h (f a) x) xs
= foldl h (f a) (x:xs). Articles by others on the same topic
There are currently no matching articles.