On Wednesday 06 May 2009 11:27:08 am 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
If you don't mind a more category theoretic tack, we can argue something like this: Lists of A are the terminal coalgebra for the functor L X = 1 + A*X. Defining them this way means that we get the unique existence of the above unfold function. Roughly, for any: ob : X -> L X there exists a unique: unfold ob : X -> [A] Such that: out . unfold ob = map (unfold ob) . ob where out : [A] -> 1 + A*[A] is the coalgebra action of the list (observing either that it's null, or what the head and tail are), and map corresponds to the functor L (so we're mapping on the X part, not the A part). Coalgebra actions ob have type: ob : X -> 1 + A*X and you can finesse that into three functions in something like Haskell: p : X -> 2, f : X -> A, g : X -> X which is what your unfold at the start does. Now, we have: p' = p . h f' = f . h h . g' = g . h Suppose we combine things back into the single coalgebra actions. Then we have: ob : X -> 1 + A*X ob' : X' -> 1 + A*X' where ob corresponds to (p,f,g) and ob' corresponds to (p',f',g'). Now, the equations above tell us that with regard to these observation functions: ob' agrees with ob . h as far as left or right goes ob' agrees with ob . h as far as As go, when applicable map h . ob' agrees with ob . h as far as Xs go. All together this means: map h . ob' = ob . h Which means it's an L-coalgebra homomorphism. Such homomorphisms are arrows in the category of L-coalgebras, for which [A] is a terminal object (giving us the unique existence property of arrows to it from any other object). So, h : X' -> X is an arrow in the L-coalgebra category. And, so are: unfold ob : X -> [A] unfold ob' : X' -> [A] Since this is a category: unfold ob . h : X' -> [A] must also be an arrow. *However*, [A] being a terminal object means that for every object, there is a unique arrow from it to [A]. We appear to have two from X': unfold ob' : X' -> [A] unfold ob . h : X' -> [A] So the uniqueness property tells us that these are the same arrow. Thus, unfold ob' = unfold ob . h unfold p' f' g' = unfold p f g . h and we're done. Hopefully that wasn't too verbose. Normally you'd have most of that covered by the time you got to proving the unfold fusion, but I wasn't sure how much of that part of the theory you'd read before. Another way you can go is to use coinduction and bisimulation (which can be ultimately explained in terms of the above primitives), which talks about making individual observations, which would go something like: If for all x: null (f x) = null (f' x) (if not null) head (f x) = head (f' x) tail (f x) = tail (f' x) (where equality on the tail is defined as being the same subsequent observations) then f and f' are the same function (by coinduction). If we look at the equations at the start: null . unfold p' f' g' = p' = p . h = null . unfold p f g . h head . unfold p' f' g' = f' = f . h = head . unfold p f g . h tail . unfold p' f' g' = unfold p' f' g' . g' (coinductive hypothesis?) = unfold p f g . h . g' = unfold p f g . g . h = tail . unfold p f g . h unfortunately it looks like I'm doing something wrong in that "coinductive hypothesis" step, by assuming that unfold p' f' g' = unfold p f g . h. However, I'm pretty sure that's how these sorts of coinductive proofs work, though I'm not familiar enough with presenting this angle to explain why you should allow it. Anyhow, if you believe the above, then we've established that all the observations you can make are equal, so our functions must be equal. Note, that it's somewhat important to have these coalgebraic/coinductive proof methods here. Miguel Mitrofanov gave you a proof that: take n . unfold p f g . h = take n . unfold p' f' g' for all n using induction. But, that is not exactly a proof that they are equal, but a proof that any finite amount of observation you can make of their output will be equal, and unfold can produce infinite objects. That may be good enough (for instance, in a total functional programming language extended with coinduction, only the inductive/recursive parts and single-step observation of coinductive values 'ought' to be subject to evaluation, so you can only make finite observations of any corecursively defined value, and the above 'take n' proof in a way covers everything you're able to do), but they feel different, to me at least. Anyhow, I'll stop rambling. Hope that helped some. -- Dan