Theorems and Proofs


--------------------------------------------------------------------------
-- Definitions
--------------------------------------------------------------------------

   hylo c d = c.map (hylo c d).d                                    {Hylo}

   fold f a = f.map (fold f a).des a                                {Fold}
 unfold f a = con a.map (unfold f a).f                            {Unfold}
 
trans f a b = con b.f.map (trans f a b).des a                      {Trans}
transit a b = con b.map (transit a b).des a                      {Transit}
            = trans id
            

--------------------------------------------------------------------------
-- (1) Relating trans <--> fold/unfold <--> hylo 
--------------------------------------------------------------------------

      fold f a  =   hylo f (des a)                              {FoldHylo}
    unfold f a  =   hylo (con a) f                            {UnfoldHylo}
fold (con b) a  = unfold (des a) b                            {FoldUnfold}

trans f a b =   hylo (con b.f) (des a)                         {TransHylo}
trans f a b =   fold (con b.f) a                               {TransFold}
trans f a b = unfold (des a) (ADT (con b.f) (des b))         {TransUnfold}

transit a b =   hylo (con b) (des a)                         {TransitHylo}
transit a b =   fold (con b) a                               {TransitFold}
transit a b = unfold (des a) b                             {TransitUnfold}


PROOF: <immediate by unfolding both sides>


--------------------------------------------------------------------------
-- (2) Free Theorems for hylo and fold/unfold
--------------------------------------------------------------------------

Assumptions:

  g is a functor
  c,c',f :: g u -> u  
  d,d',e :: t -> g t
  a  = ADT c  d
  a' = ADT c' d'

                                                                {FreeHylo}
l.c = c'.map l  &&  d'.r = map r.d  ==>    l.hylo c d =   hylo c' d'.r

                                                                {FreeFold}
l.f = f'.map l  &&  d'.r = map r.d  ==>    l.fold f a =   fold f' a'.r
l.c = c'.map l  &&  e'.r = map r.e  ==>  l.unfold e a = unfold e' a'.r
                                                              {FreeUnfold}


--------------------------------------------------------------------------
-- (3) Fusion laws for fold/unfold and hylo
--------------------------------------------------------------------------

l.f = f'.map l  ==>  l.fold f a =   fold f' a                 {FoldFusion}
e'.r = map r.e  ==>  unfold e a = unfold e' a.r             {UnfoldFusion}


PROOF:

Both laws follow from the Free Theorem for fold/unfold. Let a' = a.
For FoldFusion, let r = id. 
  It follows that d'.r = d' = d = map r.d. 
  Therefore, we can apply the Free Theorem, and since r=id and a'=a,
  we directly obtain the FoldFusion equation.
For UnfoldFusion, let l = id.
  It follows that l.c = c = c' = c'.map l.
  Therefore, we can apply the Free Theorem, and since l=id and a'=a,
  we directly obtain the UnfoldFusion equation.

With the same line of reasoning, we can obtain two special versions for 
Hylo fusion from the left (let r=id and d'=d) and right (l=id and c'=c).
                                           

l.c = c'.map l  ==>  l.hylo c d = hylo c' d                     {HyloLeft}
d'.r = map r.d  ==>    hylo c d = hylo c d'.r                  {HyloRight}


From either law we can instantiate the classical hylo fusion law. Eg, let
l=hylo a b and c'=a. 
The precondition of {HyloLeft} becomes :     hylo a b.c = a.map (hylo a b) 
which unrolls to:                  a.map (hylo a b).b.c = a.map (hylo a b)
We see that both sides are equal if b.c = id. Thus we get:


b.c = id  ==>  hylo a b.hylo c d = hylo a d                   {HyloFusion}


Similarly, we can instantiate {FoldFusion} with l=fold g b and f'=g.
The precondition expands to:                 fold g b.f = g.map (fold g b)
which is:                      g.map (fold g b).des b.f = g.map (fold g b)
We see that both sides are equal if des b.f = id. We can obtain the same
result from {HyloFusion}. Therefore, rewrite the equation by expressing
fold g b and fold f a as hylomorphisms: 
  hylo g (des b).hylo f (des a) = hylo g (des a)
and simply match it against {HyloFusion}. This gives the condition
des b.f = id immediately.

We can also specialize {UnfoldFusion} by setting r=unfold f b and e'=f.
{UnfoldFusion} yields:           unfold e a.unfold f b     = unfold f a 
with hylomorphisms:          hylo (con a) e.hylo (con b) f = hylo (con a) f
From {HyloFusion} we then take the necessary precondition: e.con b = id.             
Thus we have:


des b.f = id    ==>      fold g b.fold f a =   fold g a      {FoldFusion'}
e.con b = id    ==>  unfold e a.unfold f b = unfold f a    {UnfoldFusion'}



TO BE EXPANDED ...