Proof of duality theorem of fold?
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
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.
Am Mittwoch, 18. März 2009 13:10 schrieb Daniel Fischer:
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)
Of course, hit send and you immediately think of foldl (flip const) whatever (undefined ++ [1,2,3])
More interesting: foldl (flip const) whatever (repeat 1 ++ [1,2,3]) Daniel Fischer wrote on 18.03.2009 15:17:
Am Mittwoch, 18. März 2009 13:10 schrieb Daniel Fischer:
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)
Of course, hit send and you immediately think of
foldl (flip const) whatever (undefined ++ [1,2,3]) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
I believe R J was consciously restricting himself to finite lists in the
original post.
2009/3/18 MigMit
More interesting:
foldl (flip const) whatever (repeat 1 ++ [1,2,3])
Daniel Fischer wrote on 18.03.2009 15:17:
Am Mittwoch, 18. März 2009 13:10 schrieb Daniel Fischer:
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)
Of course, hit send and you immediately think of
foldl (flip const) whatever (undefined ++ [1,2,3]) _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
_______________________________________________
Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
participants (4)
-
Daniel Fischer -
Edward Kmett -
MigMit -
R J