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: -------------------------------------------------------------------------- -- (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 ...