% setenv TEXINPUTS :.:
\documentclass[preprint,natbib]{sigplanconf}

\newcommand{\mkw}[1]{\mbox{\fontfamily{cmr}\fontseries{b}\selectfont#1}}
\newcommand{\kw}[1]{\mbox{\texttt{#1}}}

\newcommand{\LET}{\kw{let}\,}
\newcommand{\MLET}{\mkw{let}\,}
\newcommand{\LETREC}{\kw{letrec}\,}
\newcommand{\IN}{\,\kw{in}\,}
\newcommand{\MIN}{\mkw{in}\,}
\newcommand{\CASE}{\kw{case}\,}
\newcommand{\OF}{\,\kw{of}\,}

\newcommand{\B}{\mathcal{B}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\R}{\mathcal{R}}
\newcommand{\G}{\mathcal{G}}
\newcommand{\N}{\mathcal{N}}
\newcommand{\I}{\mathcal{I}}
\newcommand{\D}{\mathcal{D}}

\newcommand{\alt}{\;\:\vert\;\:}
\newcommand{\arr}{\rightarrow}
\newcommand{\homemb}{\trianglelefteq}
\newcommand{\fv}{\mbox{\it fv}}
\newcommand{\acceptable}{\mbox{\it acceptable}}
\newcommand{\normalize}{\mbox{\it normalize}}
\newcommand{\fn}{\mbox{\it fn}}

\newcommand{\econ}[1]{[{#1}]\E}
\newcommand{\con}[1]{[{#1}]\R}
\newcommand{\conp}[1]{[{#1}]\R'}
\newcommand{\conb}[1]{[{#1}]\R''}
\newcommand{\eval}{\mapsto}

\newcommand{\asdr}{\D_{app}\((\)}
\newcommand{\axsdr}{\D_{varapp}\((\)}
\newcommand{\sdr}{\D\(\llbracket\)}
\newcommand{\edr}{\(\rrbracket\)}
\newcommand{\aedr}{\()\)}
\newcommand{\adr}[3]{\D_{app}({#1})\,\rho\,{#2}\,\sigma\,{#3}}
\newcommand{\axdr}[3]{\D_{varapp}({#1})\,\rho\,{#2}\,\sigma\,{#3}}
\newcommand{\dr}[3]{\D\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma\,{#3}}
\newcommand{\drs}[2]{\D\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma_1\,s}
\newcommand{\drsi}[2]{\D\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma_i\,s_i}
\newcommand{\drss}[3]{\D\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma_{i-1}\,{#3}}
% \newcommand{\drg}[2]{\D\llbracket {#1} \rrbracket_{\mathcal{F}',\rho}\,{#2}\,\sigma}
\newcommand{\drp}[2]{\D\llbracket {#1} \rrbracket\,\rho'\,{#2}\,\sigma}
\newcommand{\drl}[2]{\D_{let}\llbracket {#1} \rrbracket\,\rho,{#2}\,\R\,\sigma}
% \newcommand{\drlg}[2]{\D_{let}\llbracket {#1} \rrbracket_{\mathcal{F}',\rho,{#2}}\,\R\,\sigma}
\newcommand{\er}[3]{\B\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma\,{#3}}
\newcommand{\ers}[3]{\B\llbracket {#1} \rrbracket\,\rho\,{#2}\,\sigma_1\,{#3}}
\newcommand{\erss}[4]{\B\llbracket {#1} \rrbracket\,\rho\,{#2}\,{#3}\,{#4}}

\newcommand{\eqdef}{\overset{\text{\tiny def}}{=}}
\usepackage{amsmath, amsthm}
\usepackage{amssymb}
\usepackage{stmaryrd}
\usepackage{haskell}
\usepackage{url}
\usepackage{undertilde}
\usepackage{proof}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{definition}[theorem]{Definition}
\newtheorem{example}[theorem]{Example}
\newtheorem{prop}[theorem]{Proposition}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{corollary}[theorem]{Corollary}

\newcommand{\costrighteq}{\trianglerighteq}

\newcommand{\mpar}[1] % \marginpar with surounding box{\scriptsize }
{\marginpar{\scriptsize{#1}}}
\newcommand{\hrr}[1] % \hr tagged with a remark                                 
   {\par\noindent\hrulefill\\~\emph{#1}\par\noindent\hrulefill}         
\newcommand{\fixme}[1]{\hrr{{\bf FIXME}: #1}}
\newcommand{\note}[1]{\hrr{{\bf NOTE}: #1}}


\begin{document}


\conferenceinfo{Conf}{date, City.} 
\copyrightyear{2009} 
\copyrightdata{[to be supplied]} 

\titlebanner{Draft: \today}        % These are ignored unless
\preprintfooter{short description of paper}   % 'preprint' option specified.

\title{Taming Code Explosion in Supercompilation}

\authorinfo{Peter A. Jonsson \and Johan Nordlander}
           {Lule{\aa} University of Technology}
           {\{pj, nordland\}@csee.ltu.se}

\maketitle
\begin{abstract}
  Supercompilation algorithms can perform great optimizations but
  sometimes suffer from the problem of code explosion. This results in
  huge binaries which might hurt the performance on a
  modern processor. We present a supercompilation algorithm that is
  fast enough to speculatively supercompile expressions and discard
  the result if it turned out bad. This allows us to supercompile
  large parts of the imaginary and spectral parts of nofib in a matter
  of seconds while keeping the binary size increase below 5\%.
\end{abstract}

\category{D.3.4}{Programming Languages}{Processors -- Compilers,
  Optimization}
\category{D.3.2}{Programming Languages}{Language Classifications --
  Applicative (functional) languages}

\terms
Languages, Theory

\keywords
supercompilation, deforestation, Haskell


\section{Introduction}
Supercompilation  is an automatic program transformation that subsumes several program transformations which are available in production compilers \citep{Turchin:1986:TheConcept}. It is well known that the transformation is correct \citep{Sands:1996:Proving} and terminates \citep{Soerensen:2000:Convergence}. We also know that supercompilation gives remarkable optimization results on small examples: a textbook example of word counting in Haskell performs better than a low level implementation written in C \citep{Mitchell:2008:ASupercompiler}. 

Given these accomplishments, why does not your favorite compiler include a supercompiler? The two main problems are scalability of the supercompiler and the risk for code explosion. Existing implementations of supercompilers trade compilation time against great optimization and do not take the resulting program size into account. Closer investigation reveals that it is the test for non-termination, the homeomorphic embedding, that takes up to 50\% of the transformation time \citep{Mitchell:2008:ASupercompiler}. We suggest sacrificing some optimization in exchange for faster compilation by revising the design of the supercompilation algorithm. 

The faster algorithm allows us to control code explosion by
speculatively supercompile expressions and discard bad results. Even
incredibly cheap and simple tests can get a long way towards the goal: a
surprising discovery is that comparing the number of syntactic nodes
of the resulting expression with a well-chosen constant is a
remarkably accurate predictor of ``bad optimizations'' that should be
discarded. Except this size threshold our measurements use a simple
comparison of the size of the resulting expression versus the number
of reduction steps performed by the supercompiler.

The performance of our algorithm rests on two important design choices:
\begin{description}
\item[Term Representation:] We represent terms as zippers \citep{Huet:1997:Zipper} during the transformation, which gives efficient and convenient implementations of tests for non-termination and splitting of terms. As a side effect this representation also makes it easy to reduce the number of terms to test for non-termination: only test against those terms who have the same head as the current term.
\item[Term Size in Focus:] By decreasing the size of the term that our supercompiler focuses on we can effectively decrease the cost of testing for non-termination. This shows in our compilation times: they are less than 3 seconds on a modern desktop computer for all the small examples from the nofib suite \citep{Partain:1992:nofib}.
\end{description}


% XXX: Give a characterization of what optimization we sacrifice.

% XXX: Should we  mention about the complexity of the HE? % The cost of testing two terms, {\it m} and {\it n}, against each-other for non-termination is $O(sizeof(m)\times sizeof(n))$ \citep{Narendran:1987:On}. 

Our design allows us to supercompile most programs from the spectral part of nofib in less than three seconds. Some of these programs are 10 times larger than previously supercompiled Haskell programs. We do not believe that an ordinary programmer will turn on the supercompiler for his development builds, but it is certainly reasonable to do so for testing and nightly builds.


Our contributions are:

\begin{itemize}
\item A mechanism that is parametric with respect to a metric that allows us to control code explosion (Section \ref{sec:discexp1} and Section \ref{sec:discexp2}). 
\item A practical supercompilation algorithm (Section \ref{sec:scp})

\item Measurements on the imaginary and spectral parts of nofib (Section \ref{sec:measurements}).
\item Implementation tricks to speed up the actual implementation (Section \ref{sec:impl}).
\end{itemize}

\section{Language}
\label{sec:lang}
Our language of study is a higher-order functional language with let-bindings, case-expressions and primitive values.  Its syntax for expressions,
values and patterns is shown in Figure \ref{fig:language}.

\begin{figure}
\begin{tabular}{lll}
\multicolumn{3}{l}{Expressions} \\ \hline \\
  $e$ &::= & $n \alt x \alt F \alt K \alt e\,e'
      \alt  \lambda x.e \alt e
      \oplus  e'$ \\ %\alt

 &  $\alt$ &      $\CASE e \,\OF \, \{ p_i \arr e_i \} \alt \LET x = e\, \IN e' $ \\ 
\\
$p$ &::=& $n \alt K\, \overline{x}$ \\
\\
\multicolumn{3}{l}{Weak Head Normal Form} \\ \hline \\
  $w$ &::= & $n \alt \lambda x.e
    \alt K \, \overline{e}$ \\%   \alt \{ l_i = v_i \}$ & \\
\end{tabular}  
\caption{The language}
\label{fig:language}
\end{figure}

Let {\em F} range over a set $\mathcal{F}$ of global function definitions, where all functions have a specific arity and contain no free variables. This is not a severe restriction on the programmer since the input can be lambda lifted  \citep{Johnsson:1985:Lambda}. 

The language contains integer values $n$ and arithmetic operations $\oplus$, although these meta-variables can preferably be understood as ranging over primitive values in general and arbitrary operations on these. We let $+$ denote the semantic meaning of $\oplus$.

A list of expressions $e_1 \ldots
e_n$ is abbreviated as $\overline{e}$, and a list of variables $x_1 \ldots x_n$ as
$\overline{x}$.


We denote the free variables of an expression {\em e} by $\fv(e)$ and a program is an expression with no free variables and all function names defined in $\mathcal{F}$. The operational semantics is call-by-name as defined in Figure \ref{fig:redsem}. Capture free substitution expressions $\overline{e}$ for variables $\overline{x}$ in $e'$ is denoted by $[\overline{e}/\overline{x}]e'$.

\begin{figure}
\begin{tabular}{lll}
\multicolumn{3}{l}{Reduction contexts} \\ \hline \\
$\E$  &::= & 
      $\boxempty
      \alt            \E\, e
  \alt \E \oplus e \alt n \oplus \E 
        \alt  \CASE\, \E \, \OF \, \{ p_i \arr e_i \} $   \\
\\
\end{tabular} \\
\begin{tabular}{lllr}
\multicolumn{4}{l}{Evaluation relation} \\ \hline \\
$\econ{F}$ & $\eval$ & $\econ{e}$, if $F \eqdef e$   & (Global) \\
$\econ{(\lambda x.e) \,e'}$ & $\eval$ & $\econ{[e'/x]e}$ &  (Beta) \\
$\econ{\LET x=e \IN e'}$ & $\eval$ & $\econ{[e/x]e'}$ & (Let) \\
 $\econ{\CASE K \, \overline{e} \OF \, \{ K_i\,\overline{x}_i \arr e_i \}}\!\!\!\!\!$ & $\eval$ & $\econ{[\overline{e}/\overline{x}_j]e_j}$ & (KCase) \\
& & if $K = K_j$  \\
$\econ{\CASE n \OF \,\{ n_i \arr e_i \} }$ & $\eval$ & $\econ{e_j}$ & (NCase) \\
& &if $n = n_j$ \\
 $\econ{n_1 \oplus n_2}$ & $\eval$ & $\econ{n}$ & (Arith) \\
& & if $n = n_1 + n_2$  \\
\end{tabular}
\caption{Reduction semantics}
\label{fig:redsem}
\end{figure}

A reduction context $\E$ is a term containing a single hole $\boxempty$,
which indicates the next expression to be reduced. The expression
$\econ{e}$ is the term obtained by replacing the hole in $\E$ with
$e$. 


\section{Design Choices}

This section describes a number of important design choices and how
they contribute to our goal of making a practical supercompiler for
program optimization. These choices should be straightforward to
transfer to other more powerful supercompilers. 

Our guiding principle has been simple: sacrifice optimization
opportunities if it significantly improves the performance or
simplifies the implementation of the supercompiler. Our only concern
is soundness of the supercompiler, we do not have to worry about
completeness properties that could be important in theorem proving or
similar domains.

There is some overlap between what problem each design choice helps to
protect against. 
\begin{description}
\item[Code Explosion] The primary mechanism to tame code explosion is
described in Section \ref{sec:discexp1}. Section \ref{sec:boring},
Section \ref{sec:norm}, and Section \ref{sec:sharingdefs} contain
design choices that help reduce the code size.
\item[Compiler Performance] Avoiding code explosion  helps compilation performance, but this is not enough: Section \ref{sec:taintfun} contains a mechanism to avoid performing work that is unlikely to give any benefit.
\end{description}

We have also made a lot of minor non-controversial design choices in
our supercompiler which we describe in Section \ref{sec:miscdesign}.

\subsection{Discarding Expressions}
\label{sec:discexp1}

The initial function call to reverse with an accumulating parameter,
\<reverse xs []\>, is an example that will pass the test for boring
expressions since the second argument is a known constructor. Despite
this there is not much the supercompiler can do with this expression
and the end result will be a new function with one unfolding of
reverse and a second function that is isomorphic to reverse. 

Designing an algorithm that approximates what the result and how much
savings were achieved from supercompiling an arbitrary expression is
difficult. We can completely avoid to solve this problem by
speculatively supercompile the expression, have the supercompiler keep
track of the reduction steps taken, and look at the output of the
supercompiler. If the number of reduction steps taken is small or the
code size is deemed too large we discard the supercompiled expression
and supercompile the subexpressions of the current expression instead. 

\subsection{Boring Contexts}
\label{sec:boring}

There are sometimes function calls that have no static information in
their argument, making it impossible to improve them by supercompiling
them in their context. By using a simple approximation of such
function calls we save compilation time and avoid creating
specializations that do not improve the performance. We say that such
functions are in a boring context. A boring expression is an expression of the form:
\begin{equation*}
b ::= x \alt b\,b \alt n \oplus b \alt b \oplus n \alt b \oplus b
\end{equation*}
A context \<\R\> is defined as boring iff $\R = \epsilon$ or $\R = \boxempty\,\,b:\!\R'$ and $\R'$ is boring. 

\subsection{Normalization of Expressions}
\label{sec:norm}

We perform a simple normalization of expressions before comparing them
for folding possibilities. This makes the supercompiler significantly
faster. The big win is the removal of identity coercions in
expressions, which makes the memoization list a lot shorter. 


\subsection{Sharing New Function Definitions}
\label{sec:sharingdefs}

It is quite common for the case of case-rule to fire. A typical case
looks something like this:
\begin{haskell}
\hsccase{(\hscase{x}{p_1 \to x_1\\ \ldots \\ p_n \to x_n) \hskwd{of}}}{[] \to
  []\\ (x':xs') \to append xs' zs}
\end{haskell}
\noindent Once the case of case-rule is done the code is:
\begin{haskell}
\hscase{x}{p_1 \to \hscase{x_1}{[] \to []\\ (x':xs') \to append xs' zs}\\ \ldots \\ p_n \to \hscase{x_n}{[] \to []\\ (x':xs') \to append xs' zs}}
\end{haskell}

The driving algorithm will transform the call to append twice, and create two functions that are both isomorphic to append. Creating the functions at the top level and calling the same function from both branches saves both transformation work and reduces code size. 

Using a state monad for the driving algorithm, and have that monad store a memoization list augmented with the function definitions will allow the second branch to just insert a call to this new function created in the first branch, thereby saving a lot of transformation effort. 

However, if we fold too eagerly this will miss out on specialization opportunities and this will make the final program perform worse than necessary. An example is \<append (append xs ys) zs\>, which when transformed will create a function isomorphic to append itself in the first branch. After the supercompiler has transformed  the second branch it will find a recursive call to \<append (append xs' ys) zs\>, which can fold against both the call in the first branch, \<append ys zs\>, and the initial call that the transformation started from. If the former is chosen no fusion will occur.

We therefore only look for renamings, not instances, when trying to fold against things stored in the monad. If there exists a specialised version of our current function the algorithm will use that, and otherwise it will create a new specialised copy. 

\subsection{Tainting Functions}
\label{sec:taintfun}

If the same function, regardless of context, is supercompiled in
different parts of the program and the result is discarded more than a
certain number of times we make the unfolding for the function
unavailable. This prevents future attempts of specializing the
function. The concrete mechanism is that we add a special triple on
the form \<(*, \emptyset, F)\> to the store each time we discard a
result from supercompiling a function F in some context, and the
number of such triples in the store is checked for before inlining a function.

We used being discarded 3 times as
threshold for our measurements.

\subsection{Miscellaneous Design Choices}
\label{sec:miscdesign}

When supercompiling a function call \<const x y\> our supercompiler
blindly emits a call to a fresh function \<h x y\> whose body is
defined as \< (\lambda \!x y.x) x y\>. It is safe to directly inline the body
of \<const\> at the call-site but we can increase the code sharing by
allowing the supercompiler to fold against this definition from other
parts of the program.

If it turns out that there is only one call to \<h\> in the entire
supercompiled program the ordinary simplifier of the compiler will
inline it.

The reason we use evaluation contexts in our algorithm is that there is a chance that good things can happen in the interaction between evaluation contexts and an expression in the hole. There are no such possibilities with an arbitrary context that has the hole outside the focus for evaluation. 






\section{Supercompilation}
\label{sec:scp}

This section contains the definition of our supercompilation algorithm and its dependencies.



\subsection{Preliminaries}

\begin{figure}
The outer context:
\begin{equation*}
\R ::= \epsilon \alt \mathcal{G}:\R
\end{equation*}
Each frame:
\begin{equation*}
\mathcal{G} ::=  
      \boxempty \, e
      \alt            \boxempty\, \oplus\, e
      \alt            e' \oplus \boxempty
      \alt             \CASE\, \boxempty \, \OF \, \{ p_i \arr e_i \} 
\end{equation*}
Memoization element:
\begin{equation*}
\nu ::= (h, \overline{x}, \con{F})
\end{equation*} 
Memoization list:
\begin{equation*}
\rho ::= \epsilon \alt \nu:\rho
\end{equation*}
Store:
\begin{equation*}
\sigma ::= \epsilon \alt (\nu, e'):\sigma
\end{equation*}
\caption{Context definition}
\label{fig:framedef}
\end{figure}

We need a new reduction context for our supercompiler to allow it to focus on the second parameter of a primop even if the first parameter is an arbitrary expression. It will turn out to be convenient for the implementation to pattern match on the context if it is a list of single level contexts. We therefore introduce $\R$ as defined in Figure \ref{fig:framedef}.  
$\overline{\boxempty\,  e}$ denotes a list of application contexts.

If a variable appears no more than once in an expression, that expression is said to be {\em linear} with respect to that variable. Like \citet{Wadler:1990:Deforestation}, we extend the definition slightly for linear case expressions: no variable may appear in both the selector and a branch, although a variable may appear in more than one branch. 

\subsection{Algorithm Definition}
Our supercompiler is defined as two mutually recursive functions that pattern-match on expressions and contexts in order to rewrite expressions. The first algorithm is called the {\em driving} algorithm, used to perform evaluation steps, and the second algorithm is called the {\em building} algorithm, which reassembles the transformed expression. These algorithms are defined in Figure \ref{fig:drivalg}.  Both algorithms take five parameters: 1) an expression; 2) a memoization list $\rho$; 3) the context $\R$; 4) the store $\sigma$; and 5) the savings from the supercompiler so far. New function definitions are put in the store. The memoization list holds information about expressions already traversed and is used to guarantee termination. A notational convention is to use e' to denote expressions that are already transformed.


\begin{figure*}
\begin{tabular}{lllr}
General form: \\
$\dr{e}{\R}{s} = (e', \sigma', s')$ \\
~ \\
Evaluation Rules \\
$\dr{n_j}{(\CASE \boxempty\,\, \OF \{n_i \arr e_i \}:\R)}{s}$ & = & $\dr{e_j}{\R}{(s+1)} $ & (R1) \\
$\dr{n}{(n_1 \oplus \boxempty:\R)}{s}$ & = & $\dr{n_2}{\R}{(s + 1)}$, where $n_2 = n_1 + n$ & (R2) \\
~ \\
$\dr{F}{\R}{s}\, |\, F\text{ not tainted and } \R \text{ not boring} $ & = & $\adr{F}{\R}{s}$ & (R3) \\
~ \\
$\dr{x}{\R}{s} $ & = & $\axdr{x}{\R}{s}$ & (R4) \\
~ \\
$\dr{K_j}{(\overline{\boxempty\, e}:\CASE \boxempty\,\, \OF \{K_i\,\overline{x}_i \arr e_i \}:\R)}{s}$ & = & $\dr{\LET \overline{x}_j = \overline{e} \IN  e_j}{\R}{(s+5)}$ & (R5)\\
~ \\
$\dr{\lambda \overline{x}.e_1}{(\overline{\boxempty\,\,e_2}:\R)}{s}$ & = & $\dr{\LET \overline{x} = \overline{e_2} \IN e_1}{\R}{(s+1)}$ & (R6) \\
$\dr{\lambda x.e}{\R}{s}$ & = & $\MLET (e', \sigma_1, s') = \dr{e}{\epsilon}{0}$ & (R7) \\
& & $\MIN \ers{\lambda x.e'}{\R}{(s + \# s')}$ \\
~ \\
$\dr{\LET x=v \IN e}{\R}{s}$ & = & $\dr{[v/x]e}{\R}{(s+1)}$ & (R8) \\ 
$\dr{\LET x=y \IN e}{\R}{s} | y$ not freshly generated  & = & $\dr{[y/x]e}{\R}{(s+1)}$  & (R9) \\ 
$\dr{\LET x=e_1 \IN e_2}{\R}{s} | \text{ linear }x\, e_2$ & = & $\dr{[e_1/x]e_2}{\R}{(s+1)}$ & (R10) \\ 
 \hspace{11.85em}$|$ otherwise  & = & $\MLET (e_1', \sigma_1, s_1) = \dr{e_1}{\epsilon}{0} $ \\ 
& & \hspace{1.1em} $(e_2', \sigma_2,s_2) = \drs{e_2}{\R}$\\ 
& & $\MIN (\LET x = e_1' \IN e_2', \sigma_2, ? s_1 + s_2)$  & \\
~ \\
% $\dr{\LETREC F = e_1 \IN e_2}{\R}$ & = & $\drg{e_2}{\R}$,  where $\mathcal{F}' = \mathcal{F} \cup (F, e_1)$  & (R10) \\
% ~ \\
Focusing Rules\\
$\dr{e_1 \oplus e_2}{\R}{s}$ & = & $\dr{e_1}{(\boxempty\, \oplus e_2:\R)}{s}$ & (R11) \\  
$\dr{e_1\, e_2}{\R}{s}$ & = & $\dr{e_1}{(\boxempty\,\, e_2:\R)}{s}$ & (R12) \\
$\dr{\CASE e\, \OF  \{p_i \arr e_i \} }{\R}{s}$ & = & $\dr{e}{(\CASE \boxempty\, \OF  \{p_i  \arr e_i \}:\R)}{s}$ & (R13) \\
~ \\
Fallthrough \\
$\dr{e}{\R}{s}$ & = & $\er{e}{\R}{s}$ & (R14) \\
~ \\
\end{tabular}\\
\begin{tabular}{lllr}
Rebuilding Expressions \\
$\er{n}{(\boxempty\,\oplus e_2:\R)}{s}$ & = & $\dr{e_2}{(n \oplus \boxempty:\R)}{s}$ & (R15)\\
$\er{e'}{(\boxempty\,\oplus e_2:\R)}{s}$ & = & $\MLET (e_2', \sigma_1, s') = \dr{e_2}{\epsilon}{s}$ & (R16)\\
& & $\MIN \ers{e' \oplus e_2'}{\R}{s'}$ \\
$\er{e'}{(e_1' \oplus \boxempty:\R)}{s}$ & = & $ \er{e_1' \oplus e'}{\R}{s}$ & (R17) \\
$\er{e'}{(\boxempty\,e:\R)}{s}$ & = & $\MLET (e'', \sigma_1,s') = \dr{e}{\epsilon}{s}$ & (R18) \\
& & $\MIN \ers{e' e''}{\R}{s'}$ \\
$\er{x'}{(\CASE \boxempty\,\, \OF \{p_i \arr e_i \}:\R)}{s}$ & = & $\MLET (e_i', \sigma_i,s_i) = \drss{[p_i/x]e_i}{([p_i/x]\R)}{s}$ & (R19) \\
& & $\MIN (\CASE x'\, \OF \{p_i \arr e_i' \}, \sigma_i, max(s_i))$  \\
$\er{e'}{(\CASE \boxempty\,\, \OF \{p_i \arr e_i \}:\R)}{s}$ & = & $\MLET (e_i', \sigma_i, s_i) = \drss{e_i}{\R}{s}$ & (R20) \\
 & & $\MIN (\CASE e' \OF \{p_i \arr e_i' \}, \sigma_i, max(s_i))$ \\
$\er{e'}{\epsilon}{s}$ & = & $(e', \sigma, s)$ & (R21)\\
\end{tabular}
\caption{Driving algorithm and building algorithm}
\label{fig:drivalg}
\end{figure*}

There is an ordering between rules; i.e., all rules must be tried in the order they appear. Rules R11-R13 are the default focusing rules that extend the given driving context $\R$ and zoom in on the next expression to be transformed. If no other rule matches, such as for a single variable, rule R14 will match and call build to rebuild the expression.

The program is turned ``inside-out'' by moving the surrounding context
$\R$ into all branches of the case-expression through rules R19 and
R20. Rule R10 has a similar mechanism for let-expressions. Rule R9 is
only allowed to match if the variable {\em y} is not freshly generated
by the splitting mechanism described in the Section \ref{sec:splitting}.

%\begin{figure}
%\begin{tabular}{lll}
%$\drl{e}{L}$ &$\! =\, $& $\MLET (e', \sigma') = \dr{e}{\R}$ \\
%& & $\hspace{1.4em}(\sigma_1, \sigma_2) = storeSplit(\sigma', x)$ \\
%& & $\MIN (\kw{L}\, \sigma_1 \IN e', \sigma_2)$ \\
%\end{tabular}
%\caption{Driving of let-expressions}
%\label{fig:adrivlet}
%\end{figure}

%Definition of doBeta:

%\begin{verbatim}
%doBeta :: ScpEnv -> CoreExpr -> [CoreExpr] -> CoreExpr
%doBeta env (Lam b body) args@(a:as)
 %| isTypeArg a = doBeta env (substExpr (extendSubst emptySubst b a) body) as
 %| otherwise = Let (NonRec b a) (doBeta env' body as)
  %  where env' = {inSet = b:inSet env} 
%doBeta _ fn args = mkApps fn args
%\end{verbatim}



Rules R3 and R4 refer to \<\asdr \aedr\> and \<\axsdr \aedr\>, both defined in Figure \ref{fig:adrivalg}.  They can both be inlined in the definition of the driving algorithm, they are merely given a separate name for improved clarity of the presentation.

The fifth parameter to the supercompiler, the savings, is there to track  how many reduction steps the supercompiler has performed. This is currently represented as a tree in our implementation to aid us in the design of when to discard expressions, but a production compiler should use a more efficient representation. We assign the value 1 to ordinary evaluation steps in rules R1, R2, R6, R8, R9 and R10. Rule R5, the case reduction with a known constructor, is assigned the value 5 since it both decreases code size and removes a memory allocation. 

We need some more arithmetic operations on our savings beyond plain addition: \# indicates that a saving was under a lambda, ? combines branches of savings such as in rule R10 and max of all savings in rules R19 and R20. The most important saving, folding, is denoted by the exclamation mark (!). 

We use the operator $\rho|_F$ to extract  all expressions with the head {\it F} from $\rho$. Our implementation stores the partitioned $\rho$'s to avoid repeating the partitioning. Partitioning the memoization list gives significant time savings, but it can only be applied on the outermost level.



\begin{figure*}
\begin{tabular}{lllr}
$\adr{F}{\R}{s} \,|  \exists(h, \overline{y}, e_1)\! \in \!(\sigma |_F \cup \rho|_F)\,.\, [\overline{x}/\overline{y}] e_1 =  e_2$ &$\! =\, $& $(h\,\overline{x}, \sigma, !s)$  & (1) \\
$\hspace{7.1em}|\exists(h, \overline{y},  e_i)\! \in \!(\rho|_F)\,.\, e_1 \homemb^* e_2$ &$\! =\, $& $\MLET (\overline{f}', \sigma_i, s_i) = \drss{\overline{f}}{\epsilon}{s_{i-1}}$ & (2)\\
& &  \hspace{1.1em} $(f_g', \sigma_2, s_2) = \drsi{f_g}{\epsilon}$ \\
& & $\MIN ([\overline{f}'/\overline{y}] f_g', \sigma_2, max(s_i,s_2))$  \\
 $\hspace{7.1em}|\, \acceptable(e_2, e', s_1)$ &$\! =\, $&$\MLET (e', \sigma_1, s_1) = \drp{e}{\R}{s}$ &  (3) \\
& & $\MIN (h\,\overline{x}, ((h,  \overline{x}, e_2), e'):\sigma_1, s_1)$  \\
$\hspace{7.1em}|$ otherwise & $\! =\, $& $\erss{F}{\R}{((*, \emptyset, F):\sigma)}{s}$ & (4) \\
  \multicolumn{4}{l}{\hspace{2em} where $F \eqdef e$} \\
  \multicolumn{4}{l}{\hspace{4.7em} $e_2 = \normalize(\con{F})$} \\
  \multicolumn{4}{l}{\hspace{4.7em} $\rho' = (h, \overline{x}, e_2):\rho$}\\
  \multicolumn{4}{l}{\hspace{4.7em} $h$ fresh}  \\
 \multicolumn{4}{l}{\hspace{4.7em} $\overline{x} = \fv(e_2)$}\\
  \multicolumn{4}{l}{\hspace{4.7em} $(f_g, [\overline{f}/\overline{y}]) = divide(e_2, e_1)$ }\\
 ~ \\
$\axdr{x}{\R}{s}\,|\exists(h, \overline{y}, e_1)\! \in \!(\sigma \cup \rho)\,.\, [\overline{x}/\overline{y}] e_1 =  e_2$ &$\! =\, $& $(h\,\overline{x}, \sigma, !s)$  & (5) \\
 \hspace{7.95em} $|\, \acceptable(e_2, e', s_1)$ &$\! =\, $&$\MLET (e', \sigma_1, s_1) = \ers{x}{\R}{s}$ & (6) \\
& & $\MIN (h\,\overline{x}, ((h, \overline{x}, e_2), e'):\sigma_1, s_1)$ \\
\hspace{8em} $|$ otherwise & $\! =\, $& $\er{x}{\R}{s}$ & (7) \\
  \multicolumn{4}{l}{\hspace{2em} where $e_2 = \normalize(\con{x})$} \\
  \multicolumn{4}{l}{\hspace{4.7em} $\rho' = (h, \overline{x}, e_2):\rho$}\\
  \multicolumn{4}{l}{\hspace{4.7em} $h$ fresh}  \\
 \multicolumn{4}{l}{\hspace{4.7em} $\overline{x} = \fv(e_2)$}\\
\end{tabular}
\caption{Driving of applications}
\label{fig:adrivalg}
\end{figure*}

\<\axsdr\aedr\> will try to fold against expressions with a variable
in the head. This is convenient and reduces code size in general. A
good example is supercompiling the right hand sides of append in a module:
\begin{haskell}
append xs ys =  
\sdr \CASE xs \OF \{\ldots \} \edr \\
\{ Create a fresh function and transform its body \} \\
append xs ys = h xs ys \\
h xs ys = \hscase{xs}{[] \rightarrow ys\\ (x':xs') \rightarrow x':\sdr append xs' ys\edr} \\
\{ Inline append \} \\
append xs ys = h xs ys \\
h xs ys = \hscase{xs}{ [] \rightarrow ys\\ (x':xs') \rightarrow  x':\sdr \CASE xs' \OF \{\ldots \}\edr }\\
\{ Fold against h \} \\
append xs ys = h xs ys \\
h xs ys = \hscase{xs}{ [] \rightarrow ys\\ (x':xs') \rightarrow  x':h xs' ys }\\
\end{haskell}
Without variable folding this example would give one more unrolling of
the recursion which would have increased the code size.

\subsection{Termination Checking}
Folding by itself is not sufficient to ensure termination of the driving algorithm. We therefore define a predicate which is commonly referred to as ``the whistle'' in literature on supercompilation. Whenever the whistle blows, our algorithm splits the input expression into strictly smaller expressions that are transformed separately in the empty context. This might expose new folding opportunities, and allows the algorithm to remove intermediate structures in subexpressions.

The design of the predicate is inspired by the homeomorphic embedding
relation \citep{Soerensen:1995:AnAlgorithm} but adjusted to work on
our zipper representation and to admit more expressions. A specific
design criterion was that \<append xs ys\> must not be embedded in
\<append xs xs\>. It is easy to construct infinite chains of
expressions that will be admitted by this predicate by itself,
\<append xs ys\>, \<append xs ys\>, $\ldots$ is one example. However,
non-termination is still avoided because the folding mechanism will
prevent such chains to build up in $\rho$.

%  & | & sizeof(e) == sizeof(e') \&\& = XXX \\
\begin{definition}[$\homemb^*$]
\begin{equation*}
\frac{sizeof(\con{e_1}) < sizeof(\conp{e_2})}{\con{e_1} \homemb^* \conp{e_2}  = \con{e_1} \homemb \conp{e_2}}
\end{equation*}
\end{definition}

\begin{definition}[$\homemb$]
~ \\
$$
x \homemb y,\,\,\,  n_1 \homemb n_2,\,\,\,  \frac{e_1, e_2 \neq \lambda x.e,\,\,\, e_1 = e_2, \,\,\,\R \homemb \R'}{\con{e_1} \homemb \conp{e_2}}  
$$
$$
\epsilon \homemb \epsilon, \,\,\,\frac{\R \homemb \R' \,\,\, \G \homemb \G'}{\G:\R \homemb \G':\R'}, \,\,\,
\frac{\R \homemb \R'}{\R \homemb \G':\R'}
$$
$$
\frac{e \homemb e'}{\boxempty\,e \homemb \boxempty\,e'}, \,\,\,
\frac{e \homemb e'}{\boxempty \oplus e \homemb \boxempty \oplus e'}, \,\,\,
\frac{e \homemb e'}{e \oplus \boxempty \homemb e' \oplus \boxempty },
$$
$$
\frac{e_i \homemb e_i'}{\CASE \boxempty \OF \{ p_i \rightarrow e_i \} \homemb \CASE \boxempty \OF \{ p_i \rightarrow e_i'\} }, \,\,\,
$$
\end{definition}

%   Define $\homemb$ as the smallest relation on $T$
%   satisfying: 
% $$
% x \homemb y,\,\,\,  n_1 \homemb n_2,\,\,\,  \frac{e \homemb f_i \text{ for
%      some i}}{e \homemb s(f_1,\ldots,f_n)},\,\,\,  
% $$ 
% $$ 
% \frac{e_1 \homemb f_1,
%    \ldots, e_n \homemb f_n}{s(e_1,\ldots,e_n) \homemb
%    s(f_1,\ldots,f_n)}
% $$
% \end{definition}

We postpone dealing with the problem of non-termination of the
supercompiler in the case of recursive data types that appear
contravariantly in their own definition. As an aside, we note that the
inliner in GHC will also loop on such programs
\citep{Jones:2002:Secrets}.

\subsection{Expression Splitting}
\label{sec:splitting}

When the whistle has blown it is necessary to stop transforming the current expression. It is safe to just leave it in place, but by splitting the expression and transforming the parts separately it is possible to achieve more optimization.

\<Divide\> tries to preserve as much structure between its first input argument and output by first calling  an adaptation of the most specific generalisation \citep{Soerensen:1995:AnAlgorithm} to the zipper representation. Should this call fail, \<divide\> instead calls split which will always return a valid result under the conditions ensured by the driving algorithm:  \<divide\> is always called on two expressions on the form $\con{F}$ and $\conp{F}$. Divide, split and msg are defined in Figure \ref{fig:divsplitmsg}. For the presentation we ignore the issues concerned with splitting under binders in expressions since binders are treated in the same way as described by \citet{Pfenning:1991:Unification}.

The msg can return an expression which is of greater size than
its input because of binders: when splitting the two expressions \<\CASE x \OF \{ (a, b) \rightarrow a \}\> and \<\CASE x \OF \{ (a, b) \rightarrow b \}\> the result will be \<(\CASE x \OF \{ (a, b)\rightarrow z a \}, [(\lambda a.a)/z])\>.




\begin{figure*}
\begin{tabular}{ll}
$divide(\con{e_1}, \conp{e_2}) = (e, \theta)$ & iff $(e, \theta) = msg(\con{e_1},\conp{e_2}) $\\
 & and $sizeof(e) < sizeof(\con{e_1}) $\\
~\\
$divide(\con{e_1}, \conp{e_2}) = split(\con{e_1})$ \\
~ \\
$split([F]\G_1:\ldots:\G_n:\epsilon) = ([x]\G_n:\epsilon, [([F]\G_1:\ldots:\G_{n-1}:\epsilon)/x])$ & $x$ fresh\\
~ \\
$msg([e_1]\R_1,[e_2]\R_2) = (\con{e}, \theta  \theta')$ & if $\R' = \epsilon$ \\
\hspace{8.9em} $= (\conp{x}, \theta\theta' [[e]\R/x])$ & otherwise \\
\multicolumn{2}{l}{\hspace{4.3em}if $(e, \theta) = msg(e_1,e_2)$ and $(\R, \R', \theta') = msg(\R_1, \R_2)$ } \\
% & iff $  (e', \theta) = msg(e_1, e_2)$ and \\
% & $(e'', \theta') = msgR(e', \R, \R') $\\
~ \\
$msg(\boxempty\, e_1, \boxempty\, e_2) = (\boxempty\, e', \theta)$ & iff $(e', \theta) = msg(e_1, e_2)$ \\
$msg(\boxempty \oplus e_1, \boxempty  \oplus e_2) = (\boxempty \oplus e', \theta)$ & iff $(e', \theta) = msg(e_1, e_2)$ \\
$msg(e_1 \oplus \boxempty ,e_2 \oplus \boxempty) = (e' \oplus \boxempty, \theta)$ & iff $(e', \theta) = msg(e_1, e_2)$ \\
$msg(\CASE \boxempty \OF \{ p_i \rightarrow e_{1i}\},\CASE \boxempty \OF \{ p_i \rightarrow e_{2i} \}) = (\CASE \boxempty \OF \{ p_i \rightarrow e_i' \}, \theta_1  \ldots  \theta_i)$ & iff $(e_i', \theta_i) = msg(e_{1i}, e_{2i})$ \\
~ \\
$msg(\lambda x.e_1, \lambda x.e_2) = (\lambda x.e', \theta)$ & iff $  (e', \theta) = msg(e_1, e_2)$  \\
$msg(F, F) = (F, \emptyset)$ \\
$msg(K, K) = (K, \emptyset)$ \\
$msg(n, n) = (n, \emptyset)$ \\
$msg(x, x) = (x, \emptyset)$\\
$msg(e_1, e_2) = (x, [e_1/x])$ & $x$ fresh \\
~ \\
$msg(\G_1:\R_1, \G_2:\R_2) = (\G:\R, \R', \theta \theta') $ \\
\multicolumn{2}{l}{\hspace{4.3em}if $(\G, \theta) = msg(\G_1, \G_2)$ and $(\R, \R', \theta') = msg(\R_1,\R_2)$ }\\
~ \\
$msg(\R_1, \R_2) = (\epsilon, \R_1, \emptyset)$ & (default) \\
\end{tabular}
\caption{Divide, split and msg in zipper form}
\label{fig:divsplitmsg}
\end{figure*}


% \subsection{Call-By-Value Adjustment}

% With some minor changes our algorithm can also be used for languages with call-by-value semantics. Figure \ref{fig:cbvadjust} contains them.
% \begin{figure*}
% \begin{tabular}{lllr}
% $\dr{\LET x=e_1 \IN e_2}{\R}{s} | \text{linear } x\, e_2 \&\& \text{ strict }x\, e_2$ & = & $\dr{[e_1/x]e_2}{\R}{s + 1}$ & (R15) \\ 
%  \hspace{11.3em}$|$ otherwise  & = & $\MLET (e_1', \sigma_1, s_1) = \dr{e_1}{\epsilon}{0} $ \\ 
% & & \hspace{1.1em} $(e_2', \sigma_2,s_2) = \drs{e_2}{\R}{s}$\\ 
% & & $\MIN (\LET x = e_1' \IN e_2', \sigma_2,s_2)$  & \\
% \end{tabular}
% \caption{Call-by-value adjustment for rule R15}
% \label{fig:cbvadjust}
% \end{figure*}


% \subsection{Algorithm Extensions}

% Stop specializing and create functions on demand, see Figure \ref{fig:adrivalg3}.

% \begin{figure*}
% \begin{tabular}{llllr}
% $\adr{F}{\R}$ &$\! =\, $& $(h\,\overline{x}, \sigma)$  & if $\exists(h, \overline{y}, e_1)\! \in \!(\sigma \backslash F \cup \rho\backslash F)\,.\, [\overline{x}/\overline{y}] e_1 =  \con{F}$ & (1) \\
% $\adr{F}{\R}$ &$\! =\, $& $\MLET (\overline{f}', \sigma_i) = \drss{\overline{f}}{\epsilon}$ & if $\exists(h, \overline{y},  e_i)\! \in \!(\rho\backslash F)\,.\, e_1 \homemb^* \con{F}\!$ & (2)\\
% & &  \hspace{1.1em} $(f_g', \sigma_2) = \drsi{f_g}{\epsilon}$ \\
% & & $\MIN ([\overline{f}'/\overline{y}] f_g', \sigma_2)$  \\
% $\adr{F}{\R}$ &$\! =\, $& $(h\,\overline{x}, \sigma_1 \cup (h,  \lambda \overline{x}.e'))$ &if $h \in e'$  & (3a) \\
% & & $(e', \sigma_1 )$ &otherwise  & (3b) \\
%   \multicolumn{4}{l}{\hspace{2em} where $(F = e) \in \mathcal{F}$,} \\
%   \multicolumn{4}{l}{\hspace{4.7em} $\rho' = \rho \cup (h, \overline{x}, \con{F})$,}\\
%   \multicolumn{4}{l}{\hspace{4.7em} $h$ fresh,}  \\
%  \multicolumn{4}{l}{\hspace{4.7em} $\overline{x} = \fv(\con{F})$,}\\
%   \multicolumn{4}{l}{\hspace{4.7em} $(f_g, \overline{f}, \overline{y}) = split(\con{F}, e_1)$ }\\
% \multicolumn{4}{l}{\hspace{4.7em} $(e', \sigma_1) = \drp{e}{\R}$} \\
% \end{tabular}
% \caption{Driving of applications with inlining}
% \label{fig:adrivalg3}
% \end{figure*}

\subsection{Normalization of Expressions}

Finding renamings of an expression is a syntactical check, and sometimes this will miss out opportunities to fold because expressions that are semantically equivalent have different forms. 

Consider the two expressions \<F x (1 + 2)\> and \<F y (2 + 1)\> -- it is obvious to a human that these two expressions should be foldable against each other. By performing some kind of limited normalization on these expressions the second parameter will turn out to be 3 in both cases and they can fold.

We can not hope to find a normal form for our expressions in general, but performing ordinary evaluation except inlining of function calls on all subexpressions will get a long way towards our goal. It is of course important to have a normalization that terminates. 

A word of caution about making the normalization too powerful: many common optimizations change the structure of expressions. One example is changing the expression \<(x+1)+1\> to \<x+2\> which is semantically correct and clearly saves computations, but chances are that in practice the first expression came from an expression \<y + 1\> in a recursive call with an increasing parameter. Both \<(y+1)\> will be  homeomorphically embedded in both \<(x + 1) + 1\> and \<x + 2\>, but the former will be generalized to \<(z + 1, [(x+1)/z])\>  and which in turn will fold nicely against \<y + 1\>.

\subsection{Discarding Expressions}
\label{sec:discexp2}

The savings that are propagated by the supercompiler are used as input to a predicate \<accept\> which decides whether to discard or keep transformed functions. Our current implementation is remarkably simple:
\begin{haskell}
acceptable before after savings \\ 
\,| sizeof(after) > 40 = False \\
\,| sizeof(after) > 20 = (savings - 100) <= 29 \\
\,| sizeof(before) >= sizeof(after) = s - 3 <= 0 \\
\,| otherwise = s - 50 <= 29 \\
\end{haskell}


The reason this function works at all is that our algorithm will by construction emit a lot of small functions. If a function body contains many syntactic nodes it is a sign that optimization was not very successful. This typically happens in code that contains a lot of FFI-calls which are opaque to the supercompiler.



% Old notes:

% \begin{haskell}
% \hsccase{(\hscase{x}{p_1 \to x_1\\ \ldots \\ p_n \to x_n) \hskwd{of}}}{[] \to []\\ (x':xs') \to append xs' zs}
% \end{haskell}

% \begin{haskell}
% \hscase{x}{p_1 \to \hsccase{x_1}{[] \to []\\ (x':xs') \to append xs' zs}\\ \ldots \\ p_n \to \hsccase{x_n}{[] \to []\\ (x':xs') \to append xs' zs}}
% \end{haskell}

% \begin{haskell}
% \hscase{x}{p_1 \to h_1 x_1 zs\\ \ldots \\ p_n \to  h_1 x_n zs}
% \end{haskell}
% where \<h_1\> is a new function that has the body:
% \begin{haskell}
% h_1 x' zs = \hscase{x'}{[] \to  []\\ (x':xs') \to append xs' zs}
% \end{haskell}



% \subsection{Algorithm Correctness}

% We outline the argument for algorithm correctness, but since this is not our focus a lot of details are left out. 

% The algorithm is total regardless of evaluation order.

% \begin{lemma}[Totality]
% \label{lem:totality}
% Let $\con{e}$ be a well-typed expression, then $\dr{e}{\R}{s}$ and $\er{e}{\R}{s}$ are matched by a unique rule in Figure \ref{fig:drivalg}.
% \end{lemma}

% \begin{proof}[Proof sketch]
% Rule R22 will always match. Inspection shows that rules R23-R30 are exhaustive over the contexts, so they always match.
% \end{proof}

% \begin{theorem}[XXX: HE is wqo]
% The homeomorphic embedding is a well-quasi-order.
% \end{theorem}

% \begin{proof}
% XXX: Fill in
% \end{proof}

% \begin{theorem}[Termination]
%   The driving algorithm \<\sdr{}\edr\> terminates for all well-typed inputs.
% \end{theorem}

% We use the improvement theory by Sands \citep{Sands:1997:From,Sands:199X:XXX} to prove the correctness of our algorithm. The same theorem can be used regardless of evaluation order, but separate proofs are needed.

% \begin{theorem}[Total Correctness]
% \label{prop:totcorr}
% Let $\con{e}$ be an expression, and $\rho$ an environment such that
% \begin{itemize}
% \item the range of $\rho$ contains only closed expressions, and
% \item $\fv(\con{e}) \cap dom(\rho) = \emptyset$
% \end{itemize}
% then $\con{e} \costrighteq_s \rho(\dr{e}{\R})$.
% \end{theorem}


\section{Measurements}
\label{sec:measurements}

% This section reports on the performance of our supercompiler and compares how different constants affect binary sizes and achieved optimizations from a prototype implementation in GHC. 

The results supported by this section can be summarized with a single sentence: we can supercompile most programs from the spectral and imaginary part of nofib in less than two seconds of compile time while keeping the maximum binary size increase below 5\%. 

We start by establishing a base line against ghc -O2 on a small set of
examples from the imaginary part of nofib as shown in Table
\ref{tab:o2vsscp}. By turning off the features normalization of
expressions, boring contexts, discarding expressions and tainting
expressions in our supercompiler we get to something that is close to
an ordinary positive supercompiler
\citep{Soerensen:1996:Positive}. The compilation times range from 2.5
seconds to almost 10 seconds.

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s)\\
\hline 
bernouilli & +8.0 & -1.5 & +0.0 & +1.5 & +0.0 & 3.52 \\
digits-of-e1 & +16.6 & -20.3 & -19.2 & -16.0 & +0.0 & 8.67 \\
exp3\_8 & +6.0 & -16.7 & -17.6 & -17.3 & +0.0 & 2.58 \\
integrate & +20.4 & +65230.5 & +104925.9 & +93051.6 & +30.4 & 9.02 \\
primes & +6.0 & +0.2 & -13.9 & -16.0 & +0.0 & 2.46 \\
rfib & +6.0 & +1599532.1 & 0.18 & 0.18 & +0.0 & 2.45  \\
tak & +6.0 & -12.5 & -2.6 & -2.8 & +0.0 & 2.42 \\
wheel-sieve2 & +7.3 & +307.0 & 0.54 & +195.2 & +252.1 & 3.15 \\
% \hline
% Min & +6.0 & -20.3 & -19.2 & -17.3 & +0.0\\
% Max & +20.4 & +1599532.1 & +104925.9 & +93051.6 & +252.1\\
% Geometric Mean & +9.4 & +738.3 & +189.3 & +186.4 & +21.0\\
\end{tabular}
\caption{ghc -O2 compared with Supercompilation}
\label{tab:o2vsscp}
\end{table*}


We suffer from the same problem that
\citet{Bolingbroke:2010:Supercompilation} report: the supercompiler
can sometimes prevent GHC from applying other important optimizations
such as unboxing of arithmetics. Since that is a slightly different
algorithm it is not exactly the same programs that get staggering
increases in memory allocations. A particular example is {\it tak}, which
our supercompiler slightly optimizes, whereas their get an 18,000-fold
increase in memory allocations.

The situation is the reverse with {\it rfib}, where we get +1599532.1\% in
allocations and their supercompiler does not change memory allocations
at all. The optimized {\it rfib} program has a recursive function taking an
unboxed double and returning an unboxed double, making the program run
in constant memory and nearly constant allocations regardless of input
size. The supercompiled program is not unboxed and the short recursive
function that appears in the ordinary program is stretched out through
numerous other function calls making the actual program flow very hard
to follow for the human eye. 

Looking closer at what happens inside the supercompiler when it
produces this program is interesting: the whistle blows and the
expression currently transformed is split into two parts. This split
forces the inner part of the expression, which is the tight loop, to
get a return type that is boxed. It is important to notice that even
if our supercompiler used the standard versions of the homeomorphic
embedding and the msg, the whistle and the split would produce the
same results.

{\it Integrate} and {\it wheel-sieve2} are two other examples that
shows the problem with our supercompiler preventing GHC from
performing unboxing. The symptom is the same: a vast amount of
increase in allocations for the supercompiled program.

There are two examples that show a rather hefty increase in binary
size: {\it digits-of-e1} and {\it integrate}. One might argue that 
a 20\% reduction in runtime is worth a size increase of 16.6\% for 
{\it digits-of-e1}. This is obviously not the case with {\it
  integrate}, a massive slowdown combined with more than 20\% size
increase of the resulting binary.

By turning on normalization of expressions (Table
\ref{tab:scpvsscpnorm}) there is a slight decrease of binary size, a
small decrease of compilation time and no changes to the performance
of the output programs. This is a small but worthwhile improvement
over regular positive supercompilation.

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s)\\
\hline
bernouilli & -1.6 & +0.0 & +0.0 & -2.2 & +0.0 & 2.54\\
digits-of-e1 & -1.6 & +0.0 & -0.5 & +0.5 & +0.0 & 7.76\\
exp3\_8 & -1.6 & +0.0 & -0.9 & +1.6 & +0.0 & 1.71\\
integrate & -1.5 & +0.1 & -0.3 & -0.4 & -3.0 & 8.41 \\
primes & -1.8 & +0.0 & +0.0 & +0.0 & +0.0 & 1.65\\
rfib & -1.6 & +0.0 & 0.18 & 0.18 & +0.0 & 1.53 \\
tak & -1.6 & +0.0 & +0.0 & +0.5 & +0.0 & 1.48\\
wheel-sieve2 & -1.7 & +0.0 & -0.4 & -1.3 & +0.0 & 2.22\\
% \hline
% Min & -1.8 & +0.0 & -0.9 & -2.2 & -3.0\\
% Max & -1.5 & +0.1 & +0.0 & +1.6 & +0.0\\
% Geometric Mean & -1.6 & +0.0 & -0.3 & -0.2 & -0.4\\
\end{tabular}
\caption{Supercompilation compared with Supercompilation+normalization}
\label{tab:scpvsscpnorm}
\end{table*}

Table \ref{tab:scpnormvsscpnormbor} shows that by turning on boring
contexts it is possible to further shrink the binary size and reduce
compilation time. Two benchmarks are affected by this performance
wise: {\it digits-of-e1} is optimized with another 20\% reduction in memory
allocations giving a slight performance improvement while {\it tak} goes
back to the same amount of memory allocations as without
supercompilation and a slight performance decrease.

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s) \\
\hline
bernouilli & -2.1 & +0.0 & +0.8 & -1.5 & +0.0 & 1.77\\
digits-of-e1 & -1.5 & -22.6 & -4.9 & -7.4 & +0.0 & 6.93\\
exp3\_8 & -1.6 & +0.0 & +0.9 & -3.2 & +0.0 & 1.02\\
integrate & -3.9 & +0.3 & +0.9 & +1.0 & +2.3 & 6.63\\
primes & -1.5 & +0.0 & +0.0 & +5.1 & +0.0 & 0.98\\
rfib & -1.6 & +0.0 & 0.16 & 0.17 & +0.0 & 0.94\\
tak & -1.6 & +13.9 & +16.0 & +15.6 & +0.0 & 0.92\\
wheel-sieve2 & -1.6 & +0.0 & +0.0 & +0.0 & +0.0 & 1.48\\
% \hline
% Min & -3.9 & -22.6 & -4.9 & -7.4 & +0.0\\
% Max & -1.5 & +13.9 & +16.0 & +15.6 & +2.3\\
% Geometric Mean & -1.9 & -1.5 & +1.8 & +1.2 & +0.3\\
\end{tabular}
\caption{Supercompilation+normalization compared with Supercompilation+normalization+boring expressions}
\label{tab:scpnormvsscpnormbor}
\end{table*}

By discarding expressions (Table \ref{tab:scpnormborvsscpnormbordisc})
there is a further decrease of binary size and the performance loss
{\it wheel-sieve2} suffered from plain supercompilation is somewhat
mitigated. The compilation times are all shorter except for
{\it digits-of-e1} which supercompiles several expressions and discards them
only to find them in a slightly different context at a later time and
repeating this work.

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s) \\
\hline
bernouilli & -1.7 & +0.0 & -0.8 & -0.8 & +0.0 & 1.15\\
digits-of-e1 & -1.0 & +0.0 & -2.6 & +0.5 & +0.0 & 12.38\\
exp3\_8 & -2.1 & +0.0 & +0.0 & +0.0 & +0.0 & 0.58\\
integrate & -4.0 & -0.1 & -0.2 & -0.2 & +0.8 & 6.00\\
primes & -1.9 & +0.0 & +0.0 & -4.8 & +0.0 & 0.56 \\
rfib & -2.0 & +0.0 & 0.18 & 0.18 & +0.0 & 0.50\\
tak & -2.0 & +0.0 & -21.8 & -21.8 & +0.0 & 0.50\\
wheel-sieve2 & -1.9 & -73.6 & -64.8 & -65.0 & -72.2 & 0.99\\
% \hline
% Min & -4.0 & -73.6 & -64.8 & -65.0 & -72.2\\
% Max & -1.0 & +0.0 & +0.0 & +0.5 & +0.8\\
% Geometric Mean & -2.1 & -15.4 & -17.3 & -17.6 & -14.7\\
\end{tabular}
\caption{Supercompilation+normalization+boring expressions compared with Supercompilation+normalization+boring expressions+discarding expressions}
\label{tab:scpnormborvsscpnormbordisc}
\end{table*}

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s) \\
\hline
bernouilli & -1.2 & -0.8 & +0.0 & +3.1 & +0.0 & 0.64 \\
digits-of-e1 & -8.9 & +8.7 & +2.6 & -0.5 & +0.0 & 1.29 \\
exp3\_8 & -0.3 & +0.0 & +0.0 & +0.0 & +0.0 & 0.39 \\
integrate & -4.7 & -99.9 & -99.9 & -99.9 & -23.3 & 2.11 \\
primes & -0.4 & +0.0 & -3.2 & +0.0 & +0.0 & 0.36 \\
rfib & -0.4 & +0.0 & 0.18 & 0.19 & +0.0 & 0.32 \\
tak & -0.4 & +0.0 & +5.9 & +5.9 & +0.0 & 0.32 \\
wheel-sieve2 & -1.5 & -6.9 & 0.19 & -1.9 & +2.1 & 0.47 \\
% \hline
% Min & -8.9 & -95.0 & -95.0 & -95.0 & -23.3\\
% Max & -0.3 & +8.7 & +5.9 & +5.9 & +2.1\\
% Geometric Mean & -2.3 & -31.2 & -38.8 & -34.2 & -3.0\\
\end{tabular}
\caption{Supercompilation+normalization+boring expressions+discarding expressions compared with Supercompilation+normalization+boring expressions+discarding expressions+tainting functions}
\label{tab:scpnormbordiscvsscpnormbordisctaint}
\end{table*}

Tainting expressions (Table
\ref{tab:scpnormbordiscvsscpnormbordisctaint}) gives an additional
decrease of binary size and compilation with two benchmarks showing
speedups: the performance of integrate is improved compared to
ordinary optimization and {\it wheel-sieve2} is back to the same performance
as without supercompilation. {\it Digits-of-e1} becomes slightly worse, but
there is still a 16\% reduction of memory compared to ordinary
optimization and the compilation time is reduced to less than two seconds.

We finally give the full table with a greater selection of benchmarks
from both the spectral and imaginary parts of nofib in Table
\ref{tab:tot}. {\it Integrate} is the benchmark with the biggest size
increase at 4.3\%, but the supercompiler also manages to remove nearly
one fifth of the total allocations. 

\begin{table*}
\begin{tabular}{lrrrrrr}
Program & Size & Allocs & Runtime & Elapsed & TotalMem & Compilation Time (s)\\
\hline
bernouilli & +1.0 & -2.3 &  +0.0 & -2.9 &  +0.0 & 0.64 \\
digits-of-e1 &     +1.9 &   -32.9 &   -23.5 &   -21.9 &   +0.0 & 1.29 \\
exp3\_8  &     +0.1   &  -16.7  &  -17.6 &   -19.8 &    +0.0 & 0.39 \\
integrate   &       +4.3  &  -18.7  &   -0.6  &   -2.6 &    +0.0 & 2.11\\
primes   &       +0.1 &    +0.2  &  -17.1  &  -17.4  &   +0.0  & 0.36\\
rfib  &        +0.1 & +1599533.0  &    0.18    &  0.19 &    +0.0 & 0.32 \\
tak     &     +0.1  &   -0.3 &    -6.5  &   -6.5 &    +0.0 & 0.32 \\
wheel-sieve2  &      +0.1 &    +0.0    &  0.19&     +0.0  &   +0.0 & 0.47 \\
atom       &   +3.0  &  -32.3  &  -49.8   & -49.4 &   -33.3 & 1.50  \\
circsim     &     +0.6  &   -1.5   &  -2.3  &   -2.6  &   -4.8 & 1.12\\
clausify    &      +0.6   &  -1.9   &  -0.7  &   -0.7  &   +0.0 & 0.71\\
constraints &         +0.7  &  +14.3 &   -33.7 &   -33.9 &   -96.9 & 0.80\\
cryptarithm1&          +0.3   &  -7.5  &   -5.6   &  -3.4   &  +0.0 & 0.38 \\
eliza      &    +1.2 &   -40.8  &    0.00   &   0.00  &   +0.0 & 1.09\\
fish       &   +2.1  &   -4.9   &   0.01  &    0.01  &   +0.0 & 0.92 \\
gcd        &  +0.6   &  -5.8   &   0.09  &    0.10   &  +0.0 & 0.51 \\
lcss       &   +1.4  &  +10.3  &   +8.8 &   +10.2 &   -11.1 & 0.82 \\
life       &   +0.4   &  +1.2   &   0.13   &   0.14  &   +0.0 & 0.52 \\
mandel2    &      +1.3  &   +4.5  &    0.00  &    0.00  &   +0.0 & 0.99 \\
minimax    &      +0.1  &   +0.0  &    0.00  &    0.00  &   +0.0 & 0.30\\
pretty     &     +0.6  &   -3.3   &   0.00  &    0.00  &   +0.0 & 0.54 \\
primetest  &        +3.6 &    -0.2  &   +0.0 &    +0.0  &   +0.0 & 1.58\\
\end{tabular}
\caption{ghc -O2 compared with Supercompilation with all features enabled}
\label{tab:tot}
\end{table*}

{\it Circsim} is another interesting example, because it consists of about
400 lines of code and compiles in 1.12 seconds with the supercompiler
turned on. The supercompiler manages to reduce the memory allocations
slightly and give 0.6\% binary size increase.

We saw that before adding the tainting of functions it was possible
for the supercompiler to perform a lot of unnecessary work by
speculatively supercompiling an expression, discard the result,
supercompile the subexpressions, discard those results, and so on. One
possible strategy to mitigate this further is to keep the
supercompiled result around as a cache that successive
supercompilation of subexpressions can fold against, thereby avoiding
to repeat work.

Our experience so far is that the discarding of functions is not
preventing optimizations, on the contrary: programs that were
optimized by the supercompiler without discarding expressions are
actually slightly faster when discarding the large useless
specializations that ended up in the program previously.

\section{Implementation Notes}
\label{sec:impl}

This section contains an outline of the most obvious issues and areas
for improvement that any programmer will come across when implementing
a supercompiler. 


\subsection{Parallelism}

The supercompiler is currently defined in a very sequential way: it is
not possible to inspect the store unless the previous parts of the
expression is supercompiled and the store contains all the new
definitions. Beyond a lot of infrastructure hacking it appears that
lifting this restriction while preserving code sharing is an
interesting algorithmic problem that probably requires some research.

There are however some parts of the supercompiler as it is currently defined that are inherently parallel: the testing for folding and non-termination in \<\asdr\aedr\> can easily be done in parallel since the common case is that there are several possible candidates to test against. This gave a measurable speedup in an an earlier version of our prototype but had to be removed because other parts of GHC are not threadsafe. 

\subsection{Name Capture}
\label{sec:namecapture}

Avoiding name capture can cause significant churn and make the supercompiler dreadfully slow. \citet{Bolingbroke:2010:Supercompilation} report that for a particular example 42\% of their supercompilation time is spent on managing names and renaming. 

Our current implementation uses eager substitutions with the scheme outlined by \citet{Jones:2002:Secrets}. There are two obvious improvements to this: using a lazy substitution that the supercompiler applies as it traverses the expression would avoid some churn, and this could be further reduced by allowing some shadowing during supercompilation.


\subsection{Representation Improvements for the Homeomorphic Embedding}

Our implementation stores expressions annotated with their size in the memoization list. These annotations can be used for avoiding some testing altogether: an expression can only fold against an expression of equal size and an expression can never be homeomorphically embedded in a smaller expression. A similar representation was also independently suggested by Ilya Klyuchnikov so this seems to be a well known optimization in the supercompilation community.



\subsection{Splitting Typed Terms}

The most obvious difference between our implementation and the
algorithm described in this paper is that the intermediate language of
GHC is a typed language \citep{Sulzmann:2007:System}. This brings
additional complexity when generalizing similar terms of different type
against eachother.

\citet{Pfenning:1991:Unification} has already identified our problems:
the presence of binders in expressions and the presence of types in
binders. There are two advantages for our particular setting: 1) type
variables are the top element for types; and 2) it is safe to fail
during generalization and call split on the term instead.

After having implemented the type generalization we noticed that it was not performed very often in practice on our examples from nofib. The main cost related to this feature appears to be the implementation cost. 

% Suppose we split \<F e\> and \<F e'\> against each other, and the resulting term is \<F x\>. What type should {\it x} have? Answer: Not typeof(e) or typeof(e'), but the type of the parameter to g.


\section{Related Work}

\citet{Turchin:1986:TheConcept} invented supercompilation in the
context of the functional language Refal. The supercompiler Scp4
\citep{Nemytykh:2003:Supercompiler} is implemented in Refal and is the
most well-known implementation from this line of work.
\citet{Soerensen:1996:Positive} and
\citet{Secher:1999:Masters,Secher:1999:Perfect} presented
supercompilers formulated for pure first order functional languages
but never reported anything about the performance of the algorithms or
the resulting programs.

More recently there has been a spur of activity in actual implementations of supercompilers: 
\begin{description}
\item[Supero] Supero \citep{Mitchell:2008:ASupercompiler,Mitchell:2008:Transformation} could optimize a text book example of word counting written in Haskell to the same performance as a C program performing the same task. The latest version has changed the design significantly in order to improve performance of the supercompiler and \citet{Mitchell:2010:Rethinking} report compilation times below 4 seconds for all examples. 
\item[CHSC] \citet{Bolingbroke:2010:Supercompilation} presented a supercompiler with call-by-need semantics that did not require its input to be lambda lifted. 
\item[HOSC]  \citet{Klyuchnikov:2009:Proving,Klyuchnikov:2010:Towards} have implemented HOSC in Scala and used it for proving equivalence of terms.
\item[Others] \citet{Reich:2010:Supercompilation} use supercompilation to optimize programs intended to run on the Reduceron, an FPGA-based soft processor for executing lazy functional programs. They report average performance boosts on a set of programs of 40\%. Supercompilation has also been investigated in a call-by-value setting and can give good speedups there too \citep{Jonsson:2009:Positive,Jonsson:2010:Strengthening}.
\end{description}

Narrowing-driven partial evaluation
\citep{Alpuente:1998:Partial,Albert:2001:The} is the functional logic
programming equivalent of positive supercompilation but formulated as
a term rewriting system. Partial evaluators such as Ecce and Logen \citep{Leuschel:2006:Ecce} seem to be more popular approaches in the logic programming community and  more recent work has focused on scaling partial evaluation so that it can be applied to large programs \citep{Leuschel:2009:Fast,Vidal:2010:Hybrid}. 

\section{Future Work}

Supercompilation is still a rather expensive optimization, but it can
undoubtedly produce great results on high level Haskell programs. The
major obstacle we see at the moment is that supercompilation might
prevent the compiler from applying other optimizations, which in turn
can increase the runtime of the final executable by several orders of
magnitude. There are several possible ways to tackle this problem:
\begin{itemize}
\item Integrate other optimizations into the supercompiler
\item Make the supercompiler output programs that are friendly to other optimizations
\item Strengthen other optimizations so that they can optimize the output from the supercompiler
\end{itemize}

The approximation of boring expressions could be extended in several
ways to avoid transforming expressions that will give bad results. One
observation is that the first call to reverse with an accumulating
parameter (\<reverse xs []\>) is not boring since it has a known
constructor in the parameter, but by inspecting the body of
\<reverse\> it is obvious that this parameter is never used. One idea
is to extend boring expressions to utilize strictness information so
that it would discard this example because the static information
present in the context is never used.

There is certainly room to improve the decision whether to discard supercompiled expressions. The constants currently used could be tuned further, and there is also the possibility to use other information that is present in the program.

A route that we have not explored is to use different acceptable-predicates for different parts of the supercompiler. Rule R18 and R19 could be extended with a similar test.

We observed that there are sometimes several candidates in the memoization list that the supercompiler could generalize the current expression against. Our current implementation selects the first one which is not necessarily the best candidate. A ranking function between different candidates would be useful.

\citet{Bolingbroke:2010:Supercompilation} have presented a call-by-need algorithm for supercompilation. We believe that the algorithm presented in this paper could be adjusted to call-by-need semantics as well. 

\citet{Leuschel:2002:Homeomorphic} has investigated interesting
variations of the homeomorphic embedding that we believe are
compatible with our design choices and could be adapted to work on our
zipper representation.

The focus in this paper has been on a practical algorithm that can supercompile programs without risking code explosion. We believe that our previous proofs of correctness of a closely related algorithm \citep{Jonsson:2009:Positive} should go through without much adjustment for the algorithm presented.

\section{Conclusions}

We have presented a supercompilation algorithm and shown that it can give significant speedups on programs from the nofib suite even under a tight code budget constraint. We have also shown that larger programs are supercompiled in reasonable time and also benefits from the aggressive inlining and specialization that our supercompiler performs.

%\section{Introduction}

% We explore one part of the design space for a positive
% supercompiler. We deliberately sacrifice transformational power
% for reduced compilation time. Supero \citep{XXX} occupies a different
% part of the design space: the resulting binaries are much faster.

% Components: Positive Supercompilation using Leuschel's extended
% homeomorphic embedding with Supero's bowtie for generalisation. We
% improve the actual performance of the supercompiler by using a zipped
% term representation which allows us to quickly discard terms for
% testing.

% Our contributions are:
% \begin{itemize}
% \item A faster algorithm for positive supercompilation using a zipper
%   to represent the terms.
% \item A new generalisation and whistle operating on this zipped
%   representation.
% \item Heuristics to prune terms early from testing.
% \end{itemize}

% \section{Language}
% \label{sec:lang}

% Our language of study is System $F_c$ \citep{Sulzmann:2007:System}
% extended with primitive values and explicit function names.

% We let constructor symbols be denoted by {\em K}. Let {\em F} range over a
% set $\mathcal{F}$ of global function definitions, where all functions
% have a specific arity.

% The language contains integer values $n$ and arithmetic
% operations $\oplus$, although these meta-variables can preferably be
% understood as ranging over primitive values in general and arbitrary
% operations on these. We let $+$ denote the semantic meaning of
% $\oplus$.

% A program is an expression with no free variables and all function
% names defined in $\mathcal{F}$.  The intended operational semantics is
% call-by-need. Capture free substitution expressions $\overline{e}$ for
% variables $\overline{x}$ in $e'$ is denoted by
% $[\overline{e}/\overline{x}]e'$.


% \section{Supercompilation}
% \label{sec:scp}

% \begin{figure}
% The outer context:
% \begin{equation*}
% \R ::= \epsilon \alt \mathcal{G}:\R
% \end{equation*}
% Each frame:
% \begin{equation*}
% \mathcal{G} ::=  
%       \boxempty \, e
%       \alt            \boxempty \, \tau
%       \alt            \boxempty\, \blacktriangleright \gamma
%       \alt            \boxempty\, \oplus e
%       \alt            e' \oplus \boxempty
%       \alt             \CASE\, \boxempty \, \OF \, \{ p_i \arr e_i \} 
% \end{equation*}

% \begin{equation*}
% \rho ::= \epsilon \alt \nu:\rho
% \end{equation*}
% \begin{equation*}
% \nu ::= (h, \overline{x}, F, \R)
% \end{equation*} 
% \begin{equation*}
% \sigma ::= (\nu, e')
% \end{equation*}
% \caption{The definitions for Simon's algorithm}
% \label{fig:framedef}
% \end{figure}

% Our supercompiler is defined as two mutually recursive functions that
% pattern-match on expressions and contexts in order to rewrite
% expressions. The first algorithm is called the {\em driving}
% algorithm, used to perform evaluation steps, and the second algorithm
% is called the {\em building} algorithm, which reassembles the
% transformed expression. These algorithms are defined in Figure
% \ref{fig:drivalg}.  Two additional parameters appear as subscripts to
% the rewrite rules: a memoization list $\rho$ and the set of global
% functions $\mathcal{F}$. The memoization list holds information about
% expressions already traversed and is explained more in detail in
% Section \ref{sec:apprule}.

% We use e' to denote OutExprs. 

% A reduction context $\R$, as defined in Figure \ref{fig:framedef}, is
% a term containing a single hole $[\,]$, which indicates the next
% expression to be reduced. The expression $\con{e}$ is the term
% obtained by replacing the hole in $\R$ with $e$. $\overline{\boxempty\,
%   e}$ denotes a list of application contexts.

% \begin{figure*}
% \begin{tabular}{lllr}
% General form: \\
% $\dr{e}{\R} = (e', \sigma')$ \\
% ~ \\
% Evaluation Rules \\
% $\dr{e\,\blacktriangleright \gamma_1}{(\boxempty\,\blacktriangleright \gamma_2:\R)}$ & = & $\dr{e}{(\boxempty\, \blacktriangleright (\gamma_1 \circ \gamma_2):\R)}$ & (R1) \\  
% ~ \\
% $\dr{n_j}{(\CASE \boxempty\,\, \OF \{n_i \arr e_i \}:\R)}$ & = & $\dr{e_j}{\R} $ & (R2) \\
% $\dr{n}{(n_1 \oplus \boxempty:\R)}$ & = & $\dr{n_2}{\R}$, where $n_2 = n_1 + n$ & (R3) \\
% ~ \\
% $\dr{F}{\R}$ & = & $\adr{F}{\R}$ & (R4) \\
% ~ \\
% $\dr{K_j}{(\overline{\boxempty\, e}:\CASE \boxempty\,\, \OF \{K_i\,\overline{x}_i \arr e_i \}:\R)}$ & = & $\dr{\LET \overline{x}_j = \overline{e} \IN  e_j}{\R}$ & (R5)\\
% $\dr{K_j}{(\overline{\boxempty\, e}:\boxempty\, \blacktriangleright \gamma:\CASE \boxempty\,\, \OF \{K_i\,\overline{x}_i \arr e_i \}:\R)}$ & = & $\dr{\LET \overline{x}_j = \overline{e} \IN  e_j}{\R}$, XXX: KPush & (R6)\\
% ~ \\
% $\dr{\lambda x.e}{(\boxempty\,\,e':\R)}$ & = & $\dr{\LET x = e' \IN e}{\R}$ & (R7) \\
% $\dr{\lambda x.e}{(\boxempty\, \blacktriangleright \gamma:\R)}$ & = & $\dr{evalPush\, \lambda x.e \blacktriangleright \gamma}{\R}$ & (R8)\\
% $\dr{\lambda x.e}{\R}$ & = & $\MLET (e', \sigma_1) = \dr{e}{\epsilon}$ & (R9) \\
% & & $\MIN \ers{\lambda x.e'}{\R}$ \\
% ~ \\
% $\dr{\Lambda a.e}{(\boxempty\,\,\varphi:\R)}$ & = & $\dr{[\varphi/a]e}{\R}$ & (R10) \\
% $\dr{\Lambda a.e}{(\boxempty\, \blacktriangleright \gamma:\R)}$ & = & $\dr{evalPush\, \Lambda a.e \blacktriangleright \gamma}{\R}$ & (R11)\\
% $\dr{\Lambda a.e}{\R}$ & = &$\MLET (e', \sigma_1) = \dr{e}{\epsilon}$ & (R12) \\
% & &  $\MIN \ers{\Lambda a.e'}{\R}$ \\
% ~ \\
% $\dr{\LET x=v \IN e}{\R}$ & = & $\drlg{e}{\LET}$, where $\mathcal{F}' = \mathcal{F} \cup (F, v)$ & (R13) \\ 
% $\dr{\LET x=y \IN e}{\R} | y \notin$ {\it SPLITVARS} & = & $\dr{[y/x]e}{\R}$  & (R14) \\ 
% $\dr{\LET x=e \IN e'}{\R} |$ linear x e' & = & $\dr{[e/x]f}{\R}$ & (R15) \\ 
%  \hspace{11.3em}$|$ otherwise  & = & $\MLET (e_1, \sigma_1) = \dr{e}{\epsilon} $ \\ 
% & & \hspace{1.1em} $(e_2, \sigma_2) = \drs{e'}{\R}$\\ 
% & & $\MIN (\LET x = e_1 \IN e_2, \sigma_2)$  & \\
% ~ \\
% $\dr{\LETREC F = e \IN e'}{\R}$ & = & $\drlg{e'}{\LETREC}$,  where $\mathcal{F}' = \mathcal{F} \cup (F, e)$  & (R16) \\
% ~ \\
% Focusing Rules\\
% $\dr{e_1 \oplus e_2}{\R}$ & = & $\dr{e_1}{(\boxempty\, \oplus e_2:\R)}$ & (R17) \\  
% $\dr{e_1\, e_2}{\R}$ & = & $\dr{e_1}{(\boxempty\,\, e_2:\R)}$ & (R18) \\
% $\dr{e\, \varphi}{\R}$ & = & $\dr{e_1}{(\boxempty\,\, \varphi:\R)}$ & (R19) \\
% $\dr{\CASE e\, \OF  \{p_i \arr e_i \} }{\R}$ & = & $\dr{e}{(\CASE \boxempty\, \OF  \{p_i  \arr e_i \}:\R)}$ & (R20) \\
% $\dr{e \blacktriangleright \gamma}{\R}$ & = & $\dr{e}{(\boxempty\, \blacktriangleright \gamma:\R)}$ & (R21)\\
% ~ \\
% Fallthrough \\
% $\dr{e}{\R}$ & = & $\er{e}{\R}$ & (R22) \\
% ~ \\
% \end{tabular}\\
% \begin{tabular}{lllr}
% Rebuilding Expressions \\
% $\er{e'}{(\boxempty\,\oplus e_2:\R)}$ & = & $\dr{e_2}{(e' \oplus \boxempty:\R)}$ & (R23)\\
% $\er{e'}{(e_1' \oplus \boxempty:\R)}$ & = & $ \er{e_1' \oplus e'}{\R}$ & (R24) \\
% $\er{e'}{(\boxempty\,e:\R)}$ & = & $\MLET (e'', \sigma_1) = \dr{e}{\epsilon}$ & (R25) \\
% & & $\MIN \er{e' e''}{\R}$ \\
% $\er{e'}{(\boxempty\,\varphi:\R)}$ & = & $ \er{e'\, \varphi}{\R}$ & (R26) \\
% $\er{e'}{(\boxempty\ \blacktriangleright \gamma:\R)}$ & = & $ \er{e\blacktriangleright \gamma}{\R}$ & (R27) \\
% $\er{x'}{(\CASE \boxempty\,\, \OF \{p_i \arr e_i \}:\R)}$ & = & $\MLET (e_i', \sigma_i) = \drss{[p_i/x]e_i}{([p_i/x]\R)}$ & (R28) \\
% & & $\MIN (\CASE x'\, \OF \{p_i \arr e_i' \}, \sigma_i)$  \\
% $\er{e'}{(\CASE \boxempty\,\, \OF \{p_i \arr e_i \}:\R)}$ & = & $\MLET (e_i', \sigma_i) = \drss{e_i}{\R}$ & (R29) \\
%  & & $\MIN (\CASE e' \OF \{p_i \arr e_i' \}, \sigma_i)$ \\
% $\er{e'}{\epsilon}$ & = & $(e', \sigma)$ & (R30)\\
% \end{tabular}
% \caption{Two-Driving algorithm}
% \label{fig:drivalg}
% \end{figure*}

% There is an ordering between rules; i.e., all rules must be tried in
% the order they appear. Rules R17-R21 are the default focusing rules
% that extend the given driving context $\R$ and zoom in on the next
% expression to be transformed. If no other rule matches, such as for a
% single variable, rule R22 will match and call build to rebuild the
% expression.

% The program is turned ``inside-out'' by
% moving the surrounding context $\R$ into all branches of the
% case-statement through rules R28 and R29. Rule R15 has a similar
% mechanism for let-statements.

% \begin{figure}
% \begin{tabular}{lll}
% $\drl{e}{L}$ &$\! =\, $& $\MLET (e', \sigma') = \dr{e}{\R}$ \\
% & & $\hspace{1.4em}(\sigma_1, \sigma_2) = storeSplit(\sigma', x)$ \\
% & & $\MIN (\kw{L}\, \sigma_1 \IN e', \sigma_2)$ \\
% \end{tabular}
% \caption{Driving of let-statements}
% \label{fig:adrivlet}
% \end{figure}

% Definition of doBeta:

% \begin{verbatim}
% doBeta :: ScpEnv -> CoreExpr -> [CoreExpr] -> CoreExpr
% doBeta env (Lam b body) args@(a:as)
%  | isTypeArg a = doBeta env (substExpr (extendSubst emptySubst b a) body) as
%  | otherwise = Let (NonRec b a) (doBeta env' body as)
%     where env' = {inSet = b:inSet env} 
% doBeta _ fn args = mkApps fn args
% \end{verbatim}


% \subsection{Application Rule}
% \label{sec:apprule}

% Rule R4 refers to \<\asdr \aedr\>, defined in Figure
% \ref{fig:adrivalg}.  \<\asdr \aedr\> can be inlined in the definition
% of the driving algorithm, it is merely given a separate name for
% improved clarity of the presentation.


% \begin{figure*}
% \begin{tabular}{llllr}
% $\adr{F}{\R}$ &$\! =\, $& $\MLET (\overline{e}', \sigma') = \drs{\overline{e}}{\epsilon}$  & if $\exists(h, \overline{y}, e_1)\! \in \!\rho\,.\, [\overline{e}/\overline{y}] e_1 =  \con{F}$ & (1) \\
% & & $\MIN (h\,\overline{e'}, \sigma')$ \\
% $\adr{F}{\R}$ &$\! =\, $& $\MLET (\overline{f}', \sigma_i) = \drss{\overline{f}}{\epsilon}$ & if $\exists(h, \overline{y},  e_i)\! \in \!\rho\,.\, e_1 \homemb^* \con{F}\!$ & (2)\\
% & &  \hspace{1.1em} $(f_g', \sigma_2) = \drsi{f_g}{\epsilon}$ \\
% & & $\MIN ([\overline{f}'/\overline{y}] f_g', \sigma_2)$  \\
% $\adr{F}{\R}$ &$\! =\, $&$\MLET (e', \sigma_1) = \drp{e}{\R}$ \\
% & & $\MIN (h\,\overline{x}, \sigma_1 \cup (h,  \lambda \overline{x}.e'))$ &  & (3) \\
%   \multicolumn{4}{l}{\hspace{2em} where $(F = e) \in \mathcal{F}$,} \\
%   \multicolumn{4}{l}{\hspace{4.7em} $\rho' = \rho \cup (h, \overline{x}, \con{F})$,}\\
%   \multicolumn{4}{l}{\hspace{4.7em} $h$ fresh,}  \\
%  \multicolumn{4}{l}{\hspace{4.7em} $\overline{x} = \fv(\con{F})$,}\\
%   \multicolumn{4}{l}{\hspace{4.7em} $(f_g, \overline{f}, \overline{y}) = split(\con{F}, e_1)$ }\\
% \end{tabular}
% \caption{Driving of applications}
% \label{fig:adrivalg}
% \end{figure*}

% To ensure termination, we use a variation of the homeomorphic
% embedding relation $\homemb^*$ \citep{XXX} to define a predicate
% called ``the whistle''. The intuition is that when $e \homemb^* f$,
% {\em f} contains all subterms of {\em e}, possibly embedded in other
% terms. For any infinite sequence $e_0, e_1, \ldots$ there exists {\em
%   i} and {\em j} such that $i < j$ and $e_i \homemb^*
% e_j$. Polymorphic recursion might give rise to infinitely many new
% terms, and hence we consider all types $\varphi$ equivalent. This
% condition is sufficient to ensure termination.

% Whenever the whistle blows, our algorithm splits the input expression
% into strictly smaller terms that are transformed separately in the
% empty context. This might expose new folding opportunities, and allows
% the algorithm to remove intermediate structures in subexpressions.

% \section{The Homeomorphic Embedding}

% \subsection{Paralllel Homeomorphic Embedding Test}

% The homeomorphic embedding test can trivially be done in parallel, and
% since we need all the candidates that we might generalise against
% there is no risk of doing unecessary work. This saves 25 seconds on
% the first digits of e benchmark in nofib.

% \subsection{Only Whistle on Terms With the Same Head}

% We can considerably cut down on the number of terms to test against if
% we only test against terms with the same head. This can not be applied
% recursively. 

% \subsection{The Representation Problem}

% Do we think that \<flip (flip t)\> is embedded in \\
% \<\hscase{flip y}{Leaf a \to Leaf a\\ Branch l r \to Branch (flip r) (flip l)}\>

% \subsubsection{Leuschel's Form}

% The two terms are \<flip(flip(x))\> and\\ \<Branch(flip(l),
% flip(r))\>. They are not embedded.

% \subsubsection{Curried Form}

% The two terms are \<App(flip, App(flip, x))\> and\\ \<App(App(Branch,
% App(flip, l)), App(flip, r))\>. The outermost applications matches,
% the rightmost part of them are homeomorphically embedded, and all we
% have to do is to find out if \<flip\> is embedded in
% \<App(Branch,App(flip, l)) \>, which it is.

% \subsubsection{Context Form}

% The terms are \<[e_1]\R\> and \<[e_2]\R'\>.

% \begin{enumerate}
% \item $x \homemb y$
% \item $e_1 = e_2$ and $\R$ and $\R'$ are lock-step embedded.
% \item $[e_1]\R \homemb subterms\, \R'$
% \end{enumerate}

% \section{Splitting Expressions}

% \subsection{New Msg}

% Step through the term and use match to find instances, and fail
% otherwise. This is cheaper than doing the homeomorphic
% embedding on the entire list of previously seen terms and selecting
% the best out of that.

% \subsection{New Split}

% View $\con{F}$ as $[F]\, \R_1:\ldots:\R_{n-1}:\R_n:\epsilon$. Split
% gives two terms: $[F]\, \R_1:\ldots:\R_{n-1}:\epsilon$ and $[x]\,
% \R_n:\epsilon$ where {\em x} is fresh.




% \section{Performance}

% \subsection{Sharing New Function Definintions}

% It is quite common for the case of case-rule to fire. A typical case
% looks something like this:
% \begin{haskell}
% \hsccase{(\hscase{x}{p_1 \to x_1\\ \ldots \\ p_n \to x_n) \hskwd{of}}}{[] \to
%   []\\ (x':xs') \to append xs' zs}
% \end{haskell}
% \noindent Once the case of case-rule is done the code is:
% \begin{haskell}
% \hscase{x}{p_1 \to \hsccase{x_1}{[] \to []\\ (x':xs') \to append xs' zs}\\ \ldots \\ p_n \to \hsccase{x_n}{[] \to []\\ (x':xs') \to append xs' zs}}
% \end{haskell}

% The driving algorithm will transform the call to append twice, and
% create two functions that are both isomorphic to append. Creating the
% functions at the top level and calling the same function from both
% branches saves both transformation work and reduces code size. 

% Using a state monad for the driving algorithm, and have that monad
% store a memoization list augmented with the function definitions will
% allow the second branch to just insert a call to this new function
% created in the first branch, thereby saving a lot of transformation
% effort. 



% \section{Random Notes}


% % \subsection{Implementation: Name Capture}
% % \label{sec:namecapture}

% % Any implementation needs to deal with this, but previous articles
% % barely mentions it except in short remarks. 

% \subsection{Making a Stupid Supercompiler}

% Supercompilation is a complex algorithm. We can simplify parts of it
% and increase the potential sharing of functions for the entire program
% if we are supercompiling multiple functions. This suggests a
% post-phase that cleans up after the supercompiler though, which we
% discuss in Section \ref{sec:tss}.

% \subsection{Evaluation Contexts vs Other Contexts}

% We have a chance of good things happening with interaction between
% non-empty contexts $\R$ and a function in the hole. No such luck with
% an arbitrary context that has the hole outside the focus for
% evaluation. 

% % \subsection{Lambda-lift to Avoid Code Explosion}
% % \label{sec:llac}

% % case (case ... of alts) of (p, q) -> BIG 
% % = letrec f p q = BIG in case (case ... of alts) of (p, q) -> f p q

% \subsection{Boring Contexts}

% Should we specialise functions in boring contexts?

% map f xs is boring. map fst xs is not. case map f xs of alts is not.

% \subsection{Three Stage Supercompilation?}
% \label{sec:tss}

% Having a pre-phase that lambda-lifts big expressions out from case
% branches and similar constructs, as described in Section
% \ref{sec:llac}, will give ``better'' input for the supercompiler to
% work on if code size is a concern.

% A post-phase that inlines non-recursive functions that are only used
% once will compensate for the less clever supercompiler we have.

% \subsection{What if the Supercompiler is too Stupid?}

% How many function definitions do we want from append ``abc'' xs?

% \subsection{Threading Sigma, But Splitting Rho}

% Letting the folding mechanism call the same function when it is
% possible saves work during the transformation since the algorithm can
% immediately fold, and reduces total code size. 

% However, if we fold too eagerly this will miss out on specialisation
% opportunities and this will make the final program perform worse than
% necessary. An example is \<append (append xs ys) zs\>, which when
% transformed will create a function isomorphic to append itself in the
% first branch. The recursive call to \<append (append xs' ys) zs\>
% later during the transformation can fold against \<append ys zs\>, but
% this will prevent any deforestation from happening. 

% We therefore only look for renamings, not instances, when trying to
% fold against things in Sigma. If there exists a specialised version of
% our current function it will use that, and otherwise it will create a
% new specialised copy. 

% Storing the size of the term in Rho allows us to prune the list of
% possible candidates: a renaming has to be of the same size as current
% term. Also storing the function head gives more possibility to prune
% things early when there is no possible match. This turned out to have
% quite drastic performance implications: the pruning saved 20 seconds
% on the first benchmark that computes the digits of e in the nofib
% benchmark suite.

% \subsection{Msg of Typed Terms}

% Given \<f @ Int (x::[Int])\> and \<f @ Double (x::[Double])\>, how do
% we split it? For now: let the msg fail, and do the ordinary split instead. 



% \subsection{Examples}

%See Figure \ref{fig:hommsg}

%% \begin{figure*}
%% \begin{center}
%% \begin{tabular*}{0.8\textwidth}{@{\extracolsep{\fill}}ccccccc}
%% e & & f & $t_g$ & $\theta_1$ & $\theta_2$ \\
%% \hline
%% \<e\> & $\homemb$ & \<Just e\> & \<x\> & $[e/x]$ & $[Just\, e/x]$ \\
%% \<Right e\> & $\homemb$ & \<Right (e, e')\> & \<Right x\> & $[e/x]$ & $[(e, e')/x]$ \\
%% \<fac y\> & $\homemb$ & \<fac (y - 1)\> & \<fac x\> & $[y/x]$ & $[(y-1)/x]$ \\
%% \end{tabular*}
%% \end{center}
%% \caption{Example of the homeomorphic embedding and the msg}
%% \label{fig:hommsg}
%% \end{figure*}









%% \section{Related Work}

%% \section{Conclusions}

%% \subsection{Future Work}

\acks This work was partly funded by an internship at Microsoft
Research. The authors would like to thank Simon Peyton Jones for both
ideas and many suggestions to improve the presentation. We would also
like to thank Colin Runciman, Neil Mitchell, Max Bolingbroke, and Ilya
Klyuchnikov for valuable discussions about supercompilation. Simon
Marlow and Ian Lynagh answered countless questions about GHC which
helped realize our prototype implementation.

\bibliographystyle{plainnat}

\bibliography{pj,partial-eval}

\end{document}
