11institutetext: School of Computing, Dublin City University, Dublin, Ireland
11email<EMAIL_ADDRESS>
# The Next 700 Program Transformers

G.W. Hamilton  000-0001-5954-6444

###### Abstract

In this paper, we describe a hierarchy of program transformers in which the
transformer at each level of the hierarchy builds on top of those at lower
levels. The program transformer at level 1 of the hierarchy corresponds to
positive supercompilation, and that at level 2 corresponds to distillation. We
prove that the transformers at each level terminate. We then consider the
speedups that can be obtained at each level in the hierarchy, and try to
characterise the improvements that can be made.

###### Keywords:

transformation hierarchy supercompilation distillation speedups

##  1 Introduction

It is well known that programs written using functional programming languages
often make use of intermediate data structures and thus can be inefficient.
Several program transformation techniques have been proposed to eliminate some
of these intermediate data structures; for example partial evaluation [11],
deforestation [24] and supercompilation [21]. Positive supercompilation [20]
is a variant of Turchin’s supercompilation [21] that was introduced in an
attempt to study and explain the essentials of Turchin’s supercompiler.
Although strictly more powerful than both partial evaluation and
deforestation, Sørensen has shown that positive supercompilation (without the
identification of common sub-expressions in generalisation), and hence also
partial evaluation and deforestation, can only produce a linear speedup in
programs [18]. Even with the identification of common sub-expressions in
generalisation, superlinear speedups are obtained for very few interesting
programs, and many obvious improvements cannot be made without the use of so-
called ‘eureka’ steps [3].

###### Example 1

Consider the function call $nrev~{}xs$ shown in Fig. 1.

$\begin{array}[t]{lcl}\lx@intercol\mathit{nrev}~{}\mathit{xs}\hfil\lx@intercol\\\
\lx@intercol{\bf where}\hfil\lx@intercol\\\
\mathit{nrev}~{}\mathit{xs}&=&\\!\begin{array}[t]{llcl}\lx@intercol{\bf
case}~{}\mathit{xs}~{}{\bf of}\hfil\lx@intercol\\\
&\mathit{Nil}&\Rightarrow&\mathit{Nil}\\\
{}{}{}{}&\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}&\Rightarrow&\mathit{append}~{}(\mathit{nrev}~{}\mathit{xs^{\prime}})~{}(\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{Nil})\end{array}\\\
\mathit{append}~{}\mathit{xs}~{}\mathit{ys}&=&\\!\begin{array}[t]{llcl}\lx@intercol{\bf
case}~{}\mathit{xs}~{}{\bf of}\hfil\lx@intercol\\\
&\mathit{\mathit{Nil}missing}&\Rightarrow&\mathit{ys}\\\
{}{}{}{}&\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}&\Rightarrow&\mathit{Cons}~{}\mathit{x^{\prime}}~{}(\mathit{append}~{}\mathit{xs^{\prime}}~{}\mathit{ys})\end{array}{}\end{array}$
---
$\begin{array}[t]{lcl}\lx@intercol\mathit{qrev}~{}\mathit{xs}\hfil\lx@intercol\\\
\lx@intercol{\bf where}\hfil\lx@intercol\\\
\mathit{qrev}~{}\mathit{xs}&=&\mathit{qrev^{\prime}}~{}\mathit{xs}~{}\mathit{Nil}\\\
\mathit{qrev^{\prime}}~{}\mathit{xs}~{}\mathit{ys}&=&\\!\begin{array}[t]{llcl}\lx@intercol{\bf
case}~{}\mathit{xs}~{}{\bf of}\hfil\lx@intercol\\\
&\mathit{Nil}&\Rightarrow&\mathit{ys}\\\
{}{}{}{}&\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}&\Rightarrow&\mathit{qrev^{\prime}}~{}\mathit{xs^{\prime}}~{}(\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{ys})\end{array}{}\end{array}$
Figure 1: Alternative Definitions of List Reversal

This reverses the list $xs$, but the recursive function call
$(nrev~{}xs^{\prime})$ is an intermediate data structure, so in terms of time
and space usage, it is quadratic with respect to the length of the list $xs$.
A more efficient function that is linear with respect to the length of the
list $xs$ is the function $qrev$ shown in Fig. 1.

A number of algebraic transformations have been proposed that can perform this
transformation (e.g. [23]), making essential use of eureka steps requiring
human insight and not easy to automate; for the given example this can be
achieved by appealing to a specific law stating the associativity of the
$append$ function. However, none of the generic program transformation
techniques mentioned above are capable of performing this transformation.

The distillation algorithm [7, 9] was originally motivated by the need for
automatic techniques that avoid the reliance on eureka steps to perform
transformations such as the above. In positive supercompilation,
generalisation and folding are performed only on expressions, while in
distillation, generalisation and folding are also performed on recursive
function representations (process trees). This allows a number of improvements
to be obtained using distillation that cannot be obtained using positive
supercompilation.

The process trees that are generalised and folded in distillation are in fact
those produced by positive supercompilation, so we can see that the definition
of distillation is built on top of positive supercompilation. This suggests
the existence of a hierarchy of program transformers, where the transformer at
each level is built on top of those at lower levels, and more powerful
transformations are obtained as we move up through this hierarchy. In this
paper, we define such a hierarchy inductively, with positive supercompilation
at level 1, distillation at level 2 and each new level defined in terms of the
previous ones. Each of the transformers is capable of performing fusion to
eliminate intermediate data structures by fusing nested function calls. As we
move up through the hierarchy, deeper nestings of function calls can be fused,
thus removing more intermediate data structures.

The remainder of this paper is structured as follows. In Section 2, we define
the higher-order functional language on which the described transformations
are performed. In Section 3, we give an overview of process trees and define a
number of operations on them. In Section 4, we define the program transformer
hierarchy, where the transformer at level 0 corresponds to the identity
transformation, and each successive transformer is defined in terms of the
previous ones. In Section 5, we prove that each of the transformers in our
hierarchy terminates. In Section 6, we consider the efficiency improvements
that can be obtained as we move up through this hierarchy. Section 7 concludes
and considers related work.

##  2 Language

In this section, we describe the call-by-name higher-order functional language
that will be used throughout this paper.

######  Definition 1 (Language Syntax)

The syntax of this language is as shown in Fig. 2.

$\mathit{prog}$ | ::= | $\mathit{e_{0}}~{}{\bf where}~{}\mathit{h_{1}}=\mathit{e_{1}}\ldots\mathit{h_{n}}=\mathit{e_{n}}$ | Program
---|---|---|---
$\mathit{e}\in Exp$ | ::= | $\mathit{x}$ | Variable
| $|$ | $\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}$ | Constructor Application
| $|$ | $\lambda\mathit{x}.\mathit{e}$ |  $\lambda$-Abstraction
| $|$ | $\mathit{f}$ | Function Call
| $|$ | $\mathit{e_{0}}~{}\mathit{e_{1}}$ | Application
| $|$ | ${\bf case}~{}\mathit{e_{0}}~{}{\bf of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}}$ | Case Expression
| $|$ | ${\bf let}~{}\mathit{x}=\mathit{e_{0}}~{}{\bf in}~{}\mathit{e_{1}}$ | Let Expression
$\mathit{h}$ | ::= | $\mathit{f}~{}\mathit{x_{1}}\ldots\mathit{x_{n}}$ | Function Header
$\mathit{p}$ | ::= | $\mathit{c}~{}\mathit{x_{1}}\ldots\mathit{x_{n}}$ | Pattern
Figure 2: Language Syntax

Programs in the language consist of an expression to evaluate and a set of
function definitions. An expression can be a variable, constructor
application, $\lambda$-abstraction, function call, application, case or let.
Variables introduced by function definitions, $\lambda$-abstractions, case
patterns and lets are bound; all other variables are free. We assume that
bound variables are represented using De Bruijn indices. An expression that
contains no free variables is said to be closed. We write $e\equiv e^{\prime}$
if $e$ and $e^{\prime}$ differ only in the names of bound variables.

Each constructor has a fixed arity; for example $\mathit{Nil}$ has arity 0 and
$\mathit{Cons}$ has arity 2. In an expression
$\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}$, $n$ must equal the arity of
$c$. The patterns in case expressions may not be nested. No variable may
appear more than once within a pattern. We assume that the patterns in a case
expression are non-overlapping and exhaustive. It is also assumed that
erroneous terms such as
$(\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}})~{}\mathit{e}$ where $c$ is
of arity $n$ and ${\bf case}~{}(\lambda x{.e{)~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{k}}\Rightarrow\mathit{e_{k}}}}$
cannot occur.

######  Definition 2 (Substitution)

We use the notation $\theta=\\{x_{1}\mapsto e_{1},\ldots,x_{n}\mapsto
e_{n}\\}$ to denote a substitution. If $e$ is an expression, then
$e\theta=e\\{x_{1}\mapsto e_{1},\ldots,x_{n}\mapsto e_{n}\\}$ is the result of
simultaneously substituting the expressions $e_{1},\ldots,e_{n}$ for the
corresponding variables $x_{1},\ldots,x_{n}$, respectively, in the expression
$e$ while ensuring that bound variables are renamed appropriately to avoid
name capture. A renaming denoted by $\sigma$ is a substitution of the form
$\\{x_{1}\mapsto x_{1}^{\prime},\ldots,x_{n}\mapsto x_{n}^{\prime}\\}$.

######  Definition 3 (Shallow Reduction Context)

A shallow reduction context ${\cal C}$ is an expression containing a single
hole $\bullet$ in the place of the redex, which can have one of the two
following possible forms:

${\cal C}::=\bullet~{}e~{}|~{}{\bf case}~{}\bullet~{}{\bf
of}~{}p_{1}\Rightarrow e_{1}\ldots p_{n}\Rightarrow e_{n}$

######  Definition 4 (Evaluation Context)

An evaluation context ${\cal E}$ is represented as a sequence of shallow
reduction contexts (known as a zipper [10]), representing the nesting of these
contexts from innermost to outermost within which the redex is contained. An
evaluation context can therefore have one of the two following possible forms:

${\cal E}::=\langle\rangle~{}|~{}\langle{\cal C}:{\cal E}\rangle$

######  Definition 5 (Insertion into Evaluation Context)

The insertion of an expression $e$ into an evaluation context $\kappa$,
denoted by $\kappa{\bullet e{}}$, is defined as follows:

$\langle\rangle{\bullet e{}}$ | = | $e$
---|---|---
$\langle(\bullet~{}e^{\prime}):\kappa\rangle{\bullet e{}}$ | = | $\kappa{\bullet(e~{}e^{\prime}){}}$
$\langle({\bf case}~{}\bullet~{}{\bf of}~{}p_{1}\Rightarrow e_{1}\ldots
p_{n}\Rightarrow e_{n}):\kappa\rangle{\bullet e{}}$
| = | $\kappa{\bullet({\bf case}~{}e~{}{\bf of}~{}p_{1}\Rightarrow e_{1}\ldots p_{n}\Rightarrow e_{n}){}}$

${\mathcal{N}}_{p}[\\![\mathit{e}]\\!]~{}\Delta{}$ =
${\mathcal{N}}_{e}[\\![\mathit{e}]\\!]~{}\langle\rangle{~{}\Delta{}}$
---
${\mathcal{N}}_{e}[\\![\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}]\\!]~{}\langle\rangle{~{}\Delta{}}$
=
$\mathit{c}~{}({\mathcal{N}}_{e}[\\![\mathit{e_{1}}]\\!]~{}\langle\rangle{~{}\Delta{)\ldots({\mathcal{N}}_{e}[\\![\mathit{e_{n}}]\\!]~{}\langle\rangle{~{}\Delta{)}}}}$
${\mathcal{N}}_{e}[\\![\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}]\\!]~{}\langle({\bf
case}~{}\bullet{~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}^{\prime}}\ldots\mathit{p_{k}}\Rightarrow\mathit{e_{k}^{\prime}})}:\kappa\rangle{~{}\Delta{}}$
=
${\mathcal{N}}_{e}[\\![\mathit{e^{\prime}_{i}\\{x_{1}\mapsto
e_{1},\ldots,x_{n}\mapsto e_{n}\\}}]\\!]~{}\kappa{~{}\Delta{}}$
where $\exists i\in\\{1\ldots
k\\}.\mathit{p_{i}}=\mathit{c}~{}\mathit{x_{1}}\ldots\mathit{x_{n}}$
${\mathcal{N}}_{e}[\\![\lambda\mathit{x}.\mathit{e}]\\!]~{}\langle\rangle{~{}\Delta{}}$
= $\lambda
x.({\mathcal{N}}_{e}[\\![\mathit{e}]\\!]~{}\langle\rangle{~{}\Delta{}})$
${\mathcal{N}}_{e}[\\![\lambda\mathit{x}.\mathit{e}]\\!]~{}\langle(\bullet{~{}\mathit{e^{\prime}}}):\kappa\rangle{~{}\Delta{}}$
= ${\mathcal{N}}_{e}[\\![\mathit{e\\{x\mapsto
e^{\prime}\\}}]\\!]~{}\kappa{~{}\Delta{}}$
${\mathcal{N}}_{e}[\\![f{]\\!]~{}\kappa{~{}\Delta{}}}$ =
${\mathcal{N}}_{e}[\\![\mathit{\lambda x_{1}\ldots
x_{n}.e}]\\!]~{}\kappa{~{}\Delta{}}$
where $(f~{}x_{1}\ldots x_{n}=e)\in\Delta$
${\mathcal{N}}_{e}[\\![\mathit{e_{0}}~{}\mathit{e_{1}}]\\!]~{}\kappa{~{}\Delta{}}$
=
${\mathcal{N}}_{e}[\\![e_{0}{]\\!]~{}\langle(\bullet{~{}\mathit{e_{1}}}):\kappa\rangle{~{}\Delta{}}}$
${\mathcal{N}}_{e}[\\![{\bf case}~{}\mathit{e_{0}}~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}}]\\!]~{}\kappa{~{}\Delta{}}$
=
${\mathcal{N}}_{e}[\\![e_{0}{]\\!]~{}\langle({\bf case}~{}\bullet{~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}}}):\kappa\rangle{~{}\Delta{}}}$
${\mathcal{N}}_{e}[\\![{\bf let}~{}\mathit{x}=\mathit{e_{0}}~{}{\bf
in}~{}\mathit{e_{1}}]\\!]~{}\kappa{~{}\Delta{}}$ =
${\mathcal{N}}_{e}[\\![\mathit{e_{1}\\{x\mapsto
e_{0}\\}}]\\!]~{}\kappa{~{}\Delta{}}$
Figure 3: Language Semantics

######  Definition 6 (Language Semantics)

The normal order reduction semantics for programs in our language is defined
by ${\mathcal{N}}_{p}[\\![\mathit{e}]\\!]~{}\Delta{}$ as shown in Fig. 3,
where $e$ is the expression to be reduced (where it is assumed this contains
no free variables) and $\Delta$ is the function environment.

Within the rules ${\cal N}_{e}$, $\kappa$ denotes the context of the
expression under scrutiny. We always evaluate the redex of an expression
first, with the remainder of the expression given by $\kappa$.

##  3 Process Trees

The output of each of the transformers in our hierarchy are represented by
process trees, as defined in [19]. Within these process trees, the nodes are
labelled with expressions. We write $e\rightarrow t_{1},\ldots,t_{n}$ for a
process tree with root node containing the expression $e$, where
$t_{1},\ldots,t_{n}$ are the sub-trees of this root node. We also write
$e\rightarrow\epsilon$ for a process tree in which the root node has no sub-
trees. We use $root(t)$ to denote the expression in the root node of process
tree $t$. Process trees may also contain three special kinds of node:

  * •

Unfold nodes: these are of the form $h\rightarrow t$, where $h$ is a function
header and $t$ is the process tree resulting from transforming an expression
after unfolding.

  * •

Fold nodes: these are of the form $h\rightarrow\epsilon$, where folding has
been performed with respect to a previous unfold node and the corresponding
function headers are renamings of each other.

  * •

Generalisation nodes: these are of the form $t^{x}$, where the sub-tree $t$
has been generalised to variable $x$.

Within a sub-tree of a process tree, variables in unfold node function
headers, $\lambda$-abstractions and case expressions within ancestor nodes are
bound; all other variables are free. We use $fv(t)$ and $bv(t)$ to denote the
free variables (which includes generalisation variables) and bound variables
of sub-tree $t$ respectively. We denote the application of a renaming $\sigma$
to a process tree $t$ by $t\sigma$, where the renaming $\sigma$ is applied to
all the expressions in the nodes of the process tree.

When transforming an expression with a function in the redex, a level $k+1$
transformer will first transform the expression using a level $k$ transformer.
The resulting process tree is then compared to previously encountered process
trees generated at level $k$. If it is a renaming of a previous one, then
folding is performed, and if it is an embedding of a previous one, then it is
generalised. The use of process trees in this comparison allows us to abstract
away from the number and order of the parameters in functions, and to focus on
their recursive structure. We therefore define renaming, embedding and
generalisation on process trees.

######  Definition 7 (Process Tree Renaming)

Process tree $t$ is a renaming of process tree $t^{\prime}$ if there is a
renaming $\sigma$ and a relation ${\cal S}\subseteq Exp\times Exp$ between the
expressions labelling the corresponding nodes of $t\sigma$ and $t^{\prime}$
such that $t\sigma\cong t^{\prime}$, where the relation $\cong$ is defined as
follows:

1. |  $(h\rightarrow t)\cong(h^{\prime}\rightarrow t^{\prime})$, if $(h,h^{\prime})\in{\cal S}\wedge t\cong t^{\prime}$
---|---
2. |  $(h\rightarrow\epsilon)\cong(h^{\prime}\rightarrow\epsilon)$, if $\exists\sigma.(h\sigma,h^{\prime}\sigma)\in{\cal S}$
3. |  $t_{1}^{x}\cong t_{2}^{x}$, if $t_{1}\cong t_{2}$
4. |  $(\phi(e_{1},\ldots,e_{n})\rightarrow t_{1},\ldots,t_{n})\cong(\phi(e_{1}^{\prime},\ldots,e_{n}^{\prime})\rightarrow t_{1}^{\prime},\ldots,t_{n}^{\prime})$,
|  if
$((\phi(e_{1},\ldots,e_{n}),(\phi(e_{1}^{\prime},\ldots,e_{n}^{\prime}))\in{\cal
S}\wedge\forall i\in\\{1\ldots n\\}.t_{i}\cong t_{i}^{\prime}$

The first rule is for unfold nodes, where the pair of function headers must
belong to ${\cal S}$, and the corresponding sub-trees must be renamings. The
second rule is for fold nodes, where the pair of function headers must be
renamings of a pair of function headers belonging to ${\cal S}$ (from the
corresponding unfold nodes). The third rule is for generalisation nodes, where
the corresponding generalised sub-trees must be renamings. The final rule is
for all other nodes, where the pair of expressions in the corresponding root
nodes must have the same top-level syntactic constructor, and the
corresponding sub-trees must also be renamings. This includes the pathological
case where the nodes have no sub-trees (such as free variables which must have
the same name, and bound variables which must have the same de Bruijn index).

######  Definition 8 (Process Tree Embedding)

Process tree $t$ is embedded in process tree $t^{\prime}$ if there is a
renaming $\sigma$ and a relation ${\cal S}\subseteq Exp\times Exp$ between the
expressions labelling the corresponding nodes of $t\sigma$ and $t^{\prime}$
such that $t\sigma\trianglelefteq t^{\prime}$, where the relation
$\trianglelefteq$ is defined as follows:

1. |  $(h\rightarrow t)\trianglelefteq(h^{\prime}\rightarrow t^{\prime})$, if $(h,h^{\prime})\in{\cal S}\wedge t\trianglelefteq t^{\prime}$
---|---
2. |  $(h\rightarrow\epsilon)\trianglelefteq(h^{\prime}\rightarrow\epsilon)$, if $\exists\sigma.(h\sigma,h^{\prime}\sigma)\in{\cal S}$
3. |  $t_{1}^{x}\trianglelefteq t_{2}^{x}$, if $t_{1}\trianglelefteq t_{2}$
4. |  $(\phi(e_{1},\ldots,e_{n})\rightarrow t_{1},\ldots,t_{n})\trianglelefteq(\phi(e_{1}^{\prime},\ldots,e_{n}^{\prime})\rightarrow t_{1}^{\prime},\ldots,t_{n}^{\prime})$,
|  if
$((\phi(e_{1},\ldots,e_{n}),(\phi(e_{1}^{\prime},\ldots,e_{n}^{\prime}))\in{\cal
S}\wedge\forall i\in\\{1\ldots n\\}.t_{i}\trianglelefteq t_{i}^{\prime}$
5. |  $t\trianglelefteq(e\rightarrow t_{1},\ldots,t_{n})$, if $\exists i\in\\{1\ldots n\\}.t\trianglelefteq t_{i}$

The first three rules are similar to those for the renaming relation $\cong$
for unfold, fold and generalisation nodes respectively. The fourth rule is a
coupling rule, where the pair of expressions in the root nodes must have the
same top-level syntactic constructor and the corresponding sub-trees of the
root nodes must also be related to each other. This includes the pathological
case where the root nodes have no sub-trees (such as free variables which must
have the same name, and bound variables which must have the same de Bruijn
index). The final rule is a diving rule; this relates a process-tree with a
sub-tree of a larger process tree. We write $t\preceq t^{\prime}$ if
$t\trianglelefteq t^{\prime}$ and any rule other than the diving rule can be
applied at the top level.

###### Example 2

Consider the two process trees in Fig. 4 that correspond to the expressions
$\mathit{append}~{}\mathit{xs}~{}(\mathit{Cons}~{}\mathit{x}~{}\mathit{Nil})$
and
$\mathit{append}~{}(\mathit{append}~{}\mathit{xs}~{}(\mathit{Cons}~{}\mathit{x}~{}\mathit{Nil}))~{}(\mathit{Cons}~{}\mathit{y}~{}{}$
$Nil)$ respectively. Process tree (1) is embedded in process tree (2) by the
relation $\preceq$.

(1) |  [.[draw, rounded corners,minimum size=5mm]$\mathit{f}~{}\mathit{x}~{}\mathit{xs}$; [.[draw, rounded corners,minimum size=5mm]${\bf case}~{}\mathit{xs}~{}{\bf of}~{}\mathit{Nil}~{}\Rightarrow\ldots{~{};~{}\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}~{}\Rightarrow\ldots{}}$; [.[draw, rounded corners,minimum size=5mm]$xs$; ] [.[draw, rounded corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{x}~{}\mathit{Nil}$; [.[draw, rounded corners,minimum size=5mm]$\mathit{x}$;] [.[draw, rounded corners,minimum size=5mm]$\mathit{Nil}$;] ] [.[draw, rounded corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{x^{\prime}}~{}\ldots{}$; [.[draw, rounded corners,minimum size=5mm]$\mathit{x^{\prime}}$;] [.[draw, rounded corners,minimum size=5mm]$\mathit{f}~{}\mathit{x}~{}\mathit{xs^{\prime}}$;] ] ] ]
---|---
(2) |  [.[draw, rounded corners,minimum size=5mm]$\mathit{f^{\prime}}~{}\mathit{x}~{}\mathit{y}~{}\mathit{xs}$; [.[draw, rounded corners,minimum size=5mm]${\bf case}~{}\mathit{xs}~{}{\bf of}~{}\mathit{Nil}~{}\Rightarrow\ldots{~{};~{}\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}~{}\Rightarrow\ldots{}}$; [.[draw, rounded corners,minimum size=5mm]$xs$; ] [.[draw, rounded corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{x}~{}(\mathit{Cons}~{}\mathit{y}~{}\mathit{Nil})$; [.[draw, rounded corners,minimum size=5mm]$\mathit{x}$;] [.[draw, rounded corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{y}~{}\mathit{Nil}$; [.[draw, rounded corners,minimum size=5mm]$\mathit{y}$;] [.[draw, rounded corners,minimum size=5mm]$\mathit{Nil}$;] ] ] [.[draw, rounded corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{x^{\prime}}~{}\ldots{}$; [.[draw, rounded corners,minimum size=5mm,distance=1.3cm]$\mathit{x^{\prime}}$;] [.[draw, rounded corners,minimum size=5mm]$\mathit{f^{\prime}}~{}\mathit{x}~{}\mathit{y}~{}\mathit{xs^{\prime}}$;] ] ] ]
Figure 4: Embedded Process Trees

The generalisation of a process tree involves replacing sub-trees with
generalisation variables and creating tree substitutions.

######  Definition 9 (Tree Substitution)

We use the notation $\varphi=\\{x_{1}\mapsto t_{1},\ldots,$ $x_{n}\mapsto
t_{n}\\}$ to denote a tree substitution. If $t$ is an process tree, then
$t\varphi=t\\{x_{1}\mapsto t_{1},\ldots,x_{n}\mapsto t_{n}\\}$ is the result
of simultaneously substituting the sub-trees $t_{1},\ldots,t_{n}$ for the
corresponding variables $x_{1},\ldots,x_{n}$, respectively, in the process
tree $t$ while ensuring that bound variables are renamed appropriately to
avoid name capture.

######  Definition 10 (Generalisation)

The generalisation of two process trees $t$ and $t^{\prime}$ is a triple
$(t_{g},\varphi_{1},\varphi_{2})$ where $\varphi_{1}$ and $\varphi_{2}$ are
tree substitutions such that $t_{g}\varphi_{1}\cong t$ and
$t_{g}\varphi_{2}\cong t^{\prime}$.

######  Definition 11 (The Generalisation Operator $\sqcap$)

The generalisation of two process trees $t$ and $t^{\prime}$, where $t$ and
$t^{\prime}$ are related by $\preceq$, is given by $t\sqcap t^{\prime}$. The
following rewrite rules are repeatedly applied to the initial triple
$(x,\\{x\mapsto t\\},\\{x\mapsto t^{\prime}\\})$, while the process trees
associated with the same variable in each of the tree substitutions are
related by $\preceq$:

$\begin{array}[]{ccc}(t_{g},\\{x\mapsto t_{1}^{x^{\prime}}\\},\\{x\mapsto
t_{2}^{x^{\prime}}\\})&\Rightarrow&(t_{g},\\{x\mapsto t_{1}\\},\\{x\mapsto
t_{2}\\})\\\ \\\ \left(\begin{array}[]{c}t_{g},\\\ \\{x\mapsto(e\rightarrow
t_{1},\ldots,t_{n})\\}\cup\varphi,\\\ \\{x\mapsto(e^{\prime}\rightarrow
t_{1}^{\prime},\ldots,t_{n}^{\prime})\\}\cup\varphi^{\prime}\end{array}\right)&\Rightarrow&\left(\begin{array}[]{c}t_{g}\\{x\mapsto(e\rightarrow
x_{1},\ldots,x_{n})\\},\\\ \\{x_{1}\mapsto t_{1},\ldots,x_{n}\mapsto
t_{n}\\}\cup\varphi,\\\ \\{x_{1}\mapsto t_{1}^{\prime},\ldots,x_{n}\mapsto
t_{n}^{\prime}\\}\cup\varphi^{\prime}\end{array}\right)\end{array}$

In the first rule, if both the process trees related by $\preceq$ have a
generalisation node at the root, then this generalisation is removed. The
second rule adds the root node of one of the process trees that is related by
$\preceq$ into the generalised tree, and new generalisation variables are
added for the corresponding sub-trees of these root nodes. Note that it does
not matter which of the two input process trees the expressions in the
resulting generalised process tree come from, so long as they all come from
one of them (so the corresponding unfold and fold nodes still match); the
resulting generalised program will be the same.

The following rewrite rule is then exhaustively applied to the triple
resulting from the above rewrites to identify common substitutions that were
previously given different names:

$\begin{array}[]{ccc}\left(\begin{array}[]{c}t_{g},\\\ \\{x\mapsto
t,x^{\prime}\mapsto t\\}\cup\varphi,\\\ \\{x\mapsto
t^{\prime},x^{\prime}\mapsto
t^{\prime}\\}\cup\varphi^{\prime}\end{array}\right)&\Rightarrow&\left(\begin{array}[]{c}t_{g}\\{x\mapsto
x^{\prime}\\},\\\ \\{x^{\prime}\mapsto t\\}\cup\varphi,\\\
\\{x^{\prime}\mapsto
t^{\prime}\\}\cup\varphi^{\prime}\end{array}\right)\end{array}$

###### Example 3

The result of generalising the two process trees in Fig. 4 is shown in Fig. 5,
with the mismatched nodes replaced by the generalisation variable $v$.

[.[draw, rounded corners,minimum
size=5mm]$\mathit{f}~{}\mathit{x}~{}\mathit{xs}$; [.[draw, rounded
corners,minimum size=5mm]${\bf case}~{}\mathit{xs}~{}{\bf
of}~{}\mathit{Nil}~{}\Rightarrow\ldots{~{};~{}\mathit{Cons}~{}\mathit{x^{\prime}}~{}\mathit{xs^{\prime}}~{}\Rightarrow\ldots{}}$;
[.[draw, rounded corners,minimum size=5mm]$xs$; ] [.[draw, rounded
corners,minimum size=5mm]$\mathit{Cons}~{}\mathit{x}~{}\mathit{\ldots}$;
[.[draw, rounded corners,minimum size=5mm]$\mathit{x}$;] [.$v$;] ] [.[draw,
rounded corners,minimum
size=5mm]$\mathit{Cons}~{}\mathit{x^{\prime}}~{}\ldots{}$; [.[draw, rounded
corners,minimum size=5mm]$\mathit{x^{\prime}}$;] [.[draw, rounded
corners,minimum size=5mm]$\mathit{f}~{}\mathit{x}~{}\mathit{xs^{\prime}}$;] ]
] ]

Figure 5: Generalised Process Tree

######  Definition 12 (The Generalisation Substitution Operator $\downarrow$)

The operation $\downarrow$ is applied to the triple resulting from
generalisation to make the second tree substitution in the triple explicit
within the generalised process tree:

$\begin{array}[]{c}\downarrow(t_{g},\varphi,\\{x_{1}\mapsto
t_{1},\ldots,x_{n}\mapsto t_{n}\\})=t_{g}\\{x_{1}\mapsto
t_{1}^{x_{1}},\ldots,x_{n}\mapsto t_{n}^{x_{n}}\\}\end{array}$

We now show how a program can be residualised from a process tree.

######  Definition 13 (Residualisation)

A program can be residualised from a process tree $t$ as
${\mathcal{R}}_{p}[\\![\mathit{t}]\\!]~{}\Delta{}$ (where $\Delta$ is the set
of previous function definitions) using the rules as shown in Fig. 6.

${\mathcal{R}}_{p}[\\![\mathit{t}]\\!]~{}\Delta{}$ =
$(\uparrow(e,\theta),\Delta^{\prime})$
---
where
$(e,\theta,\Delta^{\prime})={\mathcal{R}}_{e}[\\![t{]\\!]~{}\\{\\}{~{}\Delta{}}}$
${\mathcal{R}}_{e}[\\![\mathit{h\rightarrow t}]\\!]~{}\rho{~{}\Delta{}}$ =
$(h^{\prime},\theta,\\{h^{\prime}=e\\}\cup\Delta^{\prime})$
where
$\begin{array}[t]{l}{\mathcal{R}}_{e}[\\![\mathit{t}]\\!]~{}(\rho\cup\\{h=h^{\prime}\\}){~{}\Delta{}}=(e,\theta,\Delta^{\prime})\\\
h^{\prime}=f~{}x_{1}\ldots x_{n}~{}(f$ is fresh$,\\{x_{1}\ldots
x_{n}\\}=fv(t))\end{array}$
${\mathcal{R}}_{e}[\\![\mathit{h\rightarrow\epsilon}]\\!]~{}\rho{~{}\Delta{}}$
= $\left\\{\begin{array}[]{ll}(h^{\prime\prime}\sigma,\\{\\},\\{\\}),&$if
$\exists h^{\prime}.(h^{\prime}=h^{\prime\prime})\in\rho\wedge h\equiv
h^{\prime}\sigma\\\ (h,\\{\\},\\{h=e\\}),&$otherwise (where
$(h=e)\in\Delta)\end{array}\right.$
${\mathcal{R}}_{e}[\\![\mathit{e\rightarrow\epsilon}]\\!]~{}\rho{~{}\Delta{}}=(e,\\{\\},\\{\\})$
${\mathcal{R}}_{e}[\\![\mathit{(c~{}e_{1}\ldots e_{n})\rightarrow
t_{1},\ldots,t_{n}}]\\!]~{}\rho{~{}\Delta{}}=(c~{}e_{1}^{\prime}\ldots
e_{n}^{\prime},\bigcup\limits_{i=1}^{n}\theta_{i},\bigcup\limits_{i=1}^{n}\Delta_{i})$
where $\forall i\in\\{1\ldots
n\\}.{\mathcal{R}}_{e}[\\![\mathit{t_{i}}]\\!]~{}\rho{~{}\Delta{}}=(e_{i}^{\prime},\theta_{i},\Delta_{i})$
${\mathcal{R}}_{e}[\\![\mathit{(\lambda x.e)\rightarrow
t}]\\!]~{}\rho{~{}\Delta{}}=(\lambda\mathit{x}.\mathit{e^{\prime}},\theta,\Delta^{\prime})$
where
${\mathcal{R}}_{e}[\\![\mathit{t}]\\!]~{}\rho{~{}\Delta{}}=(e^{\prime},\theta,\Delta^{\prime})$
${\mathcal{R}}_{e}[\\![\mathit{(e_{0}~{}e_{1})\rightarrow
t_{0},t_{1}}]\\!]~{}\rho{~{}\Delta{}}=(e_{0}^{\prime}~{}e_{1}^{\prime},\bigcup\limits_{i=1}^{2}\theta_{i},\bigcup\limits_{i=1}^{2}\Delta_{i})$
where $\forall i\in\\{0\ldots
1\\}.{\mathcal{R}}_{e}[\\![\mathit{t_{i}}]\\!]~{}\rho{~{}\Delta{}}=(e_{i}^{\prime},\theta_{i},\Delta_{i})$
${\mathcal{R}}_{e}[\\![\mathit{({\bf case}~{}e_{0}~{}{\bf
of}~{}p_{1}\Rightarrow e_{1}\ldots p_{n}\Rightarrow e_{n})\rightarrow
t_{0},\ldots,t_{n}}]\\!]~{}\rho{~{}\Delta{}}$ =
$({\bf case}~{}\mathit{e_{0}^{\prime}}~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}^{\prime}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}^{\prime}},\bigcup\limits_{i=0}^{n}\theta_{i},\bigcup\limits_{i=0}^{n}\Delta_{i})$
where $\forall i\in\\{0\ldots
n\\}.{\mathcal{R}}_{e}[\\![\mathit{t_{i}}]\\!]~{}\rho{~{}\Delta{}}=(e_{i}^{\prime},\theta_{i},\Delta_{i})$
${\mathcal{R}}_{e}[\\![\mathit{t^{x}}]\\!]~{}\rho{~{}\Delta{}}$ =
$(x~{}x_{1}\ldots x_{n},\\{x\mapsto\lambda x_{1}\ldots
x_{n}.e\\}\cup\theta,\Delta^{\prime})$
where
${\mathcal{R}}_{e}[\\![\mathit{t}]\\!]~{}\rho{~{}\Delta{}}=(e,\theta,\Delta^{\prime})$
($\\{x_{1}\ldots x_{n}\\}=bv(t)$)
Figure 6: Rules For Residualisation

Within the rules ${\cal R}_{e}$, the parameter $\rho$ contains the unfold node
function headers and the associated new function headers that are created for
them in the residualised program. On encountering an unfold node, a new
function header is created, associated with the unfold node function header,
and added to $\rho$. Note that this new function header may not have the same
variables as the one in the unfold node, as new variables may have been added
to the sub-tree as a result of generalisation. On encountering a fold node, if
it matches a corresponding unfold node, then a recursive call of the function
associated with the unfold node function header in $\rho$ is created.
Otherwise, the fold node function call and its previous definition are used
(this will only occur for process trees produced by our level 0 transformer).
Within the rules ${\cal R}_{e}$, environments $\theta$ and $\Delta$ are
returned in addition to the residual expression. $\theta$ contains the
generalisation variables and their associated extracted values. $\Delta$
contains the set of newly created function definitions. On encountering a
generalisation node, the generalised expression is extracted, added to
$\theta$, and replaced with an application of the generalisation variable. The
extracted expression is abstracted over its bound variables so that these are
not extracted outside their binder. The set of abstracted variables will also
be the arguments in the generalised variable application. The generalisation
environment $\theta$ is converted to lets at the top level using the
generalisation extraction operator $\uparrow$, which is defined as follows.

######  Definition 14 (The Generalisation Extraction Operator $\uparrow$)

The generalisation extraction operator $\uparrow$, where $\uparrow(e,\theta)$
extracts the generalisation environment $\theta$ from the expression $e$ and
is defined as follows:

$\uparrow(e,\\{x_{1}\mapsto e_{1},\ldots,x_{n}\mapsto e_{n}\\})={\bf
let}~{}\mathit{x_{1}}=\mathit{e_{1}}\ldots\mathit{x_{n}}=\mathit{e_{n}}~{}{\bf
in}~{}\mathit{e}$

##  4 A Hierarchy of Program Transformers

In this section, we define our hierarchy of transformers. The level $k$
transformer is defined as
${\mathcal{T}}_{p}^{k}{[\\![\mathit{e}]\\!]~{}\Delta{}}$, where $e$ is the
expression to be transformed and $\Delta$ is the function environment. It is
assumed that the input program contains no $\lambda$-abstractions or let
expressions ($\lambda$-abstractions can be replaced by named functions and let
expressions can be substituted). The output of the transformer is a process
tree from which the transformed program can be residualised.

###  4.1 Level 0 Transformer

Level 0 in our hierarchy essentially corresponds to the identity
transformation, and just converts a term to a corresponding process tree:

${\mathcal{T}}_{p}^{0}{[\\![\mathit{\phi(e_{1},\ldots,e_{n})}]\\!]~{}\Delta{}}=\phi(e_{1},\ldots,e_{n})\rightarrow({\mathcal{T}}_{p}^{0}{[\\![\mathit{e_{1}}]\\!]~{}\Delta{}}),\ldots,({\mathcal{T}}_{p}^{0}{[\\![\mathit{e_{n}}]\\!]~{}\Delta{}})$

The sub-terms of the original term are therefore simply mapped to the
corresponding sub-trees of the resulting process tree.

###  4.2 Level $k+1$ Transformers

Each subsequent level ($k+1$) in our hierarchy is built on top of the previous
levels. The rules for level $k+1$ transformation of programs in our language
are defined by ${\mathcal{T}}_{p}^{k+1}{[\\![\mathit{e}]\\!]~{}\Delta{}}$ as
shown in Fig. 7.

(1) |  ${\mathcal{T}}_{p}^{k+1}{[\\![\mathit{e}]\\!]~{}\Delta{}}$ = ${\mathcal{T}}_{e}^{k+1}{[\\![e{]\\!]~{}\langle\rangle{~{}\\{\\}{~{}\\{\\}{~{}\Delta{}}}}}}$
---|---
(2) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{x~{}x_{1}\ldots x_{n}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = $\begin{array}[t]{l}{\mathcal{T}}_{e}^{\kappa}{[\\![\mathit{t^{x}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}},$ if $x\in dom(\theta)\\\ $where $t={\mathcal{T}}_{e}^{k+1}{[\\![\mathit{\theta(x)~{}x_{1}\ldots x_{n}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta}}}}{}\end{array}$
(3) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{x}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = $x\rightarrow\epsilon$
(4) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{x}]\\!]~{}(\langle({\bf case}~{}\bullet{~{}{\bf of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}})}:\kappa\rangle){~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
${\mathcal{T}}_{\kappa}^{k+1}{[\\![x\rightarrow\epsilon{]\\!]~{}\langle({\bf
case}~{}\bullet{~{}{\bf of}~{}p_{1}{\Rightarrow(\kappa{\bullet
e_{1}{)\\{x{\mapsto p_{1}{\\}\ldots p_{n}{\Rightarrow(\kappa{\bullet
e_{n}{)\\{x{\mapsto
p_{n}{\\})}}}}}}}}}}}:\langle\rangle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}}$
(5) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{x}]\\!]~{}\langle(\bullet{~{}\mathit{e}}):\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = ${\mathcal{T}}_{\kappa}^{k+1}{[\\![x\rightarrow\epsilon{]\\!]~{}\langle(\bullet{~{}\mathit{e}}):\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}}$
(6) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
|
$(\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}})\rightarrow({\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{1}}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}),\ldots,({\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{n}}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}})$
(7) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{c}~{}\mathit{e_{1}}\ldots\mathit{e_{n}}]\\!]~{}\langle({\bf case}~{}\bullet{~{}{\bf of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}^{\prime}}\ldots\mathit{p_{k}}\Rightarrow\mathit{e_{k}^{\prime}})}:\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
|  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e^{\prime}_{i}\\{x_{1}\mapsto
e_{1},\ldots,x_{n}\mapsto
e_{n}\\}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$
|  where $\exists i\in\\{1\ldots
k\\}.\mathit{p_{i}}=\mathit{c}~{}\mathit{x_{1}}\ldots\mathit{x_{n}}$
(8) | ${\mathcal{T}}_{e}^{k+1}{[\\![\lambda\mathit{x}.\mathit{e_{0}}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}=(\lambda\mathit{x}.\mathit{e_{0}})\rightarrow({\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{0}}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}})$
(9) | ${\mathcal{T}}_{e}^{k+1}{[\\![\lambda\mathit{x}.\mathit{e_{0}}]\\!]~{}\langle(\bullet{~{}\mathit{e_{1}}}):\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}={\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{0}\\{x\mapsto e_{1}\\}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$
(10) | ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{f}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}=\begin{array}[t]{l}\left\\{\begin{array}[m]{l}h\sigma\rightarrow\epsilon,\hfill$ if $\exists(h=t^{\prime})\in\rho,\sigma.t^{\prime}\sigma\cong t\\\ {\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta^{\prime}{}}}}},\hfill$ if $\exists(h=t^{\prime})\in\rho,\sigma.t^{\prime}\sigma\preceq t\\\ $where $\begin{array}[t]{l}(e,\Delta^{\prime})={\mathcal{R}}_{p}[\\![\mathit{\downarrow(t^{\prime}\sigma\sqcap t)}]\\!]~{}\Delta{}\end{array}\\\ h^{\prime}\rightarrow{\mathcal{T}}_{e}^{k+1}{[\\![\mathit{\lambda x_{1}\ldots x_{n}.e}]\\!]~{}\kappa{~{}(\rho\cup\\{h^{\prime}=t\\}){~{}\theta{~{}\Delta{}}}}},\hfill$otherwise$\\\ $where $\begin{array}[t]{l}(f~{}x_{1}\ldots x_{n}=e)\in\Delta\\\ h^{\prime}=f^{\prime}~{}x_{1}^{\prime}\ldots x_{k}^{\prime}$ ($f^{\prime}$ is fresh, $\\{x_{1}^{\prime}\ldots x_{k}^{\prime}\\}=fv(t))\end{array}\end{array}\right.\\\ $where $t={\mathcal{T}}_{p}^{k}{[\\![\kappa{\bullet\mathit{f}]\\!]~{}\Delta}}{}\end{array}$
(11) |  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{0}}~{}\mathit{e_{1}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{0}}]\\!]~{}\langle(\bullet{~{}\mathit{e_{1}}}):\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$
(12) |  ${\mathcal{T}}_{e}^{k+1}{[\\![{\bf case}~{}\mathit{e_{0}}~{}{\bf of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
|  ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{0}}]\\!]~{}\langle({\bf
case}~{}\bullet{~{}{\bf
of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}}}):\kappa\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$
(13) |  ${\mathcal{T}}_{e}^{k+1}{[\\![{\bf let}~{}\mathit{x}=\mathit{e_{0}}~{}{\bf in}~{}\mathit{e_{1}}]\\!]~{}\kappa{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = ${\mathcal{T}}_{e}^{k+1}{[\\![\mathit{e_{1}}]\\!]~{}\kappa{~{}\rho{~{}(\theta\cup\\{x\mapsto e_{0}\\}){~{}\Delta{}}}}}$
(14) |  ${\mathcal{T}}_{\kappa}^{k+1}{[\\![\mathit{t}]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}$ = $t$
(15) |  ${\mathcal{T}}_{\kappa}^{k+1}{[\\![\mathit{t}]\\!]~{}(\kappa=\langle(\bullet~{}e):\kappa^{\prime}\rangle){~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
|  ${\mathcal{T}}_{\kappa}^{k+1}{[\\![(\kappa{\bullet root(t){}})\rightarrow
t,({\mathcal{T}}_{e}^{k+1}{[\\![e{]\\!]~{}\langle\rangle{~{}\rho{~{}\theta{~{}\Delta{}}}}}}){]\\!]~{}\kappa^{\prime}{~{}\rho{~{}\theta{~{}\Delta{}}}}}}$
(16) |  ${\mathcal{T}}_{\kappa}^{k+1}{[\\![\mathit{t}]\\!]~{}(\kappa=\langle({\bf case}~{}\bullet{~{}{\bf of}~{}\mathit{p_{1}}\Rightarrow\mathit{e_{1}}\ldots\mathit{p_{n}}\Rightarrow\mathit{e_{n}})}:\kappa^{\prime}\rangle){~{}\rho{~{}\theta{~{}\Delta{}}}}}$ =
|  $(\kappa{\bullet root(t){}})\rightarrow
t,({\mathcal{T}}_{e}^{k+1}{[\\![e_{1}{]\\!]~{}\kappa^{\prime}{~{}\rho{~{}\theta{~{}\Delta{}}}}}}),\ldots,({\mathcal{T}}_{e}^{k+1}{[\\![e_{n}{]\\!]~{}\kappa^{\prime}{~{}\rho{~{}\theta{~{}\Delta{}}}}}})$
Figure 7: Level $k+1$ Transformation Rules

Within the rules ${\cal T}_{e}^{k+1}$, $\kappa$ denotes the context of the
expression under scrutiny, $\rho$ contains memoised process trees and their
associated new function headers, and $\theta$ gives the let variables and
their associated values. For most of the level $k+1$ transformation rules,
normal order reduction is applied to the current term, as for the semantics
given in Fig. 3.

In rule (10), if the redex of the current term is a function, then it is
transformed by the transformer one level lower in the hierarchy (level $k$)
producing a process tree; this is therefore where the transformer builds on
all the transformers at lower levels. This level $k$ process tree is compared
to the previous process trees produced at level $k$ (contained in $\rho$). If
the process tree is a renaming of a previous one, then folding is performed,
and a fold node is created using a recursive call of the function associated
with the previous process tree in $\rho$. If the process tree is an embedding
of a previous one, then generalisation is performed; the result of this
generalisation is then residualised and further transformed. Otherwise, the
current process tree is memoised by being associated with a new function call
in $\rho$; an unfold node is created with this new function call in the root
node, with the result of transforming the unfolding of the current term as its
sub-tree.

In rule (7), if the context surrounding a constructor application redex is a
case, then pattern matching is performed and the appropriate branch of the
case is selected, thus removing the constructor application. This is where our
transformers actually remove intermediate data structures.

In rule (4), if the context surrounding a variable redex is a case, then
information is propagated to each branch of the case to indicate that this
variable has the value of the corresponding branch pattern.

In rule (13), a let variable is associated with its value in the environment
$\theta$ and the let is removed. In rule (2), if one of these let variables is
subsequently encountered, then it is replaced with a generalisation node; the
original term generalisation is therefore replaced by a tree generalisation.

The rules ${\cal T}_{\kappa}^{k+1}$ are defined on a process tree and a
surrounding context. These rules are applied when the normal-order reduction
of the input program becomes ‘stuck’ as a result of encountering a variable in
the redex position. In this case, the surrounding context is further
transformed.

##  5 Termination

In order to prove that each of the transformers in our hierarchy terminate, we
need to show that in any infinite sequence of process trees encountered during
transformation $t_{0},t_{1},\ldots$ there definitely exists some $i<j$ where
$t_{i}\preceq t_{j}$, so an embedding must eventually be encountered and
transformation will not continue indefinitely without folding or generalising.
This amounts to proving that the embedding relation $\preceq$ is a well-quasi
order.

######  Lemma 1 ($\preceq$ is a Well-Quasi Order)

The embedding relation $\preceq$ is a well-quasi order on any sequence of
process trees that are encountered during transformation at level $k>0$ in our
hierarchy.

###### Proof

The proof is by induction on the hierarchy level $k$.

For level 1, the proof is similar to that given in [12]. This involves showing
that there are a finite number of functors (function names and constructors)
in the language. The process trees encountered during transformation are those
produced at level 0, so the function names will be those from the original
program, so must be finite. Applications of different arities are replaced
with separate constructors; we prove that arities are bounded, so there are a
finite number of these. We also replace case expressions with constructors.
Since bound variables are defined using de Bruijn indices, each of these are
replaced with separate constructors; we also prove that de Bruijn indices are
bounded. The overall number of functors is therefore finite, so Kruskal’s tree
theorem can then be applied to show that $\preceq$ is a well-quasi-order at
level 1 in our hierarchy.

At level $k+1$, the process trees encountered during transformation are those
produced at level $k$ and must be finite (by the inductive hypothesis). The
number of functions in these process trees must therefore be finite, and the
same argument given above for level 1 also applies here, so $\preceq$ is a
well-quasi-order at level $k+1$ in our hierarchy.

Since we only check for embeddings for process trees resulting from the
transformation of expressions which have a named function as redex, we need to
show that every potentially infinite sequence of expressions encountered
during transformation must include expressions of this form.

######  Lemma 2 (Function Unfolding During Transformation)

Every infinite sequence of transformation steps must include function
unfolding.

###### Proof

Every infinite sequence of transformation steps must include either function
unfolding or $\lambda$-application. Since we do not allow
$\lambda$-abstractions in our input program, the only way in which new
$\lambda$-abstractions can be introduced is by function unfolding. Thus, every
infinite sequence of transformation steps must include function unfolding.

######  Theorem 5.1 (Termination of Transformation)

The transformation algorithm always terminates.

###### Proof

The proof is by contradiction. If the transformation algorithm did not
terminate, then the set of memoised process trees in $\rho$ must be infinite.
Every new process tree which is added to $\rho$ cannot have any of the
previous process trees in $\rho$ embedded within it by the homeomorphic
embedding relation $\preceq$, since generalisation would have been performed
instead. However, this contradicts the fact that $\preceq$ is a well-quasi-
order (Lemma 1).

##  6 Speedups

In this section, we look at the efficiency gains that can be obtained at
different levels in our program transformation hierarchy.

######  Theorem 6.1 (Exponential Speedups)

Exponential speedups can only be obtained above level 0 in our hierarchy if
common sub-expression elimination is performed during generalisation.

###### Proof

An exponential speedup can only be obtained if the number of recursive calls
of a function is reduced. This can only happen if some of these recursive
calls are identified by common sub-expression elimination.

###### Example 4

Consider the following program from [4]:

$\begin{array}[t]{lcl}\lx@intercol\mathit{f}~{}\mathit{x}~{}\mathit{x}\hfil\lx@intercol\\\
\lx@intercol{\bf where}\hfil\lx@intercol\\\
\mathit{f}~{}\mathit{x}~{}\mathit{y}&=&\\!\begin{array}[t]{llcl}\lx@intercol{\bf
case}~{}\mathit{x}~{}{\bf of}\hfil\lx@intercol\\\
&\mathit{Zero}&\Rightarrow&\mathit{y}\\\
{}{}{}{}&\mathit{Succ(x)}&\Rightarrow&\mathit{f}~{}(\mathit{f}~{}\mathit{x}~{}\mathit{x})~{}(\mathit{f}~{}\mathit{x}~{}\mathit{x})\end{array}{}\end{array}$

This program takes exponential time $O(2^{n})$, where $n$ is the size of the
variable $x$. During transformation at level 1 in our hierarchy, the process
tree corresponding to $(f~{}x~{}x)$ is extracted twice, but then identified by
common sub-expression elimination to obtain the following program:

$\begin{array}[t]{lcl}\lx@intercol\mathit{f^{\prime}}~{}\mathit{x}\hfil\lx@intercol\\\
\lx@intercol{\bf where}\hfil\lx@intercol\\\
\mathit{f^{\prime}}~{}\mathit{x}&=&\\!\begin{array}[t]{llcl}\lx@intercol{\bf
case}~{}\mathit{x}~{}{\bf of}\hfil\lx@intercol\\\
&\mathit{Zero}&\Rightarrow&\mathit{Zero}\\\
{}{}{}{}&\mathit{Succ(x)}&\Rightarrow&\mathit{f^{\prime}}~{}(\mathit{f^{\prime}}~{}\mathit{x})\end{array}{}\end{array}$

This program takes linear time $O(n)$ on the same input, so an exponential
speedup has been achieved. In practice we have found that such exponential
improvements are obtained for very few useful programs; it is very unlikely
that a programmer would write such an inefficient program when a much better
solution exists.

We now look at the improvements in efficiency that can be obtained without
common sub-expression elimination.

######  Theorem 6.2 (Non-Exponential Speedups)

Without the use of common sub-expression elimination, the maximum speedup
factor possible at level $k>0$ in our hierarchy for input of size $n$ is
$O(n^{k-1})$.

###### Proof

The proof is by induction on the hierarchy level $k$. For level 1, the proof
is as given in [18]; since there can only be a constant number of reduction
steps removed between each successive call of a function, at most a linear
speedup is possible. For level $k+1$, there will be a constant number of calls
to functions that were transformed at level $k$ between each successive call
of a level $k+1$ function. By the inductive hypothesis, the maximum speedup
factor for each level $k$ function is $O(n^{k-1})$, so the maximum speedup
factor at level $k+1$ is $O(n^{k})$.

###### Example 5

Consider the transformation of the naïve reverse program shown in Fig. 1,
which has $O(n^{2})$ runtime. If this program is transformed at level 1 in our
hierarchy, then no improvements are obtained. However, if we transform this
program at level 2 in our hierarchy, we end up having to transform a term
equivalent to the following at level 1:

$\mathit{append}~{}(\mathit{append}~{}\mathit{xs}~{}(\mathit{Cons}~{}\mathit{x}~{}\mathit{Nil}))~{}(\mathit{Cons}~{}\mathit{y}~{}\mathit{Nil})$

Within this term, the list $xs$ has to be traversed twice. This term is
transformed to one equivalent to the following at level 1 (process tree (2) in
Fig. 4 is the process tree produced as a result of this transformation):

$\mathit{append}~{}\mathit{xs}~{}(\mathit{Cons}~{}\mathit{x}~{}(\mathit{Cons}~{}\mathit{y}~{}\mathit{Nil}))$

Within this term, the list $xs$ has only to be traversed once, so a linear
speedup has been obtained. This linear improvement will be made between each
successive call of the naïve reverse function, thus giving an overall
superlinear speedup and producing the accumulating reverse program as shown in
Fig. 1.

Although it appears that more and more efficiency improvements will be made as
we move up our transformation hierarchy, in practice it is found that not many
efficiency improvements are made beyond level 2, as it is unlikely that a
programmer would write programs that are so inefficient that speedup factors
greater than $O(n)$ are possible.

##  7 Conclusion and Related Work

We have presented a hierarchy of program transformers in which the transformer
at each level of the hierarchy builds on top of those at lower levels. We have
proved that the transformers at each level in the hierarchy terminate, and
have characterised the speedups that can be obtained at each level. Previous
works [14, 2, 1, 25, 18] have noted that the unfold/fold transformation
methodology is incomplete; some programs cannot be synthesised from each
other. It is our hope that this work will help to overcome this restriction.

The seminal work corresponding to level 1 in our hierarchy is that of Turchin
on supercompilation [21], although our level 1 transformer more closely
resembles positive supercompilation [20]. There have been several previous
attempts to move beyond level 1 in our transformation hierarchy, the first one
by Turchin himself using walk grammars [22]. In this approach, traces through
residual graphs are represented by regular grammars that are subsequently
analysed and simplified. This approach is also capable of achieving
superlinear speedups, but no automatic procedure is defined for it; the
outlined heuristics and strategies may not terminate.

A hierarchy of program specialisers is described in [5] that shows how
programs can be metacoded and then manipulated through a metasystem
transition, with a number of these metasystem transitions giving a metasytem
hierarchy in which the original program may have several levels of metacoding.
In the work described here, a process tree can be considered to be the
metacoding of a program. However, we do not have the difficulties associated
with metasystem transitions and muli-level metacoding, as our process trees
are residualised back to the object level.

Distillation [7, 9] is built on top of positive supercompilation, so
corresponds to level 2 in our hierarchy, but does not go beyond this level.
Klyuchnikov and Romanenko [13] construct a hierarchy of supercompilers in
which lower level supercompilers are used to prove lemmas about term
equivalences, and higher level supercompilers utilise these lemmas by
rewriting according to the term equivalences (similar to the “second order
replacement method” defined by Kott [15]). Transformers in this hierarchy are
capable of similar speedups to those in our hierarchy, but no automatic
procedure is defined for it; the need to find and apply appropriate lemmas
introduces infinite branching into the search space, and various heuristics
have to be used to try to limit this search. Preliminary work on the hierarchy
of transformers defined here was presented in [8]; this did not include
analysis of the efficiency improvements that can be made at each level in the
hierarchy. The work described here is a lot further developed than that
described in [8], and we hope simpler and easier to follow.

Logic program transformation is closely related, and the equivalence of
partial deduction and driving (as used in supercompilation) has been argued by
Glück and Sørensen [6]. Superlinear speedups can be achieved in logic program
transformation by goal replacement [16, 17]: replacing one logical clause with
another to facilitate folding. Techniques similar to the notion of “higher
level supercompilation” [13] have been used to prove correctness of goal
replacement, but have similar problems regarding the search for appropriate
lemmas.

## Acknowledgements

This work owes a lot to the input of Neil D. Jones, who provided many useful
insights and ideas on the subject matter presented here.

## References

  * [1] Amtoft, T.: Sharing of Computations. Ph.D. thesis, DAIMI, Aarhus University (1993)
  * [2] Andersen, L.O., Gomard, C.K.: Speedup Analysis in Partial Evaluation: Preliminary Results. In: ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation. pp. 1–7 (1992)
  * [3] Burstall, R., Darlington, J.: A transformation system for developing recursive programs. Journal of the ACM 24(1), 44–67 (Jan 1977)
  * [4] Glück, R., Klimov, A., Nepeivoda, A.: Non-linear configurations for superlinear speedup by supercompilation. In: Proceedings of the Fifth International Workshop on Metacomputation in Russia (2016)
  * [5] Glück, R., Hatcliff, J., Jørgensen, J.: Generalization in Hierarchies of Online Program Specialization Systems. In: Workshop on Logic-Based Program Synthesis and Transformation. pp. 179–198 (1998)
  * [6] Glück, R., Jørgensen, J.: Generating Transformers for Deforestation and Supercompilation. In: Proceedings of the Static Analysis Symposium. Lecture Notes in Computer Science, vol. 864, pp. 432–448. Springer-Verlag (1994)
  * [7] Hamilton, G.W.: Distillation: Extracting the Essence of Programs. In: Proceedings of the ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation. pp. 61–70 (2007)
  * [8] Hamilton, G.W.: A Hierarchy of Program Transformers. In: Proceedings of the Second International Workshop on Metacomputation in Russia (2012)
  * [9] Hamilton, G.W., Jones, N.D.: Distillation with labelled transition systems. In: Proceedings of the ACM Workshop on Partial Evaluation and Program Manipulation. pp. 15–24. ACM (2012)
  * [10] Huet, G.: The Zipper. Journal of Functional Programming 7(5), 549–554 (1997)
  * [11] Jones, N.D., Gomard, C.K., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall (1993)
  * [12] Klyuchnikov, I.: Supercompiler HOSC 1.1: Proof of Termination. Preprint 21, Keldysh Institute of Applied Mathematics, Moscow (2010)
  * [13] Klyuchnikov, I.: Towards Higher-Level Supercompilation. In: Proceedings of the Second International Workshop on Metacomputation in Russia. pp. 82–101 (2010)
  * [14] Kott, L.: A System for Proving Equivalences of Recursive Programs. In: 5th Conference on Automated Deduction. pp. 63–69 (1980)
  * [15] Kott, L.: Unfold/Fold Transformations. In: Nivat, M., Reynolds, J. (eds.) Algebraic Methods in Semantics, chap. 12, pp. 412–433. CUP (1985)
  * [16] Pettorossi, A., Proietti, M.: A Theory of Totally Correct Logic Program Transformations. In: Proceedings of the ACM SIGPLAN Workshop on Partial Evaluation and Semantics-Based Program Manipulation (PEPM). pp. 159–168 (2004)
  * [17] Roychoudhury, A., Kumar, K., Ramakrishnan, C., Ramakrishnan, I.: An Unfold/Fold Transformation Framework for Definite Logic Programs. ACM Transactions on Programming Language Systems 26(3), 464–509 (2004)
  * [18] Sørensen, M.H.: Turchin’s Supercompiler Revisited. Master’s thesis, Department of Computer Science, University of Copenhagen (1994), dIKU-rapport 94/17
  * [19] Sørensen, M.H., Glück, R.: An Algorithm of Generalization in Positive Supercompilation. Lecture Notes in Computer Science 787, 335–351 (1994)
  * [20] Sørensen, M.H., Glück, R., Jones, N.D.: A Positive Supercompiler. Journal of Functional Programming 6(6), 811–838 (1996)
  * [21] Turchin, V.F.: The Concept of a Supercompiler. ACM Transactions on Programming Languages and Systems 8(3), 90–121 (Jul 1986)
  * [22] Turchin, V.F.: Program Transformation With Metasystem Transitions. ACM Transactions on Programming Languages and Systems 3(3), 283–313 (1993)
  * [23] Wadler, P.: The Concatenate Vanishes (Dec 1987), fP Electronic Mailing List
  * [24] Wadler, P.: Deforestation: Transforming Programs to Eliminate Trees. Lecture Notes in Computer Science 300, 344–358 (1988)
  * [25] Zhu, H.: How Powerful are Folding/Unfolding Transformations? Journal of Functional Programming 4(1), 89–112 (1994)