"Fix-Point Fusion", a seemingly minor consequence of Fix-Point Induction, remained long in obscurity. Its greatest claim to fame before 1991 was it's use by Joseph Stoy, in "Denotational Semantics" to demonstrate three inductive methods of proof. But this all began to change with the infamous Banana paper ("Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire") where Meijer et al not only gave this theorem its name but used it to prove their fusion (deforestation) laws for catamorphisms, anamorphisms, and paramorphisms. And yet is this theorem to be left to languish in the relative obscurity of Squiggol? I hope not.
In this talk I will show that Fix-Point Fusion is an extremely practical law for transforming functional programs. And I hope to give you an intuitive handle for it, along the way showing how Fix-Point Fusion embodies the essence of Scherlis's expression procedure methodology of program transformation.
In addition I will show why certain desirable program transformations (e.g., deriving Knuth-Morris-Pratt pattern matching from a naive pattern matcher) are just not doable with Fix-Point Fusion, unfold/fold, and expression procedure based transformation methods; and thus are not doable by partial evaluation and deforestation. I then show how these transformations can be achieved by extending our language with assertions.