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)
Better make that skeleton-defined finite lists: Prelude> foldr (++) [] ("this":" goes":" so":" far":undefined) "this goes so far*** Exception: Prelude.undefined Prelude> foldl (flip (++)) [] (reverse ("this":" goes":" so":" far":undefined)) "*** Exception: Prelude.undefined
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