<div dir="ltr"><span style="font-size:12.8000001907349px">Hello, I'm trying to solve the exercise 4.6.5 of Bird's "Introduction to functional programming using Haskell".</span><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">Let me quote:</span><br style="font-size:12.8000001907349px"><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">"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?"</span><br style="font-size:12.8000001907349px"><br style="font-size:12.8000001907349px"><span style="font-size:12.8000001907349px">So far reasoning by myself and googling a bit I reached to the following scanl definition using foldl (without any assumptions afaik):</span><br style="font-size:12.8000001907349px"><div style="font-size:12.8000001907349px">  Â  scanl f e = foldl (\xs next -> xs ++ [f (last xs) next]) [e]</div><div style="font-size:12.8000001907349px"><br>Furthermore, previously on the same chapter, it says that:<br>  Â  scanl f e = foldr g [e] where g x xs = e : map (f x) xs<br><br>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.<br>The induction proof I wrote is the following:<br><br><div>scanl f e = foldr g [e] </div><div>  Â  where g y ys = e : map (f y) ys</div><div>By the principle of extensionality, this is equivalent to:</div><div>  Â  scanl f e xs = foldr g [e] xs</div><div>  Â  Â  Â  where g y ys = e : map (f y) ys<br><br></div><div>We prove this equality by induction on xs.</div><div>Case([]). For the left-hand side we reason</div><div>  Â  Â  Â  scanl f e []</div><div>  Â  = {scanl.1}</div><div>  Â  Â  Â  [e]</div><div><br></div><div>  Â  Â  Â  For the right-hand side</div><div>  Â  Â  Â  foldr g [e] []</div><div>  Â  = {foldr.1}</div><div>  Â  Â  Â  [e]</div><div><br></div><div>Case(x:xs). For the left-hand side we reason</div><div>  Â  Â  Â  scanl f e (x:xs)</div><div>  Â  = {scanl.2}</div><div>  Â  Â  Â  e : scanl f (f e x) xs</div><div>  Â  = {f has unit e}</div><div>  Â  Â  Â  e : scanl f x xs</div><div>  Â  = {induction hypothesis}</div><div>  Â  Â  Â  e : foldr g [x] xs</div><div><br></div><div>  Â  Â  Â  For the right-hand side</div><div>  Â  Â  Â  foldr g [e] (x:xs)</div><div>  Â  = {foldr.2}</div><div>  Â  Â  Â  g x (foldr g [e] xs)</div><div>  Â  = {definition of g}</div><div>  Â  Â  Â  e : map (f x) (foldr g [e] xs)</div><div>  Â  = {definition of map}</div><div>  Â  Â  Â  e : foldr ((:) . (f x)) [] (foldr g [e] xs)</div></div><div style="font-size:12.8000001907349px"><br><br>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).<br>Anyway, any help or pointer that can lead me in the right direction is very much appreciated.<br><br>Thanks in advance.</div></div>