
\documentstyle[12pt]{article}
\input mssymb                                 
\input /jj/kt/tex/fixqmsfonts
\input /jj/kt/tex/laktex
\input /jj/kt/tex/illustrations
\input /var/arvind/idcompiler/macros/prelude


\pagestyle{empty}

\begin{document}


\subsection*{Kid Rewrite rules}

\subsection*{Inline Substitution}

{
\[ \begin{array}{l}
\frag{F = \underline{{\sf \lambda_{n,m}}} \; (\mv{Z_n}) \; . \;  (E) }
{{\sf Ap_{n,m}} \; (F, \; \mv{X_n}) \;\; \reduce{}{} \;\; 
 ({\tt RB}\;[\![E]\!]) \; [\mv{X_n}/\mv{Z_n} ] }\\
\end{array}\]
}\\

\subsection*{Partial Evaluation}
{
\[ \frag
{F = {\sf \lambda_{n,m}} \; (\mv{Z_n}) \; . \; (E)  }
{ {\sf Apply} \; ( F,X)\;\; \reduce{}{} \;\;
\begin{array}[t]{l}
\{ f = {\sf \lambda_{n-1,m}}\;  (\mv{z_{n-1}}) \; .  \;
(( {\tt RB}\;[\![E]\!]) \; [\mv{z_{n-1}}/\mv{Z_{2,n}},\;X/Z_1])  \\
\;\;\;\; {\sf In} \; f \}
\end{array} } \]
}\\

\newpage

\subsection*{Fetch Elimination}
{
\[ \begin{array}{l}
\frag{X = {\sf Cons} \; (X_1, \; X_2)}
{ {\sf Cons\_1} \;(X) \;\;\;
\reduce{}{}\;\;\; X_1 } \end{array} \]
}\\

{
\[ \begin{array}{l}
\frag{X = {\sf Cons} \; (X_1, \; X_2)}
{ {\sf Cons\_2} \;(X) \;\;\;
\reduce{}{}\;\;\; X_2 } \end{array} \]
}\\


\subsection*{Algebraic Identities}
{
\[ {\sf And} \; ({\sf True},  \;X) \; \reduce{}{} \; X  \] 
\[ {\sf Or} \;( {\sf False},  \;X)  \; \reduce{}{} \; X \]
\[ + \; (X ,0)  \; \reduce{}{} \; X \]
\[ *  \;(X, 1)  \;\reduce{}{} \; X \]
\[ \vdots \] }

\blank

{
\[ {\sf And} \; ({\sf False},  \;X)  \;\reduce{}{} \; {\sf False}  \] 
\[ {\sf Or} \; ({\sf True},  \;X)  \;\reduce{}{} \; {\sf True} \]
\[  *  \;( X,0)  \; \reduce{}{} \; 0 \]
\[  -   \;(X , X)  \; \reduce{}{} \; 0 \]
\[ {\sf Equal?}\; (X,\; X ) \; \reduce{}{} \; {\sf True} \]
\[ \vdots \]}



\blank
{
\[\frag
{X =  +  \;(X_1 ,\underline{m}) \hspace{1cm} \& \;\; \underline{m} > 0}
{{\sf Less} \; (X_1, \;\; X) \;\;\; \reduce{}{}\;\;\;  {\sf True} } \]
\[\frag
{X =  + \;(X_1 , \underline{m})   \hspace{1cm} \& \;\; \underline{m} > 0}
{ {\sf Less} \; (X, \;\; X_1) \;\;\; \reduce{}{}\;\;\;   {\sf False} } \]
\[\frag
{X = + \;(X_1,\underline{m}) \hspace{1cm} \& \;\;  \underline{m} > 0}
{{\sf Greater} \; (X_1,  X) \;\;\; \reduce{}{}\;\;\;   {\sf False} } \]
\[\frag{X =  + \;(X_1, \underline{m}) \hspace{1cm} \& \;\; \underline{m} > 0}
{ {\sf Equal?} \; (X_1, \; X )\;\;\; \reduce{}{}\;\;\;  {\sf False} } \]
}
\[\vdots\]

\newpage

\subsection*{Common Subexpression Elimination}
{
\[ \frag
{\mv{Y_m} = P\!F\!N_m \;(\mv{X_n})}
{PFN_m \;(\mv{X_n}) \; \;\; \reduce{}{} \;\;\;  \mv{Y_m}  } \] 
}\\

\newpage


\subsection*{Lift Free Expressions}
{
\[ \frag
{\& \;  F\!E(E,{\sf \lambda_{n,m}} \;(\mv{Z_n}) \; . \; (\{_{\sf m} \;
Y = E; \; S\; {\sf In} \; \mv{X_m} \; \} ))}
{
\begin{array}{lll}
{\sf \lambda_{n,m}} \; ( \mv{Z_n}) \; . \; (\{_{\sf m}\; Y = E; \; S\; {\sf In} \; \mv{X_m} \;  \} ) & \reduce{}{} &
\{_{\sf m} \; \begin{array}[t]{lll}
t_1 & = & E ; \\
t & = & {\sf \lambda_{n,m}} \; (\mv{Z_n}) \;.\; (\{_{\sf m} \;
 Y = t_1 ;\; S  \; {\sf In} \; \mv{X_m} \; \})  \\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; t \; \} }
\end{array} 
\end{array} }
\]}\\


\subsection*{Hoisting Code out of a Conditional}
{
\[\frag
{\& \;  F\!E(E,({\sf Boolcase_n} \; (X, \; \{_{\sf n} \;
 Y = E;\; S \;\; {\sf In} \; \mv{X_n}  \;   \}, \; \{_{\sf n} \;
 Y' = E; \; S' \; \; {\sf In} \; \mv{X_n'} \;  \})))}
{ \begin{array}{l}
{\sf Bool\_case_n} \; (X, \; \{_{\sf n} \;
 Y = E;\; S \; \; {\sf In} \; \mv{X_n} \;  \}, \; 
\{_{\sf n} \; Y' = E; \; S' \;\; {\sf In} \; \mv{X_n'} \;  \} )
\;\; \reduce{}{} \\
\hspace{2cm}{
\{_{\sf n} \; \begin{array}[t]{lll}
 t_1 & = & E;\\
 \mv{t_n} & = & {\sf Bool\_case_n} \; (X,\\
& & \hspace{0.3cm}  \; \{_{\sf n} \; Y = t_1;\; S \;\;
{\sf In} \; \mv{X_n} \;  \}, \\
& & \hspace{0.3cm} \; \{_{\sf n} \; Y' = t_1; S'
\;\; {\sf In} \; \mv{X_n'} \} )\\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; \mv{t_n} \; \} }
\end{array}}
\end{array} } \] }

\newpage

\subsection*{Eliminating Circulating Variables}

\blank
\noindent

{
\[ \begin{array}{l} 
\frag{ \begin{array}{ll}
P = \underline{{\sf \lambda_n}} \; (\mv{X_n}) \; . \; ( E) & \mid \\
B = \underline{{\sf \lambda_{n,n}}} \; (\mv{X'_n}) \; . \;  
 (\{_{\sf n} \; S \; {\sf In }\;\mv{Z_{n-1}},\; X'_n \} )
\end{array} }
{
\begin{array}{l}
{\sf WLoop_n} \;(P, \; B, \; \mv{Y_n}, \; Y_p) \;\;\; \reduce{}{} \\
\hspace{1.2cm}{
\{ \begin{array}[t]{l}
p  =  \underline{{\sf \lambda_{n-1}}} \; ( \mv{x_{n-1}}) \; . \;
({\tt RB}[\![E]\!]\;[\mv{x_{n-1}}/\mv{X_{n-1}},\; Y_n/X_n]);  \\
b =  \underline{{\sf \lambda_{{n-1},{n-1}}}} \;(\mv{x'_{n-1}}) \; . \; 
({\tt RB}[\![\{_{\sf n-1} \; S \; {\sf In} \; \mv{Z_{n-1}} \}]\!]\;
[\mv{x'_{n-1}}/\mv{X_{n-1}},\;Y_n/X'_n]) ;\\
\mv{t_{n-1}} = {\sf WLoop_{n-1}} \;(p, \; b, \; \mv{Y_{n-1}}, \; Y_p) \\
\;\;\; {\sf In} \; \mv{t_{n-1}},\; Y_n \}
\end{array} }
\end{array} }
\end{array} \] }\\

\newpage



\subsection*{Eliminating Circulating Constants  }


{
\[\frag
{\begin{array}{ll}
P = \underline{{\sf \lambda_n}} \; (\mv{X_n}) \; . \; ( E) & \mid \\
B = \underbrace{\underline{{\sf \lambda_{n,n}}} \; (\mv{X'_n}) \; . \;  
 (\{_{\sf n} \; S \; {\sf In }\; \mv{Z_n} \})}_\rho 
\;\; \&\;\;  FE(Z_n,\rho)  \\
\end{array}}
{
\begin{array}{l}
{\sf WLoop_n} \;(P, \; B,
\; \mv{Y_n}, \; Y_p) \;\;  
 \;\; \reduce{}{} \\
\hspace{2cm}
{\begin{array}{l}
{\sf Bool\_case_n} \;( Y_p, \\
\hspace{2cm}{
\{_{\sf n} \begin{array}[t]{lll}
p & = & \underline{{\sf \lambda_{n-1}}} \; ( \mv{x_{n-1}}) \; . \;
({\tt RB}[\![E]\!]\;[\mv{x_{n-1}}/\mv{X_{n-1}},\; t_n/X_n]);\\
b & = & \underline{{\sf \lambda_{n-1,n}}} \;(\mv{x'_{n-1}}) \; . \; 
({\tt RB}[\![\{_{\sf n-1} \; S \; {\sf In} \; \mv{Z_{n-1}} \}]\!]\;
[\mv{x'_{n-1}}/ \mv{X'_{n-1}},\; t_n/X'_n]);\\
\mv{t_n}  & = & {\sf Ap_{n,n}} \; (B, \; \mv{Y_n});\\
t_p & = & {\sf Ap_{n-1}} \; (p, \; \mv{t_{n-1}});\\
\mv{t_{n-1}'} & = &
 {\sf WLoop_{n-1}} \;(p, \; b, \; \mv{t_{n-1}}, \; t_p) ; \\
\multicolumn{3}{l}{ \;\;{\sf In} \; \mv{t_{n-1}'}, \; t_n \},}
\end{array}} \\
\hspace{2cm} \;\; \mv{Y_n} )
\end{array}}\\
\end{array}} \]}

\pagebreak

\subsection*{Peeling the Loop once}
{
\[
\begin{array}{lll}
\begin{array}{l}
{\sf FLoop_n} \;(U, \; D, \; B, \; \mv{X_{n}} ,\; X)\\
\end{array} & \reduce{}{} &
\begin{array}[t]{l}
{\sf Bool\_case_n} \;( X, \; 
\{_{\sf n} \begin{array}[t]{lll}
 \mv{t_{2,n}} & = & {\sf Ap_{n,n-1}} \; (B,  \; \mv{X_{n}}) ;\\
t_1 & = & {\sf +} \; ( X_1, \; D); \\
 t_{p} & = & {\sf <} \; (t_1, \; U);\\
\mv{t_n'} & = & {\sf FLoop_n} \;(U, \; D, \; B, \;  \mv{t_{n}},\; t_{p})  \\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; \mv{t_n'} \}, }
\end{array} \\
\hspace{2.3cm}  \; \mv{X_n} )
\end{array}
\end{array}
\]}

\newpage

\blank

\subsection*{Loop Body Unrolling K times }
{
\[\frag
{\hspace{1cm}\& \;\; \mbox{remainder}\; ((U\!-\!X_1)/D, \underline{k}) = 0}
{
\begin{array}{lll}
{\sf FLoop_n} \;( U, \; D, \;  B, \; \mv{X_{n}}, X_p)
& \reduce{}{} &
 \{_{\sf n} \; \begin{array}[t]{lll}
 b & = & \underline{{\sf \lambda_{n,{n-1}}}} (\mv{x_n})\;\;.\;\;
(\{_{\sf n-1}\begin{array}[t]{lll}
\mv{t_{2,n}^1} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{x_n});\\
t_1^1 & = & {\sf +} \; (X_1, \; D);\\
\mv{t_{2,n}^2} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{t_n^1});\\
t^2_1 & = & {\sf +} \; (t_1^1, \; D);\\
\multicolumn{3}{l}{ \;\;\;\;\vdots }\\
\mv{t_{2,n}^k} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{t_n^{k-1}})  \\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_{2,n}^k} \}\;); }
\end{array}\\
\mv{t_n} & = & {\sf FLoop_n} \;(U, \; D, \; b, \; \mv{X_n}, \; X_p);\\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_n} \} \;  } 
\end{array}
\end{array}}
\]}

\end{document}
