数理解析研究所講究録
918 巻 1995 年 253-267

253

Shortcut Deforestation in Calculational Form*

Erik Meijer
Utrecht University
3508 TB Utrecht
The Netherlands
erik@cs.ruu.nl

Akihiko Takano
Hitachi Advanced Research Lab
Hatoyama, Saitama 350-03
Japantakano@harl.hitachi.co.jp

Abstract
In functional programming, intermediate data structures are often used to “glue’) together
small programs. Deforestation is a program transformation to remove these intermediate
data structures automatically. We present a simple algorithm for deforestation based on two
fusion rules for hylomorphism, an expressive recursion pattern. A generic notation for hylomorphisms is introduced, where natural transformations are explicitly factored out, and it
is used to represent programs. Our method successfully eliminates intermediate data structures of any algebraic type from a much larger class of compositional functional programs
than previous techniques.

1

Introduction

In functional programming, programs are often constructed by “gluing” together small components, using intermediate data structures to convey information between them. Such data areconstructed in one component and later consumed in another component, but never appear in
the result of the whole program. The compositional style of programming has many advantagesof clarity and higher level of modularity, but these intermediate data structures give rise to an

efficiency problem.
Inspired by Turchin’s early work on the supercompiler [TNT82, Tur86], Wadler [Wad88]
introduced the idea of deforestation to tackle this problem. His algorithm for deforestation eliminates arbitrary tree-like intermediate data structures (including lists) when applied to treeless, but still
programs. There have been various attempts to extend his method
major drawbacks remain. All these algorithms basically have to keep track of all function calls
occurred previously, and suitably introduce a definition of recursive function on detecting a. The processrepetition. This corresponds to the fold step of Burstall and Darlington
of keeping track of function calls and the clever control to avoid infinite unfolding introduces
substantial cost and complexity in algorithms, which prevent deforestation to be adopted aspart of the regular optimizations in any serious compilers of functional languages.
$([\mathrm{C}\mathrm{h}\mathrm{i}92, \mathrm{S}\emptyset \mathrm{r}94])$$([\mathrm{B}\mathrm{D}77])$

Recently two new approaches to deforestation have been proposed [GLPJ93, SF93]. Both ofthem pick up the function fold as a useful template to capture the structure of programs, andapply transformations only to programs written in terms of the fold function. Both techniques
do not require any global analysis to guarantee termination and the applicability of their rules oftransformation can be checked locally. Because their theoretical basis can be found in the study*Earlier version of this paper was presented at$\mathrm{F}\mathrm{P}\mathrm{C}\mathrm{A}’ 95$

.

254

on Constructive Algorithmics1 ([Mee86, MFP91, Mee92, Mei92, Fok92, Jeu93]), we baptise themas deforestation in calculational form.
Although the method in [GLPJ93] is limited to the specific data structure of lists, it was
shown clearly that this calculation-based deforestation is more practical than the original style
deforestation and its extensions. By using theas the basis to standardize thestructure offunctions of lists, their transformation is the repetitive applications of the single rule of cancellation for a pair of foldr and build. Each application of therule can be seen as a canned application ofin the traditional deforestation.
In [GLPJ93] the rule and its correctness proof are given only in the specific context of lists, andthe extension to the other data structures is simply suggested. Once embedded in the proper
theoretical framework it becomes clear how to generalize their method to other data structures.
Sheard and Fegaras [SF93] demonstrated that folding can be defined for many algebraic types
definable in languages like ML (i.e. mutually recursive sum-of-product types). Their normalization algorithm automatically calculates a potentially normalizable fold program (analogous to atreeless program) into its canonical form. The algorithm is essentially based on the so-called fusion theorem, and repetitively replaces the nested application of two fold functions with one fold.
They also gave definitions of other recursive forms such as generalized unfolds (derive function)and primitive recursion together with their corresponding fusion theorems. The normalization
algorithms for these recursive patterns were not given.
$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}\mathrm{r}/\mathrm{b}\mathrm{u}\mathrm{i}\mathrm{l}\mathrm{d}$$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{u}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{g}/\mathrm{p}\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{c}\mathrm{i}\mathrm{n}\mathrm{g}$$\mathrm{u}\mathrm{n}\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}/\mathrm{s}\mathrm{i}\mathrm{m}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{f}\mathrm{y}/\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}$In this paper we show that a single transformation rule (and its dual), the Acid Rain Theorem[Mei94], elegantly generalizes theto any algebraic data types. We introduce a
generic notation for hylomorphisms, which generalizes both folds and unfolds and use it torepresent the structure of programs. We show the acid rain theorem can be stated as thefusion rules for hylomorphisms with no side condition. Based on these rules, we introduce a
new deforestation algorithm to eliminate intermediate data structures of any algebraic typefrom much larger class of compositional functional programs than the deforestation algorithms
above.
$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}\mathrm{r}/\mathrm{b}\mathrm{u}\mathrm{i}\mathrm{l}\mathrm{d}$.

The contribution of this paper is as follows:.

Our technique is applicable to any functional program in compositional style, and removes
intermediate data of any algebraic type. We propose a generic notation for hylomorphisms
to explicitly factor out the natural transformation, and the structure of the program isrepresented using this notation. Our new representation facilitates us to state the acidrain theorem and the rules of transformation in uniform way.
Our technique is a direct generalization of [GLPJ93]. Thanks to the categorical characterization of data types, the theorem naturally covers the dual of thetheorem. Our optimization is based on two simple local transformations: the generalization ofcancellation rule and the dual of it. The technique is also cheap andpractical to implement in real compilers.
$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}\mathrm{r}/\mathrm{b}\mathrm{u}\mathrm{i}\mathrm{l}\mathrm{d}$$\mathrm{f}\mathrm{o}\mathrm{l}\mathrm{d}/\mathrm{b}\mathrm{u}\mathrm{i}\mathrm{l}\mathrm{d}$.
.

Our method is more powerful than the method in [GLPJ93] even when restricted to thelist data structure. Typically, the function zip, which could not be deforested in bothparameters by their method, is not an exception any more. Our method successfully
deforests zip in both of its parameters (Section 4.5).
Our method also generalizes the result of [SF93] by adopting hylomorphism as the basic
form to represent programs. Because fold (catamorphism) and unfold (dual of catamorphism) are instances of hylomorphism, our method does not only work on fold programs

1For more info check out the WWW page http:$//\mathrm{W}\mathrm{W}.\mathrm{C}\mathrm{S}$. utwente.

$\mathrm{n}1/\sim \mathrm{f}\mathrm{o}\mathrm{k}\mathrm{k}\mathrm{i}\mathrm{n}\mathrm{g}\mathrm{a}/\mathrm{a}\mathrm{l}\mathrm{g}\mathrm{o}\mathrm{r}\mathrm{i}\mathrm{t}\mathrm{h}\mathrm{m}\mathrm{i}_{\mathrm{C}}\mathrm{s}$. html255

but also on the programs built up from fold and its dual. Our technique can also be
extended to work on primitive recursion.
This paper is organized as follows. In section 2 we review the previous work in program
calculation which is the theoretical base of our method. In section 3 we introduce a triplet
notation for hylomorphisms and the fusion rules for them, which are the key rules of our method.
In section 4 our transformation algorithm is defined and applied to some examples. In section
5 we discuss related work.

2

Program Calculation, Mei92,
In this section we briefly review the previous work on constructive algorithmics ([Fok92, Mei94]) and explain some basic facts which provides the theoretical basis of our deforestation algorithm. In this paper our default category for types is $CPO$ , the category of complete
partial orders with continuous functions. This choice facilitates us to handle arbitrary recursive
equations in the framework close to lazy functional programming languages.
$\mathrm{M}\mathrm{F}\mathrm{P}91$

$C$

2.1

Functors

Endofunctors on (functors from to ) capture the signature of (algebraic) data types. In
this paper we assume that all data types are defined by functors whose operation on functions
all functors defined using basic functors below and type functors (mapare continuous. In
The definition of type functors is given in section 2.3. Basicsatisfy
thiscondition.
functors)$id$functors we assume are (identity), (constants), (product),sum). We give the definitions of product and separated sum functors and related combinators.
$C$

$C$

$C$

$C’\mathcal{P}O$$A_{\perp}(\mathrm{s}\mathrm{t}\mathrm{r}\mathrm{i}_{\mathrm{C}}\mathrm{t}\mathrm{i}\mathrm{f}\mathrm{y})\mathrm{a}\mathrm{n}\mathrm{d}+(\mathrm{s}\mathrm{e}\mathrm{p}\mathrm{a}\mathrm{r}\mathrm{a}\mathrm{t}\mathrm{e}\mathrm{d}$$\cross$$\underline{A}$Definition 2.1 The product $A\cross B$ of two types
defined as:

$A$

and

$A\cross B$$=$$\{(a, b)|a\in A, b\in B\}$$(f_{\mathrm{X}g})(a, b)$$=$( a, $gb$ )$f$

The following combinators ($lefl/right$ projections and split$f\cross g=(f\mathrm{o}exl)_{\Delta}(g^{0}exr)$$exl(a, b)$

$=$

$a$

$exr(a, b)$

$=$

$b$

$(f_{\Delta}g)a$$=$characterizes their

( a,
$f$

$g$

$\Delta$) are related to the product functor:a). The standard notation for$relati_{\mathit{0}}n\approx$

category theory $is<f,$ $g>$ .

Definition 2.2 The separated sum $A+B$ of two types
are defined as:

$A$

and

$B$

$=$

$(\{0\}\cross A\cup\{1\}\cross B)_{\perp}$$(f+g)1$$=$$\perp$$=$$(0, fa)$$=$$(1, gb)$

The following combinators ($lefl/right$ injections and junc

a
inrb

$=$

$(0, a)$$=$$(1,b)$$(f\nabla g)\perp$$=$$\perp$$(f\nabla g)(\mathrm{o}, a)$

$=$

$fa$

$(f\nabla g)(1,b)$

$=$

$gb$

$\dot{i}nl$$\nabla$$f_{\Delta}g$inand its operation to functions$A+B$$(f+g)(0, a)$$(f+g)(1, b)$functor:and its operation to functions are$B$) are related to the separated sum256$f+g=(inl\mathrm{o}f)\nabla(inr\mathrm{o}g)$category theory is $[f,g]$ .

2.2characterizes their relation. The standard notation for$f\nabla g$inData Types as Initial Fixed Points of Functors

Let
be an endofunctor on . An -algebra is a strict function of type. The setis called the carrier of the algebra. Dually, an-algebra is a (not necessarily strict)function of type
. An -homomorphism : $Aarrow B$ from -algebra:to:is a function which satisfies. We use a concise notation :to represent this property. Category
is the category whose objects are -algebras andwhose morphisms are -homomorphisms. Dually,is the category of
with
.
$C$

$\mathrm{F}$$\mathrm{F}Aarrow A$$\mathrm{F}$$A$$\mathrm{F}_{-CO}$$Aarrow \mathrm{F}A$$h$$\mathrm{F}$$\mathrm{F}Aarrow A$$\mathrm{F}$$\varphi$$\psi$$\mathrm{F}Barrow B$$h$$h\mathrm{o}\varphi=\psi \mathrm{o}\mathrm{F}h$$A\mathcal{L}\mathcal{G}(\mathrm{F})$$\varphiarrow_{F}\psi$$\mathrm{F}$$\mathrm{F}$$COA\mathcal{L}_{\sim}c_{\text{ノ}}(\mathrm{F})$$\mathrm{F}- \mathrm{C}\mathrm{O}^{-}\mathrm{a}\mathrm{l}\mathrm{g}\mathrm{e}\mathrm{b}\mathrm{r}\mathrm{a}\mathrm{S}$$\mathrm{F}_{-\mathrm{C}\mathrm{O}}-\mathrm{h}_{0}\mathrm{m}\mathrm{o}\mathrm{m}\mathrm{o}\mathrm{r}\mathrm{p}\mathrm{h}\mathrm{i}_{\mathrm{S}}\mathrm{m}\mathrm{s}$The nice thing to work inis thathas an initial object andhasa final object, and their carriers coincide. By Scott’s inverse limit construction to construct
fixed points of functors, we get an -algebra:
which is initial in,
and an F-co-algebra:
which is final in. They are each other’s
inverses, and establish an isomorphismin . They also satisfy the equation. Here is the fix point operator that satisfies: $\mu h=h(\mu h)$ . We
say the type
is the (algebraic) data type defined by the functor F.
Type declarations define data types and initial algebras. For example,$C\mathcal{P}O$$A\mathcal{L}\mathcal{G}(\mathrm{F})$$in_{F}$$\mathrm{F}$$out_{F}$$COA\mathcal{L}\mathcal{G}(\mathrm{F})$$\mathrm{F}\mu \mathrm{F}arrow\mu \mathrm{F}$$\mu \mathrm{F}arrow \mathrm{F}\mu \mathrm{F}$$C$$\mu \mathrm{F}\cong \mathrm{F}\mu \mathrm{F}$$\mu(\lambda f.in_{F}\mathrm{o}\mathrm{F}f\mathrm{o}out_{F})=id_{\mu F}$$A\mathcal{L}\mathcal{G}(\mathrm{F})$$COA\mathcal{L}\mathcal{G}(\mathrm{F})$$\mu$$\mu \mathrm{F}$$nat::=$ Zero$|$

Succ $nat$

declares $in_{N}=Zero^{\nabla}$ Succ:
is the initial -algebra, where is the functor(i.e. $\mathrm{N}A=\perp+A$ and $\mathrm{N}h=id_{1}+h$ ) and $nat=\mu$ N. Here,is the terminal object in
Zero: $\perparrow nat$ is a constant.
$\mathrm{N}natarrow nat$$\mathrm{N}$$\mathrm{N}$$\mathrm{N}=\underline{\perp}+id$$\perp$$C$

andData types can be parametrized. For example, the type declaration of the list with elementsof type :list $A::=Nil|c_{ons}$ ( , list )
$A$

$A$

declares $in_{L_{A}}=$ Nil Cons :(i.e.
can take:$\nabla$$\mathrm{L}_{A}(1\mathrm{i}\mathrm{s}\mathrm{t}A)arrow \mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}$$\mathrm{L}_{A}B=\perp+(A\cross B)$$\mathrm{L}_{A}=\underline{\perp}+\underline{A}\cross\dot{i}d$

and

$A$

$A$

is the initial$\mathrm{L}_{A}h=id_{\perp}+(idA\mathrm{x}h)$$out_{L_{A}}=(id_{1}+\mathrm{h}\mathrm{d}_{\Delta}\mathrm{t}1)\mathrm{o}$iallil? : list

-algebra, with the functor). As the final-algebra, we$\mathrm{L}_{A}$$\mathrm{L}_{A}- \mathrm{C}\mathrm{o}$$Aarrow \mathrm{L}_{A}(|\mathrm{i}\mathrm{s}\mathrm{t}A)$

Here ? injects a value of type into the union type $A+A$ according as the result ofdefinition ofabove corresponds to$A$$\mathrm{x}$$\mathrm{p}$$\mathrm{p}\mathrm{x}$. The$out_{L_{A}}$$\lambda \mathrm{x}$. if is-nilx then$\perp$else (hd$\mathrm{t}\mathrm{l}\mathrm{x}$$\mathrm{x},$)We sometimes write, where we think is a bifunctor (i.e. $\mathrm{L}(A, B)=$
instead ofand $\mathrm{L}(f, h)=id_{\perp}+(f\cross h))$ .
Every parametrized type constructor is associated with a certain functor, called a type functor(a map functor). For example, the type functor list coincides the familiar map function. The typefunctor can be defined in general using the notion of catamorphism. We will give the definition
when it is available in the next section.
$\mathrm{L}(A, B)$$\mathrm{L}_{A}(B)$$\mathrm{L}$$\perp+(A\cross B)$

2.3

Catamorphisms and Anamorphisms

Initiality ofinhomomorphism:$in_{F}$$A\mathcal{L}\mathcal{G}(\mathrm{F})$$h$implies: for any -algebra, there exists a unique F:. This homomorphism is called catamorphism and denoted by$\mathrm{F}$$\varphi$$in_{F}arrow_{F}\varphi$$\mathrm{F}Aarrow A$

257. Dually, the finality of,:
implies: for any F-co-algebra
isdenotedandcalled anamorphism,:
there exists a unique
These two morphisms can equivalently be defined as least fixed points:by [$(|\varphi|)_{F}$in$out_{F}$$\psi$$COA\mathcal{L}\mathcal{G}(\mathrm{F})$$Aarrow \mathrm{F}A$$\psiarrow_{F}outF$$\mathrm{F}_{-\mathrm{C}\mathrm{O}}-\mathrm{h}\mathrm{o}\mathrm{m}\mathrm{o}\mathrm{m}\mathrm{o}\mathrm{r}\mathrm{p}\mathrm{h}\mathrm{i}_{\mathrm{S}\mathrm{m}}h$$(\psi)\iota_{r}\cdot$$(|_{-}|)_{F}$:$(|\varphi|)_{F}$$=$$(\mathrm{F}Aarrow A)arrow\mu \mathrm{F}arrow A$$\mu(\lambda f.\varphi \mathrm{o}\mathrm{F}f\mathrm{o}out_{F})$:[$(-)\mathrm{k}$$(Aarrow \mathrm{F}A)arrow Aarrow\mu \mathrm{F}$$=$$[(\psi)]_{F}$$\mu(\lambda f.in_{F}\mathrm{o}\mathrm{F}f\mathrm{o}\psi)$

We sometimes omit the sufix when it is clear from the context.
andFrom these fixed point definitions and the properties offollowing equalities hold:$\mathrm{F}$$\mu,$$in_{F}$$(|\varphi|)_{F}$$=$$\varphi^{\mathrm{o}}\mathrm{F}(|\varphi \mathrm{k}\mathrm{Q}out_{F}$$(|\varphi \mathrm{k}^{0}in_{p}$$=$$\varphi^{\mathrm{o}}\mathrm{F}(|\varphi \mathrm{h}7$$[(\psi)]_{\Gamma}$$=$$in_{F}\circ \mathrm{F}[(\psi)\mathrm{b}\circ\psi$$out_{F}\circ[(\psi)]\mathrm{r}$$=$$\mathrm{F}[(\psi)\mathrm{k}^{\circ\psi}$$out_{F}$, it is easy to see theCatamorphisms are generalized fold operations that substitute the constructors of a data typewith other operations of same signature. Catamorphisms provide a standard way to consume adata structure, and dually, anamorphisms offer a standard way for constructing data structures.
Anamorphisms are generalized unfold operations. It has been argued in [GLPJ93, SF93] thatmany standard functions over data structures can be represented using catamorphisms.

We are now ready to give the definition of type functors in general. Given an initial algebra, the type functor is defined byin:$\mathrm{T}$$\mathrm{F}(A, \mathrm{T}A)arrow \mathrm{T}A$$\mathrm{T}f=(|\dot{i}n\mathrm{o}\mathrm{F}(f, id)|)$.

For example for the example of lists,$in_{L_{A}}$

list

$f$

:

( , list )$(|(N$ ilCons)$\mathrm{L}$

$=$

$A$

$A$

$\nabla$$arrow \mathrm{l}\mathrm{i}\mathrm{s}\mathrm{t}A$$0\llcorner(f,$$id)|)_{L_{A}}$$=$$(|(Nil\nabla ConS)\mathrm{o}(id_{\perp}+(f\mathrm{x}id))|)_{L_{A}}$$=$$(|Nil\nabla(c_{ons}\mathrm{o}(f\cross id))|)L_{A}^{\cdot}$

By expanding the definition of the catamorphism, we get the definition of map function on lists.

2.4

Hylomorphisms

is what you get by composing a fold with an unfold:A hylomorphismis the fixed shape of recursion that comes with a parhylomorphisma[MFP91],
Equivalently
ticular functor.
$\mathbb{I}\varphi,$$(|\varphi|)_{F}0[(\psi)\mathrm{k}\cdot$$\psi \mathrm{k}$[$-\mathrm{k}$$-,$$[\varphi,$$\psi \mathrm{k}$:$=$$(\mathrm{F}Aarrow A)\cross(Barrow \mathrm{F}B)arrow Barrow A$$\mu(\lambda f.\varphi\circ \mathrm{F}f\mathrm{o}\psi)$

It is obvious from definitions that catamorphisms and anamorphisms are special cases of hylo$\beta|\psi*=[in_{F},$morphisms:
is a recursive function whose call graph is isomorphic to the data
Hylomorphism [.
type F. It is known most practical functions can be represented as hylomorphisms
Meertens proved in [Mee92] that every primitive recursive function on an algebraic type can be
represented as a hylomorphism on some algebraic type.
$(|\varphi|)_{F}=[\varphi,$$\varphi,$$out_{F}\mathrm{k},$$\psi \mathrm{k}$$\psi \mathrm{k}$$([\mathrm{B}\mathrm{M}94])$

$\mu$

258

Hylomorphisms enjoy many useful laws for program calculation. The law called HyloShift,$\eta$.

:$\mathrm{F}arrow$$\psi \mathrm{k}=[\varphi,$$\mathrm{G}$$\Rightarrow$$\mathrm{I}\varphi^{\mathrm{Q}}\eta,$$\eta^{\mathrm{o}}\psi \mathrm{k}$shows that natural transformations can be shifted between the two parameters of hylomorphisms.
Based on this property we will introduce a new notation for hylomorphisms in section 3.3.

3

Rules for Deforestation

3.1

Shortcut Deforestation

The core of the shortcut deforestation algorithm proposed in [GLPJ93] is the single rule ofcancellation for a pair of foldr and build:$g$:$\forall\beta.(Aarrow\betaarrow\beta)arrow\betaarrow\beta$

foldr $kz$ (build ) $=gkz$$\Rightarrow$$g$where the function build is defined asbuild $g=g$ Cons Nil.

By using foldr and build to standardize the structure offunctions oflists, their transformation is the repetitive applications of this rule. By expanding the definitionof build, we get$\mathrm{c}\mathrm{o}\mathrm{n}\mathrm{s}\mathrm{u}\mathrm{m}\mathrm{i}\mathrm{n}\mathrm{g}/\mathrm{P}^{\mathrm{r}\mathrm{o}\mathrm{d}\mathrm{u}\mathrm{C}\mathrm{i}}\mathrm{n}\mathrm{g}$$g$$\Rightarrow$! $\forall\beta.(Aarrow\betaarrow\beta)arrow\betaarrow\beta$

foldr $kz$ ( Cons $Nil$ ) $=gkz$$g$This rule can be restated in terms of catamorphisms::$g$$\Rightarrow$$\forall B.(\mathrm{L}_{A}Barrow B)arrow B$$(|\varphi|)_{L_{A}}(gin_{L}A)=g\varphi$

This law nicely captures the intuition behind a catamorphism, namely replace the constructors, the initial -algebra, by function , an arbitrary -algebra.
Now we have enough clues to generalize this rule for other algebraic types.
$\mathrm{L}_{A}$$in_{L_{A}}$3.2$\mathrm{L}_{A}$$\varphi$Acid Rain Theorem

The analysis in the previous section suggests that the following theorem holds in general$([\mathrm{M}\mathrm{e}\mathrm{i}94])$.

Theorem 3.1 (Acid Rain):$g$

Proof The free theorem$\forall A.(\mathrm{F}Aarrow A)arrow A$$([\mathrm{W}\mathrm{a}\mathrm{d}89])$$g$$(|\varphi \mathrm{D}_{F}(gin_{F})=g\varphi$

associated with the type of$f\mathrm{o}\psi_{=\varphi^{\mathrm{o}}}\mathrm{F}f$

In case is defined using recursion,
this rule is instantiated to$\Rightarrow$

$f$

is

$f(g\psi)=g\varphi$

needs to be strict as well. By taking$(|\varphi|)F^{\mathrm{O}in}F\varphi \mathrm{O}\mathrm{F}=(|\varphi|_{F})$This premise trivially holds because (as well).

$\Rightarrow$$g$$|\varphi \mathrm{k}$$\Rightarrow$$f:=(|\varphi|)_{F},$$\psi:=in_{F}$,$(|\varphi|)_{F}(gin_{F})=g\varphi$

satisfies its defining fixed point equation (and is strict$\square$

For the applications we have in mind it is more convenient to rephrase the Acid Rain theoremon the function level:

259

Theorem 3.2 (Acid Rain : Catamorphism)$g$: $\forall A.(\mathrm{F}Aarrow A)arrow Barrow A$$(|\varphi|)_{F}\mathrm{o}(gin_{F})=g\varphi$$\Rightarrow$is some fixed type that does not depend on .
One of the benefits of working on the function level is that we can take the dual of this rule.

Here

$A$

$B$

Theorem 3.3 (Acid Rain : Anamorphism)$h$:$\forall A.(Aarrow \mathrm{F}A)arrow Aarrow B$$(h_{\mathit{0}}ut_{F})0[(\psi)]_{\Gamma}=h\psi$$\Rightarrow$

It is not difficult to prove these theorems as a free theorem in the same way as the first one. We
omit the proof here.
The two acid rain theorems show how we can generalize shortcut deforestation to any algebraic data types, and moreover provide yet another deforesting transformation for values
produced by unfolding. Although these two rules are general enough to capture every casewhere we can deforest intermediate data structures of arbitrary type, it is not easy to design
an automatic deforestation algorithm based on them. It is not obvious how to find the places(redexes) in the program where these rules are applicable, and in which order we should apply
these rules when the redexes are overlapping. As they are stated in the function level and cover
the dual cases (anamorphisms), there are more chance to have overlapping redexes.
To tackle this problem we need some syntactic clue in the program for searching the candidates for or of these rules. The ideal representation of program must facilitate us finding
these candidate polymorphic functions together with catamorphisms and anamorphisms. Natural choice would be hylomorphisms, which include catamorphisms and anamorphisms as special.
cases. And most practical functions can be represented as hylomorphisms
$g$

$h$

$([\mathrm{B}\mathrm{M}94])$

3.3$\mathrm{H}\mathrm{y}\mathrm{l}\mathrm{o}\mathrm{m}\mathrm{o}\mathrm{r}\mathrm{p}\mathrm{h}\mathrm{i}_{\mathrm{S}\mathrm{n}1}\mathrm{s}$as Triplets

We adopt hylomorphisms as the basic components to represent the structure of programs. As
the preparation for designing our deforestation algorithm, we restate the above two Acid Rainrules as a single theorem about hylomorphisms.
Many functions are catamorphic on their input type and anamorphic on their output typeat the same time. For example, the function length that returns the length of a given list is a
catamorphism on list and an anamorphism on $nat$ :$A$lengthFor any natural transformation$(|\dot{i}7\mathrm{b}^{\mathrm{o}}\eta|)F$$\eta$:$=$$(|z_{er}o^{\nabla}(SucC^{\mathrm{o}}exr)|)_{L}A$$=$$[((\dot{i}d_{\perp}+\mathrm{t}1)\mathrm{o}\mathrm{i}=\mathrm{r}\mathrm{l}\mathrm{i}1?)]_{N}$$\mathrm{F}arrow \mathrm{G},$$=$$[_{\dot{i}7}\mathrm{b}^{\mathrm{o}}\eta,$$=$$[in_{G},$HyloShift inplies$outF\mathrm{I}_{F}$$\eta^{\mathrm{o}_{ou}}t_{F}\mathrm{J}_{G}=[(\eta \mathrm{o}out_{F})]G$

If we do not want to miss the chance that this kind of hylomorphism consists the redex for the
Acid Rain rules, the possibilities of HyloShift rule application have to be considered always.
To avoid this cumbersomeness by preparing a neutral representation for them, we introduce

a new notation of hylomorphisms, where the natural transformation is explicitly factored out as
an extra second parameter.

260

Definition 3.1 (Hylomorphism in triplet form) Hylomorphism [follows::$\varphi,$$\eta,$$\psi \mathrm{J}_{G,F}$

is defined as$(\mathrm{G}Aarrow A)\cross(\mathrm{F}arrow \mathrm{G})\mathrm{x}(Barrow \mathrm{F}B)arrow(Barrow A)$$[\varphi,\eta,’\psi][_{-},--\mathrm{I}\mathrm{b}_{F}G,,F$$=$

We sometimes omit the sufix$\mu(\lambda f.\varphi^{\mathrm{o}}\eta \mathrm{O}\mathrm{F}f\mathrm{o}\psi)$

when it is clear from the context.

$\mathrm{F}$$\mathrm{G},$With this notation the hylomorphisms which are essentially built up from some naturaltransformation can be
resented as it is. Now the example explained above has the proper
neutral representation as a hylomorphism:$\mathrm{r}\mathrm{e}\dot{\mathrm{p}}$$(|\dot{i}n_{G^{\mathrm{o}}}\eta|)_{F}=\mathrm{I}^{in_{G},\eta,\mathit{0}}utF\mathrm{J}_{G},F=[(\eta^{\mathrm{o}}out_{F})]G$

The function length is represented as follows:

lengthThe type functor
this kind:$\mathrm{T}$$id+exr,$$=[i_{\mathfrak{R}},$$outL_{A}\mathrm{I}_{N,L_{A}}$defined in section 2.3 can always be representable as a hylomorphism of$\mathrm{T}f=[in,$$\mathrm{F}(f, id),$outI.

With this notation, it becomes much easier to judge whether a hylomorphism is either acatamorphism or a anamorphism. If the third parameter of the hylomorphism is, it is a-catamorphism, and if its first parameter is, it is a G-anamorphism.
$out_{F}$$\mathrm{F}$$in_{G}$The HyloShift rule becomes$[\varphi,$$\eta,$$\psi \mathrm{I}_{G,F}=[\varphi^{\mathrm{o}}\eta,$$id,$$\psi \mathrm{I}_{F,F}=[\varphi,\dot{i}d,$$\eta^{\mathrm{Q}}\psi \mathrm{I}_{G},c$

Rules for Hylomorphism Fusion

3.4

The Acid Rain Theorems for catamorphism and anamorphism can be restated in terms of the
new notation for hylomorphisms.

Theorem 3.4$(\mathrm{C}\mathrm{a}\mathrm{t}\mathrm{a}- \mathrm{H}\mathrm{y}1_{0}\mathrm{F}\mathrm{u}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n})$$\tau$$[\varphi,$$\eta_{1},$:$\forall A.(\mathrm{F}Aarrow A)arrow \mathrm{F}’Aarrow A$$outF\mathrm{I}G,F[0\mathcal{T}in_{F},$$\eta_{2},$$\Rightarrow$$\psi \mathrm{I}_{F^{\prime_{L}}},=[\tau(\varphi^{\mathrm{Q}}\eta 1),$$\eta 2,$$\psi \mathrm{I}_{F}\prime_{L}$,Proof The first component of the left-hand side is just a catamorphism. The second$BarrowA$
component hylomorphism has a type
where
and
are the carriers ofand ,correspondingly. Consider the following lambda term:$(|\varphi^{\mathrm{o}}\eta 1|)_{F}$$A$$g=\lambda f.[\tau f,$As$\tau$is polymorphic,$g$$\eta 2,$$B$$\tau in_{F}$$\psi$$\psi \mathrm{J}_{F,L}$

becomes also polymorphic and has a type:$g$: $\forall A.(\mathrm{F}Aarrow A)arrow Barrow A$

This type exactly match the type requirement forproves this theorem.

$g$in Theorem 3.2, and the simple instantiation$\square$Taking the dual of this theorem, we get the following theorem.

261

Theorem 3.5$(\mathrm{H}\mathrm{y}\mathrm{l}\mathrm{o}- \mathrm{A}\mathrm{n}\mathrm{a}\mathrm{F}\mathrm{u}\mathrm{S}\mathrm{i}\mathrm{o}\mathrm{n})$$\sigma$$[\varphi,$:$\forall A.(Aarrow \mathrm{F}A)arrow Aarrow \mathrm{F}’A$$\sigma out_{F}\mathrm{J}’[\mathrm{o}in_{F},$$\eta 2c,F’\psi \mathrm{I}_{F,L}=[\varphi,$$\eta_{1},$$\eta_{1},$$\Rightarrow$$\sigma(\eta 20\psi)\mathrm{I}G,F’$

These two rules provides the theoretical basis of our deforestation algorithm.
Note that$[\varphi,$4

rule is just a special case of these rules, by taking $\tau:=id$ or $\sigma:=id$ :$\mathrm{H}\mathrm{y}\mathrm{l}\mathrm{o}\mathrm{S}\mathrm{P}\mathrm{l}\mathrm{i}\mathrm{t}-1$$\eta_{1},$$oul_{F}\mathrm{I}_{G,F}\mathrm{o}\mathbb{I}i7\triangleright,$$\eta_{2},$$\psi \mathrm{J}_{F},L=[\varphi,$$\eta_{1}0\eta_{2},$$\psi \mathrm{J}_{G,F}$

Transformation based on Hylomorphism Fusion

Our transformation algorithm is completely based on the two HyloFusion rules above, andrepetitively applies these rules until there is no redex left in the program. Both rules replace thecomposition of two hylomorphisms with one hylomorphism, so termination is vacuous. The application of the rule is always safe in the sense that every application removes some intermediate
data structure which has been passed through the eliminated composition.
The essence of our transformation algorithm is the reduction strategy which controls theorder of redexes to be picked up. How to decide the reduction order of overlapping redexes is
the main part of the algorithm.

4.1

The Language

In principle, our transformation method is applicable to any functional program as long as it
includes some compositions of hylomorphisms. But to get the most out of our method, we assume
here the programs are entirely written as compositions of hylomorphisms. Of course programs
may include some lambda expressions inside and outside of hylomorphisms, but it is not allowed
to write explicit recursion. Every recursion has to be standardized using hylomorphisms.

Basic functors and the related combinators can be freely used to combine hylomorphisms or
to define the parameters for hylomorphisms.

4.2

Two Examples of Transformation

Let us consider the following three standard functions on the list data structure. They aredefined as hylomorphisms:
length$=$map$=\mathbb{I}^{in_{L_{B}}},$$f$$[im,$ $id+eXr,$$\mathrm{L}(f, id),$$(++ys)=[\mathcal{T}\dot{i}n_{L_{A}},$

where
Here we assume that$‘\lambda n\nabla c\ldots$

’

$id,$

$out_{L_{B}}\mathrm{J}$$outL_{A}\mathrm{I}$$out_{L_{A}}\mathrm{I}$$\tau=\lambda n\nabla c.([n\nabla c, id, out_{L}A\mathrm{J}ys)\nabla C$

is a pattern that matches any ‘$f\nabla h’$.

To define $(++ys)$ in the proper abstract level, the constructors (Nil and Cons) in $ys$ are
replaced by and systematically, using another hylomorphism in the definition of . This
[GLPJ93].
exactly corresponds to the definition
$n$

$c$

$\tau$$\mathrm{o}\mathrm{f}\mapsto \mathrm{i}\mathrm{n}$262Then the composition length (map )
$f$

$0$

length (map )
$f$

$0$

is transformed as$\mathrm{Q}(++ys)$$\mathbb{I}\dot{i}n_{N},\dot{i}d+exr,$$\mathrm{o}[in_{L_{B}},$$=$:$\mathrm{o}(++ys)${definition of length, map and$=$$\mathrm{f}\mathrm{o}\mathrm{n}_{\mathrm{o}\mathrm{w}\mathrm{s}}$$out_{L}B$

$++$

}

I

$\mathrm{L}(f, id),$ $outL_{A}\mathrm{J}\circ[\tau in_{L_{A}},$$id,$ $outL_{A}\mathrm{I}$$\{\mathrm{H}\mathrm{y}1_{0}\mathrm{S}\mathrm{P}^{\mathrm{l}\mathrm{i}}\mathrm{t}-1\}$[$i_{\mathfrak{R}},$$=$$(id+exr)\mathrm{Q}\llcorner(f,id),$ $outL_{A}$I$0[\tau in_{L},$$id,$$outAL_{A}\mathrm{J}$$\{\mathrm{c}\mathrm{a}\mathrm{t}\mathrm{a}_{-\mathrm{H}\mathrm{y}}1\mathrm{o}\mathrm{F}\mathrm{u}\mathrm{s}\mathrm{i}\mathrm{o}\mathrm{n}\}$$[\tau(in_{N^{\mathrm{O}}}(id+exr)0\llcorner(f, id)),${definition of

$=$

[ ((
$\tau$$zero^{\nabla}$$in_{N}$

Succ)

and

$\mathrm{L}$$id,$ $outL_{A}\mathrm{I}$}$\mathrm{o}(id+eXr)\mathrm{o}(\perp+f\cross id)$), $id,$$out_{L}\mathrm{J}A${properties of basic functors}

$=$

[ (
$\tau$$Zero^{\nabla}$(Succ$\mathrm{o}exr$)), $id,$$out_{L_{A}}$I{definition of }$=$$\tau$[( $[Zero\nabla$ (Succ$id,$ $out_{L_{A}}$$\mathrm{o}exr$), $id,$$out_{L_{A}}\mathrm{J}ys$)$\nabla$(Succ$\mathrm{o}exr$),I

By inlining the definition of hylomorphism, we get the familiar recursive definition:

length (map ) $\mathrm{o}(++ys)=h$
where
Nil
$=gys$
where
Nil$gCons(X, xs)=$ $1+(gxs)$
Cons $(x, xs)=1+(hxs)$
$f$

$0$

$h$

$=$

$g$

$0$

$h$

Note that the intermediate list structure produced by map andis no longer generated.
Our second example includes the functions iterate and takewhile which are both anamorphisms on the list. They are usually defined by the following recursive equations:( , iterate $f(fx)$ )iterate $fx$
takewhileNil
Niltakewhile $pC_{\mathit{0}}ns(x, xs)$
$ifpx$ then $c_{onS}$ ( , takewhile $pxs$ )else Nil
They can be defined as hylomorphisms:$f$$=C_{\mathit{0}}ns$

$x$

$=$

$p$

$=$

iterate$(\mathrm{i}+ys)$

$x$

$=$

$[in_{L_{A}},$$id,$$inr\mathrm{o}(id_{\Delta}f)\mathrm{I}$takewhile $p=$$[in_{L_{A}},$$id,$$\sigma out_{L_{A}}\mathrm{I}$

$f$

where

$\sigma=\lambda h.(id_{1^{\nabla}}g)\mathrm{o}h$where$g(x, xS)=ifpx$ then $inr(x, xs)$ else $inl()$

Since takewhile can not be represented as a catamorphism, previous methods in [GLPJ93,
SF93] cannot remove the intermediate list which is consumed by takewhile. Our method naturally covers these dual cases.

263

Then the composition (takewhile ) (iterate ) is transformed as follows:$f$$\circ$$p$(takewhile ) (iterate )
$p$

$f$

$0$

{definition of takewhile and iterate}$=$$\mathbb{I}in_{L_{A}},$$id,$$\sigma out_{L_{A}}$

I

$id,$

$0[\dot{i}n_{L_{A}},$$inr\circ(id_{\Delta}f)\mathrm{I}${Hylo-AnaFusion}$=$$\mathrm{I}\dot{\iota}n_{L_{A}},\dot{i}d,$$\sigma(inr\circ(id_{\Delta}f))\mathrm{I}${definition of }$=$$\sigma$$[i_{7}\mathrm{k}_{A},$$id,$$(\dot{i}d_{\perp^{\nabla}g})\mathrm{o}(inr\mathrm{o}(id_{\Delta}f))\mathrm{I}${properties of combinators}$=$$\mathrm{I}i\eta_{L_{A}},\dot{i}d,$$g\circ(id_{\Delta}f)\mathrm{I}$By inlining the definition of hylomorphism, we get the following recursive definition:(takewhile ) (iterate ) $=h$where $hx=ifpx$ then
$p$

$0$

$f$

$C_{onS}(X, h(fx))$

else Nil

Note that the intermediate list generated by iterate has been eliminated. It is clear from thisexample that our method is more powerful than the previous methods even when restricted to
the list data structure.

4.3

Transformation Algorithm

The reduction strategy to control the order of application of the rules (Cata-HyloFusion andHylo-AnaFusion) defines our transformation algorithm.
Note that Cata-HyloFusion does not change the compositional interface to the right: thethird parameter of the right hylomorphism remains unchanged as the third parameter of thedoes not change the compositional interface
resultant hylomorphism. Dually,to the left.
We call the redexes of each rules Cata-Hylo redex and Hylo-Ana redex correspondingly. Because there are two kinds of redexes, four different cases of overlapping redexes exist:$\mathrm{H}\mathrm{y}1_{0-}\mathrm{A}\mathrm{n}\mathrm{a}\mathrm{F}\mathrm{u}\mathrm{S}\mathrm{i}\mathrm{o}\mathrm{n}$1. Two Cata-Hylo redexes overlap:$[\varphi,$$out_{F}\mathrm{I}\circ[\tau_{1}in_{F},$$\eta_{1},$$\eta 2,$$ou\mathrm{k}\mathrm{I}^{0}[\tau_{2}in_{\mathrm{c}},$$\eta 3,$$\psi \mathrm{I}$In this case the reduction of the left redex does not destroy the right one.

2. Two Hylo-Ana redexes overlap:$[\varphi,$$\eta_{1},$$\sigma_{1}out_{F}\mathrm{I}^{0}[in_{F},$$\eta_{2},$$\sigma 2out_{G}\mathrm{I}^{0}[in_{G},$$\eta 3,$$\psi \mathrm{I}$In this case the reduction of the right redex does not destroy the left one.

3. A Cata-Hylo redex (in the left) overlaps with a Hylo-Ana redex (in the right):[$\varphi,$$\eta 1,$outFI$\mathrm{I}\mathcal{T}\dot{i}nF’\eta 2,$$\sigma ou\mathrm{b}\mathrm{J}\mathrm{Q}[i_{7}\Leftrightarrow,$$\eta 3,$$\psi \mathrm{I}$In this case the reduction of either redex does not destroy the other redex.

264

4. A Hylo-Ana redex (in the left) overlaps with a Cata-Hylo redex (in the right):$[\varphi,$$\eta_{1,F}\sigma out\mathrm{I}^{0}\mathbb{I}inF’\eta 2,$ $out_{\mathrm{c}}\mathrm{I}^{0}[\tau in_{G},$$\eta_{3},$$\psi \mathrm{I}$In this case the reduction of either redex does destroy the other redex.
This observation tells us that the series of overlapping redexes of the same kind (case 1 and 2
above) are sensitive to the reduction order.

Definition 4.1 (Redex chain) A Cata-Hylo (Hylo-Ana) redex chain is the series of Cata-Hylo(Hylo-Ana) redexes with overlaps.
The following reduction strategy defines our algorithm:

Definition 4.2 (Reduction order)
1. Find all maximal Cata-Hylo redex chains, and reduce each chain from left to right.

2. Find all maximal Hylo-Ana redex chains, and reduce each chain from right to lefl.
3. Simplify the inside of each hylomorphisms using reduction rules for basic functors andrelated combinators.

4. If there exists any redex for HyloFusion rules, return to step 1 and continue reduction.
The reduction rules used in step 3 is listed in the next section.

4.4

Reduction Rules for Basic Functors

Following rules are used to reduce the functor during the transformation. These equations
describe some of the properties of basic functors and related combinators.
$exl\circ(f\cross g)$

$=$

foexl

exro

$(f\cross g)$$=$$g^{0}exr$$(f\Delta g)$

$=$

$f$

$exr\circ(f_{\Delta}g)$

$=$

$g$

$exl\Delta eXr$

$=$

$id$

$(f\cross g)\mathrm{o}(h\Delta j)$$=$$(f\circ h)_{\Delta}(g\mathrm{Q}j)$$(f\mathrm{x}g)\circ(h\mathrm{x}j)$$=$$(f\mathrm{o}h)\cross(g\mathrm{o}j)$$(f_{\Delta}g)\mathrm{o}h$$=$$(f\circ h)_{\Delta}(g\mathrm{o}h)$$(f+g)\circ inl$$=$

$inl\mathrm{o}f$$(f+g)\mathrm{o}inr$

$=$

inrog

$(f\nabla g)\circ inl$

$=$

$f$

$(f\nabla g)\circ inr$

$=$

$g$

$inl\nabla inr$

$=$

$id$

$(f\nabla g)\mathrm{o}(h+j)$$=$$(f\mathrm{o}h)\nabla(g\mathrm{o}j)$$(f+g)\mathrm{o}(h+j)$$=$$(f^{\mathrm{Q}}h)+(g\mathrm{o}j)$$f\circ(g\nabla h)$$=$$(f\mathrm{o}g)\nabla(f\mathrm{o}h)$exlo(for strict

$f$

)

265

4.5

More Examples of Transformation

To demonstrate the power of our transformation, let’s consider the following functions:$zip=[\dot{i}n_{L_{A\mathrm{x}B}},$$(id+ab\dot{i}de)\mathrm{o}ISNilo_{r,\mathit{0}}ut_{L}A\cross out_{L_{B}}\mathrm{I}$where abide $=(exl\mathrm{X}exl)\Delta(exr\cross exr)$$IsNilor((1, x),$ $(1, y))=(1, (x, y))$$IsNilor((i, x),$ $(j, y))$ $=(0, (x, y))$iterate$f=[\dot{i}n_{L_{A}},\dot{i}d,$$inr\mathrm{o}(id_{\Delta}f)\mathrm{J}$Then the composition zip ((iterate $f)\cross zip$ ) is transformed as follows:$0$

zip $\mathrm{o}((iteratef)\cross zip)${definition of zip and iterate}$=$$[in_{L_{A\cross}}(B\mathrm{X}C)’(\dot{i}d+abide)\mathrm{o}IsN\dot{i}lOr,$$\mathrm{o}([in_{L_{A}},$$id,$$\cross[in_{L_{B}\cross C},$

$out_{L_{A}}\cross out_{L_{B\mathrm{x}c}}\mathrm{I}$$inr\circ(id_{\Delta}f)\mathrm{I}$$(\dot{i}d+abide)\mathrm{o}ISNilo_{r,ou}t_{L_{B}}\cross out_{L_{C}}\mathrm{I})${property of }$=$$\cross$$[in_{L_{A\cross(}}B\mathrm{X}c)’(id+abide)\mathrm{o}IsN_{\dot{i}lOr,ou}t_{L_{A}}\cross out_{L_{B}\mathrm{x}c}\mathrm{I}$$\circ \mathbb{I}^{i}\eta L_{A}\cross in_{L_{B}\mathrm{x}C},$$id_{\mathrm{X}}((id+abide)\mathrm{Q}IsNilOr)$,$(inr\circ(\dot{i}d\Delta f))\cross(out_{L_{B}}\cross out_{l})\mathrm{C}\mathrm{I}$$=$$\{\mathrm{H}\mathrm{y}\mathrm{l}\mathrm{o}\mathrm{S}\mathrm{p}\mathrm{l}\mathrm{i}\mathrm{t}-1\}$$[in_{L_{A(B\mathrm{x}c_{)}}}(id+abide)’ \mathrm{O}IsN\dot{i}lor\mathrm{o}(id\cross \mathrm{X}((id+abide)\circ ISN\dot{i}lOr))$,$(\dot{i}nr^{\mathrm{Q}}(id_{\Delta}f))\cross(out_{L_{B}}\cross out_{L}C)\mathrm{J}$By inlining the definition of hylomorphisms, we get the familiar recursive definition:

zip $\mathrm{o}((iteratef)\cross zip)=h$( , (Nil, $zs$ ))where( , ( $ys$ , Nil))
$h$

$x$

$=$

$h$

$x$

$=$

$h(x, (ys, zS))$

$=$

Nil
Nil
$c_{on}S((X, (hdys, hdZs))$ ,$h(fx, (tly_{S}, tlZS)))$In [GLPJ93] zip has been discussed to explain the most serious limitation of their method.
It is clear from this example that our transformation has successfully lift their limitation: theboth input lists to zip have been deforested.

5

Related Work

Deforestation was first proposed by Wadler in [Wad88] as an automatic transformation to remove unnecessary intermediate data structure. The class of programs his algorithm can treat
is characterized as treeless program which is a subset of first-order programs. Based on the observation that some intermediate data structures of basic types (e.g. integers, characters, etc.)
need not to be removed, Wadler developed the blazing technique to handle such terms. He also

266

discusses to apply his method to some higher-order programs whose higher-order functions canbe treated as macros. Our method works on much wider class of higher-order programs, and it
need not expand to first-order forms. It is also easy to control what types of intermediate data
structures are to be removed with our method.
The fusion transformation proposed by Chingeneralizes deforestation to make itapplicable to all first-order programs. Combining it with his higher-order removal technique, hisalgorithm can take any first-order and higher-order program as its input. Inspired by Wadler’s
blazing deforestation, Chin devised the double annotation scheme for safe fusion to recognize andskip over terms to which his techniques do not apply. Because his method basically annotates
non-treeless subterms, the improvement to Wadler’s method comes from the power of higherorder removal. Our method accepts the example of higher-order removal in his paper andsuccessfully transforms it to the same first-order program. Moreover the example program sizet(defined as length flatten on binary tree), which cannot be handled with Chin’s method
without assuming an extra law on length and append, naturally be deforested by our method
without any extra laws.
In [FSZ94] Fegaras, Sheard and Zhou extend their normalization algorithm in [SF93] to themore general fold programs which recurse over multiple inductive structures simultaneously, suchas zip or $nth$ . Because our method always works on the function level and explicitly manipulates
the functors, it is easy to give symmetric definitions to those functions like zip.
, applies a tree grammar-based data-flow analysis to put annotations on
programs that guarantee termination of deforestation for the wider class of first-order programs
than Chin’s method. The grammar is used to approximates the set of terms that the deforestation algorithm encounters, and successfully locates the increasing (accumulating) parameterswhich could be the source of infinite unfolding.
, Gl\"uck and Jones
pick up four different transformation methods (Partial Evaluation, Deforestation, Supercompilation and Generalized Partial Computation [FNT91,
Tak91]) and discuss the difference of transformational power of each method. Because eachmethod is defined for the different language in syntactic way, it is not easy to compare without
losing the insights of each method. Calculation-based transformations provides the better device
for such comparative study.
$([\mathrm{C}\mathrm{h}\mathrm{i}92])$$0$$\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{n}([\mathrm{S}\emptyset \mathrm{r}94])$$\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{n}$$([\mathrm{S}\mathrm{G}\mathrm{J}94])$

Acknowledgments
We are grateful to Lambert Meertens, Kieran Clenaghan and Fer-Jan de Vries for providing
encouragement and valuable feedback for this research. Many thanks also to Leonidas Fegaras,
Zhenjiang Hu, Hideya Iwasaki, Ross Paterson and Masato Takeichi for their comments on thedraft of this paper.

References[BD77]

R.M. Burstall and J. Darlington. A transformation system for developing recursive
programs. JA CM, $24(1):44-67$ , 1977.

[BM94]

Richard S. Bird and Oege Moor. Relational program derivation and context-freelanguage recognition. In A.W. Roscoe, editor, A Classical Mind, pages 17-35. Prentice
Hall, 1994.

[Chi92]

Wei-Ngan Chin. Safe fusion of functional expressions. In ACM Conference on Lispand Functional Programming, San Francisco, Ca., pages 11-20. ACM, June 1992.

267[FNT91]

Y. Futamura, K. Nogi, and A. Takano. Essence of generalized partial computation.
Theoretical Computer Science, 90:61-79, 1991.

[Fok92]

M.M. Fokkinga. Law and Order in Algorithmics. PhD thesis, Universiteit Twente,
February 1992.

[FSZ94]

L. Fegaras, T. Sheard, and T. Zhou. Improving programs which recurse over multiple
inductive structures. In PEPM ’94.

[GLPJ93] A. Gill, J. Launchbury, and S.L. Peyton Jones. A short cut to deforestation. In FPCA
’93, Copenhagen. ACM, June 1993.
[Jeu93]

J. Jeuring. Theories for Algorithm Calculation. PhD thesis, University of Utrecht,
February 1993.

[Mee86]

L. Meertens. Algorithmics –towards programming as a mathematical activity. In
Proceedings of the CWI Symposium on Mathematics and Computer Science, pages
289-334. North-Holland, 1986.

[Mee92]L. Meertens. Paramorphisms. Formal Aspects of Computing, $4(5):413-424$ , 1992.

[Mei92]

E. Meijer. Calculating Compilers. PhD thesis, University of Nijmegen, February 1992.

[Mei94]

E. Meijer. Acid rain theorem. Submitted for publication, 1994.

[MFP91] E. Meijer, M.M. Fokkinga, and R. Paterson. Functional programming with bananas,
lenses, envelopes and barbed wire. In FPCA ’91, Boston, Ma., volume 523 of LNCS,
pages 124-144. Springer-Verlag, August 1991.
[SF93]

T. Sheard and L. Fegaras. A fold for all seasons. In FPCA ’93, Copenhagen, pages
233-242. ACM, June 1993.

[SGJ94], R. Gl\"uck, and N.D. Jones. Towards unifying partial evaluation, deforestation, supercompilation, and gpc. In ESOP ’94, volume 788 of LNCS. SpringerVerlag, April 1994.

$[\mathrm{s}_{\emptyset \mathrm{r}}94]$

M.H.

$\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{s}\mathrm{e}\mathrm{n}$. A grammar-based data-flow analysis to stop deforestation. In CAAP
M.H.
’94, volume 787 of LNCS. Springer-Verlag, April 1994.
$\mathrm{S}\emptyset \mathrm{r}\mathrm{e}\mathrm{n}\mathrm{S}\mathrm{e}\mathrm{n}$[Tak91]

A. Takano. Generalized partial computation for a lazy functional language. In $ACM$
Symposium on Partial Evaluation and Semantics-Based Program Manipulation, New
Haven, Connecticut., pages 1-11. ACM, 1991.

[Tak95]

A. Takano and E. Meijer. Shortcut deforestation in calculational form. In FPCA ’95,
306-313. ACM, June 1995.

[TNT82]$\mathrm{V}.\mathrm{F}$[Tur86]$\mathrm{V}.\mathrm{F}$. Turchin,$\mathrm{R}.\mathrm{M}$. Nirenberg, and$\mathrm{D}.\mathrm{V}$. Turchin. Experiments with a supercompiler.

In $ACM$ Symposium on Lisp and Functional Programming, Pittsburgh, Pennsylvania,
pages 47-55. ACM, 1982.

. Turchin. The concept of a supercompiler. $ACM$ TOPLAS, $8(3):292-325$ , July

1986.
[Wad88]

P. Wadler. Deforestation. In ESOP ’88, Nancy, France, volume 300 of LNCS.
Springer-Verlag, March 1988.

[Wad89]P. Wadler. Theorems for free! In FPCA ’89, London, ACM, September 1989.