[Haskell-cafe] Proof that scanl can be written as foldr?

Cristian Ontivero contiver at itba.edu.ar
Sat Jan 3 17:59:15 UTC 2015

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}

        For the right-hand side
        foldr g [e] []
    = {foldr.1}

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>

More information about the Haskell-Cafe mailing list