Hello, I'm trying to solve the exercise 4.6.5 of Bird's "Introduction to
functional programming using Haskell".
Let me quote:
"Prove that scanl f e can be written as a foldr, if f is associative with
unit e. Can scanl f e be written as a foldl without any assumptions on f
and e?"
So far reasoning by myself and googling a bit I reached to the following
scanl definition using foldl (without any assumptions afaik):
scanl f e = foldl (\xs next -> xs ++ [f (last xs) next]) [e]
Furthermore, previously on the same chapter, it says that:
scanl f e = foldr g [e] where g x xs = e : map (f x) xs
Using this definition, I tried proving it by induction, but since I got
stuck, I tried seeing if I could find some way to use the first duality
theorem (with the foldl definition), or fusion, but to no avail.
The induction proof I wrote is the following:
scanl f e = foldr g [e]
where g y ys = e : map (f y) ys
By the principle of extensionality, this is equivalent to:
scanl f e xs = foldr g [e] xs
where g y ys = e : map (f y) ys
We prove this equality by induction on xs.
Case([]). For the left-hand side we reason
scanl f e []
= {scanl.1}
[e]
For the right-hand side
foldr g [e] []
= {foldr.1}
[e]
Case(x:xs). For the left-hand side we reason
scanl f e (x:xs)
= {scanl.2}
e : scanl f (f e x) xs
= {f has unit e}
e : scanl f x xs
= {induction hypothesis}
e : foldr g [x] xs
For the right-hand side
foldr g [e] (x:xs)
= {foldr.2}
g x (foldr g [e] xs)
= {definition of g}
e : map (f x) (foldr g [e] xs)
= {definition of map}
e : foldr ((:) . (f x)) [] (foldr g [e] xs)
I'm not even sure the last step is useful, but I thought maybe I could
combine both foldrs into a single one (that's why I thought about the
fusion law).
Anyway, any help or pointer that can lead me in the right direction is very
much appreciated.
Thanks in advance.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20150103/1d016e84/attachment.html>