[Haskell-cafe] Unfold fusion
Martin Huschenbett
huschi at gmx.org
Wed May 6 11:48:58 EDT 2009
Adrian Neumann schrieb:
> 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?
Maybe you should read the euqation from the other direction. Then the h
becomes "fused out" and is called only once instead of many times. But
you can only do this if you can factor out h from p', f' and g'.
> 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))
>
> not very much. I kinda see why it works after I "unfold" some more, but
> I can't really prove it. I suspect I need some technique I haven't
> learned yet. I've heard about fixpoint induction, that looks promising,
> but Google knows very little about it.
>
> I hope somebody can give me some hints.
>
> Regards,
>
> Adrian
Regards,
Martin.
> ------------------------------------------------------------------------
>
> _______________________________________________
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
> http://www.haskell.org/mailman/listinfo/haskell-cafe
More information about the Haskell-Cafe
mailing list