[Haskell-cafe] Unfold fusion
Miguel Mitrofanov
miguelimo38 at yandex.ru
Wed May 6 12:06:02 EDT 2009
On 6 May 2009, at 19:27, Adrian Neumann wrote:
> Hello,
>
> I'm trying to prove the unfold fusion law, as given in the chapter
> "Origami Programming" in "The Fun of Programming". unfold is defined
> like this:
>
> unfold p f g b = if p b then [] else (f b):unfold p f g (g b)
>
> And the law states:
>
> unfold p f g . h = unfold p' f' g'
> with
> p' = p.h
> f' = f.h
> h.g' = g.h
>
> Foremost I don't really see why one would want to fuse h into the
> unfold. h is executed once, at the beginning and is never needed
> again. Can someone give me an example?
>
> So, this is what I got so far:
>
> unfold p f g.h = (\b -> if p b then [] else (f b): unfold p f g (g
> b).h
> = if p (h b) then [] else (f (h b)) : unfold p f g (g (h b))
> = if p' b then [] else f' b: unfold p f g (h (g' b))
= if p' b then [] else f' b : (unfold p f g . h) g' b
= if p' b then [] else f' b : unfold p' f' g' (g' b) -- NB!
= unfoldr p' f' g' b
This "proof" is actually biting itself on the tail; however, you can
make it work, for example, like this:
(A_n) take n ((unfold p f g . h) b) = take n (unfold p' f' g' b)
Now, A_0 is obvious (take 0 whatever = []), and A_n follows from
A_{n-1} by the previous argument. By induction, A_n holds for all n.
More information about the Haskell-Cafe
mailing list