\section{Notation, Syntax and Semantics}
\label{section:syntax}
We design our algorithms on a simple {\em kernel} language,
SP-TAC (Simple P-TAC) language based on the intermediate language P-TAC 
(Parallel Three-Address Code) \cite{Ariola89} that is used during
the compilation of Id. SP-TAC is 
a simple first order functional language, with constants, variables,
primitive operators, conditionals, user defined functions and
recursive {\em let}-blocks. It is a restricted form of P-TAC in 
several ways: there are no higher order functions, 
structured data types (like lists), or side-effects. 
Though SP-TAC is a very restrictive language to write programs in,
it is a non-strict language and it brings out the issues in
compiling non-strictness. Also,
techniques developed for partitioning SP-TAC are directly applicable
to more expressive languages.

\subsection{Abstract Syntax of SP-TAC}
\begin{myfig}{figure:syntax}{The Syntax of a Kernel Language}
\centering
\begin{tabular}{lcl}
$c$ & $\in$  & Constants\\
 $x,y$ & $\in$ &  Variables \\
 $p$  & $\in$ & Primitive operators \\
 $f$ & $\in$  &  User defined functions \\
 $se$ & $\in$ &  Simple expressions \\
 $e$ & $\in$ & Expressions\\
$st$ & $\in$ & Statements \\
$b$ & $\in$ & Blocks \\
$pr$ & $\in$ & Programs \\\\
$c$ & $::=$ & ${\bf \, true \:|\:false \:| 1\: |\: 2\:|\ldots}$ \\
$p$ & $::=$ & ${\bf\: + \:|\:-\:|\:and\:|\ldots}$\\
$se$ & $::=$ & $c\:|\:x$\\
$e$ & $::=$ & $se \: |\: b \:|\:p(se_{1},se_{2},\ldots,se_{n})\: |$\\
& & $f(se_{1},se_{2},\ldots,se_{n}) \: | \: {\bf if}\:se\:{\bf then}\:b_{1}\:{\bf else}\:b_{2}$\\
$st$ & $::=$ & $\:(y_1,y_2,\ldots,y_n)\:=\:e$\\
$b$ & $::=$ & $\{\{st\}^*\:{\bf in}\:(se_1,se_2,\ldots,se_n)\}$\\
$pr$ & $::=$ & $\{f_{i}(x_{1},x_{2},\ldots,x_{n})\:=\:b_{i}\}$
\end{tabular}
\end{myfig}
Figure~\ref{figure:syntax} shows the abstract syntax of SP-TAC.
We make the following assumptions about the language.
\begin{itemize}
\item There is no currying of user defined functions. This ensures
that we are dealing with a first order language.
\item All primitive operators are strict. That is, they require
all their inputs to produce their output value.
\item All local and bound variables are $\alpha$-renamed so that they
are defined uniquely in the program.
\end{itemize}
For notational convenience, examples in this paper are given in Id. 
It is straightforward to translate them into programs in the kernel language
\cite{Ariola91}.

\subsection{Representing SP-TAC using Graphs}
In this paper, we also use a {\em graph} representation of a block
of SP-TAC. This representation (called a {\em dataflow graph}) is similar to 
the one used in the Id compiler to perform various
optimizations \cite{Traub86}. 
The language syntax
shown in the previous section is essentially a textual representation of these
dataflow graphs. 

\begin{definition} [Dataflow Graph]
Given a block $b$, the dataflow graph $G(b)$ corresponding to $b$ is 
a directed graph. The nodes $N(b)$ in the graph consist of {\em input nodes}
-- 
corresponding to the free variables of the block, {\em output nodes} --
corresponding to the values returned by the block, and {\em operator
nodes} -- corresponding to the various operators
specified in the block.
The edges $E(b)$ of this graph correspond to the flow of values in the block. 
\end{definition}
In this paper, we treat the graph representation and the textual 
representation
as equivalent. For example, when we refer to {\em nodes} in a block, we
actually refer to the nodes in the dataflow graph corresponding to 
the block. Figure~\ref{figure:dataflow-graph} shows the dataflow graph
corresponding to the functions defined in examples 1 and 2 in
section~\ref{section:introduction}.
\begin{myfig}{figure:dataflow-graph}{Figures (a)
and (b) show examples of dataflow graphs.
Input and output nodes are denoted
by circles and constant nodes by triangles. Rectangular nodes correspond
to the various operators in the function.}
\illustration{fig10}[\hsize]
\vspace{-4ex}
\end{myfig}

\subsection{Semantics}
\begin{myfig}{figure:semantic-equations}{Semantic Equations of SP-TAC.}
\centering
$\begin{array}{lcl}
{\cal E}_c\ld n \rd & = & n, \mbox{integer $n$} \\
{\cal E}_c\ld true \rd & = & true \\		
{\cal E}_c \ld false \rd & = & false \\\\
{\cal E}_k\ld + \rd & = & \lambda(x,y).(Int?(x)\: and \: Int?(y)) \\
& & \rightarrow  x + y, error\\\\
{\cal E}_s \ld c \rd \: bve & = & {\cal E}_c \ld c \rd\\
{\cal E}_s \ld x \rd \: bve & = & bve \ld x \rd\\\\
{\cal E} \ld se \rd \: bve \: fenv  & = & {\cal E}_s \ld se \rd \: bve\\
\multicolumn{3}{l}{{\cal E} \ld p(se_1,se_2,\ldots,se_n) \rd \: bve \: fenv =}\\
\multicolumn{3}{l}{\hspace{0.25in} {\cal E}_k \ld p \rd \: ({\cal E}_s \ld se_1 \rd \: bve, \ldots,{\cal E}_s \ld se_n \rd \: bve)}\\
\multicolumn{3}{l}{{\cal E} \ld f(se_1,se_2,\ldots,se_n) \rd \: bve \: fenv =}\\
\multicolumn{3}{l}{\hspace{0.25in} fenv \ld f \rd
\: ({\cal E}_s \ld se_1 \rd \: bve, \ldots,{\cal E}_s \ld se_n \rd \: bve)}\\
\multicolumn{3}{l}{{\cal E} \ld {\bf if}\: se \: {\bf then} \: b_1 {\bf else} \: b_2 \rd \: bve \: fenv = }\\
\multicolumn{3}{l}{\hspace{0.25in} ({\cal E}_s\ld se \rd \: bve) \rightarrow ({\cal E}_b\ld b_1 \rd \: bve \: fenv),({\cal E}_b \ld b_2 \rd \: bve \: fenv)}\\
{\cal E} \ld b \rd \: bve \: fenv  & = & {\cal E}_b \ld b \rd \: bve \: fenv\\
\\
\multicolumn{3}{l}{{\cal E}_b\ld \{\{(y_{i1},\ldots,y_{im})=e_i\}^*\: {\bf in}\: (se_1,\ldots,se_n) \}\rd  \: bve \: fenv = }\\
\multicolumn{3}{l}{\mbox{\hspace{0.25in} \bf letrec}}\\
\multicolumn{3}{l}{\hspace{0.25in} newbve=[y_{ij} \mapsto ({\cal E}\ld e_i \rd \: (newbve.bve) \: fenv)\downarrow j]}\\
\multicolumn{3}{l}{\mbox{\hspace{0.25in} \bf in} \: ({\cal E}_s\ld se_1\rd  \: newbve,\ldots,{\cal E}_s\ld se_n\rd  \: newbve)}\\
\\
\multicolumn{3}{l}{{\cal E}_p\ld \{f_i(x_1,x_2,\ldots,x_n)=b_i\}^*\rd = fenv, \mbox{\bf whererec}}\\
\multicolumn{3}{l}{\hspace{0.25in}fenv = [f_i \mapsto (\lambda(y_1,y_2,\ldots,y_n).{\cal E}_b\ld b_i \rd \: [x_i \mapsto y_i]\: fenv)]}
\end{array}$
\end{myfig}

Our framework is based on denotational semantics. We  chose to do this 
because techniques for designing and
proving analyses based on abstract interpretation are 
well developed in this framework 
and these techniques handle recursive function definitions in a natural manner.
The semantics of SP-TAC itself is straightforward as it is a simple first
order language. It is based on the semantics given in \cite{Bloss88}
and specifies a non-strict semantics of the language.

Denotational semantics \cite{Schmidt} is given by defining domains 
(complete partially ordered sets)
and constructing a mapping from entities in the language
to elements of these domains. 
For SP-TAC, we need to define the following domains. 
We have the standard domains $Int$ and $Bool$ for integers and booleans. 
These domains contain an element $\bot$ that stands for the ``undefined''
value. To model multiple values, we use {\em product} domains
\cite{Schmidt}. We use $D^k$ to denote a domain formed by the k-product $D \times D \times \ldots \times D$. 
The infix operator $\downarrow$ is used to select any component of 
a value in $D^k$.

In addition to these domains, we have domains of functions that
map (multiple) values to (multiple) values. There are also domains
corresponding to variable environments and function environments.
These domains map variables to values and function names to functions
respectively. 
The formal definition of the domains we use in our
semantics are:
\begin{center}
\begin{tabular}{lr}
$Int$ & Integers \\
$Bool$ & Booleans \\
$Val = Int + Bool$& Values\\
$Fun = \bigcup_{j,k \geq 1} (Val^j \rightarrow Val^k)$&First order functions\\
$D=Val + \{error\}$& Denotable values\\
$D_T = \bigcup_{k \geq 1} Val^k + \{error\}$& Tuples of values\\
$Bve=V \rightarrow D$& Variable Environments\\
$Fenv=Fv \rightarrow Fun$&Function Environments\\
\end{tabular}
\end{center}
The various semantic functions are given below:
\begin{center}
\begin{tabular}{lr}
${\cal E}_c : Con \rightarrow Val$ & Constants\\
${\cal E}_k : Pf \rightarrow Fun$ & Primitive operators\\
${\cal E}_s : SE \rightarrow Bve \rightarrow D$ & Simple Exps\\
${\cal E}_b : Bo \rightarrow Bve \rightarrow Fenv \rightarrow D_T$
& Blocks\\
${\cal E} : Exp \rightarrow Bve \rightarrow Fenv \rightarrow D_T$
& Expressions\\
${\cal E}_p : Prog \rightarrow Fenv$ & Programs
\end{tabular}
\end{center}

Now, we describe semantic equations that define the behavior
of these semantic functions. Here is some notation used in describing
our semantic equations:
\begin{itemize}
\item If $env$ and $env'$ are two environments, we use $env'.env$ to denote the 
environment $env''$ such that $env''\ld y \rd = env' \ld y \rd$ if 
$y \in Domain(env')$, $env'' \ld y \rd = env \ld y \rd$, otherwise. 
This is the way environments are linked in a statically scoped block structured
language.
\item We also make use of a case operator 
(denoted by $\rightarrow$). The meaning of $x \rightarrow y, z$ is 
that depending on whether $x$ is $true$ or $false$ either $y$ or $z$ is
the value of the entire case expression.
\end{itemize}

The semantic equations are given in figure~\ref{figure:semantic-equations}.
For clarity of the equations, we have omitted the projections and
injections between the various domains.
Given a program $pr$, we use ${\cal E}^{pr} \ld b \rd \: bve$ to denote ${\cal E} \ld b \rd
\: bve \: ({\cal E}_p \ld pr \rd)$.


