% 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[12pt]{article}

\input /jj/ariola/macros/prelude

\begin{document}

\title{Compilation of Id$^-$:  A Subset of Id
\footnote{This technical report is created by merging
CGS memo 315 (dated November 1 1990) and CSG memo 322 
(dated December 10 1990)}}

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

\today

\maketitle

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

\bigskip

\begin{minipage}{6in}

Compilation of Id, a higher-order non-strict functional language
augmented with I-structures, is described in terms of two 
languages. 
The first language is called Kid, which is a Kernel language for Id. 
Kid is further translated into a language where
all Kid data structures and functions are represented
using only one data structure. This second language is called
P-TAC for Parallel Three Address Code.
The operational semantics of both Kid and P-TAC
are presented in terms of two {\em contextual reduction systems}.
Formalization of 
many commonly known optimizations is also presented 
in the contextual reduction framework.

\bigskip

{\bf Keywords and phrases}:
Term Rewriting Systems, Contextual Reduction Systems,
Dataflow, Functional Languages, I-structures, Compiler Optimizations.
\end{minipage}

\newpage


\section{Introduction}

\begin{figure}[htbp]
\vspace{0.5in}
\illustration{id}{2.53in}
\vspace{-0.8in}
\caption{Compilation scheme}\label{comp}
\end{figure}

We describe the compilation of Id$^-$, a subset of the Id language,
in terms of successive translations into  different languages. Each 
of the successive languages  has a precise operational semantics,
which is given in terms of rewrite rules. 
The compilation scheme is shown in Figure~\ref{comp}.
Id$^{-}$ does not contain the following features of Id:
\begin{enumerate}
\item[]
abstract types and algebraic types except lists;
\item[]
overloading;
\item[]
mutable structures. 
\end{enumerate}

Id$^-$ is first parsed into de-sugared Id$^-$, where enough parentheses 
are inserted to make operator associativity and precedence irrelevant.
Desugared Id$^-$ also does not contain  patterns in function definitions.
During the de-sugaring phase list-comprehensions and array-comprehensions are
transformed into nested loops.
We will informally describe this phase in the next Section. \\

In the next phase de-sugared Id$^-$ is translated into Kid, the Kernel
language for Id. Kid is a subset of Id except for the notion of {\em multiple
values} which have been inspired by dataflow graphs. Essentially a
Kid program contains only primitive patterns and simple expressions.  
The Kid syntax and operational semantics are given in Section
\ref{syntaxandrules}.
The translation from de-sugared Id$^-$ to Kid,
including the
compilation of complex patterns into primitive patterns, is described 
in Section \ref{idtokid}.\\

Kid serves several purposes.  Since Id is too complex to be given
direct operational semantics, it is preferable first to give a 
translation of Id  into a smaller language such as Kid. Thus,  
Id is defined indirectly
in terms of the rewrite rule semantics of Kid. 
Kid is also  the intermediate language in which a large number of
architecture independent compiler optimizations are performed. 
These  optimizations are described in Section \ref{optirules}.
We think that many other types of analyses such as 
Milner style type checking, or abstract interpretation for storage
reclamation should be performed at the Kid level.  These analyses
are  not described in this document.\\

An implementation  method that is preferred by many researchers
eliminates  explicit environments  containing the value of free
variables of a function. This requires applying a program transformation
known as lambda-lifting. Lambda-lifting involves two steps: first,
all nested function definitions ($\lambda$-expressions)
of a Kid program are ``closed'' by turning  their free variables into 
parameters. In the second step, all closed definitions are lifted to the 
top level.  Lambda-lifting should be done after optimizations have been
performed on Kid programs. There are many algorithms for doing
lambda-lifting and we do not describe any of them  in this document.
Interested reader is referred to Johnsson's paper \cite{Johnsson85}.\\

The next step is to translate a lambda-lifted Kid program into P-TAC 
\cite{Zena89},
which is a much smaller language than Kid. 
This translation calls for choosing a machine  representation for each type of
Kid value and thus, involves many low level efficiency issues.
P-TAC and its operational semantics  are given in Section \ref{ptac}.
A translation from Kid into P-TAC is given in Section \ref{pgltop-tac}.
We end the document by showing in Section \ref{signals} how a P-TAC
program is extended with Signals \cite{Traub86} which are needed to detect termination
and for resource management. \\

Our compiling approach allows the formalization of questions related to 
correctness  \cite{Zena89}. 
For example, it will make sense to talk about the correctness of lambda-lifting,
or the correctness of the translation from Kid to P-TAC. Moreover, since there exists
an independent operational semantics of Id$^-$ in terms of a even smaller subset of
kernel Id \cite{Nikhil90a}, it may be possible to
prove the correctness of the translation between de-sugared Id$^-$ and Kid.
Another advantage of our approach is that we are able to delay the introduction of 
concepts tied to specific machines or even to the dataflow computation model
until we actually generate machine code. However, in this document we do not go 
below the P-TAC level.

{\small
\begin{figure}[htbp]
\begin{tabular}{|l|} \hline
\\
$\begin{array}{lll}
U\!O\!P & \in  & \mbox{Unary Operator}\\
B\!O\!P & \in & \mbox{Binary Operator}\\
E & \in & \mbox{Expression} \\
P & \in & \mbox{Pattern}
\end{array}$ \\

$\begin{array}{lll}
\\
Variable & ::= & x \mid y \mid z \mid \cdots \mid a \mid b \mid \cdots \mid 
                 f \mid \cdots \mid x_1 \mid \cdots \mid F \mid G \mid
                 \cdots   \\

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

U\!O\!P & ::= & {\sf Negate} \mid{\sf Not} \mid {\sf nD\_Bounds} \mid
                {\sf I\_nD\_array} \mid {\sf Open\_cons}  \\

B\!O\!P & ::= & {\sf +} \mid {\sf -} \mid {\sf *} \mid \cdots \mid {\sf ==}
                \mid {\sf Eq?} \mid {\sf <} \mid \cdots \mid {\sf And}
                \mid {\sf :} \\

E &::=& Variable \mid {\sf Next} \; Variable \mid Constant \\
  &   &  \mid (U\!O\!P \; E) \mid (E \; B\!O\!P  \; E)
         \mid (E\; E) \mid E[E] \mid E.{\sf  cons\_1}
         \mid E.{\sf cons\_2} \\
  &   &  \mid (E,E) \mid (E,E,E) \mid \cdots  \\
  &   &  \mid ({\sf If} \; E \; {\sf then} \;  E \;
         {\sf else} \;E) \mid 
         \{ {\sf Case} \; E \; {\sf of} \; Clause\;[\; \mid \; Clause]^*\; \} \\
  &   &  \mid\{ {\sf While}\;E\;{\sf do}\;[Statement;]^*\;{\sf Finally}\; E \}\\
  &   &  \mid \{{\sf For}\;Variable\;\leftarrow\;E\;{\sf to}\;E\;{\sf step}\;E\;
         {\sf do}\; [Statement;]^* \; {\sf Finally} \; E \} \\
  &   &  \mid \{ {\sf Fun} \; [Variables]^* \; = \; E \} \mid
         \{ \underline{{\sf Fun}} \; [Variables]^* \; = \; E \} \\
  &   & \mid Block \\

Block & ::=& \{ [Statement;]^* \;\;{\sf In} \; E \} \\

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

Binding &::= & P \; {\sf =} \; E \\

Command & ::= & E[E]=E \mid E.{\sf cons\_1} = E \mid E.{\sf cons\_2} = E \\

Clause & ::= & P = E \\

P &::= & {\sf Nil} \mid Variable  \mid  {\sf Next} \; Variable \mid (P,P)
         \mid  (P,P,P) \mid \cdots \mid  (P : P)\\

Program &::=&  Block

\end{array} $\\
\\ \hline
\end{tabular}
\\
\caption{Grammar of de-sugared Id$^-$} \label{idsyntax}
\end{figure}
}

\section{Desugared Id$^{-}$}
The syntax of de-sugared Id$^{-}$ is described in Figure \ref{idsyntax}.
As can be seen from the grammar, de-sugared Id is fully parenthesized
and thus has no operator precedence. Thus, an Id expression like

\beginid
\null
         (f x) : map f xs
\null
\endid
becomes
\beginid
\null
         ((f x):((map f) xs))
\null
\endid

Id has curried versions of infix binary operators which are 
written by enclosing the operator in parenthesis. Thus, {\cf (+)} 
represents the curried {\cf +}, and it makes sense to write {\cf ((+) 2)} 
in Id. In de-sugared Id$^-$  we treat the curried version of an operator 
as a constant, which has a standard function definition associated with it.
For the sake of symmetry we have also included curried 
versions of all unary operators in de-sugared Id$^-$. \\

During the de-sugaring phase multi-clause functions, are turned into
equivalent case expressions, as shown in the example below
\beginid
\null
\null
        Def map f Nil  = Nil
         |  map f x:xs = (f x) : map f xs;
\null
\null
\endid
becomes
\beginid
\null
\null

        Def map  t1 t2 = { Case (t1, t2)   of
                             |  (f,  Nil)  = Nil
                             |  (f,  x:xs) = (f x) : map f xs } 
\null
\null
\endid
where t1 and t2 are new variables.
Furthermore, all function definitions are turned into 
$\lambda$~-~expressions.

\beginid
\null
\null

       map =  { Fun t1 t2 = { Case (t1, t2)   of
                                |  (f,  Nil)  = Nil
                                |  (f,  x:xs) = (f x) : map f xs } } 
\null
\null
\endid

\noindent
If the Id function is defined as substitutable ({\sf Defsubst})
 then the corresponding
$\lambda$-expression ({\sf \underline{Fun}}) is underlined. The ``underlined'' 
$\lambda$-expressions are then expanded in line during optimizations
(see Section~\ref{optirules} ). \\

The most complex part of the de-sugaring phase is the transformation of comprehensions 
into loops. This is described in detail in \cite{Nikhil88b}.  Here we only illustrate
the idea using the following example:
\beginid
\null
        {: e || x <- xs ; y <- ys}

\null
\endid
A typical translation of this 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.  Basically,
in the following 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.
%\pagebreak
\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
The above translation is correct if we treat open lists and lists 
as the same type. 
However, there are several subtle issues regarding type
checking that are  still not resolved.

{\small
\begin{figure}[htbp]
\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\_nD\_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 nD\_Bounds}
                \mid {\sf I\_nD\_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 P\_nD\_select} \mid {\sf Make\_tuple_{2} } \\

P\!FN_1 & ::= & {\sf Make\_tuple_n} \mid {\sf Apply_{n\!-\!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\_nD\_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{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 P-TAC.\\

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

\section{Translating Desugared Id$^{-}$ into Kid}
\label{idtokid}

\subsection{Simplification of Expressions}
We give the translation in terms of the following functions:\\

$\begin{array}{lllll}
\mbox{Translate Expression,} &  {\small {\tt TE}}: & \mbox{ Id$^{-}$ Expression } &
\longrightarrow & \mbox{ Kid Expression  } \\
\\
\mbox{Translate Statement,} &  {\small {\tt TS}}: & \mbox{ Id$^{-}$ Statement}
&  \longrightarrow & \mbox{ list (Kid Statement)}\\
\\
\mbox{Translate Binding, } & {\small {\tt TB}}: & \mbox{ Id$^{-}$ Binding}
& \longrightarrow & \mbox{ list (Kid Binding)} \\
\\
\mbox{Translate Operator,}
& {\small {\tt TO}}: & \mbox{ Id$^{-}$ Operator} & \longrightarrow &
\mbox{ Kid Operator}\\
\\
\mbox{Pattern Matching,}
& {\small {\tt PM}}:  & \mbox{Case\_expression} &
\longrightarrow  & \mbox{ Kid  Expression} 
\end{array}$ \\

\blank
\noindent
The exact syntax of Case\_expression is given in Section 
\ref{pattern}.\\

We will write
{\small ${\tt TE}[\![ E_1 ]\!] = E_2$}, where the expression enclosed
in double brackets represents an Id$^{-}$ expression and {\small $E_2$} is the
corresponding Kid expression. 
The whole translation is given in terms of syntactic categories.
The proper way of reading a translation function such as 
{\small ``${\tt TE}[\![(U\!O\!P\; E_1)]\!]=
\{ t_1 = {\tt TE}[\![E_1]\!] ;\;t = {\tt TO}[\![ U\!O\!P]\!] \; (t_1); \;
{\sf In}\;t \}$ '' }
is that {\small ``{\tt TE}''} when applied to a unary expression in Id$^-$ produces
the Kid expression on the right-hand-side.\\

Throughout, the emphasis is on clarity of Id$^-$ to Kid translation
rather than its efficiency.
We will use the  same conventions introduced
in Section \ref{rules}, with the addition of meta-variable
$P_i$ that ranges over Patterns.
As before {\small $\mv{X_n}$ } indicates 
multiple meta-variables.
The lower case variables, such as $t_i$, $x_i$, that appear
in the translated expression 
represent new Kid variables. 
The translation procedure given below does not
require lexical scope analysis for variables. However, after the translation
is complete a procedure to make all bound variables unique has to be applied
before any rewriting can be done.\\

A common situation in the translation procedure is the need to
replace variable {\small $X$} by a new variable $t$ in some Id expression
{\small $E$}.
This idea can be expressed by addding
another block around {\small $E$}
as in {\small $\{\;X=t; \;t'=E; \; {\sf In } \; t'\;\}$}.
To avoid clutter, we will write {\small $E\;[t/X]_B$} as a
shortand for {\small $\{\;X=t; \;t'=E; \; {\sf In } \; t'\;\}$}.
(As an aside, it should be noted that since we do not assume unicity of 
variables  during translation, we can not use the notion for naive 
substitution.  Conversely, the use of {\small $E\;[\mv{X_n}/\mv{Z_n}]_B$}
in the application rewrite rule, given earlier, would have been incorrect,
because it could lead to duplication of bound variables {\small $\mv{Z_n}$},
while expanding two different applications of the same function).

\subsubsection*{TE: Id$^{-}$ Expression $\longrightarrow$ Kid Expression}  
{\small
$\begin{array}{l}
{\tt TE}[\![X]\!] = X 
\end{array}$ \\
}

{\small
\blank
\noindent
$\begin{array}{l}
{\tt TE}[\![{\sf Next} \; X]\!] = next(X)
\end{array}$ \\
}

\blank
\noindent
Where $``next"$ is a function on identifiers that keeps the association 
between a variable and its corresponding nextified version during the 
loop translation phase. After the translation is complete,
$next({\small X})$
is treated like an ordinary identifier which is different from {\small $X$}.\\

{\small
\blank
\noindent
$\begin{array}{ll}
{\tt TE}[\![C]\!] = C 
\end{array}$ \\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![(U\!O\!P \; E)]\!] & = &  \{ \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![E]\!];\\
t & = & {\tt TO}[\![U\!O\!P]\!]\;(t_1) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t   \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![(E_1 \; B\!O\!P \; E_2)]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!]; \\
t & = & {\tt TO}[\![B\!O\!P]\!]\; (t_1, \;t_2) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![(E_1\; E_2)]\!] & = &  \{ \begin{array}[t]{lll} 
t_1 & =  & {\tt TE}[\![E_1]\!]; \\
t_2 & = &  {\tt TE}[\![E_2]\!]; \\
t & = &  {\sf Apply} \;(t_1,\;t_2)\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ E_1[E_2] ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t_2 & = & {\tt TE}[\![E_2]\!]; \\
t & = &  {\sf Ap_2} \; ({\sf Select}, \; t_1, \; t_2) \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}\\$
}

\noindent
where {\small ${\sf Select}$} is a standard function definition in Kid 
(see Section \ref{standard}).\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ E.{\sf cons\_1} ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E]\!];\\
t & = & {\sf List\_case} \;(t_1,\; {\sf Error}, \; {\sf Cons\_1}\;(t_1) )\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}\\$
}

\noindent
Similarly for {\small $E.{\sf cons\_2}$}.\\


\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![(E_1, \cdots, E_n) ]\!] & = & \{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
\multicolumn{3}{l}{ \;\;\;\;\vdots} \\
t_n & = &  {\tt TE}[\![E_n]\!]; \\
t & = &  {\sf Make\_tuple_n} \;(\mv{t_n})\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$ \\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ ({\sf If}\; E_1\; {\sf then}\; E_2\; {\sf else}\; E_3)]\!] & = & 
\{ \begin{array}[t]{lll}
t_1 & = &  {\tt TE}[\![E_1]\!];\\
t & = &  {\sf Bool\_case} \; (t_1, \; {\tt TE}[\![E_2]\!], \;
{\tt TE}[\![E_3]\!] )\\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{ \begin{array}[t]{lll}
\multicolumn{3}{l}{ {\sf Case} \; E \; {\sf of}} \\
\;\; \mid \; \;\;\;P_1  & = &  E_1 \\
\multicolumn{3}{c}{ \vdots}\\
\;\; \mid \;\;\;P_n  & = &  E_n \; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![ E ]\!]; \\
t & = & {\tt PM}[\![ \{ \begin{array}[t]{lll}
\multicolumn{3}{l}{ {\sf Case} \; (t_1) \; {\sf of}} \\
\;\; \mid \;\;\; P_1 & = & {\tt TE}[\![E_1]\!]\\
\multicolumn{3}{c}{ \vdots}\\
\;\; \mid \;\;\; P_n & = & {\tt TE}[\![E_n]\!] \; \} ]\!]
\end{array}   \\
\multicolumn{3}{l}{\;\;\;{\sf In}\;\; t \} }
\end{array}
\end{array} $ \\
}

\noindent
Where {\small ${\tt PM}$} is described in the Section \ref{pattern}.\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{  \begin{array}[t]{l}
 {\sf While} \; E \; {\sf do}\\
\;\; S_1; \\
\;\;\;\; \vdots \\
\;\; S_n; \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} &  = &
\begin{array}[t]{l}
{\tt TSLE}[\![ \{ \begin{array}[t]{l}
  {\sf While} \; {\tt TE}[\![E]\!] \; {\sf do}\\
\;\; {\tt TS}[\![S_1]\!]; \\
\;\;\;\; \vdots \\
\;\; {\tt TS}[\![S_n]\!]; \\
\;\;\;\;{\sf Finally}\;{\tt TE}[\![E_f]\!]\; \}]\!]
\end{array} 
\end{array}
\end{array}$\\
}

\blank
\noindent
Note that {\small {\tt TE}} uses an auxiliary function {\small {\tt TSLE}} which
stands for ``Translate simple loop expression''. 
However this is only done for clarity of exposition.
In fact, we are slightly abusing our notation because the expression
inside {\small ${\tt TSLE}[\![ \; ]\!]$} is
a mixture of Id$^-$ and Kid syntax.

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TSLE}[\![ \{  \begin{array}[t]{l}
 {\sf While} \; E \; {\sf do}\\
\;\; next(X_1)  = E_1;\\
\;\;\;\; \vdots \\
\;\; next(X_n)  = E_n;\\
\;\; Y_1 = E_{y_1};\\
\;\;\;\; \vdots \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
p & = &  \underline{\lambda_{n}} \; ( \mv{X_n}) \; . \;   (E);\\
b & = & \underline{\lambda_{n,n}} \; ( \mv{X_n} )  \;\; . \;\;  
( \{_{\sf n} \begin{array}[t]{l}
next(X_1)   =  E_1  ;\\
\;\;\; \vdots\\
next(X_n)  = E_n ;\\
Y_1 =  E_{y_1};\\
\;\;\; \vdots \\
\;\;\;\; \;{\sf In} \; next(X_1), \cdots, next(X_n) \; \} ); 
\end{array} \\
\blank
t_p & = &  {\sf Ap_n} \; (p,\; \mv{X_n});\\
\mv{t_{n}} &  = & {\sf WLoop_n} \; (p, \; b, \;  \mv{X_n}, \; t_p); \\
t_f & = &  E_f \;[\mv{t_n}/\mv{X_n}]_B \\
\multicolumn{3}{l}{ \;\;\;\;{\sf In} \; t_f \} }
\end{array}
\end{array} $
}\\

\blank
\noindent
Notice that the correspondence between the formal parameters of the 
procedure ``$b$" and the multiple value returned is not accidental.
It will be wrong to have {\small ($X_1,  \cdots , X_n$)} as input and
{\small ($next(X_n),\cdots, next(X_1)$)} as output,
because the values of the nextified variables come either from the surrounding
scope or from the previous iteration.
The $\lambda$-expressions corresponding to the predicate and loop
body are underlined indicating the fact that they can be 
inlined at compile time.\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{  \begin{array}[t]{l}
 {\sf For} \; X \; \leftarrow \; E_i \; {\sf to} \; E_b \; {\sf step} \;
Es \; {\sf do}\\
\;\; S_1; \\
\;\;\;\; \vdots \\
\;\; S_n; \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} &  = &
\begin{array}[t]{l}
{\tt TSLE}[\![ \{\begin{array}[t]{l}
  {\sf For} \; X \; \leftarrow \; {\tt TE}[\![ E_i ]\!] \; {\sf to}\; {\tt TE}[\![ E_b ]\!] \; {\sf step} \; {\tt TE}[\![ E_s ]\!] \;  {\sf do} \\
\;\; {\tt TS}[\![S_1]\!]; \\
\;\;\;\; \vdots \\
\;\; {\tt TS}[\![S_n]\!]; \\
\;\;\;\;{\sf Finally}\;{\tt TE}[\![E_f]\!]\; \}]\!]
\end{array} 
\end{array} \\
\end{array}$ 
}\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TSLE}[\![  \begin{array}[t]{l}
\{ {\sf For} \; X_1 \; \leftarrow \; E_i \; {\sf to} \; E_b \;
{\sf step} \; E_s \; {\sf do}\\
\;\; next(X_2)  = E_2;\\
\;\;\;\; \vdots \\
\;\; next(X_{n})  = E_n;\\
\;\; Y_1 = E_{y_1};\\
\;\;\;\; \vdots \\
\;\;\;\;{\sf Finally}\;E_f\; \} ]\!]
\end{array} & = &
\{ \begin{array}[t]{lll}
b & = & \begin{array}[t]{l}
\underline{\lambda_{n,{n-1}}} \; ( \mv{X_{n}} )\;  . \\
\hspace{0.4cm}{
( \{_{\sf n-1} \begin{array}[t]{l}
next(X_2)   =  E_2  ;\\
\;\;\; \vdots\\
next(X_{n})  = E_{n} ;\\
Y_1 =  E_{y_1};\\
\;\;\; \vdots \\
\;\;\; \;{\sf In} \; next(X_2), \cdots, next(X_{n}) \; \} ); 
\end{array} }
\end{array} \\
\blank
t_i & = &  E_i;\\
t_b & = &  E_b;\\
t_s & = &  E_s;\\
t_p & = &  {\sf \leq} \; (t_i,\; t_b);\\
\mv{t_{n}} &  = & {\sf FLoop_n} \; (t_b, \; t_s,\; b,\; t_i,\;
\mv{X_{2,n}}, \; t_p); \\
t_f & = &  E_f \;[\mv{t_n}/\mv{X_n}]_B \\
\multicolumn{3}{l}{ \;\;\;\;{\sf In} \; t_f \} }
\end{array}
\end{array} $
}\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{ {\sf Fun} \;\mv{X_n} \; =   \; E \} ]\!] & = &    
 {\sf \lambda_n} \;(\mv{X_n}) \; .   \; ({\tt TE}[\![ E]\!] )
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{ \underline{{\sf Fun}} \;\mv{X_n} \; =   \; E \} ]\!] & = &    
 \underline{{\sf \lambda_n}} \;(\mv{X_n}) \; .   \; ({\tt TE}[\![ E]\!] )
\end{array}$\\
}


\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{ S_1; \cdots S_n;\; {\sf In} \;E\}]\!] & = &
\{ \; {\tt TS}[\![S_1]\!];\\
& &\;\;\;\;\vdots\\
& & \;\;\;  {\tt TS}[\![S_n]\!];\\
& &  \;\;\; t = {\tt TE}[\![E]\!]\\
& & \;\;\;\;{\sf In}\;\;t \; \}
\end{array}$ \\
}

\subsubsection*{TS: Id$^{-}$ Statement $\longrightarrow$ 
 list (Kid Statement) }
Often an Id$^-$ statement translates into a group of Kid statements. We will enclose the translated
statement or statements within parenthesis even though parenthesis are not part of Kid syntax.
These parenthesis do not introduce a new lexical scope. \\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TS}[\![ P=E  ]\!] & = &
(t = {\tt TE}[\![ E ]\!];\;  {\tt TB}[\![ P=t  ]\!] ) 
\end{array}$\\
}


\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TS}[\![ E_1[E_2] = E_3 ]\!] & = &
( \begin{array}[t]{lll}
 t_1 & = & {\tt TE}[\![ E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!];\\
t_3 & = & {\tt TE}[\![E_3]\!];\\
t &  = &  {\sf Ap_3} \; ({\sf Store},\;t_1,\;t_2,\;t_3) )
\end{array}
\end{array}$ \\
}

\noindent
\mbox{where {\small ${\sf Store}$} is a standard function defined in Kid} 
(see Section \ref{standard} ).\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TS}[\![ E_1.{\sf cons\_1} = E_2 ]\!] & = &
( \begin{array}[t]{lll}
t_1 & = & {\tt TE}[\![ E_1]\!];\\
t_2 & = &  {\tt TE}[\![E_2]\!];\\
t & = & {\sf List\_case}\;(t_1, \; \{\; {\sf Store\_error} \; {\sf In} \; () \},
\{ \; {\sf Cons\_store\_1} \; (t_1, \; t_2) \; {\sf In} \; () \; \} \; )\;) 
\end{array}
\end{array}$ \\
}

\noindent
Similarly for {\sf cons\_2}.


\subsubsection*{TB: Id$^{-}$ Bindings $\longrightarrow$ list (Kid Binding)}  

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TB}[\![ (P_1,\cdots, P_n)= X  ]\!] & = &
( \mv{t_n} = {\sf Detuple_n} \; (X);\\
 & &\;\;{\tt TB}[\![ P_1 = t_1 ]\!];\\
& & \;\;\;\;\vdots\\
& &\;\;{\tt TB}[\![ P_n = t_n ]\!] \; )\\
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TB}[\![ (P_1 \; : \; P_2) = X ]\!] & = & (
t_1,\;t_2  =  {\sf List\_case_2}\;(X, \; (\;{\sf Error}, \; {\sf Error}\;) 
,\;( {\sf Cons\_1} \;(X),\; {\sf Cons\_2}\;(X) )\;);\\
& &\;\;{\tt TB}[\![P_1 = t_1 ]\!];\\
& &\;\;{\tt TB}[\![P_2 = t_2 ]\!] )
\end{array}\\$
}

\blank
\noindent
{\small
$ \begin{array}{lll}
{\tt TB}[\![ Y = X ]\!] & = & (Y = X)
\end{array}$
}\\

\blank
\noindent
{\small
$ \begin{array}{lll}
{\tt TB}[\![ {\sf Next} \; Y = X ]\!] & = & (next(Y)  = X)
\end{array}$
}


\subsubsection*{TO: Id$^{-}$ Operator $\longrightarrow$ Kid Operator}  

\blank
\noindent
{\small
${\tt TO}[\![ U\!O\!P ]\!]= \mbox{ the corresponding  Kid } P\!F1   $
}

\blank
\noindent
{\small
${\tt TO}[\![ B\!O\!P]\!]= \mbox{ the corresponding  Kid } P\!F2  $\\
}

\noindent
The Kid operator corresponding to Id$^-$ ``{\sf :}" is {\small {\sf Cons}}
and for ``{\sf ==}'' is {\small {\sf Equal?}}.

%\pagebreak


\subsection{Definition of Standard Functions}
\label{standard}
In our translation from Id$^-$ to Kid we have introduced two new functions
{\small ${\sf Select}$} and {\small ${\sf Store}$}.
These are not primitive operators in Kid, therefore we give their definitions. Similarly we give 
a definition for {\small ${\sf Make\_1D\_array}$}.
For the sake of brevity we give these definitions in Id$^-$.
These definitions
and {\small ${\sf Make\_1D\_array}$} can be written as follows

\blank

\beginid

\null

   Make_1D_array = { Fun b f = { (l,u) = b ;
                                  a = I_array b;
                                  i = l;
                                  d = { While i $\leq$ u  do
                                         a[i] = f i;
                                         Next i = i+1
                                        Finally () }
                                  In a } }
\null
\endid
Like lists we are treating I-arrays and functional
arrays as the same type. However, 
functional arrays have a different degree of polymorphism than
{\small {\sf I\_nD\_array}}. We are ignoring these subtle issues in the above
translation.


\beginid
\null
   Select = { Fun x i = { (l,u) =  1D_Bounds x;
                          In 
                            If (i > u Or i < l)  then
                                              Error 
                                                 else
                                              P_1D_select x i } }

\null

   Store = { Fun x i y = { (l,u) =  1D_Bounds x;
                            In 
                              If (i > u Or i < l)  then
                                              { Store_error In () }
                                                   else
                                              { P_1D_store x i y In () } } }
\null
\endid

\noindent
The above Id$^-$ definitions can be translated into Kid by adding the following rules:\\

{\small
\noindent
${\tt TE}[\![ {\sf P\_nD\_select} \; x \; i ]\!]= {\sf P\_nD\_select} \; (x, \; i) $

\blank
\noindent
${\tt TS}[\![ {\sf P\_nD\_store} \; x \; i \; y]\!]= {\sf P\_nD\_store} \; (x, \; i, \; y)$

\blank
\noindent
${\tt TE}[\![ {\sf Error}]\!]= {\sf Error}$

\blank
\noindent
${\tt TE}[\![ {\sf Store\_error}]\!]= {\sf Store\_error}$
}



\subsection{Pattern Matching: Elimination of Complex Patterns}
\label{pattern}
Pattern matching in Id follows a different philosophy than
other functional languages such as Miranda and Haskell. In both
these languages clauses in patterns are examined from top to
bottom and patterns in a clause are examined from left to right.
Within the limitations of the above rule, pattern matching does
not force the evaluation of a pattern whose type is irrefutable
(tuples are examples of irrefutable patterns) \cite{Peyton-Jones87}.
Miranda in addition allows repeated occurrences of a variable
in a clause.\\

Id pattern matching is designed to be order-insensitive and
is maximally non-strict for sequential implementations. In
Id, patterns must not overlap to allow order-insensitivity.
Id also does not permit  repeated variables.  \\

Determination of which variables are necessary to evaluate
to resolve patterns is quite tricky as illustrated by 
the following example (due to Lennart Augustsson): 

\beginid
\null

    { Case (x, y, z) of
       |   (1, 0, w) = 1
       |   (0, w, 1) = 2
       |   (w, 1, 0) = 3 }
\null
\endid

First of all notice that the patterns are non-overlapping,
i.e., only one can be true for a given {\cf x}, {\cf y} and
{\cf z}. Second,
notice that top-to-bottom and left-to-right rule will
evaluate {\cf x} and then evaluate {\cf y} or {\cf z} depending upon the
value of {\cf x}. Thus,
if {\cf x} does not terminate no answer will ever be produced.
Notice if {\cf y = 1} and {\cf z = 0} one could demand the answer {\cf 3}
regardless of the {\cf x}. Traversal of patterns in a different
order will force evaluation of different variable.\\

Id pattern matching rules will force the evaluation
of all three variables in this example because no unique sequential 
order exists. (In Miranda and Haskell, all three 
variables will be evaluated only
if {\cf y} turns out to be {\cf 1} or {\cf z} turns out to be
{\cf 0}). \\

Now we informally describe a simplified version of the
pattern matching  algorithm used by the Id compiler \cite{Nikhil88a}.
For Id$^-$ we take into consideration lists and tuples only.
In the following we describe various cases that  arise during pattern
matching. \\

The signature of the pattern matching function is
\begin{center}
${\tt PM :}$  Case\_expression 
$\;\;\; \longrightarrow \;\;\;$ Kid  Expression
\end{center}
where Case-expression is defined as follows
\[ \begin{array}{lll}
\mbox{Case\_expression} & ::= & \{  {\sf Case} \; \mbox{SE} \; {\sf of} \;
\mbox{[ $\mid$ Clause]$^*$} \} \\
\mbox{Clause} & ::= & \mbox{P = Kid\_Expression} \\
\mbox{P} & ::= & {\sf Nil} \mid \mbox{Variable} \mid {\sf ()} \mid
\mbox{(P, P)} \mid  \mbox{(P, P, P)} \mid \cdots \mid  \mbox{(P : P)} \\
\mbox{SE} & ::= & {\sf ()} \mid \mbox{(Variable, $\cdots$, Variable )}
\end{array} \]

\noindent
If the pattern is a variable, say ``{\small $X$}'', then
``{\small $X$}'' is equivalent to ``({\small $X$})''.\\

As was stated earlier, no scope analysis of variable names
is required for the translation from Id to Kid. Thus, we will not
assume that all bound variable names are unique in the Kid program
that is generated by the translation process.

\subsection*{Variable rule}
The column of  patterns corresponding to a case variable consists  only   of  variables. \\

{\small
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}, & X_i, &  \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}, & Y_1, & \mv{P1_{i+1,n}}) & = E_1 \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\; \;\;\mid & (\mv{Pm_{1,i-1}}, & Y_m, & \mv{Pm_{i+1,n}}) & = E_m  \} ]\!] =
\end{array}\\
\\
\hspace{1cm}{
\{ \begin{array}[t]{l}
t  =  X_i;\\
t_f  =  {\tt PM}[\![
\begin{array}[t]{llll}
\{ {\sf Case} & (\mv{X_{1,i-1}},\! &\! \mv{X_{i+1,n}} ) & {\sf of} \\
\;\; \;\;\mid & (\mv{P1_{1,i-1}},\! &\! \mv{P1_{i+1,n}}) & = E_1[t/Y_1]_B \\ 
\multicolumn{3}{c}{ \vdots} \\
\;\; \;\;\mid & (\mv{Pm_{1,i-1}},\! & \! \mv{Pm_{i+1,n}}) & = E_m[t/Y_m]_B  \} ]\!]
\end{array}\\
\multicolumn{1}{l}{\;\; {\sf In} \; t_f \; \}}
\end{array}}
\end{array}$\\
}

\noindent
Note that meta-variables $Y_1 \cdots Y_m$ may be distinct.

\pagebreak

\subsection*{Irrefutable pattern rule}
The column of patterns corresponding to a case variable consists
of at  least one tuple and zero or more variables. 
Without loss of generality in the following
rule we assume the tuple to  be a 2-tuple.\\

{\small
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & X_i\;, & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & Y_1\;,& \mv{P1_{i+1,n}} ) & = E_1 \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & Y_k\;,& \mv{Pk_{i+1,n}} ) & = E_k \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  (Yl_1 \;{\sf ,}\; Yl_2) \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & (Ym_1 \;{\sf ,} \; Ym_2) \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] = 
\end{array}  \\
\\
\hspace{1cm}{\begin{array}[t]{lll}
\{ t_1,t_2 & = & {\sf Detuple_2} \; (X_i);\\
\;\; t & = & X_i;\\
\;\;t_f & = & {\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & t_1 \;, & t_2 \; , & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & t_{1,1}\;,& t_{1,2}\;,& \mv{P1_{i+1,n}} ) & = E_1 [t / Y_1]_B \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & t_{k,1}\;,& t_{k,2}\;,& \mv{Pk_{i+1,n}} ) & = E_k [t / Y_k ]_B \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  Yl_1 \;,&  Yl_2 \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & Ym_1 \;, & \; Ym_2 \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] 
\end{array}  \\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; t_f  \} } 
\end{array}}
\end{array}$}

\newpage

\subsection*{Refutable pattern rule}
The column of patterns corresponding to a case variable consists of only
{\small ${\sf Nil}$}'s and {\small ($Y_1 \; {\sf :} \; Y_2$)'}s.\\ 


{\small
\blank
\noindent
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{lllll}
\{ {\sf Case} & (\mv{X_{1,i-1}}\;, & X_i\;, & \mv{X_{i+1,n}} ) & {\sf of} \\
\;\;\;\; \mid & (\mv{P1_{1,i-1}}\;, & {\sf Nil}\;,& \mv{P1_{i+1,n}} ) & = E_1 \\
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & {\sf Nil}\;,& \mv{Pk_{i+1,n}} ) & = E_k \\
\;\;\;\; \mid & (\mv{Pl_{l,i-1}}\; , &  Yl_1 \;{\sf :}\; Yl_2 \; , & \mv{Pl_{i+1,n}} ) & = E_l  \\ 
\multicolumn{5}{c}{ \vdots} \\
\;\;\;\; \mid & (\mv{Pm_{1,i-1}}\; , & Ym_1 \;{\sf :} \; Ym_2 \; , & \mv{Pm_{i+1,n}} ) & = E_m \}]\!] = 
\end{array}  \\
\\
 \hspace{1cm}{\begin{array}[t]{lll}
 {\sf List\_case} & (X_i,  &  \\
\;\;\;\;  &  & 
	{\tt PM}[\![  \begin{array}[t]{llll} \{ {\sf Case} &
	(\mv{X_{1,i-1}}\; , &  \mv{X_{i+1,n}} ) & {\sf of} \\
        \;\;\;\; \mid & (\mv{P1_{1,i-1}}\; , & \mv{P1_{i+1,n}} ) & = E_1 \\ 
	\multicolumn{4}{c}{ \vdots} \\
        \;\;\;\; \mid & (\mv{Pk_{1,i-1}}\;, & \mv{Pk_{i+1,n}} ) & = E_k \} ]\!],
	\end{array}\\
\\
\;\;\;\;  &   &   \{ \begin{array}[t]{l}
         t_h,t_t = {\sf Cons\_1}\;(X_i),\; {\sf Cons\_2} \; (X_i); \\
	 t_f= {\tt PM}[\![  \begin{array}[t]{llllll} \{ {\sf Case} &
	(t_h \;,& t_t\;,  & \mv{X_{1,i-1}}\;, &  \mv{X_{i+1,n}}) & {\sf of} \\
	\;\;\;\; \mid & (Yl_1 \;, & Yl_2\;, &  \mv{Pl_{1,i-1}}\;, & \mv{Pl_{i+1,n}} ) & = E_l \\ 
	\multicolumn{6}{c}{ \vdots} \\
	\;\;\;\; \mid & (Ym_1 \;, & Ym_2\;, &  \mv{Pm_{1,i-1}}\;, & \mv{Pm_{i+1,n}} ) & = E_m  \} ]\!] 
	\end{array}\\
         \;\;\; {\sf In} \; t_f \} \;)
         \end{array} 
\end{array} }  \\
\end{array}$
} \\

\noindent
Note that if the case expression is not exhaustive then 
an alternative that will raise a run-time error is generated.
As, for example:\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & Y_1 \; {\sf :} \; Y_2   & = E  \} ]\!]
\end{array} & = &  
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & Y_1 \; {\sf :} \; Y_2   & = E  \\
\;\; \;\;\mid & {\sf Nil}   & = {\sf Error} \}   ]\!]
\end{array}
\end{array}$ \\


\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & {\sf Nil}  & = E  \} ]\!]
\end{array} & = &  
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & X & {\sf of} \\
\;\; \;\;\mid & {\sf Nil}   & = E  \\
\;\; \;\;\mid & t_1 \; {\sf :} \; t_2   & = {\sf Error} \}  ]\!]
\end{array}
\end{array}$ \\
}



\subsection*{Mixed variable-refutable patterns}
The column of patterns corresponding to a case variable consists of
at least one refutable pattern. In such a  case each variable is replaced by
all the possible alternatives, as shown below:\\ 

{\small
\blank
$\begin{array}{l}
{\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (X_1, &   X_2, & X_3 & ) & {\sf of} \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  & Y_1 & ) &  = E_1 \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  &  Y_2 \;, & {\sf Nil} & ) & = E_2 \\
\;\;\;\; \mid & (Y_3 \; , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & =
E_3 \} ]\!] =
\end{array}   \\
\\
\hspace{1cm}{
\{ \begin{array}[t]{lll}
\mv{t_3} & = & \mv{X_3} ;\\
\;\; t_f & = & {\tt PM}[\![ \begin{array}[t]{llllll}
\{ {\sf Case} & (X_1, &   X_2, & X_3 & ) & {\sf of} \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  & {\sf Nil} & )  & = E_1[t_3 / Y_1 ]_B \\
\;\;\;\; \mid & ({\sf Nil} \;,& Y_{1,1} \; {\sf :} \; Y_{1,2} \; ,  &
t_{1,1} \; {\sf :} \; t_{1,2} & )  & = E_1[t_3 / Y_1 ]_B \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  &  {\sf Nil} \;, & {\sf Nil} & ) & = E_2[t_2 / Y_2 ]_B \\
\;\;\;\; \mid & (Y_{2,1} \; {\sf :} \; Y_{2,2} \; ,  & 
t_{2,1} \; {\sf :} \; t_{2,2} \; , & {\sf Nil} & ) & = E_2[t_2 / Y_2]_B \\
\;\;\;\; \mid & ({\sf Nil} \; , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & = E_3[t_1 / Y_3]_B \\
\;\;\;\; \mid & (t_{3,1} \; {\sf :} \; t_{3,2} \;  , & {\sf Nil} \; , & Y_{3,1} \; {\sf :} \; Y_{3,2} & ) & = E_3[t_1 / Y_3]_B \} ]\!] 
\end{array}  \\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \; t_f  \} } 
\end{array}}
\end{array}$
}\\

\blank
\noindent
This rule can be  applied only after checking that none of other rules 
apply. It should be noted that patterns can be tested in many different
orders, each giving rise to a correct program though non  necessarily
the same program. The above rules cover all legal cases.
If we ever get tuple and
list patterns in one column, the compiler will flag it as a type
violation.

\subsection*{Empty variable rule}

{\small
\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & () & {\sf of} \\
\;\; \;\;\mid & () & = E_1 \\ 
\multicolumn{3}{c}{ \vdots} \\
\;\; \;\;\mid & () & = E_m  \} ]\!]
\end{array} & = & {\bf \mbox{Compiler Error ``overlapping patterns" } } \\ 
\end{array}$\\

\blank
\noindent
$\begin{array}{lll}
{\tt PM}[\![ \begin{array}[t]{lll}
\{ {\sf Case} & () & {\sf of} \\
\;\; \;\;\mid & ()  & = E  \} ]\!]
\end{array} & = & E \\
\end{array}$ \\
}


\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,\;\mv{X_n})$ is sef if $F$ is bound to
a sef $\lambda$-abstraction and $\mv{X_n}$ are bound to sef's; 
\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}$;
\item[(7)]
Blocks ..........
\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_{opt}, 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{P-TAC: Parallel Three Address Code}
\subsection{P-TAC}
\label{ptac}
The syntax of P-TAC is given in Figure \ref{p-tac}.
{\small
\begin{figure}[htbp]
\centering{
\begin{tabular}{|l|} \hline
\\
$\begin{array}{lll}
U\!D\!F & \in & \mbox{User Defined Function}\\
G\!V & \in  & \mbox{Ground Value}\\
\end{array}$ \\
\\
$\begin{array}{llll}
Integer & ::= & {\sf {\sf 1}} \mid {\sf {\sf 2}} \mid \cdots \mid 
                                        {\sf \underline{n}} \mid \cdots & \\
Boolean & :: = & {\sf True} \mid {\sf False} & \\
Variable & ::= & x \mid y \mid z \mid \cdots \mid a \mid b \mid \cdots \mid 
f \mid \cdots \mid 
x_1 \mid x_2 \mid \cdots  & \\
M\!V_m & ::= & \underbrace{Variable, \cdots , Variable } \\
Label &::=& L \mid L1 \mid \cdots \mid L' \mid \cdots \\
P\!F1 & ::= & {\sf Negate} \mid {\sf Not} \mid {\sf Allocate} \\
P\!F2 & ::= & {\sf +} \mid {\sf -} \mid {\sf *}
\mid \cdots \mid {\sf Less} \mid {\sf Equal?} \mid {\sf P\_select} & \\
P\!F3 & ::= & {\sf Ack\_store} \\
U\!D\!F & ::=& F \mid G \mid \cdots &   \\
S\!E & ::= & Variable \mid U\!D\!F  \mid G\!V &  \\
S\!E_m & ::= & \underbrace{S\!E, \cdots, S\!E}_m & \\
G\!V & ::= & Integer \mid Boolean \mid {\sf ()} \mid Label \mid {\sf Error} \mid \top &\\
E_1 & ::=& S\!E \mid P\!F1 \; (S\!E) \mid P\!F2 \;(S\!E_2) 
\mid P\!F3 \; (S\!E_3) \mid
{\sf Ap_n} \; (S\!E_{n+1})  \\
& & \mid {\sf Dispatch_n} \; (S\!E , \underbrace{E , \cdots, E}_n) \mid 
{\sf WLoop_1} \; (S\!E_4) \mid {\sf FLoop_1} \; (S\!E_5) \mid Block \\
E_m & ::= & S\!E_m \mid  {\sf Ap_{n,m}} \; (S\!E_{n+1}) \mid
{\sf Dispatch_{n,m}} \; (S\!E , \underbrace{E_m , \cdots, E_m}_n) \\
& & \mid {\sf WLoop_m} \; (S\!E_{m+3}) \mid 
{\sf FLoop_m} \; (S\!E_{m+4}) \mid Block_m \\
Block_m & ::= & \{_{\sf m} \; [Statement;]^* \;\; {\sf In} \;S\!E_m \} &  \\
Statement &::= & Binding \mid Command \mid  {\sf Store\_Error} & \\
Command & ::= & {\sf P\_store} \; (S\!E_3) \mid \top_s \\
Binding &::= & M\!V_m = E_m & \\
\end{array} $\\
\\ \hline
\end{tabular}
}
\\
\caption{Grammar of P-TAC} \label{p-tac} 
\end{figure}
}
In P-TAC, I-structure Storage is modelled in greater detail which requires
the notion of Labels. All composite objects, that is, data structures and
closures are stored in I-structure store and assigned  unique labels,
which are treated as constants that can be substituted  freely.

\subsection{Rewrite rules of P-TAC}
\label{p-tacrules}
In the following $V$ stands for a ground value.

\subsection*{$\delta$ rules}
{\small
\[ \begin{array}{lcl}
+ \; (\underline{m}, \;  \underline{n}) & \reduce{\delta}{}
& \underline{+ (m,\;  n)} \\
& \vdots & 
\end{array} \]
}

\subsection*{Conditional rule}
{\small
\[ \begin{array}{lll}
\hspace{0.5cm}{\sf Dispatch_{n,m}} \; (\underline{i} , \;
\mv{E_{i-1}} , \; E_i, \; \mv{E_{i+1,n}})   &
\reduce{}{} & E_i 
\end{array} \]
}

\subsection*{I\_structure rules }
{\small
\[\begin{array}{lll}
{\sf Allocate} \;\;(\underline{n}) & \reduce{}{} & L
\end{array} \]
}
\noindent
where {\small $L$} is a brand new label.\\
{\small
\[ \begin{array}{l}
\frag{{\sf P\_store} \; (L, \; \underline{i},\; V)}
{ {\sf P\_select} \;(L, \; \underline{i}) \;\;\;
\reduce{}{}\;\;\; V }
\end{array} \]
}
{\small
\[ \begin{array}{l}
\frag{{\sf P\_store} \; (L, \; \underline{i},\; V)}
{ {\sf P\_store} \; (L,\;\underline{i}, \;V^{'})  \;\;
\reduce{}{}\;\; {\sf \top_s} }
\end{array} \]
}

\noindent
where {\small $V$}
is either an Integer or a Boolean or a Label or {\sf Error}.\\
\noindent
The following rules are the same as the corresponding rules
in Kid.

\subsection*{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{}{} \;\; 
({\tt RB}[\![E]\!]) \; [\mv{X_n}/\mv{Z_n} ] }\\
\end{array}\]
}

\noindent
A similar rule applies for $\underline{{\sf \lambda_{n,m}}}$.
 
\subsection*{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} \]  
}
{\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} \]
}

\subsection*{Multivariable rule}
{\small
\[\begin{array}{lll}
\mv{X_n} \;= \;\mv{Y_n} \;\;\reduce{}{} \;\; (X_1 = Y_1; \cdots X_n = Y_n) 
\end{array}\]
}

\subsection*{Substitution rules}
{\small
\[ \begin{array}{lll}
\frag{X = Y}{ X \reduce{}{} Y}\\ 
\frag{X = V}{ X \reduce{}{} V}
\end{array}\]
}
\noindent
where {\small $V$}
is either an Integer or a Boolean or a Label or {\sf Error}.\\

\subsection*{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} \]
} 

\subsection*{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}\]
} 

\section{Translation of Kid into P-TAC}
\label{pgltop-tac}

Prior to translating Kid to P-TAC, $\lambda$-lifting is 
performed. A Kid program after $\lambda$~-lifting only
contains closed $\lambda$-expressions. 
The translator, given a Kid program, produces the corresponding 
P-TAC program and a set, ``D" , of definitions.
The set D is initialized with constants  that are introduced
by the translator.

\subsection{Simple Kid Expressions} 

\blank
\noindent
{\small
$\begin{array}{ll}
{\tt TE}[\![X]\!] = X \;\; & \;\;
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{ll}
{\tt TE}[\![C]\!] = C 
\end{array}$ \\
}

\noindent
where {\small $C$} ranges over Integers and Booleans.\\

\blank
\noindent
{\small
$\begin{array}{ll}
{\tt TE}[\![{\sf Negate} \; (X) ]\!] = {\sf Negate} \; (X)  
\end{array}$ 
}\\

\noindent
The same holds for ${\sf Not}$. \\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf +}\; (X, \; Y) ]\!]  & = & {\sf +} \; (X, \; Y)
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf WLoop_m}\; (P, \; B, \; \mv{X_m}, \; X_b) ]\!]  & = & {\sf WLoop_m}\; (P, \; B, \; \mv{X_m}, \; X_b)
\end{array}$\\
}

\noindent
The same holds for FLoop.\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Bool\_case_m} \; (X, \;  E_1, \; E_2 ) ]\!] & = &
\{_{\sf m}\; \begin{array}[t]{lll}
 t & = & BooltoInt \; (X); \\
 \mv{t_m} & = & {\sf Dispatch_{2,m}} \; (t,\; E_1, \; E_2);\\ 
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_m} \}}
\end{array}
\end{array}$
}\\

\noindent
$BooltoInt$ is a coercion function
which converts {\small {\sf True}} to {\small {\sf 0}} and {\small {\sf False}}
to {\small {\sf 1}}. \\


\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ \{_{\sf m} \; X_1 = E_1;\; \cdots \; X_n = E_n;\;
                S_1;\; \cdots \; S_m \;  {\sf In} \;\mv{Y_m} \; \}]\!] & = &
\{_{\sf m} \; \begin{array}[t]{lll}
X_1 & = & {\tt TE}[\![E_1]\!];\\
\multicolumn{3}{l}{ \;\;\;\vdots}\\
X_n & = &  {\tt TE}[\![E_n]\!];\\
\multicolumn{3}{l}{ \;\; {\tt TS}[\![S_1]\!]; }\\
\multicolumn{3}{l}{ \;\;\;\vdots}\\
\multicolumn{3}{l}{ \;\; {\tt TS}[\![ S_m ]\!]; }\\
\multicolumn{3}{l}{ \;\;{\sf In}\;\;\mv{Y_m} \;  \} }
\end{array}
\end{array}$ \\
}

\subsection{Data Structure Representations}

There are usually several reasonable ways to represent each data structure
in terms of a P-TAC array. For each type we present one representation,
though not necessarily the most efficient one.
We have included a  ``type'' tag field for all composite objects, even though
it  is not needed by the P-TAC interpreter since
Id is a statically typed language.  We might need types information
for other reasons, such as, garbage collection,
and printing  values in a partially executed program. \\

\subsection*{Tuples}
All n-tuple data types may be represented as follows:

\illustration{tuple}{1.5in}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Make\_tuple_n} \; (\mv{X_n}) ]\!] &  = &
\begin{array}[t]{l}
\{ t = {\sf Allocate} \; (\underline{n+1});\\
\; \; {\sf P\_store} \;  (t, \; {\sf Type}, \; ``n\_tuple"); \\
\; \; {\sf P\_store} \; ( t, \; 1 ,\; X_1); \\
\;\;\; \vdots \\
\;\; {\sf P\_store} \; (t, \; \underline{n}, \; X_n); \\
\;\;\;\; {\sf In} \;  t \}
\end{array}
\end{array}$
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Detuple_m} \; (X) ]\!]  & = & \{_{\sf m}
\begin{array}[t]{lll}
t_1 & = &  {\sf P\_select} \; ( X , 1) ;\\
\multicolumn{3}{l}{\;\;\;\; \vdots }\\
t_m & = & {\sf P\_select} \; (X, \underline{m}) ;\\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_m} \}}
\end{array}
\end{array}$ 
}

\pagebreak

\subsection*{1D-Arrays}
1D-arrays ``${\sf Array} \;(l,u)$'' may be represented as  follows:

\illustration{array}{2.5in}

\noindent
The constant definition ${\sf Headersize}   =  2$ should be included in the set ``D''.


\blank
\noindent
{\small
$\begin{array}{ll}
{\tt TE}[\![{\sf nD\_Bounds} \; (X) ]\!] = {\sf P\_select} \; (X,\;{\sf Bounds})   
\end{array}$ \\
}



\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE} [\![  {\sf I\_array} \; (X) ]\!] & = &
\{ \begin{array}[t]{lll}
l & = & {\sf P\_select} \; ( X, \; {\sf Lower}); \\
u & = & {\sf P\_select} \; (X, \; {\sf Upper}); \\
s & = & {\sf -} \;(u,\;  l);\\
size & = & {\sf +}\;( s,\;  3); \\
t & = & {\sf Allocate} \; (size); \\
\multicolumn{3}{l}{ {\sf P\_store } \; (t, \; {\sf Type}, \; ``Array"); }\\
\multicolumn{3}{l}{ {\sf P\_store } \; (t, \; {\sf Bounds}, \; X); } \\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; t   \} }
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf P\_1D\_select}  \;(X_1, \; X_2 ) ]\!] &  = &
\{ \begin{array}[t]{lll}
t_b & = & {\sf P\_select}  \;(X_1, \; {\sf Bounds} );\\
l & = & {\sf P\_select}  \;(t_b, \; {\sf Lower} );\\
t_1 & = & {\sf -} \;(X_2,\;l);\\
t_2 & = & {\sf +} \;(t_1,\;{\sf Headersize});\\
t & = & {\sf P\_select}  \;(X_1, \; t_2 )\\
\multicolumn{3}{l}{\;\;\; {\sf In} \;  t \}}
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf P\_1D\_store}  \;(X_1, \; X_2,\;X_3 ) ]\!] &  = &
\{ \begin{array}[t]{lll}
t_b & = & {\sf P\_select}  \;(X_1, \; {\sf Bounds} );\\
l & = & {\sf P\_select}  \;(t_b, \; {\sf Lower} );\\
t_1 & = & {\sf -} \;(X_2,\;l);\\
t_2 & = & {\sf +} \;(t_1,\;{\sf Headersize});\\
t & = & {\sf P\_store}  \;(X_1, \; t_2,\;X_3 ) \\ 
\multicolumn{3}{l}{\;\;\; {\sf In} \;  t \} }
\end{array}
\end{array}$\\
}

\noindent
A representation that will be more efficient for computing the
slot address may want to store $l$ and $u$ values redundantly in
two additional fields.

\subsection*{2D-Arrays}

The translation given below assumes that the matrix is stored in the row
major order.  The following constant definitions should be included
in the set ``D''.

\blank
\noindent
\[ \begin{array}{llllll}
{\sf First\_dim} & = & 1 & {\sf Second\_dim} & = & 2 \\
{\sf First\_index} & = & 1 & {\sf Second\_index} & = & 2 
\end{array} \]

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE} [\![  {\sf I\_2D\_array} \; (X) ]\!] & = &
\{ \begin{array}[t]{lll}
d_1 & = & {\sf P\_select} \; ( X, \; {\sf First\_dim}); \\
d_2 & = & {\sf P\_select} \; ( X, \; {\sf Second\_dim}); \\
l_1 & = & {\sf P\_select} \; ( d_1, \; {\sf Lower}); \\
u_1 & = & {\sf P\_select} \; (d_1, \; {\sf Upper}); \\
l_2 & = & {\sf P\_select} \; ( d_2, \; {\sf Lower}); \\
u_2 & = & {\sf P\_select} \; (d_2, \; {\sf Upper}); \\
s_1 & = & {\sf -} \;( u_1,\;  l_1);\\
s_2 & = &  {\sf -} \;(u_2,\;  l_2);\\
s_1' & = & {\sf +}\;(s_1,\;  1);\\
s_2' & = &  {\sf +} \;(s_2, \;  1);\\
s & = &  {\sf *}\;(s_1',\;  s_2'); \\
size & = &  {\sf +}\;(s,\;  {\sf Headersize}); \\
t & = & {\sf Allocate} \; (size); \\
\multicolumn{3}{l}{ {\sf P\_store } \; (t, \; {\sf Type}, \; ``Array"); }\\
\multicolumn{3}{l}{ {\sf P\_store } \; (t, \; {\sf Bounds}, \; X); } \\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; t   \} }
\end{array}
\end{array}$\\
}

\blank
\noindent
Translation for {\sf I\_nD\_array} can be given in a similar
fashion.

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf P\_2D\_select}  \;(X_1, \; X_2 ) ]\!] &  = &
\{ \begin{array}[t]{lll}
b & = & {\sf P\_select}\;(X_1,\;{\sf Bounds});\\
d_1 & = & {\sf P\_select}\;(b,\;{\sf First\_dim});\\
d_2 & = & {\sf P\_select}\;(b,\;{\sf Second\_dim});\\
l_1 & = & {\sf P\_select}\;(d_1,\;{\sf Lower});\\
u_1 & = & {\sf P\_select}\;(d_1,\;{\sf Upper});\\
l_2 & = & {\sf P\_select}\;(d_2,\;{\sf Lower});\\
u_2 & = & {\sf P\_select}\;(d_2,\;{\sf Upper});\\
r & = & {\sf - }\;(u_2,\;l_2);\\
r' & = & {\sf + }\;( r, \; 1);\\
i & = & {\sf P\_select}\;(X_2,\;{\sf First\_index});\\
j & = & {\sf P\_select}\;(X_2,\;{\sf Second\_index});\\
i' & = & {\sf -} \; (i,\;l_1);\\
j' & = & {\sf -} \; (j,\;l_2);\\
o & = & {\sf *} \; (i',\;r');\\
o' & = & {\sf +} \; (o,\;{\sf 1});\\
ad & = & {\sf +} \; (o,\;j');\\
ad' & = & {\sf +} \; (ad,\;{\sf Headersize});\\
t & = & {\sf P\_select}  \;(X_1, \;ad' )\\
\multicolumn{3}{l}{\;\;\; {\sf In} \;  t \} }
\end{array}
\end{array}$\\
}

\noindent
A similar rule applies for {\small ${\sf P\_2D\_store}$},
and higher dimensional arrays.

\subsection*{Lists} 
The list data type can be represented as  follows:

\illustration{list}{3in}

\noindent
It is often possible to store niladic constructors using
much less space by combining them with pointers. We won't discuss
such machine dependent representations in this paper. \\


\noindent
The following constant definitions should be included
in the set ``D''.

\blank
\noindent
\[ \begin{array}{lll}
{\sf Nil\_size}& = & 2\\
{\sf Cons\_size} & = & 4\\
{\sf Nil\_Tag} & = & 0\\ 
{\sf Cons\_Tag} & = & 1\\ 
\end{array} \]

\blank
\noindent
{\small
$ {\tt TE}[\![ {\sf Nil}  ]\!] = \begin{array}[t]{l}
\{  t = {\sf Allocate} \; ({\sf Nilsize});\\
 \;\; {\sf P\_store} \;  (t, \; {\sf Type}, \; ``List"); \\
 \; \; {\sf P\_store} \; (t,  \; {\sf Tag}, \; {\sf Nil\_Tag}); \\
\;\;\;\; {\sf In} \;  t \}
\end{array}$
}\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Open\_cons}  \;() ]\!] &  = &
\{ \begin{array}[t]{l}
t  =  {\sf Allocate} \; ({\sf Cons\_size});\\
{\sf P\_store} \;  (t, \; {\sf Type}, \; ``List"); \\
{\sf P\_store} \;  (t, \; {\sf Tag}, \; {\sf Cons\_Tag}); \\
\;\;\; {\sf In} \;  t \}
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Cons\_1} \; (X) ]\!] &  = &
 {\sf P\_select} \; (X,\;{\sf Hd})
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Cons\_2} \; (X) ]\!] &  = &
{\sf P\_select} \; (X,\;{\sf Tl})
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Cons} \; (X_1, X_2) ]\!] &  = &
\{ \begin{array}[t]{l}
t  =  {\sf Allocate} \; ({\sf Cons\_size});\\
{\sf P\_store} \;  (t, \; {\sf Type}, \; ``List"); \\
{\sf P\_store} \;  (t, \; {\sf Tag}, \; {\sf Cons\_Tag}); \\
{\sf P\_store} \; (t, \; {\sf Hd}, \; X_1); \\
{\sf P\_store} \; (t, \; {\sf Tl}, \; X_2); \\
\;\;\; {\sf In} \;  t \}
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TS}[\![ {\sf Cons\_store\_1} \; (X_1 , X_2)  ]\!]  & = & 
\begin{array}[t]{l}
 {\sf P\_store} \; ( X_1 , {\sf Hd}, X_2)   ;\\
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TS}[\![ {\sf Cons\_store\_2} \; (X_1 , X_2)  ]\!]  & = & 
\begin{array}[t]{l}
 {\sf P\_store} \; ( X_1 , {\sf Tl}, X_2)   ;\\
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf List\_case_m} \; (X, \;  E_1, \; E_2 ) ]\!] & = &
\{_{\sf m} \begin{array}[t]{lll}
 t & = & {\sf P\_select} \;(X, \; {\sf Tag});\\
 \mv{t_m} & = & {\sf Dispatch_{2,m}} \; (t,\; E_1, \; E_2);\\ 
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_m} \}}
\end{array}
\end{array}$
}\\

\subsection{Function Calls and Closures}

At the machine level, the  apply
operator checks if the arity of the function has been satisfied
or not, and in case the arity has not been satisfied, it stores  the 
argument in a data stucture called a closure.
There is great choice in representing  closures and associated 
function calling conventions.  In fact, a function can be compiled
using  several different calling conventions and the compiler can pick 
up the most appropriate one for a given application. As an illustration
we chose the following representation for the
closure data type:\\

\illustration{closure}{2in}

\noindent
The constant definition 
${\sf Closure\_size}  = 5$ should be  included in the set ``D''.

\blank
\noindent
We begin by describing a  procedure that builds a  closure given an old
closure and an argument.\\

\blank
\noindent
{\small
${\sf Make\_closure} = \underline{{\sf \lambda}} \; (cl, X)  \;\;  . \;\;
(\{ \begin{array}[t]{lll}
f & = & {\sf P\_select} \; (cl, \; {\sf Funcname}); \\
f_{fc} & = & {\sf P\_select} \; (cl, \; {\sf Fastcallname}); \\
n & = & {\sf P\_select} \; (cl, \; {\sf Arity}); \\
ch & = & {\sf P\_select} \; (cl, \; {\sf Chain}); \\
cl' & = & {\sf Allocate} \; ({\sf Closure\_size});\\
\multicolumn{3}{l}{ {\sf P\_store} \; (cl', \; {\sf Type}, \; ``Closure"); } \\
\multicolumn{3}{l}{{\sf P\_store} \; (cl', \; {\sf Functionname}, \; f); } \\
\multicolumn{3}{l}{ {\sf P\_store} \; (cl', \; {\sf Fastcallname},\;f_{fc});} \\
\multicolumn{3}{l}{ {\sf P\_store} \; (cl', \; {\sf Arity}, \; n');} \\
\multicolumn{3}{l}{ {\sf P\_store} \; (cl', \; {\sf Chain}, \; ch');} \\
n' & = & {\sf -}\;(n,\;1); \\ 
ch' & = & {\sf Ap_2} \;({\sf Arg\_chain} , \; X,\;ch);\\
\multicolumn{3}{l}{ \;\;\;{\sf In} \; cl' \} \; ) } 
\end{array}$\\
}

\noindent
where the function to build argument chains is defined as follows:\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\sf Arg\_chain} = \underline{ {\sf \lambda} }\; ( X, Xs)  &  . &
(\; \begin{array}[t]{l}
\{ xs' = {\sf Allocate} \;(2);\\
\; \; {\sf P\_store} \; (xs', {\sf Arg}, X);\\
\; \; {\sf P\_store} \; (xs', {\sf Rest}, Xs);\\
\;\;\;{\sf In} \; xs' \} \;)
\end{array}
\end{array}$\\
}

\noindent
The argument chain can be destructured using the following function:\\

\blank
\noindent
{\small
${\sf Args_n} = \underline{ {\sf \lambda} } \; (X)  \;\; . \;\;
(\{_{\sf n} \;  \begin{array}[t]{lll}
t_1 & = & {\sf P\_select} \; (X, \; Chain);\\ 
\;a_n & = & {\sf P\_select} \; (t_1, \; {\sf Arg});\\ 
\;t_2 & = & {\sf P\_select} \; (t_1, \; {\sf Rest});\\ 
\;a_{n-1} & = & {\sf P\_select} \; (t_2, \; {\sf Arg});\\ 
\;t_3 & = & {\sf P\_select} \; (t_2, \; {\sf Rest});\\ 
\multicolumn{3}{l}{ \;\;\;\; \vdots} \\
\;a_1 & = & {\sf P\_select} \; (t_{n-1}, \; {\sf Arg});\\
\multicolumn{3}{l}{ \;\;\;\; {\sf In} \;  \mv{a_n}  \} \; ) }  
\end{array}$ \\
}

\noindent
These three definitions must be included 
in the ``D'' set. \\

\noindent
Now we can give the translation for the apply operator.
As stated earlier, the apply basically checks to see
if the arity is satisfied and either makes a new closure or
calls {\small {\sf Ap}}.

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Apply} \; (F, \; X) ]\!]  & = & \{ \begin{array}[t]{lll}
n & = & {\sf P\_select} \; (F, \;  {\sf Arity});\\
fire_b & = & {\sf Equal?} \; (n,\;  1);\\
fire_i & = & BooltoInt(fire_b); \\
res & = & {\sf Dispatch_{2,2}} \; (fire_i, \\
& & \;\;\;\;\{\begin{array}[t]{lll}
fun & = & {\sf P\_select}\; (F ,  \;{\sf Functioname});\\
as & = & {\sf P\_select} \;(F,  \;{\sf Chain});\\
as' & = & {\sf Ap_2} \; ({\sf Arg\_chain}, \; X, \;as);\\
res' & = & {\sf Ap} \; (fun, \; as');\\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; res'   \}, }
\end{array}\\
&  &\;\;\;\; {\sf Ap_2} \; ({\sf Make\_closure}, \; F,\; X))\\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; res   \} }
\end{array}
\end{array}$\\
}

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf Ap_{n,m}} \; (F, \; \mv{X}) ]\!]  & = &\{_{\sf m} \; \begin{array}[t]{lll}
f' & = & {\sf P\_select} \; (F,  {\sf Fastcallname});\\
\mv{t_m} & = & {\sf Ap_{n,m}} \;(f',\mv{X} );\\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; \mv{t_m} \; \}}
\end{array}
\end{array}$\\
}

\noindent
The only thing that remains to be described is the creation of the
first closure for a function. It is built as a consequence of translating
a $\lambda$-expression.\\

\blank
\noindent
{\small
$\begin{array}{lll}
{\tt TE}[\![ {\sf \lambda_{n}}\;  (\mv{X_n}) \; . \; (E) ]\!]  & = &
\begin{array}[t]{l}
\{ cl = {\sf Allocate} \; ({\sf Closure\_size}); \\
 \;\; {\sf P\_store} \; (cl, \; {\sf Type}, \; ``Closure");\\
 \;\; {\sf P\_store} \; (cl, \; {\sf Functioname}, \; `T_c);\\
 \;\; {\sf P\_store} \; (cl, \; {\sf Fastcallname}, \; `T_{fc});\\
 \;\; {\sf P\_store} \; (cl, \; {\sf Arity}, \; \underline{n});\\
 \;\; {\sf P\_store} \; (cl, \; {\sf Chain}, \; ``End");\\
 \;\;\;\; {\sf In} \; cl \}
\end{array} 
\end{array}$\\
}

\noindent
The following two function definitions are included in the
set D.\\

\begin{center}
{\small
$\begin{array}{l}
 T_c =  {\sf \lambda_{1}} \;  (Xs) \;\; .\;\; 
\{ \begin{array}[t]{lll}
\mv{X_n} & = & {\sf Ap_{1,n}} \; ({\sf Args_n},\;  Xs);\\
\;\; t & = & {\tt TE}[\![E]\!]; \\
\multicolumn{3}{l}{\;\;\; {\sf In} \;  t  \} } 
\end{array}\\
T_{fc} = {\sf \lambda_{n}} \; (\mv{X_n}) \;\;  . \;\;  {\tt TE}[\![ E ]\!]
\end{array}$}
\end{center}

\noindent
{\small $`T_c$} indicates the name {\small $T_c$} and not the value associated
to $T_c$.  Note that {\small ${\tt TE}[\![E]\!]$} can  be computed  once
and shared between the curried aabd the fastcall version of the function.
The same translation rule applies for {\small ${\sf \underline{\lambda_{n}}}$}.\\

\section{Signals}
\label{signals}

Before introducing signals,
the P-TAC program is canonicalized, that is,
all blocks are flattened and variables and values are
substituted. Furthermore, dead code should be eliminated.
We  add signals only to non-strict combinators, 
and to combinators that produce side-effect, such as {\sf P\_store}.
The output of a strict operator can be interpreted as the signal that the
instruction has indeed fired.
We give the signal transformation using the translation functions
{\tt S}, {\tt SE} and {\tt SC}.
The transformation is applied also to each constant definition in
``D" . \\

\blank
\noindent
{\small
${\tt S}[\![ {\sf \lambda_{n,m}} \; (\mv{X_n}). \{_{\sf m}\; \begin{array}[t]{lll} 
Y_1 & = &  Se_1\\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_n & = &  Se_n \\
Y_{n+1} & = &  Nse_1 \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_{n+m} & = &  Nse_m \\
\multicolumn{3}{c}{C_1} \\
\multicolumn{3}{c}{ \vdots }\\
\multicolumn{3}{c}{C_k}\\
\multicolumn{3}{l}{ \;\;  \; {\sf In} \; \mv{R_m} \} ]\!]}
\end{array} =
\begin{array}[t]{l}
{\sf \lambda_{n,m+1}}\; (\mv{X_n})\;. \\
\hspace{0.2cm}{
( \{_{\sf m+1}\; \begin{array}[t]{lll}
Y_1 & = &  Se_1\\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_n & = &  Se_n \\
Y_{n+1}, \; S_1 & = &  {\tt SE}[\![Nse_1]\!] \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
Y_{n+m},\;S_m & = &  {\tt SE}[\![ Nse_m]\!] \\
S_{m+1} & = & {\tt SC}[\![ C_1]\!];  \\
\multicolumn{3}{l}{ \;\;\; \vdots }\\
S_{m+k} & = & {\tt SC}[\![ C_k]\!]; \\
S' & = & {\sf Sync_{m+k+i}} \; (Deadvariables, \; \mv{S_{m+k}} )    \\
\multicolumn{3}{l}{ \;\;\; {\sf In} \; \mv{R_m} ,\; S' \} ) }  
\end{array} }
\end{array}$\\
}

\noindent
Where $Se_i$ stands for an expression involving strict operators,
whilst $Nse_i$ stands for either an applicative or a 
loop expression. $Deadvariables$ 
are the parameters that are not being used in the body
of the function. \\

\blank
\noindent
{\small
${\tt SE}[\![ {\sf WLoop_{n}} \; (P,B,\mv{Y_n}, Y) ]\!] = 
{\sf WLoop_{n}'} \; (P,B,\mv{Y_n}, S_p, Y) $\\
}

\blank
\noindent
Where $S_p$ is the signal associated with the invocation of the
predicate. \\
 
\blank
\noindent
{\small
${\tt SE}[\![ {\sf Ap_{n,m}} \; (F,\;\mv{X_n}) ]\!] = 
{\sf Ap_{n,m+1}} \; (F,\;\mv{X_n}) $
}

\blank
\noindent
{\small
${\tt SC}[\![ {\sf P\_store} \; (X,\;I\;Z) ]\!] = 
 {\sf Ack\_store} \; (X,\;I\;Z) $\\
}

\blank
\noindent
Where ${\sf Ack\_store}$ is a new P-TAC function symbol of
arity 3, which generates a ${\sf Signal}$ when the store actually
takes place.\\

\noindent
The new rewrite rules are:

\blank 
\noindent
{\small
$\begin{array}{lll}
\\
\hspace{0.5cm}{\sf WLoop_n'} \; (P, \; B, \; \mv{X_n}, S, \; {\sf True}) & \reduce{}{} &
\{_{\sf n+1} \begin{array}[t]{lll}
 \mv{t_n}, S_b & = & {\sf Ap_{n,{n+1}}} \; (B, \;  \mv{X_n}) ;\\
  t_{p}, S_p & = & {\sf Ap_{n,2}} \; (P, \; \mv{t_n});\\
 S'         & = & {\sf Sync_3} \; (S, \; S_b, \; S_p) ; \\
\mv{t_n'}, S_l & = & {\sf WLoop_n'} \;(P,  \; B,   \; \mv{t_n}, \;S',\; t_{p})  \\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_n'} , \; S_l \} }
\end{array}
\\
\\
\hspace{0.5cm}{\sf WLoop_n'} \; (P, \; B, \;  \mv{X_n}, \; S, \; {\sf False}) & \reduce{}{} &
\mv{X_n}, \; S  
\end{array}$ \\
}

\blank
\noindent
{\small
$ \hspace{0.5cm}{\begin{array}{lll}
{\sf Ack\_store} \;( L ,\; \underline{i}, \; V) & \reduce{}{} &
\begin{array}[t]{l}
\{ t = {\sf Signal};\\
\; {\sf P\_store} \;( L, \; \underline{i}, \; V); \\
\;\;\; {\sf In} \; t \}
\end{array}
\end{array}}$ }

\blank
\noindent
{\small
$ \hspace{0.5cm}{\begin{array}{lll}
{\sf Sync_n} \;( \mv{V_n}) & \reduce{}{} & ()
\end{array}}
$} \\

\noindent
${\sf Sync}$  produces a void value when all the signals are received.
 

\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}

We would like to thank Shail Aditya for reading several earlier drafts of this
paper and suggesting changes for better readability.
This paper has benefitted a lot by informal discussions
with the members of Computation Structures Group.

\bibliography{idcompiler}
\bibliographystyle{abbrv}

\newpage

\tableofcontents

\vfill

\end{document}


%%%%%%%%%%%%%% JUNK
%%%%
{\small
\[\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{2cm}
\{ \begin{array}[t]{llll}
 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}}) \; . \; 
(\{_{\sf n-1} \; S \; {\sf In} \; \mv{Z_{n-1}} \}\;[\mv{x'_{n-1}}/\mv{X_{n-1}},\;Y_n/X_n]); \\
\mv{y_{n-1}'} & = & {\sf WLoop_{n-1}} \;(p, \; b, \; \mv{Y_{n-1}}, \; Y_p); \\
\multicolumn{3}{l}{{\sf In} \;\; Y_n' , Y_n \} }\\
\end{array} 
\end{array}} \] }\\


 ELIMINATING CONSTANTS
\beginid
\null
\null
          { x = 0;
            y = 5;
            t = a + b;
            If p(x) then
              { x1 = t;
                y  = x + 1;
               In
                 {While p(x1) do
                    Next y = x1 + 1;
                  Finally x1 + y } }
              else x + y }

\null
\endid
*********************************************
In the strategy for WNF:

%{\tt \cal{E}}[\![{\sf FLoop_n} \; ( U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf True})]\!] \; {\cal IS} \; {\cal FS} =
%{\tt \cal{E}}[\![ \{_{\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}
%\\
%\\
%{\tt \cal{E}}[\![{\sf FLoop_n} \; (U, \; D, \; B, \;  \mv{X_{n}}, \; {\sf False})]\!] \; {\cal IS} \; {\cal FS} =  \mv{X_{n}}  \\
%\\

%{\tt \cal{E}}\mean{{\sf Cons\_store\_1} \;(X,\; Y'  )}  \; {\cal IS} \; {\cal FS}=  \top_s  \hspace{1cm} 
%\mbox{if (lookup ($X$, ${\cal IS}$))} =
%{\sf Cons\_store\_1} \;(X,\;Y)  \\ 
%\\
%{\tt \cal{E}}\mean{{\sf Cons\_store\_2} \;(X,\; Y'  )}  \; {\cal IS} \; {\cal FS}=  \top_s   \hspace{1cm} 
%\mbox{if (lookup ($X$, ${\cal IS}$))} =
%{\sf Cons\_store\_2} \;(X,\;Y)  \\
\\
%\end{array}$
%$\begin{array}{l}

%{\tt \cal{E}}[\![{\sf nD\_store} \;(X, \; Y, \; Z') ]\!]  \; {\cal IS} \; {\cal FS}= \top_s    \hspace{1cm} 
%\mbox{if (lookup ($X$, ${\cal IS}$))} =
%{\sf P\_nD\_store}\;(X, \; Y, \; Z)\\ 



% Substitution
It should be
noted that in contextual rewriting, the statement above the line
must be in the context (lexical scope) of the expression below the
line.  This raises some subtle free variable capture possibilities
in case of function application.


%EQUIVALENCE
\begin{tightlist}
\item[(i)]
$\alpha$-equivalence;
\item[(ii)]
tree-equivalence;
\item[(iii)]
observational-equivalence and congruence.
\end{tightlist}



%\begin{fact}
%The blow-up rule, $\reduce{blw}{}$, and the I-fetch rule,
%$\reduce{I\mbox{-}f}{}$, are the only interfering rules in Kid.
%\end{fact}
%
%The {\em blow-up} rule can 
%invalidate the precondition of any rule.
%The {\em I-fetch} rule interferes with itself as  shown
%by the example below:
%\[ \begin{array}{l}
%\{{\sf I\mbox{-}store}\; l\; 1; \\
%\;\;{\sf I\mbox{-}store}\; l\; 2; \\
%\;\;x = \underbrace{\underbrace{{\sf I\mbox{-}fetch}\;l}_{\rho_1}}_{\rho_2};\\
%\;\;\;{\sf in}\; x \}
%\end{array} \]
%The subterm ${\sf I\mbox{-}fetch}\;l$ matches the (LHS) of
%the {\em I-fetch} rule.  However, the precondition for the
%rule can be  satisfied by either the subterm ({\sf I-store} $l$ $1$)
%or by the subterm  ({\sf I-store} $l$ $2$). Thus, redexes
%$\rho_1$ and $\rho_2$, shown above, do overlap and, consequently,
%the {\em I-fetch} rule interferes with itself.
%
%\vspace{-0.2cm}
%\begin{proof}
%We want to show that $\forall$ (canonical) $M$, $M_1$, $M_2$ $\in$ $A$,
%and $\forall$ $i$-rule, $j$-rule $\in\;R_{P\mbox{-}TAC}$,
%the following holds:
%\[ M \reduce{i}{} M_1 \;\; \wedge\;\;
%M \reduce{j}{} M_2 \;\; \Longrightarrow \;\;
%\exists M_3 \mbox{ such that }\]
%\[ M_1 \reduce{}{0/1}
%M_3 \;\; \wedge \;\;
%M_2 \reduce{}{0/1} M_3 \]
%\begin{enumerate}
%\item
%({\em Non-interfering rules}) Suppose the $i$-redex does not 
%interfere with the $j$-redex. By inspecting the non-interfering
%rules of $R_{P\mbox{-}TAC}$, and the structure of canonical terms, we can see 
%that the  $i$-redex and $j$-redex have to be disjoint.  
%By the definition of interference,
%the $i$-reduction (analogously, the $j$-reduction)
%cannot invalidate the precondition of the $j$-redex ($i$-redex).
%Therefore, the $i$ and $j$ reductions commute. 
%\item
%({\em Interfering rules}) 
%\begin{enumerate}
%\item[2.1]
%Let $i$-rule be $\reduce{blw}{}$ and $j$-rule be different from
%$\reduce{blw}{}$. 
%Since only the {\em blow-up} rule  can destroy the
%precondition for the $blw$-redex, in the following 
%diagram $M_2$ is still a $blw$-redex. 
%\[ \begin{array}{l}
%\hspace{0.7cm}\mbox{\small $M$}\\
%\hspace{0.3cm} \dlreduce{blw}{} \;\;
%\drreduce{j}{} \\
%\;\top \; \lreduce{blw}{}\;  \mbox{\small $M_2$}
%\end{array} \]
%
%\item[2.2]
%Let both $i$-rule and $j$-rule be $\reduce{blw}{}$. Then,
%\vspace{-0.2cm}
%\[ \begin{array}{l}
%\hspace{0.7cm}\mbox{\small $M$}\\
%\\
%\hspace{0.7cm}\mbox{\small $\top$}
%\end{array} \]
%\item[2.3]
%Let both $i$-rule and $j$-rule be $\reduce{I\mbox{-}f}{}$. Then $M$
%is a $blw$-redex which can not be destroyed by
%the {\em I-fetch} reductions.
%Hence $M_1$ and $M_2$ are also $blw$-redexes.
%\[ \begin{array}{l}
%\hspace{0.7cm}\mbox{\small $M$}\\
%\hspace{0.3cm} \dlreduce{I\mbox{-}f}{} \;\; \drreduce{I\mbox{-}f}{} \\
%\;\mbox{\small $M_1$}\hspace{0.5cm}\mbox{\small $M_2$}\\
%\;\;\;\drreduce{}{} \;\;\; \dlreduce{}{}\\
%\hspace{0.6cm} \top
%\end{array} \]
%\end{enumerate}
%\end{enumerate}
%\end{proof}
%

%\begin{definition}[WNF]
%An expression E is in Weak Normal Form iff
%\begin{tightlist}
%\item[(i)]
%If E is a block then all RHS expressions are not a redex (note that the RHS can't be a block);
%\item[(ii)]
%If E is not a block then E is not a redex.
%\end{tightlist}
%\end{definition}
