[Haskell-cafe] Proof of duality theorem of fold?
Daniel Fischer
daniel.is.fischer at web.de
Wed Mar 18 08:10:05 EDT 2009
Am Mittwoch, 18. März 2009 12:57 schrieb R J:
> I'm trying to prove the following duality theorem of fold for finite lists:
>
> foldr f e xs = foldl (flip f) e (reverse xs)
>
> where
>
> reverse :: [a] -> [a]
>
> reverse [] = []
>
> reverse (x:xs) = reverse xs ++ [x]
>
> flip :: (a -> b -> c) -> b -> a -> c
> flip f y x = f x y
>
> foldr :: (a -> b -> b) -> b -> [a] -> b
> foldr f e [] = e
> foldr f e (x : xs) = f x (foldr f e xs)
>
> foldl :: (b -> a -> b) -> b -> [a] -> b
> foldl f e [] = e
> foldl f e (x : xs) = foldl f (f e x) xs
>
>
> I'm stuck on the induction case. Can someone help? Here's what I've got
> so far:
>
> Proof:
>
> Case _|_.
>
> Left-side reduction:
>
> foldr f e _|_
> = {case exhaustion of "foldr"}
> _|_
>
> Right-side reduction:
>
> foldl (flip f) e (reverse _|_)
> = {case exhaustion of "reverse"}
> foldl (flip f) e _|_
> = {case exhaustion of "foldl"}
> _|_
>
> Case [].
>
> Left-side reduction:
>
> foldr f e []
> = {first equation of "foldr"}
> e
>
> Right-side reduction:
>
> foldl (flip f) e (reverse [])
> = {first equation of "reverse"}
> foldl (flip f) e []
> = {first equation of "foldl"}
> e
>
> Case (x : xs).
>
> Left-side reduction:
>
> foldr f e (x : xs)
> = {second equation of "foldr"}
> f x (foldr f e xs)
> = {induction hypothesis: foldr f e xs = foldl (flip f) e (reverse
> xs)} f x (foldl (flip f) e (reverse xs))
= (flip f) (foldl (flip f) e (reverse xs)) x
>
> Right-side reduction:
>
> foldl (flip f) e (reverse (x : xs))
> = {second equation of "reverse"}
> foldl (flip f) e (reverse xs ++ [x])
Now prove the
Lemma:
foldl g e (ys ++ zs) = foldl g (foldl g e ys) zs
for all g, e, ys and zs of interest.
(I don't see immediately under which conditions this identity could break,
maybe there aren't any)
Then the last line of the right hand side reduction can be rewritten as the
new last of the left.
More information about the Haskell-Cafe
mailing list