[Haskell-cafe] Proof of duality theorem of fold?
R J
rj248842 at hotmail.com
Wed Mar 18 07:57:06 EDT 2009
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))
Right-side reduction:
foldl (flip f) e (reverse (x : xs))
= {second equation of "reverse"}
foldl (flip f) e (reverse xs ++ [x])
_________________________________________________________________
Hotmail® is up to 70% faster. Now good news travels really fast.
http://windowslive.com/online/hotmail?ocid=TXT_TAGLM_WL_HM_70faster_032009
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.haskell.org/pipermail/haskell-cafe/attachments/20090318/a5770695/attachment.htm
More information about the Haskell-Cafe
mailing list