Dan Doel dan.doel at gmail.com
Wed May 6 16:26:15 EDT 2009

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