% ``Lambda-S: a parallel, recursive lambda-calculus with synchronization and side-effects''
%
% Arvind    Maessen    Nikhil    Stoy
% Prepared for ICFP 97
% November 1996

\documentstyle[11pt, lcscover]{article}

% ----------------
% HORIZONTAL MARGINS
% Left margin 1 inch (0 + 1)
\setlength{\oddsidemargin}{0in}
% Text width 6.5 inch (so right margin 1 inch).
\setlength{\textwidth}{6.5in}
% ----------------
% VERTICAL MARGINS
% Top margin 0.5 inch (-0.5 + 1)
\setlength{\topmargin}{-0.5in}
% Head height 0.25 inch (where page headers go)
\setlength{\headheight}{0.25in}
% Head separation 0.25 inch (between header and top line of text)
\setlength{\headsep}{0.25in}
% Text height 9 inch (so bottom margin 1 in)
\setlength{\textheight}{9in}
% ----------------
% PARAGRAPH INDENTATION
\setlength{\parindent}{0in}
% SPACE BETWEEN PARAGRAPHS
\setlength{\parskip}{\medskipamount}
% SPACE BETWEEN LINES
\setlength{\baselineskip}{16pt}
% ----------------
% STRUTS
% HORIZONTAL STRUT.  One argument (width).
\newcommand{\hstrut}[1]{\hspace*{#1}}
% VERTICAL STRUT. Two arguments (offset from baseline, height).
\newcommand{\vstrut}[2]{\rule[#1]{0in}{#2}}
% ------------
% HORIZONTAL LINE ACROSS PAGE:
\newcommand{\hdivider}{\noindent\mbox{}\hrulefill\mbox{}}
% ------------
% EMPTY BOXES OF VARIOUS WIDTHS, FOR INDENTATION
\newcommand{\hm}{\hspace*{1em}}
\newcommand{\hmm}{\hspace*{2em}}
\newcommand{\hmmm}{\hspace*{3em}}
\newcommand{\hmmmm}{\hspace*{4em}}
% ------------
% VARIOUS CONVENIENT WIDTHS RELATIVE TO THE TEXT WIDTH, FOR BOXES.
\newlength{\hlessmm}
\setlength{\hlessmm}{\textwidth}
\addtolength{\hlessmm}{-2em}

\newlength{\hlessmmmm}
\setlength{\hlessmmmm}{\textwidth}
\addtolength{\hlessmmmm}{-4em}

\newlength{\hlesspic}
\setlength{\hlesspic}{\textwidth}
\addtolength{\hlesspic}{-2in}

% ------------
% ``TIGHTLIST'' ENVIRONMENT (no para space between items, small indent)
\newenvironment{tightlist}%
{\begin{list}{$\bullet$}{%
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{1.5em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
}
}%
{\end{list}
}
% ------------
% ITALICISE WORDS
\newcommand{\ie}{{\em i.e.,\/}}
\newcommand{\eg}{{\em e.g.,\/}}
\newcommand{\etal}{{\em et al.\/}}
\newcommand{\etc}{{\em etc.\/}}
\newcommand{\via}{{\em via\/}}
\newcommand{\vs}{{\em vs.\/}}
\newcommand{\viz}{{\em viz.,\/}}
% ------------
% CODE FONT (e.g. {\cf x := 0}).
\newcommand{\cf}{\small\tt}
% ------------------------------------------------
% ID CODE DISPLAYS.
% Id code displays are enclosed between \bid and \eid.
% Most characters are taken verbatim, in typewriter font,
% Except:
%  Commands are still available (beginning with \)
%    but use ` and ' instead of { and }
%  Math mode is still available (beginning with $)
%    but use ~ and ! for ^ and _

\outer\def\beginid{%
%  \begin{tabbing}
  \begin{list}{$\bullet$}{%
    \setlength{\topsep}{0in}
    \setlength{\partopsep}{0in}
    \setlength{\itemsep}{0in}
    \setlength{\parsep}{0in}
    \setlength{\leftmargin}{2em}
    \setlength{\rightmargin}{0in}
    \setlength{\itemindent}{0in}
  }\item[]
%  \catcode`\{=12
%  \catcode`\}=12
  \catcode`\&=12
  \catcode`\#=12
  \catcode`\%=12
  \catcode`\~=12
%  \catcode`\_=12
%  \catcode`\^=12
%  \catcode`\~=7
%  \catcode`\!=8
%  \catcode`\'=2
%  \catcode`\`=1
  \obeyspaces
  \obeylines
  \small\tt}

\outer\def\endid{%
  \end{list}
%  \end{tabbing}
  }

{\obeyspaces\gdef {\ }}

% ------------------------------------------------
% COUNTERS FOR TEMPORARILY SAVING COUNTER VALUES

\newcounter{TempCounter}
\newcounter{PrintTermination}
\newcounter{PrintMonotonicity}
\newcounter{GCZcorrectness}

% ================================================================

\newcommand{\FIXTHIS}{{\em [***** FIX THIS *****]}}

% Left and Right brackets for syntactic terms
\newcommand{\LL}{$[\![$}
\newcommand{\RR}{$]\!]$}

% BETA_G symbol
\newcommand{\BetaLet}{$\beta_{let}$}

% LAMBDA-Let0 symbol
\newcommand{\LambdaZero}{${\lambda}_{0}$}

% LAMBDA-C symbol
\newcommand{\LambdaC}{${\lambda}_{C}$}

% LAMBDA-B symbol
\newcommand{\LambdaB}{${\lambda}_{B}$}

% LAMBDA-S symbol
\newcommand{\LambdaS}{${\lambda}_S$}

% GOESTO (single reduction step)
\newcommand{\goesto}{$\longrightarrow$}

% GOESTOTO (zero or more reduction steps)
\newcommand{\goestoto}{\makebox[0em][l]{$\:\longrightarrow$}{$\longrightarrow$}}

% GOESTOTOSIGMA (zero or more reduction steps, under strategy sigma)
\newcommand{\goestotosigma}{
$\stackrel{\sigma}
          {\mbox{\goestoto}}$
}

% GOESTOTOSIGMAZERO (zero or more reduction steps, under strategy sigma_0)
\newcommand{\goestotosigmazero}{
$\stackrel{\sigma_0}
          {\mbox{\goestoto}}$
}

% ISIN
\newcommand{\isin}{$\in$}

% ISNOTIN
\newcommand{\isnotin}{$\not\in$}

% EMPTYSTMT

\newcommand{\emptystmt}{$\epsilon$}

% BARRIER

\newcommand{\BAR}{\mbox{\tt ---}}

% UNION

\newcommand{\union}{$\cup$}

% INTERSECT

\newcommand{\intersect}{$\cap$}

% CHECK MARK

\newcommand{\chekmark}{$\surd$}

% IS DEFINED AT

\newcommand{\defat}{\!\uparrow\!}

% IS UNDEFINED AT

\newcommand{\undefat}{\!\downarrow\!}

% NEW RULE

\newcommand{\NEW}{{\small$(\clubsuit)$}}

% DEFINITIONS, PROPOSITIONS, etc.

\newtheorem{Definition}{Definition}

\newtheorem{Proposition}[Definition]{Proposition}

% ================================================================
% HERE BEGINS THE DOCUMENT

\begin{document}

\title{
{\LambdaS}: an Implicitly Parallel $\lambda$-Calculus
with Letrec, Synchronization and Side-Effects
}

\author{
\begin{tabular}[t]{ll}
Arvind \hmm & {\it MIT Lab for Computer Science}  \\
% ----
J-W.~Maessen \hmm & {\it MIT Lab for Computer Science} \\
% ----
R.S.~Nikhil \hmm & {\it Digital Equipment Corp., Cambridge Research Lab} \\
% ----
J.E.~Stoy \hmm & {\it Oxford University Computing Laboratory}
\end{tabular}
}

\researchcredit{This research was conducted at the MIT Laboratory for
Computer Science.  Funding for this project was provided in part by
the Advanced Research Projects Agency of the Department of Defense
under Ft. Huachuca contract C-DABT63-95-C0150.}
\toappear{Submitted to ICFP '97}
\trnumber{Computation Structure Group Memo 393}

\maketitle

\begin{abstract}
{\LambdaS} extends the $\lambda$-calculus with
letrecs, barriers, and updateable memory cells with synchronized
operations.  The calculus is designed to be useful for reasoning about
compiler optimizations and, thus, allows reductions anywhere, even
inside $\lambda$'s.  Despite the presence of side-effects, the
calculus retains fine-grained, implicit parallelism and non-strict
functions; there is no global, sequentializing store.  Barriers, for
sequencing, capture a robust notion of termination.  Although
{\LambdaS} was developed as a foundation for the parallel functional
languages pH and Id, we believe that barriers give it wider
applicability-- to sequential and explicitly parallel languages.  In
this paper we describe the {\LambdaS}-calculus and its properties
which are based on a notion of observable information in a term. We
also describe reduction strategies to compute the maximal observable
information.
\end{abstract}

% ================================================================

\section{Introduction}

The $\lambda$-calculus {\cite{Barendregt81a}} and its variants have
been invaluable in capturing the essence of languages such
as Haskell {\cite{Hudak92c}}, SML \cite{Milner90a} and Scheme
{\cite{Clinger91}}, providing the theoretical foundation for reasoning
about and transforming programs in these languages.  In this paper we
describe the {\LambdaS}-calculus, another variant, intended as the
formal basis for the parallel programming languages pH
{\cite{Aditya95a}} (an extension of Haskell) and Id
{\cite{Nikhil91b}}.

{\LambdaS} incorporates implicit parallelism, letrecs, synchronization
and side-effects.  The fine-grained parallelism evident in functional
(especially non-strict) languages is exploited by default.  Together
with letrec, it permits programs with dynamic cyclic dependencies, a
popular technique in lazy programs.  The {\em barrier\/} is a control
mechanism for sequencing.  Side-effects are bundled with data-oriented
synchronization in two mechanisms called I-structures
{\cite{Arvind89b}} and M-structures {\cite{Barth91a}}.  We believe
{\LambdaS} meets the following goals:
\begin{tightlist}

\item
An easy-to-understand operational semantics of pH.  This includes a
definition of observable values and a standard parallel reduction
strategy to compute these values.

\item
Maximum flexibility, in order to reason about compiler optimizations.
For example, it should permit reductions {\em inside\/} $\lambda$'s
and conditionals (because this is what compilers do) even though such
reductions may not occur during execution.

\end{tightlist}
The novelty of {\LambdaS} lies in the way it treats barriers and
side-effects.  In the FP literature, introduction of side-effects is
usually in the context of a sequential operational semantics (see, for
example, {\cite{Felleisen89}} and {\cite{Mason91}} for call-by-value
languages, or state monads in Haskell {\cite{Launchbury94}}), and
state is often modeled by a single global store with sequential
operations.  {\LambdaS}, on the other hand, introduces no such
sequentialization, nor a separate store.  The ``store'' is distributed
throughout the term and we give small-step semantics for its
manipulation. This is crucial for preserving implicit, fine-grained
parallelism.  Our barrier semantics captures a robust notion of
``termination''.  We believe it is powerful enough to explain
call-by-value languages and sequential languages extended with
concurrency primitives, and raw (unsynchronized) side-effects.  Despite the
presence of side-effects, our calculus places {\em no\/} restrictions
on where reductions may take place in the term.

The introduction of side-effects requires a precise definition of {\em
sharing\/}.  There is a large body of literature dealing with sharing,
such as {\cite{Wadsworth71}}, {\cite{Launchbury93}},
{\cite{Ariola95b}} and {\cite{Abadi91}}; these are motivated not by
side-effects but by efficiency considerations (graph reduction,
optimality, \etc), and often do not address letrecs and parallelism.

In this paper, we build up to {\LambdaS} in three stages.
{\S}{\ref{sec-LambdaC}} describes {\LambdaC}, extending the
$\lambda$-calculus with letrecs, conditionals, constants and
functional data structures.  The technical results of {\LambdaC} have
already been achieved by Ariola and Blom {\cite{ariola96d}}; we use
this section to introduce our (somewhat different) notation and
machinery.  The results are similar for the functional subset, but the
Ariola and Blom semantic model does not carry over to barriers and
side-effects.  {\S}\ref{sec-LambdaB} describes {\LambdaB}, adding
sequencing barriers to {\LambdaC}.  {\S}{\ref{sec-LambdaS}} describes
{\LambdaS}, the full calculus, adding side-effects and data-oriented
synchronization.  In {\S}{\ref{sec-standard-reduction}} we discuss
parallel reduction strategies.

In each proposition we present, we follow the convention that, unless
a limitation is explicitly stated, it holds for {\LambdaC}, {\LambdaB}
and {\LambdaS}.  Due to space limits, we omit all proofs, deferring
them to a companion technical report {\cite{Arvind96a}} (in
preparation).  Furthermore, we assume that {\LambdaS} terms are
generated from a statically typed language (like pH), and thus ignore
reductions precluded by static type-checking.

% ================================================================

\section{{\LambdaC}: Letrecs, Constants and Functional Data Structures}

\label{sec-LambdaC}

{\LambdaC} is purely functional (no side-effects). Letrecs allow
sharing of computations by binding an expression to an identifier
which may be used in a number of places---including recursively in its
own definition.  While this may be viewed as merely an optimization in
a purely functional language, it is semantically essential for
barriers and side-effects.  Theoretically, we could work without
conditionals, constants and functional data structures, but we include
them to improve intuition.

The calculus will be presented by describing the syntax of terms,
equivalence rules for ignoring trivial syntactic differences
between terms, and reduction rules.\footnote{ As usual, the
\mbox{``$e$ {\goesto} $e_1$''} denotes one application of a reduction
rule; \mbox{``$e$ {\goestoto} $e_1$''} denotes a finite sequence (zero
or more) of reductions.  A {\em redex} is a term or subterm which is
capable of reduction by one of the rules.  }  Then, we discuss
equivalence between terms using a notion of printable observations.
Finally, we discuss garbage collection, or erasure of irrelevant
terms, which other authors often include in their reduction rules.

\hdivider \\
\hmm
\begin{tabular}[t]{lcll}
\multicolumn{4}{c}{\bf Syntax of {\LambdaC}} \\
\multicolumn{4}{l}{Expressions:} \\
$E$  & $::=$  & $x$ $\mid$ $E$ $E$ $\mid$ ${\lambda}x.E$  & Identifiers, applications, abstractions \\
     & $\mid$ & \{ $S$ {\tt in} $E$ \}                    & Letrec blocks \\
     & $\mid$ & {\tt Cond}($E$,$E$,$E$) $\mid$ PF$_k$($E_1$,$\cdots$,$E_k$) \hmm & Conditionals, primitive fn of arity $k$ \\
     & $\mid$ & CN$_0$ $\mid$ CN$_k$($E_1$,$\cdots$ $E_k$) & Constants, constructors of arity $k$\\
\multicolumn{4}{l}{Non-initial expressions:} \\
     & $\mid$ & \underline{CN$_k$}($SE_1$,$\cdots$ $SE_k$) & Constructor values of arity $k$\\
\multicolumn{4}{l}{Statements (in blocks):} \\
$S$  & $::=$  & {\emptystmt}                   & Empty statements \\
     & $\mid$ & $x = E$                        & Bindings \\
     & $\mid$ & $S$ {\tt ;} $S$                & Parallel statements \\
% \multicolumn{4}{l}{Primitives and constants and constructors:} \\
% PF$_1$	& $::=$  & {\tt negate} $\mid$ {\tt not} $\mid$ {\tt Proj$_1$}
% 		  $\mid$ {\tt Proj$_2$} $\mid$ $\cdots$	\hmm & Primitive fns of arity 1 \\
% PF$_2$ & $::=$  & {\tt +} $\mid$ {\tt -} $\mid$ $\cdots$ & Primitive fns of arity 2 \\
% CN$_0$ & $::=$  & {\it Number}  $\mid$ {\it Boolean} $\mid$ $\cdots$ & Constants \\
% CN$_2$ & $::=$  & {\tt cons} $\mid$ $\cdots$ & Constructors of arity 2 \\
\end{tabular} \\
\hdivider

The syntax of {\LambdaC} is shown above.  Constants CN$_0$ include
numbers and booleans; functional data structure constructors CN$_k$
include ``{\tt cons}''; primitives PF$_k$ include arithmetic operators
and projection functions ({\tt Proj$_j$}) to select components of
functional data structures.  Non-initial expressions do not appear in
user-written programs, but only as part of the reduction process.
Arguments of \underline{CN$_k$}() are always {\em simple
expressions\/} ($SE$, defined shortly: identifiers and values); with
recursive blocks, this allows us to write cyclic data structures
finitely.  In a letrec block ``\mbox{\tt \{ $S$ {\tt in} $E$ \}}'',
$E$ is called its {\em return expression\/}.  We use the general term
``statement'' for $S$ because {\LambdaS} will later introduce
components that just perform side-effects.  Empty statements are a
technical convenience that become useful in {\LambdaB} and {\LambdaS}.
The left-hand side identifiers in the bindings of $S$ must be
pair-wise distinct.  The block has recursive scoping rules---any
left-hand side identifier may be referred to in any right-hand side
expression, as well as in the return expression.

% ------------------------------------------------

{\bf Syntax of Values and Simple Expressions in {\LambdaC}:} During
reduction we need to {\em instantiate\/} an
identifier's use with its definition.  We cannot instantiate arbitrary
expressions, as this may replicate work and destroy {sharing}.  We
identify two subsets of {\LambdaC}, {\em Values\/} and {\em
Identifiers}, together known as {\em Simple Expressions\/}, that are
substitutable:

\hmm
\begin{tabular}[t]{lcll}
$SE$ & $::= $ & $x$ \hm $\mid$ \hm $V$       & Identifiers and values \\
$V$  & $::= $ & ${\lambda}x.E$ \hm $\mid$ \hm CN$_0$ \hm $\mid$ \hm \underline{CN$_k$}($SE_1$,$\cdots$ $SE_k$) \hmmmm & \\
\end{tabular}

% ----------------

\subsection{{\LambdaC} Syntactic Equivalence Rules}

\label{sec-LambdaC-equivalence-rules}

As in {$\lambda$}-calculus, bound variable names are just dummy
names---their exact choice does not matter.  Further, the exact
textual order of statements in a parallel composition does not
matter:

\hmm
\begin{tabular}[t]{llll}
  \multicolumn{4}{l}{$\alpha$-renaming:} \\
  \hm & ${\lambda}x.e$            & $\equiv$  & ${\lambda}t.(e[t/x])$ \\
      & \{ $x=e$ ; $S$ in $e_0$ \}  & $\equiv$  & \{ $t=e$ ; $S$ in $e_0$ \}$[t/x]$ \\
  \multicolumn{4}{l}{Equivalence properties of ``{\tt ;}''} \\
      & {\emptystmt} {\tt ;} $S$            & $\equiv$ & $S$ \\
      & $S_1$ {\tt ;} $S_2$                 & $\equiv$ & $S_2$ {\tt ;} $S_1$ \\
      & $S_1$ {\tt ;} ($S_2$ {\tt ;} $S_3$) & $\equiv$ & ($S_1$ {\tt ;} $S_2$) {\tt ;} $S_3$\\
\end{tabular}

$\alpha$-renaming is done in the standard way; we omit details here.
We use ``$e$[$t$/$x$]'' to denote expression $e$ with all free
occurrences of identifier $x$ replaced by identifier $t$.  We use $e'$
and $S'$ to denote renamed versions of $e$ and $S$. $t$ is always an
identifier which does not otherwise occur in the left-hand term of the rule.

% ------------------------------------------------

\subsection{{\LambdaC} Reduction Rules}

\label{sec-LambdaC-reduction-rules}

{\bf Function Application ($\beta$-reduction):}

\hmm
$({\lambda}x.e_1) \; e_2$ {\goesto} \{ $t$ $=$ $e_2$ in $e_1[t/x]$ \} \hmmmm ({\BetaLet})

There are two things to note about {\BetaLet}.  First, $e_2$ can be an
arbitrary expression, not just a value---this makes it {\em
non-strict}.  Second, we always preserve exactly one copy of
$e_2$---unlike traditional $\beta$, which may copy or erase $e_2$
depending on the number of uses of $x$ in $e_1$.  Together with the
restricted instantiation rule below, this preserves {\em sharing\/}
and side-effects, and is important for the semantics of barriers.
{\BetaLet} produces graph structured terms, whereas traditional
$\beta$ produces trees.

% ------------

{\bf Instantiation (Substitution):} Given $x=a$ in a letrec block,
{\em where $a$ is a simple expression}, these reduction rules specify
that we can replace uses of $x$ by $a$:

\hmm
\begin{tabular}[t]{lllr}
\{ $x$ $=$ $a$ ; $S$ in $C[x]$ \}  	& \goesto & 
	\{ $x$ $=$ $a$ ; $S$ in $C[a]$ \} \hmmmm & (Inst1) \\
% ----------------
$x$ $=$ $a$ ; $SC[x]$              	& \goesto & 
	$x$ $=$ $a$ ; $SC[a]$             & (Inst2) \\
% ----------------
\\
% ----------------
$x$ $=$ $a$                          	& \goesto & $x$ $=$ $C[a]$
					& (Inst3)   \\
	& & where $a \;=\; C[x]$
\end{tabular}

For lack of space we omit the obvious definitions of $C[\;]$ and
$SC[\;]$ which are contexts (expressions and statements, respectively,
into which we can plug an expression).  There are no restrictions--
substitutions can even occur inside $\lambda$'s.  The calculus thus
permits infinite unfolding of cyclic terms; we leave it to reduction
strategies to control this.

% ----------------

{\bf Block flattening:} \\
\hmm
\begin{tabular}[t]{llll}
$x$ $=$ \{ $S$ in $e$ \} & \goesto & $x$ $=$ $e'$ {\tt ;} $S'$ \hmmmm & (Flat) \\
\end{tabular}

% ----------------

{\bf Expression lifting:} Each rule below ``lifts out'' a nested
expression by giving it a name (using $\alpha$-renaming where
necessary to avoid name conflicts).  To prevent instantiation and
lifting from alternating forever, lifting rules are inapplicable when
$e$ is a simple expression.

\hmm
\begin{tabular}[t]{llll}
\{ $S$ in $e$ \}         & \goesto & \{ $S$ {\tt ;} $t$ $=$ $e$ in $t$ \}
					& (LiftB) \\
% --------
($e$ $e_2$)              & \goesto & \{ $t$ $=$ $e$ in $t$ $e_2$ \}
					& (LiftAp1) \\
% --------
($e_1$ $e$)              & \goesto & \{ $t$ $=$ $e$ in $e_1$ $t$ \}
					& (LiftAp2) \\
% --------
{\tt Cond}($e$, $e_1$, $e_2$) &
    \goesto &
    \{ $t$ $=$ $e$ in {\tt Cond}($t$, $e_1$, $e_2$) \} \hmm &
    (LiftCond) \\
% --------
{\tt $PF_k$($\cdots$, $e$, $\cdots$) } &
    \goesto &
    \{ $t$ $=$ $e$ in $PF_k$($\cdots$, $t$, $\cdots$) \} \hmm &
    (LiftPF)
\end{tabular}

Flattening and lifting produce new juxtapositions that trigger other
reductions.  For example:
\beginid
f = \{  $S_1$  in  ${\lambda}x.e_1$ \};  x = f a;      $\stackrel{{\rm(Flat)}}{\longrightarrow}$      f = ${\lambda}x.e_1'$ ;  $S_1'$;  x = f a;
\endid
which then allows us to instantiate {\tt f} by ${\lambda}x.e_1'$ in
the application.  Note that we do not lift expressions from $\lambda$
bodies, nor from the arms of a conditional.  While safe in {\LambdaC},
such rules would be incorrect in {\LambdaB} and {\LambdaS} because
they would ``expose'' (make observable) potential non-terminations or
side-effects that would normally be protected by those contexts.

% ------------

{\bf Constants, conditionals, delta rules:}
As usual, we regard constants (CN$_0$) as already evaluated, and:

\hmm
\begin{tabular}[t]{lllll}
{\tt Cond(True, $e_1$, $e_2$)} &
    \goesto &
    $e_1$ \hmmmm &
    (CondT) \\
% ---
{\tt Cond(False, $e_1$, $e_2$)} &
    \goesto &
    $e_2$ \hmmmm &
    (CondF) \\
PF$_k$($v_1$,$\cdots$,$v_k$) &
    \goesto &
    $w$ \hmmm &
    ($\delta$) &
    {\eg} {\tt +(\underline{$n$},\underline{$m$})}
                 {\goesto}
                 \underline{\tt $n+m$} \\
{\tt proj$_j$(\underline{\rm CN$_k$}($e_1$, $\cdots$, $e_j$, $\cdots$))} &
    \goesto &
    $e_j$ \hmmm &
    (Proj) &
\end{tabular}

% ----------------

{\bf Constructors:}
\label{sec-LambdaC-constr-eval}
Constructor terms in the initial program are reduced to constructor
values:

\hmm
\begin{tabular}[t]{llll}
  CN$_k$($\cdots$, $e_j$, $\cdots$) &
  \goesto &
  \{ $\cdots$ ; {\tt $t_j$ = $e_j$}; $\cdots$ {\tt in} \underline{\rm CN$_k$}( $\cdots$, $t_j$, $\cdots$) \} \hmmmm &
  (Cons)
\end{tabular}

Here, $e_j$ need not be a simple expression.  The resulting
``\underline{\rm CN$_k$}()'' term has identifier arguments and,
thus, there are no lifting rules for constructors.

% ------------------------------------------------

\subsection{Comparing terms for information content}

\label{sec-LambdaC-printable-values}

Having presented the calculus for {\LambdaC}, we must now ask if there
is a non-trivial notion of the ``meaning'' of a term that is preserved
under reduction.  It is traditional here to discuss the ``normal
form'' of a term and reduction strategies to achieve it.\footnote{ It
is also possible to map terms to a separate space of denotational
meanings (see, \eg\ \cite{Stoy94}), but for {\LambdaB} and {\LambdaS}
this is quite complicated and (for {\LambdaS})
rather indirect.  } Unfortunately, because of letrec blocks, direct
syntactic characterizations (such as normal forms) are problematic.
First, terms may contain irrelevant clutter (since {\BetaLet} does not
discard argument expressions). But even if we are tempted to use
``garbage collection'' rules to erase clutter, the following result
suggests that letrec blocks make syntactic comparisons futile:
\begin{Proposition}
[Non-confluence (Ariola and Klop {\cite{ariola94}})] {\LambdaC} is not confluent.
\end{Proposition}
To see this, consider this term, which represents an infinite
list of alternating 1's and 2's:
\beginid
\{  x  =  \underline{Cons}(1, y) ; y  =  \underline{Cons}(2, x)    in    x  \}
\endid
Let us take two paths, by substituting for {\tt x} and for
{\tt y}, respectively.  The resulting terms are:
\beginid
\{  x  =  \underline{Cons}(1, y) ; y  =  \underline{Cons}(2, \underline{Cons}(1, y))    in    x  \} \hmmmm    $(M_1)$
\{  x  =  \underline{Cons}(1, \underline{Cons}(2, x)) ; y  =  \underline{Cons}(2, x)    in    x  \} \hmmmm    $(M_2)$
\endid

From this point on, in $M_1$ the {\tt y} definition will always
contain {\tt y}, whereas in $M_2$ the {\tt y} definition will always
contain {\tt x}, \ie\ we can never bring these two terms together
syntactically again.  However, $M_1$ and $M_2$ will behave identically
in all contexts.

Thus, instead of syntactic comparisions, we compare observable
behavior.  We first discuss the ``instantaneous print'' or
Print{\LL\RR} of a term.  Then we discuss the ``full print'' or
Print*{\LL\RR} of a term, \ie\ what can be observed about a term after
reduction.

% ----------------------------------------------------------------

\subsubsection{Print{\LL\RR}: instantaneous observable information in a term}

Print{\LL$e$\RR} transforms a term into the syntax $E_P$.  It
preserves constants and constructors; replaces applications,
conditionals and nested letrecs by the symbol ``$\bot$''; replaces any
$\lambda$-expression with the symbol ``$\lambda$'' (and ignores the
$\lambda$-body), and so on.

To handle cyclic terms, we define printing in two stages: a
Print{\LL\RR} function captures the graph structure of the term, and
an Unfold() function flattens graphs into trees that can be compared.
Print{\LL\RR} produces terms with the following syntax:

\hmm
\begin{tabular}{lclcl}
$E_P$	& ::= & $V_P$     & $\mid$ & \{ $S_P$ in $SE_P$ \} \\
$S_P$	& ::= & \emptystmt & $\mid$ & $x = V_P$ \hm $\mid$ \hm $S_P$ ; $S_P$ \\
$SE_P$	& ::= &	$x$       & $\mid$ & $V_P$	\\
$V_P$	& ::= & $\bot$    & $\mid$ & $\lambda$ \hm $\mid$ \hm CN$_0$ \hm $\mid$ \hm CN$_k$($SE_{P_1}$, $\cdots$ $SE_{P_k}$)
\end{tabular}

Print{\LL\RR} simply discards $\lambda$ bodies, applications,
conditionals, nested blocks, {\etc}:

\hmm
\begin{tabular}[t]{llll}
Print{\LL}\{ $S$ {\tt in} $E$ \}{\RR}	&$=$&	
	\{ Print$_S${\LL}$S${\RR} in Print$_{SE}${\LL}$E${\RR} \}  \hmm & \\
Print{\LL}$E${\RR}			&$=$& 	Print$_V${\LL}$E${\RR}
		& {\em otherwise} \\
\\
Print$_S${\LL\emptystmt\RR}		&$=$&	\emptystmt	\\
Print$_S${\LL}$x = E${\RR}		&$=$&	$x =$ Print$_V${\LL}$E${\RR} \\
Print$_S${\LL}$S_1$; $S_2${\RR}		&$=$&
	Print$_S${\LL}$S_1${\RR} ; Print$_S${\LL}$S_2${\RR} & \\
\\
Print$_V${\LL}$\lambda x.E$ {\RR}		&$=$&	$\lambda$ & \\
Print$_V${\LL}CN$_0$ {\RR}			&$=$&	CN$_0$ & \\
Print$_V${\LL}\underline{CN$_k$}($\cdots$, $e_j$, $\cdots$){\RR} &$=$&
	CN$_k$($\cdots$, Print$_{SE}${\LL}$e_j${\RR}, $\cdots$) & \\
Print$_V${\LL}$E${\RR}			&$=$&	$\bot$ 		& {\em otherwise} \\
\\
Print$_{SE}${\LL}$x${\RR}               &$=$& $x$ \\
Print$_{SE}${\LL}$E${\RR}               &$=$& Print$_V${\LL}$E${\RR} \\
\end{tabular}

Unfold$_n$() does a finite unfolding of outputs of Print{\LL\RR},
producing trees with the following syntax:

\hmm
\begin{tabular}{lcl}
$T_P$   & ::= &	   $\bot$ \hm $\mid$ \hm
                   $\lambda$  \hm $\mid$ \hm
                   $\Omega$   \hm $\mid$ \hm
                   CN$_0$     \hm $\mid$ \hm
                   CN$_k$($T_{P1}$, $\cdots$ $T_{Pk}$)
\end{tabular}

It prints values, and follows bindings (including arguments of data
structures) by keeping an environment of bindings.  However, it
follows bindings through the environment only up to a finite depth $n$,
bottoming out by printing $\Omega$. $\Omega$ is equivalent to $\bot$, but
we use it as a technical convenience to distinguish partially-unfolded
printable terms from unevaluated printable terms.

\hmm
\begin{tabular}[t]{llll}
Unfold$_n(\{ S_P{\rm \ in\ }SE_P \})$	&$=$&	
		Unfold$'_n(SE_P)$ (Env $S_P$ \{$\forall x. x \mapsto \bot$\})
		& generate nodes \\
Unfold$_n(V_P)$		&$=$&	$V_P$ \\
\\
Unfold$'_0(x)$ $\rho$	&$=$&	$\Omega$		& \\
Unfold$'_n(x)$ $\rho$	&$=$&	Unfold$'_{n-1}(\rho(x))$ $\rho$
		& one unfolding \\
Unfold$'_n($CN$_k$($\cdots$, $e_j$, $\cdots$)$)$ $\rho$
	&$=$&	CN$_k$($\cdots$, Unfold$'_{n}(e_j)$ $\rho$, $\cdots$) \\
Unfold$'_n(V_P)$ $\rho$		&$=$&	$V_P$		&	{\em otherwise} \\
\\
Env({\emptystmt}) $\rho$ 	&$=$&	$\rho$		& \\
Env$(x = V_P)$ $\rho$ 		&$=$&	$\rho\{ x \mapsto V_P \}$ 	& \\
Env$(S_{P1}; S_{P2})$ $\rho$	&$=$&	
		Env$(S_{P1})$ (Env$(S_{P2})$ $\rho$)
\end{tabular}

Because Print{\LL\RR} does not unfold cyclic terms, it always
terminates.  When we Print{\LL\RR} these terms representing an
infinite list of ones:
\beginid
\{  x  =  Cons(1, x)                       in    x  \}
\{  x  =  Cons(1, y);  y  =  Cons(1, x)    in    x  \}
\endid
we get $E_P$ terms that look the same as the original $E$ terms.  When
we then Unfold$_n$() them, we obtain a list of $n$ ones terminated by
$\Omega$:
\beginid
Cons(1, Cons(1, Cons(1, \ldots $\Omega$)\ldots)
\endid

In order to compare $T_P$ trees, we define the following ordering:

\hmm
\begin{tabular}[t]{lcll}
$\Omega$	&$=$&		$\bot$ & \\
$\bot$		&$\sqsubseteq$&	$T_P$ & \\
$\lambda$	&$\sqsubseteq$&	$\lambda$ &\\
CN$_0$		&$\sqsubseteq$& CN$_0$ & \\
CN$_k$($v_1$, $\cdots$, $v_j$ $\cdots$, $v_k$) & $\sqsubseteq$ &
	CN$_k$($v_1$, $\cdots$, $v_j'$ $\cdots$, $v_k$) \hm & 
			if $v_j \sqsubseteq v_j'$ \\
\end{tabular}

We now have a way to compare $E_P$ terms.  A term $E_1$
``contains less information'' than another term $E_2$ if each finite
unfolding of $E_1$ is less than some finite unfolding of $E_2$; and,
equivalence of two $E_P$ terms can be derived in the
usual way from this ordering:

\hmm
\begin{tabular}[t]{lcl}
$E_{P1} \sqsubseteq E_{P2}$ & $\hmm\Leftrightarrow\hmm$ &
	$\forall n. \exists m. {\rm Unfold}_n(E_{P1}) \sqsubseteq
		{\rm Unfold}_m(E_{P2})$ \\
$E_{P1} = E_{P2}$ & $\hmm\Leftrightarrow\hmm$ &
        $E_{P1} \sqsubseteq E_{P2} \hm {\rm and} \hm E_{P2} \sqsubseteq E_{P1}$
\end{tabular}

\begin{Proposition}[Print monotonicity]
\label{prop-print-monotonicity}
If $e$ {\goestoto} $e_1$ then \mbox{\rm Print{\LL}$e${\RR}} $\sqsubseteq$ \mbox{\rm Print{\LL}$e_1${\RR}}
\end{Proposition}

{\LambdaC} is not confluent, but two reduction paths can always
be reunited so their print values match:

\begin{Proposition}[Print confluence in {\LambdaC}]
\label{prop-print-confluence}
If $e${\goestoto} $e_1$
and $e${\goestoto} $e_2$,
then there exist $e'_1$ and $e'_2$
such that $e_1${\goestoto} $e'_1$
and $e_2${\goestoto} $e'_2$,
and Print{\LL}$e'_1${\RR} $=$ Print{\LL}$e'_2${\RR}
\end{Proposition}

The following theorem is very important: it assures us that we have
not lost any computational power by enforcing sharing using letrec
blocks and restricted substitution.

{\bf Definition ({\LambdaZero}):} Let {\LambdaZero} be the calculus without any
restriction on instantiation, \ie\ an identifier may be instantiated
by an arbitrary expression, not just a simple expression.
\begin{Proposition}[Fundamental theorem of graph reduction in {\LambdaC}
(Ariola and Blom \cite{ariola96d})] \hm \\
\hmm
If $e$ {\goestoto} $e_1$ in
{\LambdaZero}, then $\exists e_2$ such that $e$ {\goestoto} $e_2$
in {\LambdaC}, and Print{\LL$e_1$\RR} $\sqsubseteq$ Print{\LL$e_2$\RR}.
\end{Proposition}

% ----------------------------------------------------------------

\subsubsection{Print*: all potentially observable information in a term}

Print*{\LL\RR} is a set of printed terms representing the maximal
printable information that can be obtained from a term or any of its
reductions.  We obtain Print*{\LL$e$\RR} by looking at the outcome of
every possible reduction sequence starting at $e$.  A reduction
sequence of a term $e$ is a partial function from natural numbers {\bf
N} to $E$.  It is partially defined up to some $n$ (with $s_0$ being
$e$ itself), and it is a reduction sequence in that for any two
adjacent defined elements $s_{j-1}$, $s_j$, the former reduces in one
step to the latter.  We write $s_j{\defat}$ or $s_j{\undefat}$ when
$s$ is defined or undefined, respectively, at $j$.

{\bf Definition (Reduction Sequence):} \\
\hmm
$\mbox{\em RS}(e) = \{ s \mid
                s_0=e
                \hm \wedge \hm
                \forall j. s_j{\undefat} \Rightarrow s_{j+1}{\undefat}
                \hm \wedge \hm
                \forall j>0. s_j{\defat} \Rightarrow s_{j-1} \longrightarrow s_j
\}$

The Complete Reduction Sequences for an expression $e$ are all
reduction sequences starting at $e$ which are either infinte, or whose
final term contains no redexes:

{\bf Definition (Complete Reduction Sequences):}  \\
\hmm
$\mbox{\em CRS}(e) = 
	\{ s \in \mbox{\em RS}(e) \mid
                                  \forall j>0.
                                      s_j{\defat} \wedge
				      s_{j+1}{\undefat} \Rightarrow
					   \not\!\exists e'. 
					   s_j \longrightarrow e') \}$

If we Print{\LL\RR} each term in a sequence, we get an ascending chain
of $E_P$ terms (monotonicity).  Intuitively, we want the least upper
bound of this chain as the ``final'' print value.  However, since
chains may be infinite and $E_P$ terms only form a {\em preorder}, we
use the domain ${E_P}^* \supset E_P$ which is isomorphic to the ideal
completion of $E_P$ (and where the isomorphism preserves $E_P$), in
which we can take least upper bounds:

{\bf Definition (Print*{\LL\RR}):}
\hm
Print*{\LL}$e${\RR} $=$
    \{ ${\displaystyle\bigsqcup_{j \in \omega, s_j{\defat} }}$
            Print{\LL}$s_j${\RR}
       $\mid$
	    $s \in \mbox{\em CRS}(e)$ \}

\begin{Proposition}[Print* determinacy in {\LambdaC}]
\label{prop-printstar-determinacy}
In {\LambdaC}, Print*{\LL$e$\RR} has precisely one element.
\end{Proposition}

\begin{Proposition}[Print* preservation in {\LambdaC}]
\label{prop-printstar-preservation}
In {\LambdaC}, if $e$ {\goestoto} $e_1$ then {\rm Print*}{\LL}$e${\RR}
							$=$ {\rm
							Print*}{\LL}$e_1${\RR}.
\end{Proposition}

% ------------------------------------------------

\subsubsection{Termination}

\label{sec-LambdaC-stable-terms}

A stable term is one whose Print{\LL\RR} no longer changes under
further reduction:

{\bf Definition (stable terms):} A term $e$ is {\em stable\/} if
    Print*{\LL}$e${\RR} $=$ \{ Print{\LL}$e${\RR} \}.

It is undecidable in general whether a term is stable; this motivates
the identification of the following classes of stable terms.

{\bf Definition (terminated terms):} {\em Terminated\/} terms are
described by the following syntax: \\
\hmm \begin{tabular}[t]{lll}
         {\it ET} & $::=$  & $V$ \hm $\mid$ \hm  \{ $H$ in $SE$ \} \\
         $H$      & $::=$  & $x = V$ \hm $\mid$ \hm $H$ {\tt ;} $H$
     \end{tabular}

A terminated expression contains no applications, conditionals, \etc,
unless they are inside a $\lambda$-abstraction or arm of a
conditional.
\begin{Proposition}[Stability of terminated terms]
\label{prop-stability}
If $e$ {\isin} {\it ET}, then $e$ is stable.
\end{Proposition}

Consider the following two terms:
\beginid
x = $\bot$      {\it and}          \{  x = Cons(1,x)    in    x \}
\endid

When we Print{\LL\RR} and unfold them, the former gives $\bot$,
whereas the latter gives \mbox{\tt Cons(1, Cons($\cdots$,$\Omega$))}.
It is for this reason alone that we make a distinction between $\bot$
and $\Omega$, and this motivates the following:

{\bf Definition (ground-printing terms):} In a {\em ground-printing}
term $e$, Unfold$_n($Print{\LL}$e${\RR}$)$ does not contain $\bot$ for
every $n$ larger than some $m$.

Note that a ground-printing term is always stable, but it may not have
terminated; this is possible because Print{\LL\RR} does not explore
``irrelevant'' computations, which may {\em never} terminate.

% ----------------------------------------------------------------

\subsection{Garbage Collection of irrelevant terms in {\LambdaC}}

\label{sec-LambdaC-GC}

Our {\BetaLet} rule does not discard argument terms, even if the
formal parameter is unused.  Thus, terms may contain irrelevant
clutter.  Our calculus is free of GC rules, and we can study GC as a
separate topic.

{\bf Definition (garbage collection, or GC):} GC is a transformation from $E$ to
$E$ that erases part of a term,\footnote{
The Print{\LL\RR} function, of course, erases irrelevant differences,
but it transforms $E$ to $E_P$ and
does not preserve deep structure (\eg\ $\lambda$ bodies).
}
such that for any context $C$, Print*{\LL}$C[e]${\RR} $=$ Print*{\LL}$C[$GC{\LL}$e${\RR}$]${\RR}

The following is a proposed garbage collection process:\footnote{
FV($e$) are the free variables of $e$.  BV($s$) are the top-level
bound variables of statement $s$, \ie\ the left-hand sides of all
bindings comprising $s$.  FV($s$) are the free variables of statement
$s$, \ie\ the free variables of the right-hand sides of all bindings
comprising $s$, minus the variables that $s$ itself defines (\ie\
minus BV($s$)).
}

{\bf Definition (garbage collection rule GC$_0$):} \\
\hmm \{ $S_G$ {\tt ;} $S$ in $e$ \}  \goesto  \{ $S$ in $e$ \}
\hmm where \hmm ${\forall}x$ {\isin} FV$(S)$ {\union} FV$(e)$: $x$ {\isnotin} BV$(S_G)$

In other words, if $S$ and $e$ do not use any identifier defined by
$S_G$, then $S_G$ can safely be erased.  GC$_0$ can be applied
anywhere (including inside $\lambda$ bodies).

\begin{Proposition}[GC of unreachable terms (in {\LambdaC})]
\label{prop-GC0}
In {\LambdaC}, GC$_0$ is a correct rule.
\end{Proposition}

% ================================================================

\section{{\LambdaB}: adding Barriers to {\LambdaC}}

\label{sec-LambdaB}

We now add a control mechanism called the {\em barrier\/}, which
sequences statements in a letrec block.  {\LambdaB} remains purely
functional (no side-effects).  Barriers get their practical motivation
from controlling side-effects which are discussed later, but their
semantic implications are evident in a purely functional setting.
Since {\LambdaB} differs from {\LambdaC} in only a small way, we
present it here informally.\footnote{
However, it should be noted that this presentation and the semantics
of barriers themselves differ from indirect semantics given previously
\cite{Aditya95b}.} 
The new syntax is:

\hmm
\begin{tabular}[t]{lcll}
$S$  & $::=$  & $S_1$ {\BAR}  $S_2$   \hmmmm    & Barriers
\end{tabular}

$S_1$ (the {\em pre-region\/}) must terminate before $S_2$ (the {\em
post-region\/}) is visible to the rest of the term.  The sequencing
involves only these two subterms.  Our static recursive
scoping rule for letrec bindings remains the same---in this respect,
there is no difference between barriers and semicolons.  To
$\alpha$-renaming and semicolon equivalences, we add a new syntactic
equivalence:

\hmm
\begin{tabular}[t]{lll}
       (($H$ {\tt ;} $S_1$) {\BAR} $S_2$) & $\equiv$ & $H$ {\tt ;} ($S_1$ {\BAR} $S_2$) \\
\end{tabular}

(Recall, from our discussion on terminated terms, that: $H$ $::=$
$x = V$ $\mid$ $H$ {\tt ;} $H$). This allows value bindings to
escape from pre-regions.  The escaped bindings may enable other
instantiations in the surrounding context.  When all such bindings
escape, the barrier can be discharged:

\hmm
\begin{tabular}[t]{llll}
% ---
{\emptystmt} {\BAR} $S$         & \goesto & $S$ \hmmmm & (BAR1) \\
% ---
$S$ {\BAR} {\emptystmt}         & \goesto & $S$        & (BAR2)
\end{tabular}

It follows that the barrier can be discharged as soon as the pre-region
has terminated:

\hmm $(H$ {\BAR} $S)$  {\goesto} $(H$ {\tt ;} $S)$

In Print{\LL\RR}, we add a clause that omits statements from
post-regions:

\hm
\begin{tabular}[t]{lllr}
Print$_S${\LL} $S_1$ {\BAR} $S_2$ {\RR} & $=$ & Print$_S${\LL}$S_1${\RR}
\end{tabular}

A terminated term in {\LambdaB} contains no barriers unless it is
inside a $\lambda$ or conditional (just as it contains no application
unless it is inside such sub-terms).

All {\LambdaC} propositions hold in {\LambdaB} except for Prop.
{\ref{prop-GC0}} (correctness of GC$_0$).  The post-region of a
barrier has no effect on the computation until the barrier is
discharged:
\begin{Proposition}[Opacity of post-regions]
\label{prop-post-region-opacity}
If $C[S_1$ {\BAR} $S_2]$ {\goestoto} $C'[S'_1$ {\BAR} $S'_2]$
then \\
\hmm
   $\exists$ $C''$ such that
   $C[S_1${\BAR}$S_2]$    {\goestoto}
   $C''[ S'_1${\BAR}$S_2]$ {\goestoto}
   $C'[ S'_1${\BAR}$S'_2]$
\end{Proposition}
{\ie} it is always possible to concentrate on $S_1$ and ignore $S_2$ until
the barrier is discharged.
\begin{Proposition}[Barrier associativity]
\label{prop-barrier-associativity}
In all contexts, $S_1{\BAR}(S_2{\BAR}S_3) \equiv (S_1{\BAR}S_2){\BAR}S_3$
\end{Proposition}
The sole difference between {\LambdaC} and {\LambdaB} is this:
\begin{Proposition}[Barriers constrain results]
\label{prop-barrier-constraining}
Print*{\LL}$C[S_1$\BAR$S_2]${\RR}
$\sqsubseteq$
Print*{\LL}$C[S_1${\tt ;}$S_2]${\RR}
\end{Proposition}
where the $P_1{\sqsubseteq}P_2$ means that for every $p_1$ in $P_1$,
there is a $p_2$ in $P_2$ such that $p_1{\sqsubseteq}p_2$.  Barriers
essentially make it possible to observe non-termination.  When placed
before a barrier, the left-hand term below will allow the barrier to
discharge, whereas the right-hand term will not: 
\beginid 5                        \{ x = $\bot$ in 5 \} \endid

% ----------------

{\bf Garbage collection of irrelevant terms in {\LambdaB}:} Because
GC$_0$ can affect termination, which is now observable, GC$_0$ is no
longer correct for {\LambdaB}.  We constrain the GC rule so that only
unreachable bindings which have terminated are erased.

{\bf Definition (garbage collection rule GC$_v$):} \\
\hmm
\{ $B$ {\tt ;} $S$ in $e$ \}  \goesto  \{ $S$ in $e$ \}
\hm
\begin{tabular}[t]{l}
where ${\forall}x$ {\isin} FV$(S)$ {\union} FV$(e)$:  $x$ {\isnotin} BV$(B)$ \\
and $B$ is defined by the syntax: \hm $B$  $::=$  $x = V$  \hm  $\mid$  \hm  $B$ {\tt ;} $B$
\end{tabular}

\begin{Proposition}[GC of unreachable terminated terms]
\label{prop-GCv}
GC$_v$ is a correct rule.
\end{Proposition}

% ================================================================

\section{{\LambdaS}: adding side-effects and data-oriented synchronization}

\label{sec-LambdaS}

{\LambdaS} is the full calculus, obtained by adding updateable memory
cells that are dynamically allocated in a {\em
heap}.\footnote{Functional data structures in {\LambdaC} could also
have been explained with an explicit heap.}  Each cell can be in a
{\em full\/} or {\em empty\/} state, which affects the behavior of
cell operations.  Our formulation preserves small-step semantics
(local rules) for fine-grain parallelism; there is no global ``store''.

% --------

\begin{figure}[t]
\hdivider \\
\hmm
\begin{tabular}[t]{lcll}
\multicolumn{4}{l}{Expressions:} \\
$E$  & $::=$  & $x$
                $\mid$ $E$ $E$
                $\mid$ ${\lambda}x.E$
                $\mid$ \{ $S$ {\tt in} $E$ \}
                $\mid$ {\tt Cond}($E$,$E$,$E$) & (as before) \\
     & $\mid$ & PF$_k$($E_1$,$\cdots$,$E_k$)
                $\mid$ CN$_0$ $\mid$
                CN$_k$($E_1$,$\cdots$ $E_k$) & (as before) \\
     & $\mid$ & {\tt allocate()}                           & Cell allocation \\
     & $\mid$ & {\tt I-Fetch}($E$) $\mid$ {\tt M-Fetch}($E$)  & I- and M-structure fetch \\
\multicolumn{4}{l}{Non-initial expressions:} \\
     & $\mid$ & \underline{CN$_k$}($SE_1$,$\cdots$ $SE_k$)   & (as before) \\
     & $\mid$ & {\tt O}$_j$		                     & Cell identifiers \\
\multicolumn{4}{l}{Statements (in blocks):} \\
$S$  & $::=$  & {\emptystmt} $\mid$ $x = E$ $\mid$ $S$ {\tt ;} $S$ $\mid$ $S$ {\BAR}  $S$ & (as before) \\
     & $\mid$ & {\tt S-Store($E$,$E$)}	                  & Synchronized store \\
\multicolumn{4}{l}{Non-initial statements:} \\
     & $\mid$ & {\tt heap}			           & Heap allocator \\
     & $\mid$ & {\tt empty(O$_j$)} $\mid$ {\tt error(O$_j$)} $\mid$ {\tt full(O$_j$,$V$)} & Empty, error, full cells \\
% \multicolumn{4}{l}{Primitives and constants and constructors:} \\
% PF$_1$	& $::=$  & {\tt negate} $\mid$ {\tt not} $\mid$ {\tt Proj$_1$}
% 		  $\mid$ {\tt Proj$_2$} $\mid$ $\cdots$			& (as before) \\
% PF$_2$ & $::=$  & cons $\mid$ $\cdots$			& (as before) \\
% CN$_0$ & $::=$  & {\it Number}  $\mid$ {\it Boolean} $\mid$ $\cdots$ & (as before)
\end{tabular}
\caption{\label{fig-lambda-s-syntax}{\bf Syntax of {\LambdaS}}}
\hdivider
\end{figure}
The syntax of {\LambdaS} is shown in Figure
{\ref{fig-lambda-s-syntax}}.  {\tt allocate()} produces a new, {\tt
empty} cell named by a {\em cell identifier\/} {\tt O}$_j$.  {\tt S-Store},
{\tt I-Fetch} and {\tt M-Fetch} are cell operations that depend on
and affect the cell state.  Just before execution, we introduce a
``{\tt{heap}}'' term as follows:

\hmm
\begin{tabular}[t]{llll}
$e$ &
\goesto &
\{ {\tt heap} in $e$ \} \hmmmm ($e$ is the entire program)
\end{tabular}

This is not a reduction rule; it just prepares the orginal program for
execution.

% ------------------------------------------------

{\bf Syntax of Values and Simple Expressions in {\LambdaS}:} we add cell identifiers:

\hmm
\begin{tabular}[t]{lcll}
$V$     & $::= $ & ${\lambda}x.E$ $\mid$ CN$_0$ $\mid$ \underline{CN$_k$}($x_1$,$\cdots$ $x_k$) \hmm & (as before) \\
	& $\mid$ & {\tt O}$_j$			& Cell identifiers \\
\end{tabular}

% ------------------------------------------------

{\bf Heap Terms in {\LambdaS}:} as before, heap terms are
``quiescent'' (including value statements):

\hmm
\begin{tabular}[t]{lcll}
$H$  & $::= $ & $x = V$
              $\mid$ $H$ {\tt ;} $H$                   & (as before) \\
     & $\mid$ & {\tt heap}                      \hmmmm & Heap allocator  \\
     & $\mid$ & {\tt {empty}({O}$_j$)}
                $\mid$ {\tt {error}({O}$_j$)}
                $\mid$ {\tt {\tt full}({O}$_j$,$V$)} \hmmmm & Empty, error, full cells
\end{tabular}

% ----------------------------------------------------------------

The syntactic equivalence rules ($\alpha$-renaming, semicolons,
barriers) remain unchanged.

% ----------------------------------------------------------------

\subsection{{\LambdaS} Reduction Rules}

\label{sec-LambdaS-reduction-rules}

{\bf New lifting rules:}
Here, $t$ represents a variable which does not otherwise occur, and $e$ {\isnotin} {\it SE}:

\hmm
\begin{tabular}[t]{llll}
% ------------
{\tt S-Store($e$,$e_2$)} &
   \goesto &
   {\tt ( $t$ = $e$ ; S-Store($t$,$e_2$) )} \hmmmm &
   (LiftS-Store1) \\
% ----
{\tt S-Store($e_1$,$e$)} &
   \goesto &
   {\tt ( $t$ = $e$ ; S-Store($e_1$,$t$) )} \hmmmm &
   (LiftS-Store2)
\end{tabular}


% ----------------

{\bf Cell operations:} {\tt allocate()} creates a new memory cell,
named by a new cell identifier:

\hmm
\begin{tabular}[t]{llll}
{\tt ( heap ; $x$ = allocate() )} &
\goesto &
{\tt ( heap ; empty({O}$_j$); $x$ = {O}$_j$ )} \hmm &
(Alloc) \\
% ----
& & \hm where {\tt {O}$_j$} is a new cell identifier \\
\end{tabular}

The {\tt heap} term remains unchanged; it merely enables allocation.
Because there are no rules to move the {\tt heap} term into
$\lambda$'s, into conditionals or below barriers, allocation cannot
occur in such regions; allocation can only occur in ``exposed''
computations.  This rule also sequentializes: only one allocation can
occur at a time.  This can be trivially relaxed to a fixed degree of
parallelism $p$ by introducing $p$ {\tt heap} terms at the start.  It
can even be relaxed to an unlimited degree of parallelism by adding
the reduction rule:

\hmm {\tt heap} {\goesto} {\tt heap} ; {\tt heap}

(we merely have to ensure that our standard reduction strategy does
not get stuck in this rule.)  We can store a value into an empty cell,
but not into a full cell:

\hmm
\begin{tabular}[t]{llll}
{\tt ({empty}({O}$_j$); S-Store({O}$_j$, $v$))} &
\goesto &
{\tt {\tt full}({O}$_j$, $v$)} \hmmmm &
(S-Store) \\
% ----------------
{\tt ({\tt full}({O}$_j$, $v$); S-Store({O}$_j$, $w$))} &
\goesto &
{\tt error({O}$_j$)} \hmmmm &
(S-StoreErr)
\end{tabular}

The argument terms must be a cell identifier and a value, not
arbitrary expressions, \ie\ a cell can only store a value.  The
I-Fetch and M-Fetch rules say that a value can be extracted from a
full cell.  However, they differ in the resulting state of the cell:

\hmm
\begin{tabular}[t]{llll}
{\tt ({\tt full}({O}$_j$, $v$); $x$ = I-Fetch({O}$_j$))}
& \goesto &
{\tt ({\tt full}({O}$_j$, $v$); $x$ = $v$)} \hmmmm &
(I-Fetch) \\
% ----
{\tt ({\tt full}({O}$_j$, $v$); $x$ = M-Fetch({O}$_j$))}
& \goesto &
{\tt ({empty}({O}$_j$); $x$ = $v$)} \hmmmm &
(M-Fetch) \\
\end{tabular}

I-Fetch leaves the cell unchanged, allowing further reads. M-Fetch
empties the cell, requiring another {\tt S-Store} before further
reads.  This captures the ``I-structure'' and ``M-structure''
synchronization behavior in pH.  These rules make {\LambdaS} {\em
non-deterministic}.  Consider these two program fragments:

\hmm
\begin{tabular}[t]{llll}
		{\hm} &
		{\tt empty({O}$_1$) ;} &
		{\hm} &
		{\tt empty({O}$_1$) ;} \\

\makebox[2em][l]{\hm} &
\makebox[3in][l]{\tt S-Store({O}$_1$, $v$) ;} &
\makebox[2em][l]{\hm} &
                {\tt S-Store({O}$_2$, $m$) ;} \\
% ----------------
                {\hm} &
                {\tt S-Store({O}$_1$, $w$) ;} &
                {\hm} &
                {\tt S-Store({O}$_2$, $n$) ;} \\
% ----------------
                {\hm} &
                {\tt x = I-Fetch({O}$_1$)} &
                {\hm} &
                {\tt y = M-Fetch({O}$_2$)}
\end{tabular}

Since ``{\tt{;}}'' permits various orderings, we can produce any of
the following outcomes (respectively):

\hmm
\begin{tabular}[t]{llll}
\makebox[2em][l]{\goestoto} &
\makebox[3in][l]{\tt Error({O}$_1$); x = I-Fetch({O}$_1$)} &
\makebox[2em][l]{\goestoto} &
                {\tt Error({O}$_2$); y = M-Fetch({O}$_1$)} \\
% ----------------
                or &
                {\tt Error({O}$_1$); x = $v$} &
                or &
                {\tt Full({O}$_2$, $m$); y = $n$} \\
% ----------------
                or &
                {\tt Error({O}$_1$); x = $w$} &
                or &
                {\tt Full({O}$_2$, $n$); y = $m$}
\end{tabular}

% ----------------------------------------------------------------

\subsection{Properties of {\LambdaS}}

Print{\LL\RR} and Print*{\LL\RR} remain unchanged.  Print*{\LL\RR} can
now contain more than one element.  Print monotonicity
(Prop.~{\ref{prop-print-monotonicity}}) continues to hold, but Print
confluence (Prop.~{\ref{prop-print-confluence}}), Print* determinacy
(Prop.~{\ref{prop-printstar-determinacy}}), and Print* preservation
(Prop.~{\ref{prop-printstar-preservation}}) no longer hold; performing
an {\tt M-Fetch} may preclude certain reductions that would have been
possible by doing that {\tt M-Fetch} later.  The net effect is that
the set of reachable values becomes smaller.  Thus, Print*
preservation (Prop.~{\ref{prop-printstar-preservation}}) must be
weakened:
\begin{Proposition}[Print* contraction]
If $e$ {\goestoto} $e_1$ then Print*{\LL}$e_1${\RR} $\subseteq$ Print*{\LL}$e${\RR}
\end{Proposition}
All other propositions continue to hold: Stability of terminated terms
(Prop.~{\ref{prop-stability}}); Opacity of post-regions
(Prop.~{\ref{prop-post-region-opacity}}); Barrier associativity
(Prop.~{\ref{prop-barrier-associativity}}); Barriers constrain results
(Prop.~{\ref{prop-barrier-constraining}}), and GC$_v$ of unreachable
terminated terms (Prop.~{\ref{prop-GCv}}).  A more aggressive GC rule
could also eliminate {\tt S-Store}'s and full cells for which it can be
shown that no matching {\tt I-} or {\tt M-Fetch} is possible.

% ----------------------------------------------------------------

\subsection{I-Structure Subset of {\LambdaS}}

{\bf Definition (I-structure subset):} $\lambda_I$ is {\LambdaS}
without the {\tt M-Fetch} syntax and rules.  

This subset is important
because cells with {\tt S-Store} and {\tt I-Fetch} operations express
the same idea as ``logic variables'', ``single-assignment variables'',
``communication variables'', {\etc} found in logic and constraint
programming languages.  If a reduction sequence terminates without a
store error, then the print-result is unique:
\begin{Proposition}[Termination is unique (in $\lambda_I$)]
If $e$ {\goestoto} $e'$ and $e'$ is terminated and error-free, \\
\hmm then Print*{\LL}$e${\RR} $=$ \{ Print{\LL}$e'${\RR} \}
\end{Proposition}
and all reduction sequences produce a store error on a location {\tt
{O}$_j$} if any one of them does:
\begin{Proposition}[Store error confluence (in $\lambda_I$)]
If $e$ {\goestoto} $e_1$ and $e$ {\goestoto} $e_2$, \\
\hmm and $e_1$ is $C[${\tt error(O$_j$)}$]$,
then $e_2$ {\goestoto} $e'_2$,
where $e'_2$ is $C'[${\tt error(O$_j$)}$]$
\end{Proposition}
Thus, although $\lambda_I$ is non-deterministic (as demonstrated in
the left column of the example in Section
{\ref{sec-LambdaS-reduction-rules}}), it is more benign: if we
consider all programs containing any {\tt error()} as equivalent, then
$\lambda_I$ can be considered to produce deterministic results (this
is exactly the view taken in the language pH).

% ================================================================

\section{Reduction Strategies for {\LambdaS}}

\label{sec-standard-reduction}

A {\em reduction strategy\/} is a method to choose amongst many
available redexes.  Traditionally, a {\em standard\/} reduction
strategy $\sigma$ produces a term with at least as much information as
is obtainable from any other strategy, {\ie} if \mbox{$e${\goestoto}
$e_1$} in the calculus, then there is an $e_2$ such that
{\mbox{$e$\goestotosigma $e_2$}} according to the standard reduction
strategy $\sigma$, and Print{\LL}$e_1${\RR} $\sqsubseteq$
Print{\LL}$e_2${\RR}.  This notion needs elaboration in the presence
of non-determinism.  Consider the following example (let {\tt x} be an
empty cell):

\beginid
\{  S-Store(x,1);
   (  y1 = M-Fetch(x)  ---  S-Store(x,2) );          $(F_1)$
   y2 = M-Fetch(x)                                   $(F_2)$
in
   (y1, y2) \}
\endid

The two {\tt M-Fetch} operations may execute in any order.  If $F_1$
executes first, the result of the block will be (1,2).  If $F_2$
executes first, then $F_1$ waits on an empty cell, and the result is
($\bot$,1).  No {\em deterministic\/} strategy can produce both
outcomes.  This motivates the following two variants of standard
reduction.  Let Print$\stackrel{*}{_\sigma}${\LL\RR} be a version of
Print*{\LL\RR} that uses only reductions permitted by the strategy.

{\bf Definition (Strong and Weak standard reduction):} A reduction strategy
$\sigma$ is {\em strongly standard\/} when
\hmm ${\forall}e$. Print$\stackrel{*}{_\sigma}${\LL$e$\RR}
$=$
Print*{\LL$e$\RR} \hmm
and {\em weakly standard\/} when
\hmm ${\forall}e$. Print$\stackrel{*}{_\sigma}${\LL$e$\RR}
$\subseteq$
Print*{\LL$e$\RR}.

Any deterministic strategy can only hope to be weakly standard.  But
even such a strategy is non-trivial.  If we threw in the (irrelevant)
statement {``\mbox{\tt y3=$\bot_y$}''} in the above example, it must
not get stuck in $\bot_y$ and produce ($\bot$,$\bot$); it must still
produce either (1,2) or ($\bot$,1).

In this section, we develop a weakly standard {\em parallel\/}
strategy.  We first define a {\em kernel\/} language, a subset of $E$
(assuring ourselves that we have not thereby lost expressive power).
Then, we limit instantiation and reduction to the outermost parts of
the term.  This enforces the barrier synchronization discipline and
prevents infinite recursion; it also harmlessly postpones some
operations which can safely be left until they appear in an exposed
context.  Finally, we ensure that we choose {\em fairly\/} among
available instantiations, to avoid getting stuck in an infinite
sequence of reductions that are irrelevant to the observable part of a
term.

% ----------------

The kernel language is defined by the following (compare with Fig. \ref{fig-lambda-s-syntax}):

\hmm
\begin{tabular}[t]{lcl}
\multicolumn{3}{l}{\bf Kernel Terms:} \\
$E$  & $::=$  & $x$ $\mid$ $SE$ $SE$ $\mid$ ${\lambda}x.E$ $\mid$ \{ $S$ {\tt in} $SE$ \}                     \\
     & $\mid$ & {\tt Cond}($SE$,$E$,$E$) $\mid$ PF$_k$($SE_1$,$\cdots$,$SE_k$)
                $\mid$ CN$_0$ $\mid$ \underline{CN$_k$}($x_1$,$\cdots$ $x_k$) \\
     & $\mid$ & {\tt allocate()} $\mid$ {\tt O}$_j$
                $\mid$ {\tt I-Fetch}($SE$)
                $\mid$ {\tt M-Fetch}($SE$) \\
$S$  & $::=$  & {\emptystmt} $\mid$ $x = E$ $\mid$ $S$ {\tt ;} $S$ $\mid$ $S$ {\BAR}  $S$ \\
     & $\mid$ & {\tt heap}
                $\mid$ {\tt S-Store($SE$,$SE$)}
                $\mid$ {\tt empty({O}$_j$)}
                $\mid$ {\tt error({O}$_j$)}
                $\mid$ {\tt full({O}$_j$,$V$)}
\end{tabular}

An initial term can be {\em kernelized\/} by repeated application of
the ``lifting'' rules: LiftB, LiftAp1, LiftAp2, LiftCond, LiftPF,
LiftS-Store1, LiftS-Store2, and Cons.

% \hmm
% \begin{tabular}[t]{llll}
% \multicolumn{3}{l}{In the lift rules below, $e$ {\isnotin} {\it SE}:}\\
% % --------
% \{ $S$ in $e$ \}         & \goesto & \{ $S$ {\tt ;} $t$ $=$ $e$ in $t$ \}
% 					& (LiftB) \\
% % --------
% ($e$ $e_2$)              & \goesto & \{ $t$ $=$ $e$ in $t$ $e_2$ \}
% 					& (LiftAp1) \\
% % --------
% ($e_1$ $e$)              & \goesto & \{ $t$ $=$ $e$ in $e_1$ $t$ \}
% 					& (LiftAp2) \\
% % --------
% {\tt Cond($e$, $e_1$, $e_2$) } &
%     \goesto &
%     {\tt \{ $t$ = $e$ in Cond($t$, $e_1$, $e_2$) \} } \hmm &
%     (LiftCond) \\
% % --------
% {\tt $PF_k$($\cdots$, $e$, $\cdots$) } &
%     \goesto &
%     {\tt \{ $t$ = $e$ in $PF_k$($\cdots$, $t$, $\cdots$) \} } \hmm &
%     (LiftPF) \\
% % --------
%       CN$_k$($\cdots$, $e_j$, $\cdots$) &
%       \goesto &
%       {\tt \{ $\cdots$ ; $t_j$ = $e_j$; $\cdots$ in \underline{\rm CN$_k$}( $\cdots$, $t_j$, $\cdots$) \}} &
%       (Cons) \\
% % ------------
%       {\tt S-Store($e$,$e_2$)} &
%       \goesto &
%       {\tt ( $t$ = $e$ ; S-Store($t$,$e_2$) )} \hmmmm &
%       (LiftS-Store1) \\
% % ------------
%       {\tt S-Store($e_1$,$e$)} &
%       \goesto &
%       {\tt ( $t$ = $e$ ; S-Store($e_1$,$t$) )}        &
%       (LiftS-Store2)
% \end{tabular}

\begin{Proposition}[Kernelization confluence]
kernelization is confluent up to syntactic equivalence
($\alpha$-renaming, properties of ``{\tt ;}'' and ``{\BAR}'') and is
strongly normalizing (always terminates).
\end{Proposition}
\begin{Proposition}[Kernelization is static]
A kernel expression remains a kernel expression after further reduction.
\end{Proposition}
\begin{Proposition}[Expressivity of kernel language]
If $e_k$ is the kernelized version of $e$, then \\
\hmm \mbox{\rm Print*{\LL}$e${\RR} $=$ Print*{\LL}$e_k${\RR}}.
\end{Proposition}

The remaining reduction rules are called {\em dynamic\/} rules:
{\BetaLet}, Inst2, Flat, CondT, CondF, $\delta$, Proj, BAR1,
Alloc, S-Store, S-StoreErr, I-Fetch, M-Fetch.

% \hmm
%   \begin{tabular}[t]{llll}
%   % ---
%     $({\lambda}x.e_1) \; e_2$  &
%     {\goesto} &
%     \{ $t$ $=$ $e_2$ in $e_1[t/x]$ \} &
%     ({\BetaLet})\\
%   % ---
%     $x$ $=$ $a$ ; $SC[x]$ &
%      \goesto &
%     $x$ $=$ $a$ ; $SC[a]$             & (Inst2) \\
%   % ---
%     $x$ $=$ \{ $S$ in $e$ \} &
%     \goesto &
%     $x$ $=$ $e'$ {\tt ;} $S'$
%     & (Flat) \\
%   % ---
%     {\tt Cond(True, $e_1$, $e_2$)} &
%     \goesto &
%     $e_1$ \hmmmm &
%     (CondT) \\
%    % ---
%     {\tt Cond(False, $e_1$, $e_2$)} &
%     \goesto &
%     $e_2$ \hmmmm &
%     (CondF) \\
%    % ---
%     PF$_k$($v_k$, $\cdots$, $v_k$) &
%     \goesto &
%     $v$ \hmmm &
%     ($\delta$) \\
%    % ---
%     {\tt proj$_j$(\underline{\rm CN$_k$}($x_1$, $\cdots$, $x_j$, $\cdots$))} &
%     \goesto &
%     $x_j$ \hmmm &
%     (Proj) \\
%    % ---
%     {\emptystmt} {\BAR} $S$ &
%     \goesto &
%     $S$            \hmmmm &
%     (BAR1) \\
%   % ---
%     $S$ {\BAR} {\emptystmt} &
%     \goesto &
%     $S$            \hmmmm &
%     (BAR2) \\
%   % ---
%     {\tt ( heap; $x$ = allocate() )} &
%     \goesto &
%     {\tt ( heap; ( empty({O}$_j$); $x$ = {O}$_j$ ))} &
%     (Alloc) \\
%   % ----
%     & & \hm where {\tt {O}$_j$} is a new cell identifier \\
%   % ----
%     {\tt ({empty}({O}$_j$); S-Store({O}$_j$, $v$))} &
%     \goesto &
%     {\tt {\tt full}({O}$_j$, $v$)} &
%     (S-Store) \\
%   % ----
%     {\tt ({\tt full}({O}$_j$, $v$); S-Store({O}$_j$, $w$))} &
%     \goesto &
%     {\tt {\tt error}({O}$_j$)} &
%     (S-StoreErr) \\
%   % ----
%     {\tt ({\tt full}({O}$_j$, $v$); $x$ = I-Fetch({O}$_j$))}
%     & \goesto &
%     {\tt ({full}({O}$_j$, $v$); $x$ = $v$)} &
%     (I-Fetch) \\
%   % ----
%     {\tt ({\tt full}({O}$_j$, $v$); $x$ = M-Fetch({O}$_j$))}
%     & \goesto &
%     {\tt ({empty}({O}$_j$); $x$ = $v$)} &
%     (M-Fetch)
%   \end{tabular}

% ----------------

{\bf Limited contexts for instantiation and reduction:} We want to
perform reductions only where computations are ``exposed'' (avoiding
$\lambda$-bodies, arms of conditionals, and post-regions) and we want
to prevent useless unfolding of cyclic data structures.  We thus limit the
contexts\footnote{ Technically we need to specify, separately,
contexts for plugging in an $E$ given an $E$, for plugging in an $S$
given an $E$, for plugging in an $E$ given an $S$, and so on.  We
overload things, hoping the meaning is always clear.  } where an
identifier may be instantiated and where reductions may occur:

\hmm
\begin{tabular}[t]{lclc}
\multicolumn{4}{l}{\bf Limited instantiation contexts:}\\
$C[\;]$ & $::=$   & $[\;]$ \hm
                    $\mid$ $[\;]$ $SE$ \hm
                    $\mid$ {\tt Cond}($[\;]$,$E$,$E$) \hm
                    $\mid$ PF$_k$($\cdots$,$[\;]$,$\cdots$) \\
$SC[\;]$ & $::=$  & $x = C[\;]$ \hm
                    $\mid$ $SC[\;]$ {\tt ;} $S$ \hm
                    $\mid$ $SC[\;]$ {\BAR} $S$ \hm
                    $\mid$ {\tt S-Store}($C[\;]$, $E$) \hm
                    $\mid$ {\tt S-Store}($E$, $C[\;]$) \\
\multicolumn{4}{l}{\bf Limited reduction contexts:}\\
$C[\;]$ & $::=$  & $[\;]$ \hm $\mid$ \{ $SC[\;]$ {\tt in} $SE$ \} \\
$SC[\;]$ & $::=$  & $[\;]$ \hm
                    $\mid$ $x = [\;]$ \hm
                    $\mid$ $SC[\;]$ {\tt ;} $S$
                    $\mid$ $SC[\;]$ {\BAR} $S$ \hm
\end{tabular}

% ----------------

{\bf Fairness:} The only remaining way to get stuck in
an irrelevant sequence of reductions is by repeatedly
applying recursive $\lambda$-expressions.  We avoid this by insuring
that we instantiate only a finite amount before turning our attention to
other reductions.  We decorate a $\lambda$-expression with a positive
integer, decrementing it each time we instantiate it.  Eventually, the
decoration reaches zero, disallowing further instantiation:

\hmm
\begin{tabular}[t]{lllll}
% ----
$x$ $=$ $a$ ; $SC[x]$ &
\goesto &
$x$ $=$ $a$ ; $SC[a]$ &
$a$ $\neq$ ${\lambda}^ny.e$ \hmm &
(Inst2a) \\
% ----
$x$ $=$ ${\lambda}^ny.e$ ; $SC[x]$ &
\goesto &
$x$ $=$ ${\lambda}^{n-m}y.e$ ; $SC[{\lambda}^my.e]$  \hmm &
$n \ge m>0$ \hmm &
(Inst2b) \\
\end{tabular}

% ----------------
\parbox{\textwidth}{
\hdivider\\
{\bf Definition ($\sigma_n$, the weak standard reduction strategies for {\LambdaS})} \\
\hm 1. Compute the kernel form of the initial term. \\
\hm 2. While the term is not a terminated term: \\
    \hmmm 2.1 Decorate all $\lambda$ abstractions with the positive integer $n>0$. \\
    \hmmm 2.2 Apply the dynamic rules (with limited contexts, \etc), in
    any order, even in parallel, \\
    \hmmm \hmm until no longer possible. \\
\hdivider}

This is a family of strategies, parameterized by $n$ and by the
choices in Step 2.2.  Still, for any $n$, each invocation of this step
will always terminate.  The choices in this step represent a kind of
non-determinism.  For {\LambdaC} and {\LambdaB}, this non-determinism
is benign---there is still a unique outcome, and this strategy will
find it, even if $n=1$ (and so it is strongly standard).  However in
{\LambdaS} any particular choice of $n$, no matter how large, can
force the program's non-determinism to be resolved too early, thereby
ruling out some outcomes. Consider this variant on our previous
example:

\beginid
\{  f =  $\lambda$j. if (j > 1) then f (j-1)
            else \{  (  y = M-Fetch(x) --- S-Store(x,2))   $(F_1)$
                 in
                    y \}
   S-Store(x,1);
   y1 = f $m$;
   y2 = M-Fetch(x)                                         $(F_2)$
in
   (y1, y2) \}
\endid

Now {\tt f} must be instantiated $m$ times before $F_1$ executes.  Again, if
$F_1$ executes before $F_2$, the result is (1,2), but if $F_2$
executes first, the result is ($\bot$,1).  However, if $n<m$, it
forces us to execute $F_2$ first, so the only possible outcome is
($\bot$,1).

% ----------------

{\bf Other interesting reduction strategies:} Closely related is the
strategy $\sigma$ which non-de\-ter\-minis\-ti\-cal\-ly chooses the $n$ used to
annotate the $\lambda$'s at each step.  By choosing a sufficiently
large $n$ at each step we insure that every possible outcome can be
reached by some choice of reductions within the strategy.  Thus,
$\sigma$ is strongly standard.

Suppose we ignore fairness; call this strategy $\sigma_0$.  This would
have the same termination behavior as $\sigma_n$, but may print
less of an answer than $\sigma_n$.  Consider this program:

\beginid
\{   K = $\lambda$x.$\lambda$y.x ;   loop = $\lambda$x.loop x    in    K v (loop a) \}
\endid

Neither $\sigma_n$ nor $\sigma_0$ will terminate; however, under
$\sigma_n$ we will eventually print (the value of) {\tt v}, whereas
under $\sigma_0$ we may print $\bot$ forever by never reducing the
{\tt K} application.  For programs that {\em do\/} have a terminal
form, $\sigma_0$ is adequate---fairness is not necessary:

\begin{Proposition}[$\sigma_0$ is standard for terminating terms] \hm \\
\hmm If $e$ {\goestoto} $e_1$ and $e_1$ {\isin} $ET$, then $e$ {\goestotosigmazero} $e_2$ and
Print{\LL}$e_1${\RR} $\sqsubseteq$ Print{\LL}$e_2${\RR}
\end{Proposition}

Recall that {\LambdaC} (purely functional) {\em is} deterministic.  A
{\em lazy\/} reduction strategy focuses on ``outermost'' redexes,
always picking one that is needed to produce the answer.  Ariola
{\etal} {\cite{ariola96d}} show such a strategy, and show that it is
standard for {\LambdaC}.  We can give a parallel strategy $\sigma_{\rm
plazy}$ identical to $\sigma_n$, except that we continue evaluation
only while the term is not ground-printing (defined in
Sec.~\ref{sec-LambdaC-stable-terms}).  The final term may still
contain redexes, but further reductions will not affect the printed
value (and so termination here makes sense).  Indeed, $\sigma_{\rm
plazy}$ finds answers equivalent to those found by lazy reduction.

% ================================================================

\section{Conclusion}

In this paper, we have described {\LambdaS}, a fine-grained parallel
extension of the $\lambda$-calculus with letrec, barriers (for
sequencing), and synchronized side-effects.  The calculus avoids any
encoding into the reduction rules of considerations inspired by
reduction strategy.  This makes the calculus more flexible and,
therefore, more useful for reasoning about program transformations.

Based on the notion of observable information, we have discussed a
number of important properties of {\LambdaS} and its important
sub-calculi, {\LambdaC}, {\LambdaB} and {$\lambda_I$}. We have
described parallel strong and weak standard reduction strategies to
compute the maximum information in a term.  A simple variation of our
strategy subsumes traditional lazy evaluation.

Our barrier semantics capture a robust notion of termination: in
($S_1$ {\BAR} $S_2$), we wait for all of the {\em dynamic\/}
computation in $S_1$.  We believe that this gives {\LambdaS} wide
applicability, and will allow us to model a spectrum of languages:
fine-grained implicitly parallel languages like pH and Id; totally
sequential languages (by inserting barriers everywhere); and points in
between, such as Scheme extended with futures.  Barrier sequencing
also makes raw (unsynchronized) side effects manageable locally
without compromising parallelism globally.

We believe that {\LambdaS} is a simple, flexible, and powerful
calculus that will facilitate the study of realistic parallel
languages with side-effects.

% ================================================================

\small

\bibliographystyle{abbrv}

\bibliography{icfp97}


% ----------------------------------------------------------------


% ----------------------------------------------------------------
\end{document}

