[Haskell-cafe] Unfold fusion

[Adrian Neumann]

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))

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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: PGP.sig
Type: application/pgp-signature
Size: 194 bytes
Desc: Signierter Teil der Nachricht
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20090506/7a1a2b79/PGP.bin