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

%\input /jj/ariola/macros/prelude
\input prelude

\begin{document}

\title{Compilation of Id$^-$:  A Subset of Id}

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

\date{November 1, 1990}

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

\section{Introduction}

\begin{figure}[htbp]
%%\vspace{0.5in}
\illustration{id}
%%\illustrationx{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
\null
        {: e || x <- xs ; y <- ys}

\null
\null
\endid
A typical translation of this list-comprehension is given in terms of nested
map-list operations followed by a list flattening operation. In Id we make 
use of ``open lists'' 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}  \\

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}

\subsection{Kid}
\label{pgl}
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 in the operational semantics of Kid.
The syntax of Kid is given in Figure \ref{pglsyntax}.
Every expression, except a block  or $\lambda$-expression,
consists of
a combinator followed by the corresponding number of arguments.
The translation from Id$^{-}$ to Kid also has the flavor of turning
an applicative TRS into a functional one. \\

An important feature of Kid is the concept of 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.
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 they are useful in  expressing some optimizations. 
Thus, in Kid a binding has the form {\small $MV = E$}, where  $MV$ stands for multiple
variable. 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 combinator {\small ``${\sf Apply}$"} appears
as a {\small $P\!F2_1$} in the grammar
because all Id$^-$ procedures return only one result. 
We also use subscripted combinators to express a family
of combinators. 
For example, {\small ${\sf Make\_tuple_n}$} stands for
{\small ${\sf Make\_tuple_2}$},
{\small ${\sf Make\_tuple_3}$}, \etc .
Subscripts in a combinator do not necessarily represent the number of
values to be returned by the application of the combinator. \\

We will use the following conventions to minimize the use of subscripts.

{\small 
\[ \begin{array}{lll}
{\sf \{}  & \mbox{is the same as} & {\sf \{_1  }\\
{\sf Bool\_case} & \mbox{is the same as} & {\sf Bool\_case_1}\\
{\sf List\_case} & \mbox{is the same as} & {\sf List\_case_1}\\
{\sf WLoop} & \mbox{is the same as} & {\sf WLoop_1}\\
{\sf FLoop} & \mbox{is the same as} & {\sf FLoop_1}\\
{\sf Ap_n} & \mbox{is the same as} & {\sf Ap_{n,1}}\\
{\sf \lambda_n} & \mbox{is the same as} & {\sf \lambda_{n,1}}\\
\end{array}\]
}


\subsection{The Rewrite Rules of Kid }
\label{rules}

We now present a set of rewrite rules, $R_{Kid}$,
to define the operational semantics for Kid.
$R_{Kid}$ is a Contextual Rewrite System described in \cite{Zena90a}.
We assume that a primitive
function is only applied 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 & Variable \mbox{ and } Constant \\
C & \in & Constant\\
S_i, \; SS_i & \in & Statement \\
S,\;S' & \in & [Statement]^* \\
E_i & \in & Expression\\
\end{array}
\]
}

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. To avoid these problems, we will
assume that all bound variables in a Kid program have been assigned
unique names to begin with. When the possibility of free variable capture
arises during rewriting, we will rename  all bound variables of an 
expression to completely new variables explicitly,
by applying the function ${\tt RB}$  to the expression. 
For example,
\[ \begin{array}{l}
{\tt RB} \; [\![ \{ x =  {\sf +} \; (a, \; 1) \; {\sf In} \; x \} ]\!] =
\{ x' =  {\sf +} \; (a, \; 1) \; {\sf In} \; x' \}\\
\end{array} \]

The notation {\small $E \; [Y/X]$ }
means the substitution of $Y$ for $X$ in $E$. Usually
this implies  avoiding capture of free variables.
However, due to our assumption that all variables occurring in a term to be
reduced are unique, {\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
%\linebreak
~{\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])$}.\\

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

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

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

{\small
\[\begin{array}{l}
\frag{X = {\sf Nil}}  
{{\sf List\_case_m} \; (X,\; 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}\]
}

\subsection*{Arity Detection rule}
{\small
\[\frag{F = \lambda_n (\mv{Z_n}).E} 
{{\sf Apply}\;(F, \; X)   \;\; \reduce{}{} \;\;
{\sf Apply_1}\;(F, \; \underline{n},\; X) } 
\]
}

{\small
\[\frag{F = \lambda (Z).E} 
{{\sf Apply}\;(F, \; X)   \;\; \reduce{}{} \;\;
{\sf Ap}\;(F, \; X) } 
\]
}

{\small
\[\frag{F_i = {\sf Apply_i}\;(F, \;\underline{n},\; X_i) \;\; \;\; i < (n\!-\!1) }
{{\sf Apply}\;(F_i, \; \mv{X_{i+1}}) \;\; \reduce{}{} \;\;
{\sf Apply_{i+1}}\; (F, \; \underline{n},\;\mv{X_{i+1}})} 
\] }

{\small
\[\frag{F_{n\!-\!1} = {\sf Apply_{n\!-\!1}}\;(F, \;\underline{n},\; \mv{X_{n\!-\!1}}) \;\;  \;\; i = (n\!-\!1) }
{{\sf Apply}\;(F_{n\!-\!1}, \; \mv{X_{n}}) \;\; \reduce{}{} \;\;
{\sf Ap}\; (F, \; \mv{X_n})} \\
\] }


\noindent
\hspace{0.5cm}{Similar rules apply for $\underline{{\sf \lambda_n}}$.}


\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
\hspace{0.5cm}{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} \]
}

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

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

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

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


\subsection*{Array rules}
{\small 
\[\begin{array}{l}
\frag{X={\sf I\_nD\_array} \; (X_b)}
{{\sf nD\_Bounds}\; (X) \;\; \reduce{}{}\;\;X_b}
\end{array} \]
}

\blank
\noindent
{\small
\[\frag{{\sf P\_nD\_store} \; (X, \; Y,\; Z) }
{{\sf P\_nD\_select} \;(X, \; Y)\;\;
\reduce{}{}\;\;\;  Z } \]
}

{\small
\[\frag{{\sf P\_nD\_store} \; (X, \; Y,\; Z) }
{{\sf P\_nD\_store} \;(X, \; Y,\; Z')\;\; \reduce{}{}\;\;\;  \top_s } \]
}

\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 = C}{ X \reduce{}{} C}
\end{array}\]
}

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

\pagebreak

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


\newpage

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

\pagebreak

\section{Optimizations of Kid Programs}
\label{optirules}
Following is a partial list of optimizations rules for Kid.
Optimizations include all $R_{Kid}$ rules,
except  the application rule.
Optimizations should be performed after type checking
and after all bound variables have been assigned
unique names.
Applicability of certain optimization rules requires
some semantic check such as ``$\underline{m} \; > \; 0$''.
We write such semantic predicates above the line but following
an ``\&". \\

It is believed that all optimizations to be presented in this
section preserve at least partial correctness. So far this has been 
proven for only a small subset of them \cite{Zena89}.

%\pagebreak

\subsection*{Kid Rewrite rules}
All Kid rewrite rules can be applied at compile time 
except for the Application rule, which can cause non-termination.

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

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

A similar rule applies for $\underline{{\sf \lambda_{n,m}}}$.\\

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

\subsection*{Algebraic Identities}
{\small
\[ {\sf And} \; ({\sf True},  \;X) \; \reduce{}{} \; X  \] 
\[ {\sf Or} \;( {\sf False},  \;X)  \; \reduce{}{} \; X \]
\[ + \; (X ,0)  \; \reduce{}{} \; X \]
\[ *  \;(X, 1)  \;\reduce{}{} \; X \]
\[ \vdots \] }
The above rules preserve total correctness, while
the following rules preserve only partial correctness.
Any algebraic rule that does not have a precondition can be included
in the following rules.

\blank

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

The following rules are also partially correct but are not confluent.

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

\subsection*{Common Subexpression Elimination}
{\small
\[ \frag
{\mv{Y_m} = P\!F\!N_m \;(\mv{X_n})}
{PFN_m \;(\mv{X_n}) \; \;\; \reduce{}{} \;\;\;  \mv{Y_m}  } \] 
}\\
\noindent
Primitive functions   {\sf I\_nD\_array}, {\sf Open\_cons},
{\sf Apply} and ${\sf Ap_{n,m}}$ are excluded from this optimization
because they (may) cause side-effects.

\subsection*{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}}}$.
(See the  restrictions in the common subexpression elimination rule).


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

\subsection*{Eliminating Circulating Variables}

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

\noindent
A similar optimization applies to for-loops.

\subsection*{Eliminating Circulating Constants  }

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

\subsection*{Peeling the Loop once}
{\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}
\]}

\blank

\subsection*{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 & = & \underline{{\sf \lambda_{n,{n-1}}}} (\mv{x_n})\;\;.\;\;
(\{_{\sf n-1}\begin{array}[t]{lll}
\mv{t_{2,n}^1} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{x_n});\\
t_1^1 & = & {\sf +} \; (X_1, \; D);\\
\mv{t_{2,n}^2} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{t_n^1});\\
t^2_1 & = & {\sf +} \; (t_1^1, \; D);\\
\multicolumn{3}{l}{ \;\;\;\;\vdots }\\
\mv{t_{2,n}^k} & = & {\sf Ap_{n,{n-1}}} \; (B, \; \mv{t_n^{k-1}})  \\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_{2,n}^k} \}\;); }
\end{array}\\
\mv{t_n} & = & {\sf FLoop_n} \;(U, \; D, \; b, \; \mv{X_n}, \; X_p);\\
\multicolumn{3}{l}{ \;\; {\sf In} \; \mv{t_n} \} \;  } 
\end{array}
\end{array}}
\]}

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

{\small
\begin{figure}[htbp]
\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}
}

\section{P-TAC: Parallel Three Address Code}
\label{ptac}
\subsection{P-TAC}
The syntax of P-TAC is given in Figure \ref{p-tac}.
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:

%\illustrationx{tuple}{1.5in}
\illustration{tuple}

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

%\illustrationx{array}{2.5in}
\illustration{array}

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

%\illustrationx{list}{3in}
\illustration{list}

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

%\illustrationx{closure}{2in}
\illustration{closure}

\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*{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
