% TRANSLATION OF ID INTO KID
% TRANSLATION OF KID INTO P-TAC
% 
%*****************************************************************************
% History:
% 
%       -  Note that in the store rules we do not need the test
%          to check if the indexes are grounded because the
%          Store is always inside an if and the boolean expression tests
%          if the index is inside bounds.
%*****************************************************************************
 

\documentstyle[10pt]{article}

\input /jj/ariola/macros/prelude

\begin{document}

\title{A Syntactic Approach to Program Transformations}

\author{{\it Zena M. Ariola}\\
Aiken Computational Laboratory\\
Harvard University \and
{\it Arvind}\\
Laboratory for Computer Science\\
Massachusetts Institute of Technology
}

\date{December 10, 1990}

\maketitle

\begin{center}
{\bf Abstract}
\end{center}

\bigskip

\begin{minipage}{6in}
Kid, a language for expressing compiler
optimizations for functional languages is introduced. The language
is $\lambda$-calculus based but treats let-blocks as first
class objects. The language goes beyond $\lambda$-calculus by including
I-structures which are essential to express efficient translations
of list and array comprehensions. A calculus and a interpreter
for Kid are developed. Many commonly known 
program  transformations are also presented. A {\em partial evaluator}
for Kid is developed and a notion of {\em correctness} of Kid
transformations based on the syntactic structure of
terms and {\em printable answers} is presented.

\bigskip

{\bf Keywords and phrases}:
$\lambda$-calculus, Term Rewriting Systems, Contextual Reduction Systems, Confluence, Optimizations,
Correctness.
\end{minipage}


\section{Introduction}

Most compilers have a machine independent 
phase followed by one or more back-ends that generate
code for  specific machines. Compiler optimizations
in the machine-independent phase have long term pay offs
and are consequently very desirable. Clean semantics of
declarative languages offer great opportunities for 
machine-independent optimizations and analyses. It
is, therefore, desirable to have an intermediate
language with proper semantics  where
optimizations can be expressed as source-to-source
transformations.  Such an intermediate  language must have the 
capability to express operational concerns. The idea
of having a calculus that reflects what happens operationally
goes back to the work of Plotkin \cite{Plotkin75}. \\


Experience of many researchers has shown that 
the $\lambda$-calculus with constants is not
adequate as an intermediate language for
compilers of functional languages.  One of
its primary deficiency is the inability to
capture the sharing of  subexpressions. 
Avoiding repeated evaluation of an expression 
is a central concern in implementations of
non-strict  functional languages.  Not surprisingly graph reduction
\cite{Wadsworth}, \cite{Turner} \cite{Joh84}, 
has been one of the popular ways of 
implementing functional languages, but it is only 
recently that people have investigated suitable
calculus for graph rewriting \cite{Dutch86}, \cite{Kennaway90},
and \cite{Bru87}. \\

Another major short coming of $\lambda$-calculus, or any other purely 
functional language, is the inability to express
``efficient'' translations of list and array comprehensions.
The usual translations \cite{Peyton-Jones87}
are unnecessarily sequential and elude to other implementation tricks
to avoid construction of intermediate data structures. We believe
I-structures are essential to express realistic translation of
many constructs in a language such as Haskell \cite{Hudak90a} and
Miranda \cite{Turner85}.\\
 
We, therefore, introduce Kid, a programming language, and its associated
calculus. 
Kid is essentially the $\lambda$-calculus plus the
block construct. However, the ``block'' is not treated merely as syntactic sugar for
applications. 
Kid also contains I-structures \cite{Arvind89c} which take us beyond the
realm of pure functional languages. Kid 
embodies the novel idea of {\em multiple values} as well.
Kid is a much more refined version of the language
P-TAC presented earlier by the authors \cite{Zena89}.\\

Having formalized the calculus, what we want to show is that 
questions related to correctness of optimizations can be
precisely formalized. Usually questions related to correctness
take us in the realm of model theories, because, equality
of terms can not be derived from the formal system.
As an example, consider a very simple rule, called {\sf alg},
\[ {\sf And}\;({\sf True}, \; X) \;\reduce{}{} \; X \]
A notion of $\alpha$-equivalence will certainly not be enough to show that
the above rule is safe.
However, by defining different notions of equivalence
between terms in a syntactic domain, 
we will be able to relate any two term $M$ and $N$ such that
$M \reduce{}{{\sf alg}} N$.
As we will see, these equalities are based on the answer 
associated to a term, where the answer is the maximal information
that a term can produce.
Informally, we will consider an optimization to be correct if
for any two programs $M$ and $N$, where $N$ is the optimized version of $M$,
the answer of $N$ is more defined than the answer of $M$. If
the optimized program produces more information, we are still willing to
call that optimization correct.
What we are after is a complete {\em syntactic characterization of
interesting program equivalences}.\\

In Section \ref{syntaxandrules} we introduce Kid
and informally explain the translation of list comprehensions using
I-structures.
In Section \ref{crsintro} we introduce 
Contextual Reduction Systems (CRS's) and give basic rules for CRS's.
A notion of canonical terms is also developed. Kid
rewrite rules and a calculus for Kid are presented
in Section \ref{rules}. We also present the notion of
printable answers associated with Kid terms and give a normalizing 
interpreter that produces these answers for any Kid term.
Section \ref{optirules} contains optimizations and a partial evaluator for Kid.
The correctness of Kid transformations is presented next.
Finally we give our thoughts on future work.


{\small
\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
\\
$\begin{array}{lll}
M\!V & \in & \mbox{Multiple Variable}\\
S\!E & \in  & \mbox{Simple Expression} \\
P\!Fi_m & \in & \mbox{Primitive Function with i arguments and m outputs}\\
Ap\_E_m & \in & \mbox{Applicative Expression with m outputs}\\
Case\_E_m & \in & \mbox{Case Expression with m outputs}\\
Loop\_E_m & \in & \mbox{Loop Expression with m outputs}\\
lambda\_E & \in & \mbox{Lambda Expression}\\
E\_m & \in & \mbox{Expression with m outputs}\\
\end{array}$ \\
\\
$\begin{array}{llll}
Variable & ::= & x \mid y \mid z \mid \cdots \mid a \mid b \mid \cdots \mid 
               f \mid \cdots \mid x_1 \mid \cdots   \\

{M\!V}_m & ::= & \underbrace{Variable, \cdots,  Variable}_m  \\

Constant & ::= & Integer \mid Boolean \mid {\sf ()} \mid  ({\sf Not})
                 \mid \cdots \mid {\sf (+)} \mid {\sf (-)} \mid \cdots \\
         &     & \mid {\sf Nil} \mid {\sf Make\_array}
                 \mid {\sf Error} \mid {\top} \\

S\!E & ::= & Variable  \mid Constant \\

{S\!E}_m & ::= & \underbrace{S\!E, \cdots,  S\!E}_m \mid 
                 S\!E,S\!E_{m-1} \mid S\!E,S\!E,S\!E_{m-2} \mid \cdots  \\

P\!F1_1 & ::= & {\sf Negate} \mid  {\sf Not}\mid  {\sf Bounds}
                \mid {\sf I\_array} \mid {\sf Open\_cons}
                \mid  {\sf Cons\_1} \mid {\sf Cons\_2} \\

P\!F1_m & ::= & {\sf Detuple_m} \\

P\!F2_1 & ::= & {\sf +} \mid {\sf -} \mid {\sf *} \mid \cdots \mid
                {\sf Equal?} \mid  {\sf Eq?} \mid {\sf <} \mid \cdots
                \mid {\sf And} \mid  {\sf Cons} \mid {\sf Apply} \mid {\sf Apply}_{pe} \mid
                 {\sf P\_select} \mid {\sf Make\_tuple_{2} } \\

P\!FN_1 & ::= & {\sf Make\_tuple_n} \mid {\sf Apply_{n\mbox{-}2}}  \\

Ap\_E_m & ::= & {\sf Ap_{n,m}} \; ( S\!E_{n+1}) \\

Case\_E_m & ::= & {\sf Bool\_case_m} \; (S\!E, \; E_m, \; E_m )  \mid
                  {\sf List\_case_m} \; (S\!E, \; E_m, \; E_m )  \\

Loop\_E_m & ::=& {\sf WLoop_m} \; (S\!E_{m+3} )
                 \mid {\sf FLoop_m} \; (S\!E_{m+4} ) \\

lambda\_E &::=& {\sf \lambda_{n,m}} \; (MV_n) \; . \; (E_m)
                \mid \underline{{\sf \lambda_{n,m}}} \; (MV_n) \; . \; (E_m) \\

E_1 &::=& {S\!E}_1 \mid  P\!F1_1 \;(S\!E) \mid P\!F2_1 \;(S\!E_2)
          \mid  P\!FN_1 \; (S\!E_n) \mid Ap\_E_1  \mid
    Case\_E_1 \mid Loop\_E_1 \mid lambda\_E \mid Block_1 \\

E_m &::=& {S\!E}_m \mid PF1_m \; (S\!E) \mid Ap\_E_m \mid Case\_E_m
          \mid Loop\_E_m  \mid Block_m \\

Block_m & ::= & \{_{\sf m}\;[Statement;]^* \;\;{\sf In} \; S\!E_m \}   \\

Statement &::= & Binding \mid Command \\

Binding &::= & M\!V_m = E_m \\

Command & ::= &  {\sf P\_store} \; (S\!E, \; S\!E,\; S\!E) \mid
                 {\sf Cons\_store\_1} \; (S\!E, \; S\!E ) \mid
        {\sf Cons\_store\_2}  \; (S\!E, \; S\!E )\mid 
                 {\sf Store\_error} \mid \top_s  \\

Program &::=& Block_1

\end{array} $\\
\\ \hline
\end{tabular}
}
\\
\caption{The Grammar of Kid}  \label{pglsyntax} 
\end{figure}
}

\section{Kid : The Kernel Id Language}
\label{syntaxandrules}

Id is a high level functional language \cite{Nikhil90c}
augmented with a novel data structuring facility 
known as I-structures \cite{Arvind89c}. Id,
like most modern functional languages,
is non-strict, and has higher-order functions and a Milner-style
type system. It also has a fairly large syntax
to express currying, loops, list and array comprehensions, and pattern
matching for all algebraic types.
We have found it difficult to give direct operational
semantics of Id because of its syntactic complexities.
Kid, a kernel language for Id, has been developed 
to give precise (though indirect) operational semantics of Id.
Kid has also proved to be an extremely useful intermediate
language for the Id compiler \cite{Zena90b}. Within the compiler, all machine
independent optimizations are expressed as source-to-source 
program transformations on Kid. We believe I-structures
are an essential feature of Kid, and are needed to express the semantics
of the purely functional subset of Id. \\

Kid has only uncurried operators and no complex expressions.
A major subset of Kid is simply the $\lambda$-calculus with constants and
let-blocks.
However, unlike other functional languages,
let-blocks play a fundamental role, that is, they can not be eliminated by
systematic substitution of variables.
The syntax of Kid is given in Figure \ref{pglsyntax}.
Every expression, except a block  or $\lambda$-expression,
consists of a function symbol
followed by the corresponding number of arguments.
{\em The ordering of statements within a block is irrelevant}.\\

An important feature of Kid is the concept of {\em multiple values}.
The expression
\[    x, \; y = \{_2 \;  a = \cdots ; \; b = \cdots ;\;
{\sf In} \; a, \; b \}\]
is a well-formed-expression, where ``$x, \; y$" indicates   multiple
variables, not to be confused with a 2-tuple in Id \cite{Nikhil90c}.
The 2 after the curly brace indicates that two values are to be returned
by this block expression.
Multiple values  avoid packaging values in a data structure, 
and are useful in  expressing some optimizations. 
Thus, in Kid a binding has the form {\small $MV = E$}, where  $MV$ stands for multiple
variables. Suppose  we have $m$ variables on the
left-hand-side, then the expression  E on the right-hand-side must 
return $m$ values. In the sequel we capture the number of
values that an expression produces by subscripting the corresponding syntactic
category. Thus, to express the above binding we will write
{\small $MV_m = E_m$}.
Note that  the function symbol {\small ${\sf Apply}$} appears
as a {\small $P\!F2_1$} in the grammar
because we assume that all user-defined procedures return only one result. 
We also use subscripted function symbols to express a family
of functions. 
For example, {\small ${\sf Make\_tuple_n}$} stands for
{\small ${\sf Make\_tuple_2}$},
{\small ${\sf Make\_tuple_3}$}, \etc .
Subscripts in a function symbol do not necessarily represent the number of
values to be returned by the application of the function. 
By convention, we drop the subscript when its value is one.\\

Kid also contains  While-loops and For-loops because these play a
significant role in program transformations. These constructs 
also play a major role when Kid is further translated into a still lower-level
language and machine code \cite{Zena90b}.\\

We briefly describe the use of I-structures in the translation of
list comprehensions.
A typical translation of a list-comprehension is given in terms of nested
map-list operations followed by a list flattening operation 
\cite{Peyton-Jones87}. In Id, we make 
use of ``open lists'' , a type of I-structure,
to generate a tail recursive  program.
The translation of the list comprehension expression
{\cf \{: e || x <- xs ; y <- ys\}}
may be fiven as follows:

\beginid
\null
        { h1  =  Open_cons ();
          hn  = { For x <- xs do
                   Next h1 = 
                      { Case ys of
                         | Nil = h1
                         | y:yss = 
                              { h =  Open_cons ();
                                h1.cons_2 = h.cons_2;
                               In { For y <- ys do
                                      t  = Open_cons ();
                                      t.cons_1 = e;
                                      h.cons_2 = t;
                                      Next h = t;
                                   Finally h }}};
                  Finally h1 };                 
          hn.cons_2 = Nil;
         In h1.cons_2 }
\null
\endid
\noindent

Basically,
in the above program, a open list (signified by {\cf h} in the inner loop) 
is generated for each element of {\cf xs}
and then these open lists are ``glued''
together in the outer loop.\\

A translation of functional subset of Id including I-structures is
given in \cite{Zena90b}. \\

We now digress to introduce
contextual reduction systems before giving the calculus and the operational
semantics of Kid.

\section{Contextual Reduction Systems}
\label{crsintro}

A Contextual Reduction System is a pair ({\cal A}({\sf F}, {\sf S}), R) , where
{\cal A} is a set of terms, and R is a set of context sensitive rules.
${\sf F}$ includes at least the {\small ${\sf Ap_{n,m}}$} primitive. 
The saliant syntactic features of the terms in {\cal A} 
can be seen by the grammar given in Figure
\ref{crsterms}.
{\small
\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
\\
$\begin{array}{lll}
S\!E & \in  & \mbox{Simple Expression} \\
E_m & \in  & \mbox{Expression with $m$ outputs} \\
{\sf F_{n,m}} & \in & \mbox{Primitive Function of $n$ arguments and
$m$ outputs  }\\
{\sf S_n} & \in & \mbox{Primitive command of $n$ arguments }\\
\end{array}$ \\
\\
$\begin{array}{llll}
S\!E & ::= & Variable  \mid {\sf F}_0 \\
S\!E_m & ::= & \underbrace{{S\!E}, \cdots , {S\!E}}_m  \\
M\!V_m & ::= & \underbrace{Variable, \cdots , Variable}_m \\
lambda\_E & ::= & {\sf \lambda_{n,m}}\;(M\!V_n)\;.\;(E_m)\\
E_m &::=& S\!E_m \mid {\sf F_{n,m}} \; (S\!E_n) \mid  lambda\_E \mid
Block_m \\  
Block_m & ::= & \{  \; [Statement;]^* \mbox{  } {\sf In} \mbox{  } S\!E_m
\}   \\
Statement & ::= & Binding \mid Command \\
Binding & ::= & M\!V_m = E_m \\
Command & ::= & {\sf S}_n \;(S\!E_n) \\ 
Term &::=& Block
\end{array} $ \\
\\ \hline
\end{tabular}
}
\\
\caption{Syntax of terms of a CRS}  \label{crsterms}
\end{figure}
} 
This grammar can be related to the Kid
grammar by defining ${\sf F}$ to be {\sf +}, {\sf Apply}, 
{\sf WLoop$_m$}, {\sf P\_select}, \etc and ${\sf S}$ to be {\sf P\_store},
{\sf Cons\_store}, \etc respectively.  

\subsection{Basic Definitions}

The applicability of a context sensitive rule depends upon both
the structure of the term and a precondition on the context
in which the term occurs. For example, the
context sensitive rule corresponding to the well known rule ``
{\small ${\sf Cons\_1} \; ({\sf Cons} \; X_1 \; X_2) \; \reduce{}{} \; X_1$}'' is
{\small
$$\frag{ X = {\sf Cons} \; (X_1, \; X_2)}
{{{\sf Cons\_1} \;(X)\;\;\;
\reduce{}{}\;\;\; X_1 }}$$ }
\noindent
where the binding {\small $X = {\sf Cons }\;(X_1,\; X_2)$}
over the line denotes a precondition, and {\small $X$},
{\small  $X_1$}, and {\small  $X_2$}
denote meta-variables.
A way of reading the above rule is that 
{\small ${\sf Cons\_1}\;(X)$ }
can be rewritten to {\small $X_1$} if the binding
{\small $X={\sf Cons}\;(X_1,\;X_2)$} occurs in the context of
{\small ${\sf Cons\_1} \; (X)$}. \\

A {\em context}
is a term with an arbitrary number of {\small  $\Box_E$}, expression 
holes,
and {\small  $\Box_S$}, statement holes. Formally contexts are terms generated by the grammar of Figure
\ref{crsterms}, where
{\small $\Box_E$} and {\small  $\Box_S$} are added to 
$S\!E$ and $Statement$ categories, respectively. 
Thus, given a context {\small  $C[\Box_S,\; \Box_E ]$}, 
and a {\em substitution}, $\sigma$, for the
meta-variables {\small $X$}, {\small  $X_1$} and
{\small $X_2$} such that
{\small $$C[ (X = {\sf Cons} \; (X_1, \;X_2))^{\sigma}, \;
({\sf Cons\_1}\; (X))^{\sigma}]$$}
is a term, we say 
{\small \[ C[ (X = {\sf Cons} \; (X_1, \; X_2))^{\sigma}, \;
({\sf Cons\_1}\; (X))^{\sigma}] \;\; \reduce{}{}
C[(X = {\sf Cons}\; (X_1, \; X_2))^{\sigma} ,\; X_1^{\sigma}] \hspace{1.5cm} (1)\] }
\noindent
where $\longrightarrow$ stands for ``rewrites to". 
From (1) we can observe that the precondition of the rule is not affected by the
rewriting, however, the precondition
usually affects the outcome of the rewriting.

\begin{definition}[Context sensitive rule]
A rule is an ordered set of preconditions, $P_1 \cdots P_n$, and a left-hand-side, l, and a right-hand-side,
r, and is written as 
\[ \frag{P_1 \mid \cdots \mid P_n} { l \;\; \reduce{}{}\;\; r }\] 
where $P_i$ is a statement and l and r are expressions.
\end{definition}

\begin{definition}[Redex]
Given a rule 
{ $\frag{P_1 \mid \cdots \mid P_n} { l\;\; \reduce{}{}\;\; r }$ }
and a term $M  \equiv  C[S_1 ,\cdots, S_n , E]$,
$E$ is said to be a {\bf redex}  iff
\begin{tightlist}
\item[(1)] $E  \equiv  l^{\sigma}$  ;
\item[(2)] $S_j$ $\equiv$ $P_j^{\sigma}$ $\;\;\forall$ j, $1 \leq j \leq n$;
\end{tightlist}
where $\sigma$ is a substitution. 
\end{definition}

\begin{definition}[Reduction Relations]
Given terms M, N $\in$ \cal{A}   and a rule $\tau$ $\in$ R, M reduces to N in one step 
($M \reduce{\tau}{} N$),  iff 
$M  \equiv  C[P_1^{\sigma} ,\; \cdots, P_n^{\sigma} ,\; l^{\sigma}]$, 
and $N$ $\equiv$ $C[P_1^{\sigma}, \;\cdots , P_n^{\sigma}, \; r^{\sigma}]$. \\
The one-step rewriting relation  $\reduce{}{}_R$ =  $ \bigcup_{\tau \; \in R}(\reduce{\tau}{})$.\\
The transitive reflexive closure of $\reduce{}{}_R$ is written as $\reduces{}{}_R$.
\end{definition}

\subsection{Basic Rules of Contextual Reduction System's ($R_{\mbox{CRS}}$)}

One has to deal with the problem
of free-variable capture
in any formal system with bound variables. 
In the $\lambda$-calculus, the problem
is usually solved either by making some 
{\em variable convention}, 
as for example, assuming that all free variables
are different from the bound variables, 
or by adopting a {\em variable-free notation}
such as that of DeBruijn \cite{DeBruijn}.
According to the variable convention given in
\cite{Barendregt}, the term
$(\lambda  x.xx)(\lambda  x.xx)$ is a legal term, 
while the term $(\lambda  y. (\lambda  x. +(x, y)) x$ is not
a legal term, because the variable $x$ appears both free and bound.
The convention
allows one to express application in terms of a {\em naive} form
of substitution, which does not require $\alpha$-renaming at execution time. 
In a system with let-blocks,
in order to avoid the free-variable capture as well as a to
allow naive substitution, we have to adopt a even more
stringent convention: {\em all} bound variables in an expression must be
unique and different from variables free
in the whole program. 
In order to maintain this invariant 
we will occasionally rename  all bound variables of  a
subterm to completely new variables explicitly,
by applying the function ${\cal RB}$  to the subterm. 
For example,
\[ \begin{array}{l}
{\cal RB} \; [\![ \{ x =  {\sf +} \; (a, \; 1) \; {\sf In} \; x \} ]\!] =
\{ x' =  {\sf +} \; (a, \; 1) \; {\sf In} \; x' \}\\
\end{array} \]

\noindent
An example of the use of ${\cal RB}$ function arises
in the use of the application rule
(see Section \ref{kidrewriterules}) as shown below
{\small
\[\begin{array}{l}
\frag{F = {\sf \lambda_{n,m}} \; (\mv{Z_n}) \; . \;  (E) }
{{\sf Ap_{n,m}} \; (F, \; \mv{X_n}) \;\; \reduce{}{} \;\; 
({\cal RB}[\![E]\!]) \; [\mv{X_n}/\mv{Z_n} ] }\\
\end{array}\]
}



\noindent
All contextual reduction systems have the following rules,
named $R_{CRS}$.


\subsubsection*{Substitution rules}
{\small
\[ \begin{array}{lll}
\frag{X = Y}{ X \reduce{}{} Y}\\ 
\frag{X = C}{ X \reduce{}{} C}
\end{array}\]
}
\noindent
where meta-variable $C$ stands for a constant, and {\small $X$} and
{\small $Y$} stand for distinct variables.

\subsubsection*{Block Flattening rule}
{\small
\[ \begin{array}{lll}
\begin{array}{lll}
\{_{\sf m} \;\mv{X_n} \; = \;  \{_{\sf n} \; SS_1;\;SS_2;\;\cdots & & \;
\{_{\sf m} \; \mv{X_n}  \; = \; \mv{Y_n};\\
\hspace{1.8cm}\;\;\;\;{\sf In}\;\; \mv{Y_n} \} &
\reduce{}{} & \;\;\;\;\;\;\; {SS_1};\;{SS_2};\;\cdots \;  \\
\;\;\;\;\;\; S_1;\;\cdots \;\; S_n\;  & & \;\;\;\;\;\;\; S_1; \; \cdots \;  \; S_n\; \\
\hspace{0.9cm}{\sf In} \;\mv{Z_m}\}  & & \hspace{0.9cm}{\sf In} \;\mv{Z_m}\} 
\end{array} 
\end{array} \]
} 

\subsubsection*{Multivariable rule}
{\small
\[\begin{array}{lll}
\mv{X_n} \;= \;\mv{Y_n} \;\;\reduce{}{} \;\; (X_1 = Y_1; \cdots X_n = Y_n) 
\end{array}\]
}
\begin{lemma}
$R_{\mbox{CRS}}$ is Strongly Normalizing and Confluent.
\end{lemma}
\begin{proof}
Since there are only a finite number of blocks and occurrences of
a variable in a term $M$, $R_{CRS}$ is
strongly normalizing.
It is easy to see that the block flattening rules are {\em locally
confluent}. 
Since variable substitution rules within a flattened block are
also {\em locally confluent}, the  uniqueness of the normal form of 
$M$ follows trivially from Newman's Lemma
\cite{Barendregt}.
\end{proof}\\

\subsection{Canonical Forms of terms in a CRS}

The notion of $\alpha$-equivalence between terms as defined in the $\lambda$-calculus,
makes too fine a distinction in a CRS calculus, for example,
the following two Kid terms have apparently
different syntactic structure. 
\[ \begin{array}{lll}
\{x = 8;\; t' = \{y = x;\; t = x + y \; {\sf In} \; t \} \; {\sf In} \; t'\} &
\mbox{  and  } &
\{x = 8; \; y = x;\; t = x + y \; {\sf In} \; t \} 
\end{array} \]
However, we consider the difference between the above two terms
merely ``syntactic noise''.
Eliminating this syntactic noise 
is the motivation behind the following definitions.

\begin{definition}[Canonical form]
Let N be the normal form of a term M with respect to
$R_{\mbox{CRS}}$. $\overline{M}$, the canonical form of M, is the term obtained
by deleting from N all bindings of the form $x = y$ (where
$x$ and $y$ are distinct variables) or $x = v$ ( where $v$ is a constant).
\end{definition}

\begin{definition}[$\alpha$-equivalence]
Two terms M and N are said to be $\alpha$-equivalent,
if $\overline{M}$ and $\overline{N}$ can be transformed into 
each other by a consistent renaming of bound variables.
\end{definition}

\begin{lemma}
Each term has a unique canonical form. 
\end{lemma}

\section{Contextual Reduction System of Kid}
\label{rules}

We now present a set of rewrite rules, $R_{Kid}$,
which give an intuitive understanding of how Kid terms may get evaluated.
If we call $A$ the set of Kid terms generated by the grammar of
Figure \ref{pglsyntax}, then the structure $\langle A , R_{Kid} \rangle$
is a Contextual Reduction System. 
We assume that a primitive
function is applied only to arguments of appropriate
types, i.e., the type checking has been done statically.\\

All the variables that appear on the left-hand-side of the rules are
meta-variables that range over appropriate syntactic categories.
By convention, we use capital letters for meta-variables and
small letters for Kid variables.
All  variables that appear on the right-hand-side
of the rules are either meta-variables or  ``new'' Kid variables.
We will make use of the following  convention regarding meta-variables:
{\small 
\[ \begin{array}{lll}
X_i,\;Z_i,\;Y_i,\;F_i,\;P,\;B,\;U,\;D & \in & {\small Variable} \mbox{ and } {\small Constant} \\
C & \in & {\small Constant } \\
S_i, \; SS_i,\;S' & \in & {\small Statement} \\
E_i & \in & {\small Expression} \\
\end{array}
\]
}

The notation {\small $E \; [Y/X]$ }
means the substitution of {\small $Y$} for
{\small $X$} in {\small  $E$}. 
Due to our assumptions 
{\small $E \; [Y/X]$ } will simply indicate
naive substitution, that is, substitution where no danger of free-variable-capture
exists and where {\small $X$} can be replaced by {\small $Y$}
without regards to scope. 
Moreover, we will use the notation
{\small $\mv{X_{n,m}}$} to stand for  {\small $(X_n,\cdots,X_m)$},
{\small $\mv{X_m}$  for $\mv{X_{1,m}}$},
and ~{\small $E\;[\mv{Y_n}/\mv{X_n} ]$} for
{\small $E\;[Y_1/X_1, \cdots ,Y_n/X_n]$}, which
is the same as {\small $(\cdots((E\;[Y_1/X_1])\;[Y_2/X_2])\cdots)\;[Y_n/X_n])$}.\\

\noindent
In the following, $\underline{n}$ represents a numeral.

\subsection{Kid Rewrite Rules}
\label{kidrewriterules}

\subsubsection*{$\delta$ rules}
{\small
\[ \begin{array}{lcl}
+ \; (\underline{m}, \;  \underline{n}) & \reduce{\delta}{}
& \underline{+ (m,\;  n)} \\
& \vdots & \\
{\sf Equal?}\;(\underline{n}, \; \underline{n})
& \reduce{\delta}{} & {\sf True} \\
{\sf Equal?}\;(\underline{m}, \; \underline{n} ) 
& \reduce{\delta}{} & {\sf False}
\hspace{2cm} \mbox{(if m $\neq$ $n$)}
\end{array} \]
}
\subsubsection*{Case rules}
{\small
\[\begin{array}{lll}
{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) & \reduce{}{} & E_1 \\
{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) & \reduce{}{} & E_2 \\
{\sf List\_case_m} \; ({\sf Nil},\; E_1, \; E_2) & \reduce{}{} & E_1 
\end{array} \]
}
{\small
\[\begin{array}{l}
\frag{X = {\sf Open\_cons} \;() }
{{\sf List\_case_m} \; (X,\; E_1, \; E_2) \; \; \reduce\;\;E_2 }
\end{array}\]
}
\subsubsection*{Arity Detection rule}
{\small
\[\begin{array}{lll}
\frag{F = \lambda (Z).E} 
{{\sf Apply}\;(F, \; X)   \;\; \reduce{}{} \;\;
{\sf Ap}\;(F, \; X) } &  \\
\frag{F = \lambda_n (\mv{Z_n}).E  }
{{\sf Apply}\;(F, \; X)   \;\; \reduce{}{} \;\;
{\sf Apply_1}\;(F, \; \underline{n},\; X) }       & n > 1 
\end{array}
\] }
\noindent
\hspace{0.5cm}{Similar rules apply for $\underline{{\sf \lambda_n}}$.}
{\small
\[\begin{array}{lll}
\frag{F_i = {\sf Apply_i}\;(F, \;\underline{n},\; \mv{X_i})  }
{{\sf Apply}\;(F_i, \; X) \;\; \reduce{}{} \;\;
{\sf Apply_{i+1}}\; (F, \; \underline{n},\;\mv{X_{i+1}})} & i < (n\!-\!1)\\
\frag{F_i = {\sf Apply_i}\;(F, \;\underline{n},\; \mv{X_i}) }
{{\sf Apply}\;(F_i, \; X) \;\; \reduce{}{} \;\;
{\sf Ap_n}\; (F, \; \mv{X_n})}  & i = (n\!-\!1)
\end{array}
\] }
\subsubsection*{Application rule}
{\small
\[\begin{array}{l}
\frag{F = {\sf \lambda_{n,m}} \; (\mv{Z_n}) \; . \;  (E) }
{{\sf Ap_{n,m}} \; (F, \; \mv{X_n}) \;\; \reduce{}{} \;\; 
({\cal RB}[\![E]\!]) \; [\mv{X_n}/\mv{Z_n} ] }\\
\end{array}\]
}
\noindent
\hspace{0.5cm}{A similar rule applies for $\underline{{\sf \lambda_{n,m}}}$.}
\subsubsection*{Loop rules} 
{\small
\[\begin{array}{lll}
{\sf WLoop_n} \; (P, \; B, \; \mv{X_n}, \; {\sf True}) & \reduce{}{} & \{_{\sf n} \begin{array}[t]{lll}
 \mv{t_n} & = & {\sf Ap_{n,n}} \; (B, \;  \mv{X_n}) ;\\
 t_{p} & = & {\sf Ap_n} \; (P, \; \mv{t_n});\\
\mv{t_n'} & = & {\sf WLoop_n} \;(P,  \; B,   \; \mv{t_n},\; t_{p})  \\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; \mv{t_n'} \} }
\end{array}
\\
{\sf WLoop_n} \; (P, \; B, \;  \mv{X_n}, \; {\sf False}) & \reduce{}{} &
\mv{X_n}  
\end{array} \]
}
\noindent
\hspace{0.5cm}{In the following two rules we assume that the index variable is the first variable in $\mv{X_n}$.}
{\small
\[\begin{array}{lll}
{\sf FLoop_n} \; ( U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf True}) & \reduce{}{} & \{_{\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}
\\
{\sf FLoop_n} \; (U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf False}) & \reduce{}{} &  \mv{X_{n}}  
\end{array} \]
}
\subsubsection*{Tuple rule}
{\small
\[\begin{array}{l}
\frag{ X = {\sf Make\_tuple_n} \; (\mv{X_n})}
{{\sf Detuple_n} \; (X) \; \; \reduce{}{} \;\; \mv{X_n}}
\end{array} \]
} 
\subsubsection*{List rules}
{\small
\[\begin{array}{lll}
{\sf Cons} \; (X, \; Y) & \reduce{}{} & \{
\begin{array}[t]{lll}
t & = & {\sf Open\_cons} \;(); \\
\multicolumn{3}{l}{ {\sf Cons\_store\_1 } \; (t,\;X); }\\
\multicolumn{3}{l}{ {\sf Cons\_store\_2 } \; (t,\;Y) }\\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; t \} }
\end{array}
\end{array}\]
}
{\small
\[ \frag{{\sf Cons\_store\_1} \; (X, \; Y) }
{{\sf Cons\_1} \;(X  )\;\;\; \reduce{}{}\;\;\;  Y  } \]
}
\noindent
{\small
\[\frag{{\sf Cons\_store\_2} \; (X, \; Y) }
{{\sf Cons\_2} \;(X  )\;\;\; \reduce{}{}\;\;\;  Y  } \]
}
{\small
\[ \frag{{\sf Cons\_store\_1} \; (X, \; Y) }
{{\sf Cons\_store\_1} \;(X,  \;Y') \;\;\; \reduce{}{}\;\;\;  \top_s  } \]
}
{\small
\[ \frag{{\sf Cons\_store\_2} \; (X, \; Y) }
{{\sf Cons\_store\_2} \;(X,  \;Y') \;\;\; \reduce{}{}\;\;\;  \top_s  } \]
}
\subsubsection*{Array rules}
{\small 
\[\begin{array}{l}
\frag{X={\sf I\_array} \; (X_b)}
{{\sf Bounds}\; (X) \;\; \reduce{}{}\;\;X_b}
\end{array} \]
}
\noindent
{\small
\[\frag{{\sf P\_store} \; (X, \; Y,\; Z) }
{{\sf P\_select} \;(X, \; Y)\;\;
\reduce{}{}\;\;\;  Z } \]
}
{\small
\[\frag{{\sf P\_store} \; (X, \; Y,\; Z) }
{{\sf P\_store} \;(X, \; Y,\; Z')\;\; \reduce{}{}\;\;\;  \top_s } \]
}
\subsubsection*{Propagation of $\top$}
{\small
\[ \begin{array}{lll}
\begin{array}{lll}
\{_{\sf m} \; X = \top; \; S_1; \cdots S_n \; {\sf In} \; \mv{Z_m}  \; \} &
\reduce{}{} & \;\;\;  \top 
\\
\{_{\sf m} \;  \top_s; \; S_1; \cdots S_n \; {\sf In} \; \mv{Z_m} \; \} &
\reduce{}{} & \;\;\;  \top 
\end{array} 
\end{array}\]
} 

\noindent
The rules for propagating $\top$ were motivated by a discussion
with Vinod Kathail.

\begin{theorem}
Kid is Confluent upto $\alpha$-renaming on canonical terms.
\end{theorem}
\begin{proof}
See \cite{Zena89}.
\end{proof}

\subsection{Printable Values and Answer of a Kid Term}

We now define the printable information
associated with a term. The grammar for printable values
for Kid is given in Figure \ref{pvalue}.
A precise notion of printable values is essential
to develop an interpreter for Kid as well as to discuss
the correctness of optimizations
(see Sections \ref{interpreter} and {\ref{correct}, respectively).

{\small
\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
\\
$\begin{array}[c]{llll}
Atoms & ::= & Integers \mid Booleans \mid {\sf Error} \mid ``{\sf Function}"
\mid \Omega \\
List & ::= & \langle {\sf List} \;  PV \; List \rangle \mid {\sf Nil} \\
Tuple & ::= & \langle {\sf 2\_Tuple} \; PV \; PV \rangle \mid
\langle {\sf 3\_Tuple} \; PV \; PV \; PV \rangle \mid \cdots \\
Array & ::= & \langle {\sf n\_Array} \; Tuple \; PV \cdots PV \rangle \\
PV & ::= & Atoms \mid List \mid Tuple \mid Array \mid \top \\
\end{array}$\\
\\ \hline
\end{tabular}
}
\\
\caption{Grammar of Printable Values}  \label{pvalue} 
\end{figure}
}

The following procedure, ${\cal P}$, produces the
printable value associated with a term.
$\rho$ and $\sigma$ represent, respectively,
the list of bindings that have as RHS either a $\lambda$-expression
or an allocator, \ie {\sf Make\_tuple}, {\sf I\_array}, {\sf Open\_cons}, and
the list of store commands, \ie the I-structure store.
The procedure ${\cal L}$ is used to lookup the value of a variable
or a location in $\rho$ and $\sigma$, respectively.
Given a program, \ie a closed term, $M$, the ${\cal P}rint$
procedure is invoked as follows:
\[ {\cal P}rint \; (M) = {\cal P} \;[\![M]\!] \; {\sf Nil}\; {\sf Nil}\]

\noindent
where ${\cal P}$ is:\\
{\small
$\begin{array}{l}
{\cal P}[\![ \{ S_s; \; A_s;\; B_s \; {\sf In} \; X \} ]\!] \; \rho \; \sigma =
{\cal P}[\![X]\!] \; (A_s:\rho) \; (S_s: \sigma)\\
\end{array}$
}

\noindent
{\small
$\begin{array}{l}
{\cal P}[\![\underline{n}]\!] \; \rho \; \sigma = \underline{n}\\
{\cal P}[\![{\sf True}]\!] \; \rho \; \sigma = {\sf True}\\
\end{array}$
}

\noindent
{\small
$\begin{array}{l}
{\cal P}[\![{\sf False}]\!] \; \rho \; \sigma = {\sf False}\\
{\cal P}[\![{\sf \top}]\!] \; \rho \; \sigma = {\sf \top}\\
{\cal P}[\![{\sf Nil}]\!] \; \rho \; \sigma = {\sf Nil}\\
\end{array}$
}

\noindent
{\small
$\begin{array}{l}
{\cal P}[\![X]\!] \; {\rho} \; \sigma =
\left\{ \begin{array}{lll}
\langle {\sf n\_Tuple}\; \; ({\cal P}[\![X_1]\!] \; \rho \; \sigma)
\cdots ({\cal P}[\![X_n]\!] \; \rho \; \sigma)]\!] \rangle
& \mbox{ if ${\cal L}$(X, $\rho$)}= {\sf Make\_tuple_n} (X_1,\cdots,X_n)\\
\langle {\sf List} \; \; ({\cal P}[\![X.1]\!] \; \rho \; \sigma)\;
({\cal P}[\![X.2]\!] \; \rho  \; \sigma)]\!] \rangle
& \mbox{ if ${\cal L}$(X, $\rho$)}= {\sf Open\_cons} ()\\
\langle {\sf Array} \;  \langle {\sf 2\_Tuple}\;
\underline{l} \; \underline{u} \rangle\; ({\cal P}[\![X.\underline{l}]\!] \; \rho  \; \sigma)
\cdots ({\cal P}[\![X.\underline{u}]\!] \; \rho \; \sigma)]\!] \rangle
& \mbox{ if ${\cal L}$(X, $\rho$)}= {\sf I\_array} (Y)\\
& \mbox{ and ${\cal L}$(Y, $\rho$)} = {\sf Make\_tuple}\;(\underline{l},\; \underline{u})\\ 
\mbox{``Function''} &  \mbox{ if ${\cal L}$(X, $\rho$)}=
{\sf \lambda}\mv{X_n}\; .\; (E) \;\mbox{ or } \\
&\mbox{ if ${\cal L}$(X, $\rho$)}=
{\sf Apply_{i}}\;(F, \; \underline{n}, \; \mv{X_i})\; \wedge
\; i < (n\!-\!1)\\
\Omega & \mbox{Otherwise}\\
\end{array}
\right.  \\
\\
\end{array}$
}

\noindent
{\small
$\begin{array}{l}
{\cal P}[\![X.i]\!] \; \rho \; \sigma =
\left\{ \begin{array}{lll}
{\cal P}[\![Y]\!] \; \rho \; \sigma
& \mbox{ if ${\cal L}$(X.i, $\sigma$)}= Y
\\
\Omega & \mbox{ if ${\cal L}$(X.i, $\sigma$)}=  \mbox{not found}\\
\end{array}
\right.  \\
\\
\end{array}$
}

\noindent
Notice that the printable value of a finite term can be an infinite tree.
For example, the ${\cal P}$rint of :
{\small
$$\begin{array}{l}
\{ x = {\sf Open\_cons}\;();\\
\;{\sf Cons\_store\_1}\;(x,\;1);\\
\;{\sf Cons\_store\_2}\;(x,\;x);\\
\;\;\; {\sf In} \; x \}
\end{array}$$
}
is {\small $\langle \; {\sf List} \; 1 \; \langle \; {\sf List} \; 1 \; \langle
\cdots  \rangle \cdots \rangle \;\rangle$},
that is, an infinite list of 1's.\\

We want to define the answer associated with a term in terms of printable 
values. Furthermore, we want to describe the answer independently of any interpreter,
\ie method of computing it.
We need to define an ordering on printable values.

\begin{definition}[Partial Order on Printable Values]
Let $a$ and $b$ be Printable Values; $a \sqsubseteq b$ iff
\begin{tightlist}
\item[(i)]
$a = \Omega$; or
\item[(ii)]
$b=\top$; or
\item[(iii)]
both $a$ and $b$ are $Atoms$ and $a=b$; or
\item[(iv)]
$a = \langle {\sf n\_Tuple}\; a_1 \cdots a_n \rangle $ and
$b = \langle {\sf n\_Tuple}\; b_1 \cdots b_n \rangle $ and
$a_i \sqsubseteq b_i$ $\forall$ $1 \leq i \leq n$; or 
\item[(v)]
$a = \langle {\sf List}\; a_1 \;  a_2 \rangle $ and
$b = \langle {\sf List}\; b_1 \;  b_2 \rangle $ and
$a_1 \sqsubseteq b_1$ and $a_2 \sqsubseteq b_2$; or
\item[(vi)]
$a = \langle {\sf n\_Array}\; abounds \; a_1 \cdots a_n \rangle $ and
$b = \langle {\sf n\_Tuple}\; bbounds \; b_1 \cdots b_n \rangle $ and
$abounds = bbounds$ and $a_i \sqsubseteq b_i$ $\forall$ $1 \leq i \leq n$.
\end{tightlist}
\end{definition}

\begin{theorem}
\label{cpo}
$PV$ is a complete partial order with respect to $\sqsubseteq$.
\end{theorem}
For the proof see \cite{Courcelle}.
\begin{lemma}
\label{approx}
Given a term M, 
$M \reduce{}{} N \;\; \Longrightarrow \;\;
{\cal P}rint\;(M) \sqsubseteq {\cal P}rint\;(N) . $
\end{lemma}

\noindent
Pictorially:
\[ \begin{array}{llllll}
M & \reduce{}{} & M_1 & \reduce{}{} & M_2 & \cdots \\
{\cal P}rint(M) & \sqsubseteq & {\cal P}rint(M_1) & \sqsubseteq & 
{\cal P}rint(M_2) & \cdots \\
\end{array} \]

\blank
\noindent
Intuitevely, the answer of a term may be defined as the
limit of this chain, that is, the answer is the
maximum printable value that can be obtained by reducing
a term. We need the following definitions to give a precise
definition of ``Answer".



\begin{definition}[Reduction Graph of a term]
Given a term M, the reduction graph of M, ${\cal G}(M)$, is defined as
\[ \{ N \mid M \reduces{}{} N \}. \]
\end{definition}

\begin{definition}[Printable Reduction Graph of a term]
Given a term M, the printable reduction graph of M, ${\cal PG}(M)$, is defined as
\[ \{ {\cal P}rint \; (N) \mid M \reduces{}{} N \}. \]
\end{definition}

\begin{definition}[Answer]
Given a term M, the Answer of M, ${\cal P}rint^*(M)$, is defined as
$$ \sqcup \; {\cal PG}(M).  $$
\end{definition}

In order for the above definition to make
sense we need to show that the limit of the
printable reduction graph exists and is unique.

\begin{theorem}
$\forall$ M, ${\cal PG}$(M) is directed.
\end{theorem}
\begin{proof}
Given $a$, $b$ $\in$ ${\cal PG}$(M), we have:
\[ \exists M_1, M_2 \mbox{ such that }
a={\cal P}rint(M_1),\; M \reduces{}{} M_1
\;\wedge \; b={\cal P}rint(M_2), \; M \reduces{}{} M_2 .\]
By confluence, $\exists$ $M_3$ such that
\[ M_1 \reduces{}{} M_3 \; \wedge  \; M_2 \reduces{}{} M_3 \]
By lemma \ref{approx},
\[ a \sqsubseteq c \; \wedge \; b \sqsubseteq c, \; c ={\cal P}rint(M_3) \]
\end{proof}

Since ${\cal PG}$(M) $\subseteq$ $PV$ is directed, by
theorem \ref{cpo} we know that the limit exists and is
unique.


\subsection{An Interpreter to Compute the Answer of a Kid term}
\label{interpreter}
The set of rewrite rules given in Section \ref{rules} per se do not define the
operational semantics of Kid, they define a calculus to prove properties of
programs.  From a computational point of view we need to specify a
{\em strategy} to apply these rules. Furthermore, the reduction
strategy should be normalizing with respect to the definition
of the answer. 
Intuitevely the interpreter should stop when it is known
that no more printable information can be
gotten by further reductions.\\

The strategy consists in evaluating the
outermost redexes first, and in case of a block, evaluating
all the right-hand-side redexes in parallel.
We will represent a block as {\small $\{ Ss; \; As; \;
Bs \; {\sf In} \; X \}$ },
where
{\small
\[ \begin{array}{ll}
Ss & \mbox{\normalsize represents a set of store commands in the block}\\
As & \mbox{\normalsize represents a set of $\lambda$-bindings and
allocator bindings in the block}  \\
Bs & \mbox{\normalsize represents a set of bindings, excluding $\lambda$-binding
and allocators, in the block} 
\end{array} \]
}

\noindent
The interpreter ${\cal E}$ keeps track of store commands it encounters
in $\sigma$, an I-structure store. It also keeps track of
$\lambda$-bindings and allocator bindings encountered in $\rho$. At the
start of the evaluation, both $\rho$ and $\sigma$
are considered to be empty.\\

The rules for propagating $\top$ imply that whenever new store commands are
added to the store a check has to be made for inconsistencies, that is, multiple
writes into the same location. We will assume this function is performed
by ${\cal CC}$. Thus, ${\cal CC}$ ($\rho$ $\cup$ $Ss$) returns either a new consistent store or $\top_s$.
While evaluating a block, we need to substitute variables and constants
and eliminate the corresponding binding. We also need to flatten blocks.
Though all nested blocks can be flattened in one go, we need to merge in one step only
the block expressions on the RHS of bindings
in the top-level block. Any substitution or block flattening can create
new redexes on the RHS of bindings in a block.
According to the $\top$ propagation rules, if a binding of
the form ${\small x = \top}$ exists in any block then that block
goes to $\top$. This can also be done during the substitution 
process.
We will assume a function ${\cal F\&S}$ (for flatten and substitute) that accomplishes
all this. In addition to the new block, it returns a flag showing
if any substitutions or flattening was done. Thus,
{\small
$$\begin{array}{l}
{\cal F\&S}[\![ \{ X = 1; Y = \{ {\sf P\_store} \;(W,\;I,\;Z);\;
Z = X +3 \; {\sf In} \; Z \} \;{\sf In} \; Y \} ]\!] \\
\hspace{2cm}{= \begin{array}[t]{l}
\{ {\sf P\_store}\;(W,\;I,\;Z); \; Z = 1+3;\; {\sf In} \; Z \}, {\sf True}
\end{array}}
\end{array}$$ 
}

We will also assume the existence of a function ${\cal ERHS}$ which is only applied to a block expression.
It may be described informally as
$$\begin{array}{l}
{\cal ERHS} [\![ \{ Ss;\;As;\;X_1=E_1;\cdots X_n=E_n\; 
{\sf In} \; X_i \} ]\!] \;\rho \;\sigma =\\
\hspace{2cm}{\{ Ss;\;As;\;X_1={\cal E}[\![E_1]\!] \; \rho \;
\sigma ;\cdots X_n={\cal E}[\![E_n]\!]\; 
\rho \;\sigma\; {\sf In} \; X_i \}}
\end{array}$$

Given a program $M$, the ${\cal E}$ procedure is invoked as follows:
\[ {\cal E}val \;[\![ M]\!] = {\cal E} [\![M]\!] \; {\sf Nil} \; {\sf Nil} \]

\noindent
{\bf The Interpreter:}\\
\noindent
{\small
$\begin{array}{l}
{\tt \cal E}[\![+ \; (\underline{m},\;\underline{n})]\!] \; \rho \; \sigma =  \underline{+ (m,\;  n)} \\
{\tt \cal{E}}[\![ {\sf Equal?}\;(\underline{n}, \; \underline{n}) ]\!] \; \rho  \; \sigma=
{\sf True} \\
{\tt \cal{E}}[\![ {\sf Equal?}\;(\underline{n}, \; \underline{m}) ]\!] \; \rho \; \sigma=
{\sf False} \\
\end{array}$
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}[\![{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) ]\!]\; 
\rho \; \sigma= {\tt \cal{E}}[\![E_1]\!] \; \rho \; \sigma \\
{\tt \cal{E}}[\![{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) ]\!] \; \rho  \; \sigma= {\tt \cal{E}}[\![ E_2]\!]  \; \rho \; \sigma\\
{\tt \cal{E}}[\![{\sf List\_case_m} \; ({\sf Nil},\; E_1, \; E_2) ]\!] \; \rho \; \sigma   =
{\tt \cal{E}}[\![ E_1]\!] \; \rho \; \sigma \\
{\tt \cal{E}}[\![{\sf List\_case_m} \; (X,\; E_1, \; E_2) ]\!] \; \rho \; \sigma   =
{\tt \cal{E}}[\![ E_2]\!] \; \rho \; \sigma  \hspace{1cm} \mbox{if ${\cal L}$ ($X$, $\rho$)} = {\sf Open\_cons}\;() 
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}\mean{{\sf Apply}\;(F, \; X)} \; \rho \; \sigma =  
\left\{ \begin{array}{ll}
{\tt \cal{E}}[\![{\sf Ap}\;(F, \;  X)]\!] \; \rho \; \sigma  & \mbox{if ${\cal L}$ ($F$, $\rho$)} = \lambda Z\;.\;(E)  \\
{\sf Apply_1}\;(F, \; \underline{n},\; X) &
 \mbox{if ${\cal L}$ ($F$, $\rho$)} = \lambda_n (\mv{Z_n}).(E) \; \wedge \;  n > 1 \\
{\sf Apply_{i+1}}\;(F, \; \underline{n},\; \mv{X_{i+1}}) &
 \mbox{if ${\cal L}$ ($F$, $\rho$)} = {\sf Apply_i}\; (F, \; \underline{n},\;\mv{X_i})\; \wedge \;
i < (n\!-\!1)\\
{\tt \cal{E}}[\![ {\sf Ap_n}\;(F, \; \mv{X_n})]\!]  \; \rho \; \sigma &
\mbox{if ${\cal L}$ ($F$, $\rho$)} = {\sf Apply_i}\; (F, \; \underline{n},\;\mv{X_i})\;\wedge \;  i = (n\!-\!1) \\
\end{array} 
\right.  \\
{\tt \cal{E}}[\![{\sf Ap_{n,m}} \; (F, \; \mv{X_n})]\!] \; \rho \; \sigma  =
{\tt \cal{E}}[\![({\cal RB}\;[\![ E ]\!] )\;[\mv{X_n}/\mv{Z_n}]]\!] \; \rho \; \sigma \;\; \mbox{where 
${\cal L}$ ($F$, $\rho$)}  = \lambda_{n,m} (\mv{Z_n}).E\\
\end{array}$\\
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}[\![{\sf WLoop_n} \; (P, \; B, \; \mv{X_n}, \; {\sf True})]\!] \; 
\rho \; \sigma = 
{\tt \cal{E}}[\![ \{_{\sf n} \begin{array}[t]{lll}
 \mv{t_n} & = & {\sf Ap_{n,n}} \; (B, \;  \mv{X_n}) ;\\
 t_{p} & = & {\sf Ap_n} \; (P, \; \mv{t_n});\\
\mv{t_n'} & = & {\sf WLoop_n} \;(P,  \; B,   \; \mv{t_n},\; t_{p})  \\
\multicolumn{3}{l}{ \;\;\; \;\; {\sf In} \; \mv{t_n'} \} ]\!]  \; \rho \; \sigma }
\end{array}
\\
{\tt \cal{E}}[\![{\sf WLoop_n} \; (P, \; B, \;  \mv{X_n}, \; {\sf False})]\!] \; \rho \; \sigma =
\mv{X_n}  \\
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}\mean{{\sf Detuple_n} \; (X)} \; \rho \; \sigma  = \mv{X_n} \hspace{1cm} \mbox{ if
${\cal L}$ ($X$, $\rho$)} = {\sf Make\_tuple} \; \mv{X_n}  \\
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}\mean{{\sf Cons} \; (X, \; Y)} \; \rho \; \sigma =  {\tt \cal{E}}[\![ \{
t  =  {\sf Open\_cons} \;(); \; {\sf Cons\_store\_1 } \; (t,\;X); \;
{\sf Cons\_store\_2 } \; (t,\;Y) \;
\; {\sf In} \; t \}  ]\!] \; \rho \; \sigma \\
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}\mean{{\sf Cons\_1} \;(X  )}  \; \rho \; \sigma=  Y   \hspace{1cm}  \mbox{if ${\cal L}$ ($X$, $\sigma$)} =
{\sf Cons\_store\_1} \;(X,\;Y)  \\ 
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}\mean{{\sf Cons\_2} \;(X  )}  \; \rho \; \sigma=  Y   \hspace{1cm}  \mbox{if ${\cal L}$ ($X$, $\sigma$)} =
{\sf Cons\_store\_2} \;(X,\;Y)  \\ 
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal E}[\![{\sf Bounds} \;(X) ]\!]  \; \rho \; \sigma= X_b    \hspace{1cm}  \mbox{if ${\cal L}$ ($X$, $\rho$)} =
{\sf I\_array}\;(X_b)\\ 
\end{array}$ 
}

\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}[\![{\sf P\_select} \;(X, \; Y) ]\!]  \; \rho \; \sigma= Z    \hspace{1cm}  \mbox{if ${\cal L}$ ($X$, $\sigma$)} =
{\sf P\_store}\;(X, \; Y, \; Z)\\ 
\end{array}$
}

\blank
\noindent
{\small
$\begin{array}{l}
{\tt \cal{E}}[\![ \{ Ss; \; As; \; Bs  \; {\sf In} \;X\}]\!] \;
\rho \; \sigma  = e \\
\hspace{2cm}{\mbox{where $e$ is obtained by the execution of the following
program written in pseudo-Id}}\\
\hspace{2.5cm}{
\{ \begin{array}[t]{l}
  blk,- = {\cal F\&S}(\{ Ss; \; As; \; Bs  \; {\sf In} \;X\});\\
  \; flag = {\sf True};\\
  \;  {\sf In} \; {\sf If} \; blk \; = \top \; {\sf then} \; \top \\
\hspace{2cm} { {\sf else} \;\;  \begin{array}[t]{l}
     \{  {\sf While} \; flag \; {\sf do}\\
    \;\; \mbox{ Suppose $blk$ is } \{Ss;\;As;\;Bs \; In \; X \}\\ 
   \;\;is = {\cal CC}(\sigma \cup Ss);\\
   \;\;fs = \rho \cup As ;\\
   \;\;{\sf next} \; blk, {\sf next} \; flag  = \begin{array}[t]{l}
     {\sf If} \; is = {\sf \top_s} \; {\sf then} \; ({\sf \top},
     {\sf False}) \\
      \;\;\;\;\; {\sf else} \;  {\cal F\&S}({\cal E\_RHS}(blk,is,fs))  \\
      \end{array}\\
\;\; {\sf finally} \; blk \} \}   \\
\end{array}     }  \\
\end{array} }    \\
\\ 
\end{array}$
}

\noindent
If none of the above clauses apply, then\\
\noindent
{\small
${\cal E}[\![ E]\!] \; \rho \; \sigma = E$
}

\begin{theorem}[Soundness]
Given a term M,
\[ {\cal E}val[\![M]\!] = N \Longrightarrow 
{\cal P}rint^*(M) = {\cal P}rint(N) \]
\end{theorem}

\begin{theorem}[Normalization Theorem]
Given a term M,
\[ {\cal P}rint^*(M) \mbox{ is finite } \Longrightarrow
{\cal P}rint({\cal E}[\![M]\!]) = {\cal P}rint^*(M) . \]
\end{theorem}

\section{Optimizations of Kid Programs}

%It is also possible to partially evaluate
%a Kid term by applying $R_{Kid}$ rules. We illustrate
%this point next by considering only some of the
%$R_{Kid}$ rules.

\subsection{Optimizations as Rewrite rules (${\bf R_{opt}}$)}
\label{optirules}
Following is a partial list of optimization rules 
or source-to-source transformations that can
be expressed as rules in the CRS for Kid.
Optimizations should be performed after type checking
and after all bound variables have been assigned
unique names. A strategy for applying optimizations is discussed
in the next section.
Applicability of certain rules requires
some semantic check such as ``$\underline{n} \; > \; 1$''.
We write such semantic predicates above the line but following
an ``\&". \\


${\bf R_{opt}}$} is as follows:
\[ {\bf R_{opt}} = {\bf R_{Kid}} \cup {\bf R_{oi}} \cup {\bf R_{io}}
- \{ {\sf Ap_{n,m}}-\mbox{rule},\; {\sf Cons}-\mbox{rule} \}  \]
where ${\bf R_{oi}}$ and ${\bf R_{io}}$ are defined below.


\subsection*{${\bf R_{Kid}}$}

All Kid rewrite rules, except the ${\sf Cons}$-rule,
can be applied at compile time. However,
care needs to be excercised in applying some rules such as
the {\em Application rule,} because these can cause non-termination.
A similar problem exists with ${\sf WLoop}$ and ${\sf FLoop}$.
We will assume that the user will {\em annotate} the program to indicate when these
rules are safely applicable.


\section*{${\bf R_{oi}}:$}

${\bf R_{oi}}$ rules are applied ``{\em outside in}'', as will be shown in the next section.

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

\noindent
An underlined $\lambda$ corresponds to the ${\sf Defsubst}$
annotation in Id. It indicates that the function is substitutable at compiler
time. Notice, if the user underlines a recursive procedure,
the above rule will cause non-termination.
This mechanism of underlining is often used in term rewriting systems to turn
a set of rules into an equivalent strongly normalizing set of rules \cite{Klop85}.
This mechanism also allows us to control
the applicability of the loop rules.
If the $\lambda$'s corresponding to predicate ($P$) and loop body ($B$) of a loop expression are
{\em not underlined}, then the loop rule can not be applicable more than
once. If the user wants to unfold loops more than once at compiler time then, he
must annotate the loop to indicate this. When a loop in Id is 
annotated to be unfolded, then
the translation from Id to Kid will generate underlined $\lambda$'s
for $P$ and $B$.


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

{\small
\[ \frag
{F_i = {\sf Apply_i} \; (F,\; \underline{n},\; \mv{X_i}) \;\wedge\;
F = {\sf \lambda_{n,m}} \; (\mv{Z_n}) \; . \; (E)  }
{ {\sf Apply}_{pe} \; ( F_i,\;X)\;\; \reduce{}{} \;\;
\begin{array}[t]{l}
\{ f = {\sf \lambda_{n-i-1,m}}\;  (\mv{z_{n-i-1}}) \; .  \;
(( {\cal RB}\;[\![E]\!]) \; [\mv{z_{n-i-1}}/\mv{Z_{i+2,n}},
\;\mv{X_{i+1}}/\mv{Z_{i+1}}])  \\
\;\;\;\; {\sf In} \; f \}
\end{array} } \]
}

\noindent
A similar rule applies for $\underline{{\sf \lambda_{n,m}}}$.\\
${\sf Apply}_{pe}$ indicates an ${\sf Apply}$ which the user has annotated for
partial evaluation.
Notice the difference with the previous rule. Instead of underlining
the $\lambda$, the information is associated with the application.
The rational being that we want to avoid the
generation of too many specialized functions.
This rule can also cause non termination, if an application in a recursive definition is annotated
for partial evaluation.
A more sophisticated strategy, that
we have not explored yet, would try to compute
some fixpoint in case of such an annotation.

\subsubsection*{Fetch Elimination}
{\small
\[ \begin{array}{l}
\frag{X = {\sf Cons} \; (X_1, \; X_2)}
{ {\sf Cons\_1} \;(X) \;\;\;
\reduce{}{}\;\;\; X_1 } \end{array} \]
}
{\small
\[ \begin{array}{l}
\frag{X = {\sf Cons} \; (X_1, \; X_2)}
{ {\sf Cons\_2} \;(X) \;\;\;
\reduce{}{}\;\;\; X_2 } \end{array} \]
}
{\small
\[ \begin{array}{l}
\frag{X = {\sf Cons} \; (X_1, \; X_2)}
{ {\sf List\_case} \;(X,\;E_1,\;E_2) \;\;\;
\reduce{}{}\;\;\; E_2 } \end{array} \]
}
\noindent
The above rules are useful because we do not
reduce {\small ${\sf Cons}\;(X_1,\;X_2)$} into {\small ${\sf Open\_cons}$} at compile time.
\subsubsection*{Algebraic Identities}
{\small
\[\begin{array}{lll}
\begin{array}[t]{lll}
\multicolumn{3}{c}{{\bf Alg_1}}\\
\\
{\sf And} \; ({\sf True},  \;X) \; & \reduce{}{} &  \; X  \\
{\sf Or} \;( {\sf False},  \;X)  \; & \reduce{}{} & \; X \\
{\sf +} \; (X ,0)  \; & \reduce{}{} &\; X \\
{\sf *}  \;(X, 1)  \; & \reduce{}{} & \; X \\
\multicolumn{3}{c}{\vdots }
\end{array} &
\begin{array}[t]{lll}
\multicolumn{3}{c}{{\bf Alg_2}}\\
\\
{\sf And} \; ({\sf False},  \;X)  \; & \reduce{}{} & \; {\sf False}  \\
{\sf Or} \; ({\sf True},  \;X)  \; & \reduce{}{} & \; {\sf True} \\
{\sf *}  \;( X,0)  \; & \reduce{}{} & \; 0 \\
{\sf -}   \;(X , X)  \; & \reduce{}{} & \; 0 \\
{\sf Equal?}\; (X,\; X ) \; & \reduce{}{} & \; {\sf True}\\
\multicolumn{3}{c}{\vdots }
\end{array} &
\begin{array}[t]{l}
\multicolumn{1}{c}{{\bf Alg_3}}\\
\\
\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} }\\
\hspace{2cm}{\;\; \;\;\vdots }
\end{array}
\end{array}$$
}
\subsubsection*{Eliminating Circulating Variables}

Suppose in the Id loop body of an Id program there exists an
expression like ``{\cf Next  x~=~x}~"~, then the variable {\cf x}
can be made into
a free variable  of the loop and its circulation can be avoided.
Without loss of generality we assume that the nextified variable to
be eliminated  is the last one.

{\small
\[ \begin{array}{l} 
\frag{ \begin{array}{ll}
P = {\sf \lambda_n} \; (\mv{X_n}) \; . \; ( E) & \mid \\
B = {\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  =  {\sf \lambda_{n-1}} \; ( \mv{x_{n-1}}) \; . \;
({\cal RB}[\![E]\!]\;[\mv{x_{n-1}}/\mv{X_{n-1}},\; Y_n/X_n]);  \\
b =  {\sf \lambda_{{n-1},{n-1}}} \;(\mv{x'_{n-1}}) \; . \; 
({\cal 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} \] }

\noindent
A similar optimization applies to for-loops.

\subsubsection*{Eliminating Circulating Constants  }

Suppose in the loop body there exists an
expression like ``{\cf Next x = t }", where the variable {\cf t} is a free
variable of the loop body then its circulation can be avoided. Such 
situations may arise as a consequence of lifting invariants from a loop.
The following example illustrates this transformation:
\beginid
\null
       { While (p x y) do 
           Next x = t;
           Next y = f x y;
         Finally  y}
\endid
\null

\noindent
This may be transformed as follows:
\beginid
\null
     If (p x y) then 
             { y1 = f x y;
              In
                { While (p t y1) do 
                    Next y1 = f t y1;
                  Finally  y1} }
                 else
              y
\null
\endid
Notice that it is only after the first iteration that the value
of ``{\cf x}'' is {\cf t}. 
Thus, to avoid the  circulation of the nextified variable ``{\cf x}'', the loop
has to be peeled once. This rule can be expressed as follows. Please note
that we could have also written {\small $Z_n$} instead of
{\small $t_n$} on the right-hand-side.

{\small
\[\frag
{\begin{array}{ll}
P = {\sf \lambda_n} \; (\mv{X_n}) \; . \; ( E) & \mid \\
B = \underbrace{{\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 & = & {\sf \lambda_{n-1}} \; ( \mv{x_{n-1}}) \; . \;
({\cal RB}[\![E]\!]\;[\mv{x_{n-1}}/\mv{X_{n-1}},\; t_n/X_n]);\\
b & = & {\sf \lambda_{n-1,n}} \;(\mv{x'_{n-1}}) \; . \; 
({\cal 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}} \]}

\subsubsection*{Peeling the Loop}
{\small
\[
\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}
\]}
Notice that the above rule is again applicable to the Floop generated
on the RHS. To avoid unbounded number of applications of this rule
the user will have to indicate how many times the loop
peeling should be performed.

\subsubsection*{Loop Body Unrolling K times }
{\small
\[\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 & = & {\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}}
\]}

\noindent
Suppose {\small $r =  remainder((U-X_1)/D, \underline{k})$} , and
$r$ is not  zero. We can still apply the above transformation
by first peeling the loop $r$ times. Notice, $k$ has to be
supplied by the user.

\section*{{\bf R$_{\mbox{\bf io}}:$}}

These optimizations need to be applied ``inside-out'', because that way bigger and bigger
common expressions or expressions to be lifted can be formed.
Furthermore these optimizations are only applied to side-effect-free
expressions (sef's) defined below:

\begin{definition}[Side-effect-free expression\\]
\vphantom{$N^N$}
\begin{tightlist}
\item[(1)]
Variables and constants are sef;
\item[(2)]
all {\small $P\!F_{n,m}\;(\mv{X_n})$ },
except {\small ${\sf I\_array}$, ${\sf Open\_cons}$,
${\sf Apply}$, ${\sf WLoop}$ and ${\sf FLoop}$},
are sef;
\item[(3)]
{\small ${\sf Bool\_Case_m}\;(X,\;E_1,\;E_2)$} is sef if {\small $E_1$} and
{\small $E_2$} are sef; similarly for
{\small ${\sf List\_Case}$}.
\item[(4)]
${\sf \lambda_{n,m}}x.E$ is sef if $E$ is sef;
\item[(5)]
${\sf Ap_{n,m}} \;(F,\;X)$ is sef if $F$ is bound to
a sef $\lambda$-abstraction; 
\item[(6)]
${\sf WLoop_m}\;(P,B,\mv{X_n},\;Y)$ is sef if $P$ and $B$ are bound to sef $\lambda$-abstractions;
similarly for ${\sf FLoop}$.
\end{tightlist}
\end{definition}

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

\subsubsection*{Lift Free Expressions}
{\small
\[ \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} }
\]}\\
\noindent
Where {\small $F\!E (e,e')$} return true if the expression $e$ is free in $e'$. 
This optimization allows us to deal with loop invariants, that is, expressions that do not depend
on the nextified variables.
A similar rule applies for $\underline{{\sf \lambda_{n,m}}}$.
This rule in conjunction with the loop rules will
cause loop invariants to be lifted from loops.

\subsubsection*{Hoisting Code out of a Conditional}
{\small
\[\frag
{\& \;  F\!E(E,({\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'} \;  \})))}
{ \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} } \] }


\subsection{A Partial Evaluator for Kid}
\label{partialevaluator}

Applying ${\bf R_{kid}}$ rules and ${\bf R_{oi}}$ rules is like
{\em partial evaluation} of a Kid program. In the following
we present an efficient strategy for applying ${\bf R_{kid}}$
and ${\bf R_{oi}}$ rules using the function
${\cal EV}$.
However, space does not permit us to give a full interpreter.
Therefore, we illustrate our strategy using a few carefully chosen rule,
\ie $R_{CRS}\; \cup\; \{ \delta \mbox{ rules}, \;
Case \mbox{ rules for booleans}, \; {\sf P\_select} \mbox{ rule } \}$.
The extension of ${\cal EV}$ to other rules 
of ${\bf R_{kid}}$ and ${\bf R_{oi}}$ is straightforward.
As usual, initially $\rho$ and $\sigma$ would be empty.\\


\noindent
{\small
$\begin{array}{l}
{\cal EV}[\![+ \; (\underline{m},\;\underline{n})]\!] \; \rho \; \sigma =  \underline{+ (m,\;  n)} \\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) ]\!]\;
\rho \; \sigma= {\cal EV}[\![E_1]\!] \; \rho \; \sigma \\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) ]\!] \;
\rho \; \sigma= {\cal EV}[\![ E_2]\!]  \; \rho \; \sigma\\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; (X,\;   E_1, \;  E_2) ]\!] \;\rho  \; \sigma= 
{\sf Bool\_case_m} \; (X,\; ({\cal EV}[\![E_1]\!]\; \rho \; \sigma),
\;({\cal EV}[\![E_2]\; \rho \; \sigma)\!]) \\
\end{array}$
}

\blank
\noindent
{\small
$\begin{array}{l}
{\cal EV}[\![{\sf P\_select} \;(X, \; Y) ]\!]  \; \rho \; \sigma= Z    \hspace{1cm}  \mbox{if (${\cal L}$ ($X$, $\sigma$))} =
{\sf P\_store}\;(X, \; Y, \; Z)\\ 
%\\
{\cal EV}[\![ \{ Ss; \; As; \; Bs \; {\sf In} \; X \} ]\!]
\; \rho \; \sigma = e\\
\hspace{2cm}{\mbox{where $e$ is obtained by the execution of the following program written in pseudo-Id}}\\
\hspace{2.5cm}{
\{ \begin{array}[t]{l}
  blk,- = {\cal F\&S}(\{ Ss; \; As; \; Bs \; {\sf In} \; X \});\\
  \; flag = {\sf True};\\
   \;{\sf If} \; blk = \top \; {\sf then } \; \top\\
\;\;\; {\sf else}\\
   \{\; blk= \{ \begin{array}[t]{l}
     {\sf While} \; flag \; {\sf do}\\
    \;\; \mbox{ Suppose $blk$ is } \{Ss;\;As;\;Bs \; In \; X \}\\ 
   \;\;is = {\cal CC}(\sigma \cup Ss);\\
   \;\;fs = \rho \cup As;\\
   \;\;{\sf next} \; blk, {\sf next} \; flag  = \begin{array}[t]{l}
     {\sf If} \; is = {\sf \top_s} \; {\sf then} \; ({\sf \top},
     {\sf False} ) \\
      \;\;\;\;\; {\sf else} \;  {\cal F\&S}({\cal EV'\_RHS}(blk,is,fs))  \\
      \end{array}\\
\;\; {\sf finally} \; blk \} \\
\end{array}\\
 \; \mbox{ Suppose blk' is } \{Ss';\;As;'\;Bs' \; {\sf In} \; X' \}\\ 
   \;\;is = {\cal CC}(\sigma \cup Ss);\\
   \;\;fs = \rho \cup As;\\
   \;\; blk''= {\sf If} \; is = {\sf \top_s} \; {\sf then} \;( {\sf \top},
     {\sf False} ) \\
      \;\;\;\;\;\hspace{1cm} {\sf else} \;  ({\cal EV\_RHS}(blk'',is,fs))  \\
\;\;\;{\sf In} \; blk'' \} \}\\
\end{array} }
\end{array}$\\
}
{\small
$\begin{array}{l}
\hspace{2cm}{\mbox{where}} \\
\\
\hspace{2.5cm}{{\cal EV'\_RHS}([\![ Ss; \; As;\; X_1 = E_1; \cdots
X_n=E_n \;  {\sf In} \; X_i ]\!] \; \rho \; \sigma =}\\
\hspace{4cm}{
\{ Ss; \; As; \; X_1 = {\cal EV'}(E_1,\;\rho \;\sigma); \cdots
 X_n = {\cal EV'}(E_n,\;\rho \;\sigma) \; {\sf In} \; X_i \} }\\
\\
\hspace{2cm}{\mbox{and the function ${\cal EV'}$ given below
unlike ${\cal EV}$ does not go inside encapsulators.}} \\
\\
\hspace{2.5cm}{
\begin{array}{l}
{\cal EV'}[\![+ \; (\underline{m},\;\underline{n})]\!] \; \rho \; \sigma =  \underline{+ (m,\;  n)}\\
{\cal EV'}[\![{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) ]\!]\;
\rho \; \sigma= E_1 \\
{\cal EV'}[\![{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) ]\!] \;
\rho \; \sigma=  E_2 \\
{\cal EV'}[\![{\sf P\_select} \; (X,\;Y) ]\!] \; \rho \; \sigma=  Z,\;{\sf True} \hspace{1cm} \mbox{if (${\cal L}$ ( $X$, $\sigma$))} =
{\sf P\_store}\;(X, \; Y, \; Z)\\ 
\mbox{ else } \\
{\cal EV'}[\![E]\!]\;\rho \; \sigma = E\\
\end{array}
}
\end{array}$\\
}

\noindent
{\small
$\begin{array}{l}
\mbox{else} \\
{\cal EV}[\![ E]\!] \; \rho \; \sigma = E
\end{array}$  \\
}

\begin{theorem}[Normalization Theorem]
Given terms M and N, and let R= $R_{CRS}\; \cup\; R_{kid} \; \cup R_{oi}$
\[ M \;  \reduces{}{}_{R}\; N \;\; \Longrightarrow \;\; {\cal EV}[\![ M]\!] \; {\sf Nil} \; {\sf Nil} = N. \]
\end{theorem}

We do not describe the strategy for ${\bf R_{io}}$ rules because it
requires choosing a data structure for Kid programs. These rules should
be applied from inside out.  Unfortunately ${\bf R_{io}}$ rules can trigger some ${\bf R_{oi}}$
optimizations. For example, the cse-rule may trigger an algebraic rule, such as,
the equality rule.\\

Briefly the overall strategy for optimizations is as follows:\\
\begin{tightlist}
\item[(1)]
apply ${\bf R_{Kid}}$ $\cup$ ${\bf R_{oi}}$ - 
$\{ {\sf Ap_{n,m}}-\mbox{rule},\; {\sf Cons}-\mbox{rule} \; \}$, 
from outside in, as explained in Section  \ref{partialevaluator};
\item[(2)]
apply ${\bf R_{io}}$ rules from inside out;
\item[(3)]
if there is any change in the expression in step (2) go to step (1),
else stop.
\end{tightlist}

We beleive that the above strategy is normalizing with respect to ${\bf R_{opt}}$.\\

An other interesting question about
optimizations is whether ${\bf R_{opt}}$ is 
confluent. We have shown in 
\cite{Zena89} that ${\bf Alg_3}$ rules cause ${\bf R_{opt}}$ to be
non confluent. However, this is not a serious drawback
because the cases where the confluence is lost are the ones where the
unoptimized program would have produced no information .

\subsection{Correctness of Optimizations}
\label{correct}
\begin{definition}[Observational Equivalence]
Given two terms M and N, M and N are said to be 
Observationally Equivalent iff
\[ {\cal P}rint^* \;(M) \equiv {\cal P}rint^* \;(N). \]
\end{definition}

For correctness, observational equivalence is not enough. It has to be shown that no
context can distinguish between optimized and unoptimized term.

\begin{definition}[Observational Congruence]
Given two terms M and N, M and N are said to be 
Observationally Congruent iff 
\[ \forall \; C[\Box],\;\; {\cal P}rint^* \;(C[M]) \equiv {\cal P}rint^* \;(C[N]) \; . \]
\end{definition}

\begin{definition}[Correctness]
An optimizer (A,$R_{opt}$) of (A,R) is correct iff
\[ \forall \; M \in  A, M \reduces{}{}_{R_{opt}} N \Longrightarrow
\begin{array}[t]{l}
(i) \;\; {\cal P}rint^*(M) \sqsubseteq {\cal P}rint^*(N) \mbox{   and   }\\
(ii)\;\; {\cal P}rint^*(N)=\top \Longrightarrow {\cal P}rint^*(M)=\top.
\end{array} \]
\end{definition}

Notice that condition $(ii)$ is needed because $\top$ is higher than all print values and
we do not want the optimizer to take all programs to $\top$.

%\begin{lemma}
%Let R be the set
%\{algebraic identities, eliminating circulating variables rule, 
%eliminating circulating constants rule, peeling the loop once rule, loop body
%unrolling k times\}.
%\[M \reduce{}{}_R N \;\; \Longrightarrow \;\; M \cong_{obs} N. \]
%\end{lemma}

It is believed that all optimizations presented in Section  \ref{optirules}
preserve correctness, though this 
has been proven for only a small subset of them so far \cite{Zena89}.
In general, correctness of an optimization is difficult to prove. However, some
optimizations can be proven correct easily because they are {\em derived} rules.

\begin{definition}[Derived rule]
A rule $r$ is said to be derived in $R$ iff
\[M \reduce{}{r} M_1 \Longrightarrow \exists \; M_2,\;\;
M \reduces{}{}_{R} M_2\;\; \wedge \;\; M_1 \reduces{}{}_{R} M_2\]
\end{definition}

\begin{corollary}
Given an optimizer (A,$R_{opt}$) of (A,R),
\[\forall \; r \in  R, r \mbox{ is derived}
\;\; \Longrightarrow \;\; (A,R_{opt}) \mbox{ is correct }.  \]
\end{corollary}

\begin{lemma}
All ${\bf R_{Kid}}$ rules, Inline Substitution and Fetch Elimination are derived rules,
and hence correct.
\end{lemma}

Unfortunately, it is not always possible to mimic inside $R_{Kid}$
what an optimizations does. Therefore, 
we introduce a notion of {\em graph equivalence}, which is useful for proving
the correctness of {\em cse}-like rules. The terms of a graph may be 
described by the grammar of Figure \ref{pglsyntax}
by changing the definition of the {\small $S\!E$} syntactic
category with {\small $S\!E$ = $E$}.
Graphs for a Kid term can be generated by applying 
a new substitution rule, called the E\_substitution rule.
\subsubsection*{E\_substitution rule}
{\small
\[ \begin{array}{lll}
\frag{X = E}{ X \reduce{}{} E}
\end{array}\]
}

where $E$ can be any {\em side-effect free expression}. \\

\noindent
Suppose ${\bf R'_{CRS}}$ be
\{E\_substitution rule,
Block flattening rule, Multivariable rule\}.

\begin{definition}[Unravelled form]
Let N be the normal form of a term M with respect to
$R'_{\mbox{CRS}}$.
U(M), the unravelling form of a term M, is the term
obtained
by deleting from N all bindings of the form
{\small $X = E$} (where E is a side-effect free expression).
\end{definition}

Notice that the unravelled version of a term is not necessarily a tree.

\begin{definition}[graph-equivalence $\equiv_{g}$]
Two terms M and N are said to be graph-equivalent,
if
\[ U(M) \; \equiv_{\alpha} \; U(N). \] 
\end{definition}

\begin{corollary}
Given an optimizer (A,$R_{opt}$) of
(A,R),
\[ \forall \; M,\; N \in  A,\; [
M \reduce{}{}_{opt} N \;\Longrightarrow \; M \equiv_{g} N]
\;\; \Longrightarrow \;\; (A, R_{opt}) \mbox{ is correct }. \]
\end{corollary}

\begin{lemma}
Let R be the set \{Common subexpression elimination rule,
lift free expressions rule, Hoisting code out of a conditional rule \}.
\[M \reduce{}{}_R N \;\; \Longrightarrow \;\; M \equiv_{g} N. \]
\end{lemma}

Hence ${\em cse}$-like rules are correct.

\section{Conclusions}

Kid goes a long way towards expressing many machine independent implementation
concerns. Since Kid has a proper calculus associated with it,
correctness issues can be handled at an abstract level. 
Kid is central to the current restructuring of the Id compiler
which is already being used by at least 4 or 5 groups to generate
code for their machines by just changing back end of the compiler.
The major deficiency of Kid is the inability to express storage reuse.
We believe a language with a proper calculus which
does not obscure parallelism and which can express storage
reuse would be extremely useful
in practical compilers for functional and other declarative languages.\\

Some of the important optimizations that we currently
perform in the Id compiler but have not
included in $R_{opt}$ are {\em dead code elimination}, {\em loop variable
induction} to hoist array bound checking, and {\em array subscript analyses}.
These optimizations do not fit in the CRS model very well. A better
formalization of these optimizations would be very useful.

%\section*{Acknowledgments}

\bibliography{paper}
\bibliographystyle{abbrv}

\newpage

\tableofcontents

\vfill

\end{document}



We now want to define a different notion of equivalence, that is more tied
up with the computational behavior of a term.  To that end, we define a notion
of printed value of a term, which represents the information contained
in that term. The notion of answer clearly depends on
the particular system we want to consider, therefore,
in the following we will give the basic definitions
and leaving the definition of what it means to print a
term after we have introduced Kid. \\

Let ${\cal P}$ be the information contained in a term.



Summing up we have defined four different kind of equivalences:
\begin{tightlist}
\item[(i)]
$\alpha$-equivalence ($\equiv_{\alpha}$ );
\item[(ii)]
graph-equivalence ($\equiv_{graph}$ );
\item[(iii)]
observational-equivalence ($\equiv_{obs}$ );
\item[(iv)]
observational-congruence ($\cong_{obs}$ );
\end{tightlist}

The implications goes as follows:
\[ \cong_{obs} \; \Longrightarrow \; \equiv_{obs} \; \Longrightarrow \; \equiv_{graph} \; \Longrightarrow \;
\equiv_{\alpha} \]



\begin{definition}[Weak Normal Form]
\blank
\begin{tightlist}
\blank
\item[(i)]
If E is not a redex then E is in Weak Normal Form;
\item[(ii)]
If $E_1 \cdots E_n$ are not redexes and $S_1 \cdots S_m$ are not redexes then
\[\{ S_1 \cdots S_m \; \lambda_s \; X_1 = E_1; \cdots X_n = E_n \; {\sf In} \; X \} \]
where $\lambda_s$ is a set of function definitions, is in Weak Normal Form.
\end{tightlist}
\end{definition}

Notice that we do not require the $\lambda$'s to be in normal from.
***************
\begin{definition}[Partial Order on Basic domain]
A partial order on the basic domain, Atoms, is defined as follows:
\begin{tightlist}
\item[(i)]
$\bot$ $\sqsubseteq$ a, $\forall$ a $\in$ Atoms
\item[(ii)]
a $\sqsubseteq$ $\top$, $\forall$ a $\in$ Atoms
\item[(iii)]
if a $\neq$ $\bot$  or a $\neq$ $\top$  and 
b $\neq$ $\bot$ or
b $\neq$ $\top$ then a and b are
incomparable, that is, a $\not\sqsubseteq$ b and
b $\not\sqsubseteq$ a. 
\end{tightlist}
\end{definition}

The partial order on the product domains, $List, \;Tuple$,
and $Array$, is defined accordingly \cite{Schmidt}.


\noindent
To understand the 
above definition let us first consider the finite case, \ie
when $M$ has a normal form.
If $M$ has a normal form, then the unicity is guaranteed by the
unicity of the normal form and the lemma \ref{approx}.
Consider,
$$\begin{diagram}
& & M & & \\
& \SW & & \SE & \\
M_1 & & & & M_2\\
& \SE & & \SW &\\
& & M_3 & & \\
\end{diagram}$$
by lemma \ref{approx} we know
\[ \begin{array}{l}
{\cal P}rint\;(M) \sqsubseteq {\cal P}rint\;(M_1) \;\; \wedge \;\;
{\cal P}rint\;(M) \sqsubseteq {\cal P}rint\;(M_2) \;\; \wedge \\
{\cal P}rint\;(M_1) \sqsubseteq {\cal P}rint\;(M_3) \;\; \wedge \;\;
{\cal P}rint\;(M_2) \sqsubseteq {\cal P}rint\;(M_3)
\end{array} \]
By transitivity, we have,
\[ {\cal P}rint\;(M) \sqsubseteq {\cal P}rint\;(M_3) \]
That is, ${\cal P}rint\;(M_3)$ is the least upper bound of the
directed set of possible values.\\

Notice that, while the confluence property guarantees the
unicity of the normal form, if it exists, 
the cofinality property, given below, guarantees the unicity of an
infinite normal form, that is, if a reduction 
system has the cofinality property than there exists a reduction
sequence that is maximal in the sense that it captures all possible
information about the term \footnote{Personal communication
with Jan Wilham Klop}.

\begin{definition}[Cofinality Property]
A term M has the cofinality property (CP) if there exists a reduction sequence
$M \reduce{}{} M_1 \reduce{}{} M_2 \cdots \reduce{}{} M_n $
such that for all M' $\in$ ${\cal G}\;(M)$ 
\[\exists \; i, \;\; M' \reduces{}{} M_i. \]
\end{definition}

\begin{definition}
A reduction system (A,R), has the Cofinality property if 
\[ \forall \; M \in A,\;\; CP(M). \]
\end{definition}


\begin{corollary}
Kid has the CP property.
\end{corollary}
\begin{proof}
Since Kid is countable, and:
\[ (A,R) \mbox{ countable } \models CR \Longrightarrow (A,R) \models CP. \]
\end{proof}
\begin{theorem}
Given a term M, the Answer of M exists and it is unique.
\end{theorem}
\begin{proof}
It follows trivially from the cofinality property of Kid.
\end{proof}

\subsection{A Partial Evaluator for Kid}
\label{partialevaluator}

Let $R_{opt}$ = $R_{CRS}\; \cup\; \{ \delta \mbox{ rules}, \;
Case \mbox{ rules for booleans}, \; {\sf P\_select} \mbox{ rule } \}$.
Now consider 
the following interpreter ${\cal EV}$. As usual initially $\rho$
and $\sigma$ would be empty.\\


\noindent
{\small
$\begin{array}{l}
{\cal EV}[\![+ \; (\underline{m},\;\underline{n})]\!] \; \rho \; \sigma =  \underline{+ (m,\;  n)} \\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) ]\!]\;
\rho \; \sigma= {\cal EV}[\![E_1]\!] \; \rho \; \sigma \\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) ]\!] \;
\rho \; \sigma= {\cal EV}[\![ E_2]\!]  \; \rho \; \sigma\\
%\\
{\cal EV}[\![{\sf Bool\_case_m} \; (X,\;   E_1, \;  E_2) ]\!] \;\rho  \; \sigma= 
{\sf Bool\_case_m} \; (X,\; {\cal EV}[\![E_1]\!]\; \rho \; \sigma,\;{\cal EV}[\![E_2]\; \rho \; \sigma\!]) \\
\end{array}$
}

\blank
\noindent
{\small
$\begin{array}{l}
{\cal EV}[\![{\sf P\_select} \;(X, \; Y) ]\!]  \; \rho \; \sigma= Z    \hspace{1cm}  \mbox{if (${\cal L}$ ($X$, $\sigma$))} =
{\sf P\_store}\;(X, \; Y, \; Z)\\ 
%\\
{\cal EV}[\![ \{ Ss; \; As; \; Bs \; {\sf In} \; X \} ]\!]
\; \rho \; \sigma = e \hspace{0.5cm}{\mbox{where $e$ is obtained by the execution of the following program written in pseudo-Id}}\\
\hspace{2.5cm}{
\{ \begin{array}[t]{l}
  blk,- = {\cal F\&S}(\{ Ss; \; As; \; Bs \; {\sf In} \; X \});\\
  \; flag = {\sf True};\\
   \;{\sf If} \; blk = \top \; {\sf then } \; \top\\
\;\;\; {\sf else}\\
   \{\; blk= \{ \begin{array}[t]{l}
     {\sf While} \; flag \; {\sf do}\\
    \;\; \mbox{ Suppose $blk$ is } \{Ss;\;As;\;Bs \; In \; X \}\\ 
   \;\;is = {\cal CC}(\sigma \cup Ss);\\
   \;\;fs = \rho \cup As;\\
   \;\;{\sf next} \; blk, {\sf next} \; flag  = \begin{array}[t]{l}
     {\sf If} \; is = {\sf \top_s} \; {\sf then} \; ({\sf \top},
     {\sf False} ) \\
      \;\;\;\;\; {\sf else} \;  {\cal F\&S}({\cal EV'\_RHS}(blk,is,fs))  \\
      \end{array}\\
\;\; {\sf finally} \; blk \} \\
\end{array}\\
 \; \mbox{ Suppose blk' is } \{Ss';\;As;'\;Bs' \; {\sf In} \; X' \}\\ 
   \;\;is = {\cal CC}(\sigma \cup Ss);\\
   \;\;fs = \rho \cup As;\\
   \;\; blk''= {\sf If} \; is = {\sf \top_s} \; {\sf then} \;( {\sf \top},
     {\sf False} ) \\
      \;\;\;\;\;\hspace{1cm} {\sf else} \;  ({\cal EV\_RHS}(blk'',is,fs))  \\
\;\;\;{\sf In} \; blk'' \} \}\\
\end{array} }
\end{array}$
}
{\small
$\begin{array}{l}
\hspace{2cm}{\mbox{where}} \\
\\
\hspace{2.5cm}{{\cal EV'\_RHS}([\![ Ss; \; As;\; X_1 = E_1; \cdots
X_n=E_n \;  {\sf In} \; X_i ]\!] \; \rho \; \sigma =}\\
\hspace{4cm}{
\{ Ss; \; As; \; X_1 = {\cal EV'}(E_1,\;\rho \;\sigma); \cdots
 X_n = {\cal EV'}(E_n,\;\rho \;\sigma) \; {\sf In} \; X_i \} }\\
\\
\hspace{2cm}{\mbox{and the function ${\cal EV'}$ given below
unlike ${\cal EV}$ does not go inside encapsulators.}} \\
\\
\hspace{2.5cm}{
\begin{array}{l}
{\cal EV'}[\![+ \; (\underline{m},\;\underline{n})]\!] \; \rho \; \sigma =  \underline{+ (m,\;  n)}\\
{\cal EV'}[\![{\sf Bool\_case_m} \; ({\sf True },\;   E_1, \;  E_2) ]\!]\;
\rho \; \sigma= E_1 \\
{\cal EV'}[\![{\sf Bool\_case_m} \; ({\sf False },\;   E_1, \;  E_2) ]\!] \;
\rho \; \sigma=  E_2 \\
{\cal EV'}[\![{\sf P\_select} \; (X,\;Y) ]\!] \; \rho \; \sigma=  Z,\;{\sf True} \hspace{1cm} \mbox{if (${\cal L}$ ( $X$, $\sigma$))} =
{\sf P\_store}\;(X, \; Y, \; Z)\\ 
\mbox{ else } \\
{\cal EV'}[\![E]\!]\\
\end{array}
}
\end{array}$\\
}

\noindent
{\small
$\begin{array}{l}
\mbox{else} \\
{\cal EV}[\![ E]\!] \; \rho \; \sigma = E
\end{array}$  \\
}



\blank
\noindent
{\small
$\begin{array}{l}
\end{array}$\\
}

%\blank
%\noindent
%Where the function mentioned above as so defined,
%
%\blank
%\noindent
%${\sf Fun} \; {\tt f\&s} \; B = \{
%\begin{array}[t]{l}
%B' = {\tt f\&s\_rhs} \; B;\\ 
%B'' = {\tt f1} \; B';\\
%B'''= {\tt s} \; B'';\\
%\;\;{\sf In} \; B''' \}
%\end{array} $ 
%
%
%\blank
%\noindent
%${\sf Fun} \; {\tt f\&s\_rhs} \; [\![ \{ X = E; \; \cdots \; {\sf In} \; Y \} ]\!]=
%\{ X = {\tt f\&s} \;[\![ E ]\!] \cdots {\sf In}\; Y \}$\\
%
%\blank
%\blank
%\noindent
%{\tt op'\_rhs} (B) applies OP' to each RHS expression using $is$ plus
%$\Delta$\_is as the stores, where $\Delta$\_is
%are the store commands associated with the block
%B. A global change flag (OR of all OP' flags) is also
%returned.\\
%
%
%\blank
%\noindent
%op\_rhs (B) applies OP to each RHS expression using $is$ plus
%$\Delta$\_is as the stores. \\
%
%
%
%\blank
%\noindent
%$f1 [\![ \Delta\_is; \; x_i = \{ \Delta\_is';
%\; y_i = E_i; \;{\sf In} \; y_i \};
%\; x_j = E_j {\sf In} \; x_i \} ]\!] = \{
%\begin{array}[t]{l}
%\Delta\_is + \Delta\_is';\\
%x_i = y_i;\\
%y_i = E_i;\\
%x_j = E_j;\\
%{\sf In} \; x_j \}\\
%\end{array} $

\begin{theorem}[Normalization Theorem]
Given terms M and N,
\[ M \;  \reduces{}{}_{R_{opt}}\; N \;\; \Longrightarrow \;\; {\cal EV}[\![ M]\!] \; {\sf Nil} \; {\sf Nil} = N. \]
\end{theorem}

%\blank
%\noindent
%Where the function mentioned above as so defined,
%
%\blank
%\noindent
%${\sf Fun} \; {\tt f\&s} \; B = \{
%\begin{array}[t]{l}
%B' = {\tt f\&s\_rhs} \; B;\\ 
%B'' = {\tt f1} \; B';\\
%B'''= {\tt s} \; B'';\\
%\;\;{\sf In} \; B''' \}
%\end{array} $ 
%
%
%\blank
%\noindent
%${\sf Fun} \; {\tt f\&s\_rhs} \; [\![ \{ X = E; \; \cdots \; {\sf In} \; Y \} ]\!]=
%\{ X = {\tt f\&s} \;[\![ E ]\!] \cdots {\sf In}\; Y \}$\\
%
%\blank
%\blank
%\noindent
%{\tt op'\_rhs} (B) applies OP' to each RHS expression using $is$ plus
%$\Delta$\_is as the stores, where $\Delta$\_is
%are the store commands associated with the block
%B. A global change flag (OR of all OP' flags) is also
%returned.\\
%
%
%\blank
%\noindent
%op\_rhs (B) applies OP to each RHS expression using $is$ plus
%$\Delta$\_is as the stores. \\
%
%
%
%\blank
%\noindent
%$f1 [\![ \Delta\_is; \; x_i = \{ \Delta\_is';
%\; y_i = E_i; \;{\sf In} \; y_i \};
%\; x_j = E_j {\sf In} \; x_i \} ]\!] = \{
%\begin{array}[t]{l}
%\Delta\_is + \Delta\_is';\\
%x_i = y_i;\\
%y_i = E_i;\\
%x_j = E_j;\\
%{\sf In} \; x_j \}\\
%\end{array} $

%\subsection{A strategy for Partial Evaluation using $R_{opt}$}

Space does not permit us to give a full partial evaluator
for $R_{opt}$. We explain briefly a strategy for applying
$R_{opt}$ rules in an efficient manner.
\begin{enumerate}
\item[(1)]
apply all rules, except Common Subexpression Elimination,
from outside in, as explained in Section  \ref{partialevaluator};
\item[(2)]
apply Common Subexpression Elimination from inside out;
\item[(3)]
if there is any change in the expression in step (2) go to step (1),
else stop.
\end{enumerate}
The only optimizations that can be triggered as a consequence
of CSE (step (2)) are the algebraic rules such as, equality.
However, even the optimization that is triggered can in
turn cause other optimizations to be triggered. Thus, it is 
important to go back to step (1) at the end of step (2).\\

There are several optimizations for which it is not easy to 
decide automatically whether and when to apply them profitably.
Such optimizations include {\em Partial Evaluation},
{\em Loop Peeling}, and {\em Loop Unrolling}.
The last one of these also requires specification of a value for $k$.
The current Id compiler uses annotations provided by the user
to trigger these optimizations. Assuming
the existence of such annotations, we believe that the above
strategy computes the normal form with respect to all the
optimizations. Though we have not proved this yet, we
believe this is easy to show for optimizations in step (1).\\

Other interesting questions about
optimizations are whether $R_{opt}$ is strongly
normalizing and confluent. We have shown in 
\cite{Zena89} that some algebraic rules cause $R_{opt}$ to be
non confluent. However, this is not a serious drawback
because the cases where the confluence is lost are the one where the
unoptimized program would have produced no information . The
strongly normalizing property can not hold in presence
of the apply rule. However, any practical compiler can stop on
some other bases such as the number of times an
optimization is applied or the number of
optimization passes. This will just produce a partially
optimized program. \\

A more sophisticated strategy that
we have not explored yet would try to compute
some fixpoint in case of apply rule and partial evaluation rule.

We need to define an ordering on printable values. This is
the motivation behind the following definitions.\\

It is common to represent trees \cite{Lloyd} by sequences
of non-negative integers.
Before giving the definition of a tree, we need to introduce some
notation. 
We let $\omega^*$ to denote the set of all finite sequences
of non-negative integers. A sequence over $\omega$ is
represented in square brakets, \ie [$i_1,\cdots,i_n$],
$i_1 \cdots i_n \in \omega$.
If $m$ and $n$ are sequences, then [$m$,$n$] denotes
the concatenation of sequences $m$ and $n$.
If $m$ is a sequence and $i$ $\in$ $\omega$, then [$m$,$i$]
denote the sequence [$m$,$[i]$].
$\epsilon$ denotes the empty sequence.
As usual, $\mid X \mid$, denotes the cardinality of the set $X$.

\begin{definition}[Tree]
T $\subseteq$ $\omega^*$, is a tree, iff
\begin{tightlist}
\item[(i)]
$\forall$ n $\in$ $\omega^*$, $\forall$ i,j $\in$ $\omega$
$[n,i] \; \in \; T, j < i \Longrightarrow [n,j] \; \in \; T$; 
\item[(ii)]
$\forall$ n $\in$ T, the set $\{ i \mid [n,i] \in \; T \}$ is finite.
\end{tightlist}
\end{definition}

Condition $(ii)$ guarantees that the tree is finitely branching.
We let $br(n,t)$ be the function that returns the cardinality of
the set $\{ i \mid [n,i] \in \; t \}$.\\

The alphabet of printable values is a ranked
alphabet, in the sense that each symbol has an associated
arity. If we let $ar$ be the function that given a symbol
returns the corresponding arity, we have:
\[ \forall \; s \in \; Atoms,\;\; ar(s)=0; \; \mbox{ and }\;
ar({\sf List})= ar({\sf 2\_Tuple})=2\;
\mbox{ and }\;ar({\sf 3\_Tuple})=ar({\sf 2\_Array})=3 \cdots \]

Notice that a ${\sf 2\_Array}$ constructor has arity 3, where the
fisrt component is the bound tuple. 

\begin{definition}[Printable Value]
A Printable Value is a function $t:dom(t)\rightarrow PV$, such that
\begin{tightlist}
\item[(i)]
dom(t) $\neq$ $\epsilon$;
\item[(ii)]
$\forall$ n $\in$ dom(t), ar(t(n))=$\mid \{ i:[n,i]\in dom(t)\}\mid$
\end{tightlist}
\end{definition}

We say the $dom(t)$ underlines $t$.\\

For example, the infinite list of 1's seen before, is represented by the
sequence $(12)^*$, with the function $t$ defined as follows
\[ \begin{array}{l}
t(2^n) = {\sf List}, \; \forall\;n \geq 0;\\
t(2^n 1) = 1, \; \forall\;n \geq 0;
\end{array} \]

The set ${\cal PV}_\top$ is the set of all terms over $PV$, extended with a
top element.
We can define an ordering relation over ${\cal PV}_\top$, as follows: 

\begin{definition}[Partial Order on $PV_{\top}$]
Given f, g $\in$ ${\cal PV}_\top$, f $\sqsubseteq$ g iff:
\begin{tightlist}
\item[(i)]
dom(f) $\subseteq$ dom(g);
\item[(ii)]
$\forall$ s $\in$ dom(f),
\hspace{2cm}{
\item[(ii.1)]
br(s,dom(f)) $\neq$ 0 $\wedge$ (f(s) = {\sf List}) $\vee$ 
(f(s)={\sf n\_Tuple})
$\Longrightarrow$ f(s) = g(s)
\item[(ii.2)]
br(s,dom(f)) $\neq$ 0 $\wedge$ (f(s) = {\sf n\_Array}) 
$\Longrightarrow$ f(s) = g(s)  $\wedge$  f(s.1)= g(s.1)
\item[(ii.3)]
br(s,dom(f)) = 0 $\wedge$ (f(s) $\neq$ $\Omega$)
$\Longrightarrow$ f(s) = g(s)
}
\end{tightlist}
\end{definition}

Notice that condition $(ii.2)$ requires that two arrays must have the same bounds.

