[Haskell-cafe] Proof of duality theorem of fold?
Daniel Fischer
daniel.is.fischer at web.de
Wed Mar 18 09:38:34 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)
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
More information about the Haskell-Cafe
mailing list