Re: [Haskell-cafe] Proof of duality theorem of fold?
I believe R J was consciously restricting himself to finite lists in the original post. 2009/3/18 MigMit miguelim...@yandex.ru 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 ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] 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___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof of duality theorem of fold?
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.
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Proof of duality theorem of fold?
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
Re: [Haskell-cafe] Proof of duality theorem of fold?
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
Re: [Haskell-cafe] Proof of duality theorem of fold?
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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
