% Lambda-talk: formal semantics for pH
%
% Arvind et. al.
% November 20, 1995 ... March 25, 1996 ... July 1996 ... Aug 1996 ... Sep 1996

\documentstyle[11pt, fullpage, 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}
% ----------------
% 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}
% ------------
% ``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
% only not in lncs!!
\newcommand{\ie}{{i.e.,}}
\newcommand{\eg}{{e.g.,}}
\newcommand{\etal}{{et al.}}
\newcommand{\etc}{{etc.}}
\newcommand{\via}{{via}}
\newcommand{\vs}{{vs.}}
\newcommand{\viz}{{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{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}
  }

{\obeyspaces\gdef {\ }}

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

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

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

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

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

% LAMBDA-Let symbol
\newcommand{\LambdaLet}{${\lambda}_{let}$}

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

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

% LAMBDA-I symbol
\newcommand{\LambdaLetI}{${\lambda}_{letI}$}

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

% LAMBDA-BM symbol
\newcommand{\LambdaLetBM}{${\lambda}_{letBM}$}

% 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}{\tt ---}

% UNION

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

% INTERSECT

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

% NEW RULE

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

% DEFINITIONS, PROPOSITIONS, etc.

\newtheorem{Definition}{Definition}

\newtheorem{Proposition}[Definition]{Proposition}

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

\begin{document}

\title{A Lambda Calculus with Letrecs and Barriers}


\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{Invited Paper in 16th Foundations of Software and Theoretical
Computer Science, Hyderabad, India, Dec. 1996}
\trnumber{Computation Structure Group Memo 395}

\maketitle

\bibliographystyle{plain}

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

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


\section{Introduction}

\label{sec-introduction}

It is often said that pure functional languages like
Haskell\cite{Hudak92c} are merely ``syntactic sugar'' for a version of
the lambda calculus extended with constants and data structures.  In
fact the semantics of these languages is more complicated than that,
but an understanding of the lambda calculus is nevertheless crucial in
their study. The lambda calculus also plays an important role as a
vehicle for explaining the semantics of a much broader class of
languages such as Lisp\cite{Steele90}, ML\cite{Milner90a},
Scheme\cite{Clinger91}, Id{\cite{Nikhil91b}} and pH{\cite{Aditya95a}}
(a parallel dialect of Haskell).  The importance of a small, simple,
formal system cannot be overstated: at the very least it helps in
teaching the language and building intuitions about it; it is also an
unambiguous point of appeal for reasoning about the correctness of
program equivalences.

A practically important class of program equivalences are the
optimizations performed by a compiler.  The lambda calculus and its
variants are used as the basis for kernel languages in some compilers.
The task of designing the required transformations and optimizations
is eased by restricting attention to a simpler and more regular
language.

In this paper we will describe some extensions which make the pure
lambda calculus much more useful, both for discussing the semantic
essence of ``real'' languages, and also as an intermediate language
for a compiler.

We will begin by a quick overview of the pure lambda calculus extended
with constants.  This is followed by a discussion of inadequacy of
this system to address some pragmatic aspects of even purely
functional languages (Sect.~\ref{sec-Lambda-Problems}).  In
Sect.~\ref{sec-LambdaLet} we describe {\LambdaLet}, a lambda calculus
with recursive let blocks (i.e., letrecs), and discuss why it is more
appropriate as a kernel language; we also discuss the complications
letrecs add. In Sect.~\ref{sec-LambdaLetB}, we discuss {\LambdaLetB}
which is {\LambdaLet} extended with sequentializing constructs called
barriers.  We then mention some more extensions we have studied, which
continue to be the target of active research.

\section{The Pure $\lambda$ Calculus with Constants}

\label{sec-Lambda}

We begin by looking at the pure $\lambda$ calculus.  The calculus
itself is very small, yet it is possible to express every sequential
computable function as a $\lambda$-expression.  This power comes from
several important notions.  First, we can write anonymous (unnamed)
functions.  Second, the calculus is higher-order.  We can thus write
functions which take functions as arguments and return functions as
results.  Finally, $\lambda$ calculus does not limit {\em where} we
are permitted to perform evaluation.  As a result, we can discuss the
effects of evaluation order on the calculus.

The material in this section will be very familiar to those who have
encountered the $\lambda$ calculus before.  This presentation
highlights the aspects of $\lambda$ calculus which are important to
later sections and introduces some notation which will recur
throughout the paper.

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

\subsection{Syntax}

\label{sec-lambda-syntax}

The $\lambda$ calculus has by far the simplest syntax of any of the
calculi described here (We concern ourselves only with abstract
syntax---we use parentheses freely to clarify grouping.  We also
freely define syntactic categories as subsets or unions of other ones,
trusting that this will cause no confusion):
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$E$  & $::=$  & $x$                            & Identifiers \\
     & $\mid$ & $\lambda x.E$                 & Abstractions \\
     & $\mid$ & $E\;E$                        & Applications \\
     & $\mid$ & {\tt cond}($E$,$E$,$E$)      & Conditionals \\
     & $\mid$ & PF$_k$($E_1$,$\cdots$,$E_k$) & Primitive function applications, $k \geq 1$ \\
     & $\mid$ & CN$_0$                       & Constants \\
     & $\mid$ & CN$_k$($E_1$,$\cdots$,$E_k$) & Constructor applications, $k \geq 1$
\\
% ---
PF$_1$ &
$::=$  &
{\tt not} $\mid$ {\tt Proj$_1$} $\mid$ {\tt Proj$_2$} $\mid$ $\cdots$  \hm &
Primitive functions of arity 1  \\
% ---
PF$_2$ &
$::=$  &
{\tt +} $\mid$ {\tt -} $\mid$ $\cdots$ &
Primitive functions of arity 2 {} \\
% ---
$\vdots$ &      &    & \\
CN$_0$ & $::=$  & {\it Number}  $\mid$ {\it Boolean}  & Constructors of arity 1 {} \\
CN$_2$ & $::=$  & {\tt cons}   $\mid$  $\cdots$       & Constructors of arity 2 {} \\
$\vdots$ &      &    & 
\end{tabular}
\end{tabbing}

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

\subsection{Renaming: An Equivalence Rule}

\label{sec-lambda-rename} 

In many calculi there are some choices that, though leading to
syntactically different terms, do not lead to terms that differ in any
{\em essential\/} way.  For example, in renaming a bound variable {\tt
x} to avoid free-variable capture, it does not really matter whether
the fresh name chosen is {\tt y} or {\tt z}, even though the two
choices lead to terms that are not syntactically ``equal''.  $\lambda$
calculus formalizes this notion as $\alpha$ reduction\footnote{ As
usual, the notation \mbox{$e$ {\goesto} $e_1$} means that $e$ reduces
to $e_1$ by a single application of a reduction rule to $e$ or to one
of its subterms, and \mbox{$e$ {\goestoto} $e_1$} means that $e$
reduces to $e_1$ by a finite sequence (zero or more) of such steps.  A
term or subterm which is capable of reduction by one of the rules is
called a {\em redex}.  }:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$\lambda x.E$   &\goesto&       $\lambda x'.E[x/x']$ \hmmmm   & $x' \notin FV(E)$
\end{tabular}
\end{tabbing}
Here we read $E[x/x']$ as ``substitute $x'$ for for every free
occurrence of $x$ in E''.  Ordinarily, we assume that terms $e_{1}$
and $e_{2}$ interconvertible using only $\alpha$ renaming are {\em
equivalent}, and write $e_{1} \equiv e_{2}$.  A reduction rule (to be
introduced later) is applicable to a term if it is applicable to {\it
any\/} equivalent term.

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

\subsection{Reduction Rules for the $\lambda$ Calculus}

\label{sec-lambda-reduce}

The most critical rule in $\lambda$ calculus is the $\beta$ rule:
\begin{tabbing}
\hm
$({\lambda}x.e_1) \; e_2$ {\goesto} $e_1'[e_2/x]$\\
\hm     where $e_{1}'$ is a renaming of $e_{1}$ to avoid free variable
capture
\end{tabbing}
Any expression to which the $\beta$ rule can be applied is referred to
as a $\beta$ redex.
Note that redexes can occur anywhere in a $\lambda$ expression; for
example, in $\lambda x. (\underline{(\lambda y. \underline{(\lambda z.
z)\; y})\; x})\; x$ both the underlined subexpressions are $\beta$
redexes.

$\delta$ rules specify the behavior of each primitive function.
They are all of the form:
\begin{tabbing}
\hm
\begin{tabular}[t]{lllll}
PF$_k$($v_1$,$\cdots$,$v_k$)&
    \goesto &
    $v$ \hmmmm &
    ($\delta$)
\end{tabular}
\end{tabbing}
Obviously we cannot list all the $\delta$ rules here, but an example is:
\begin{tabbing}
\hm
\begin{tabular}[t]{llll}
{\tt +(\underline{n}, \underline{m})} &
    \goesto &
    \underline{\tt p} \hm &
    where
\underline{\tt n}, \underline{\tt m} and \underline{\tt p} represent numbers and
          $p = n+m$
\end{tabular}
\end{tabbing}
This rule should be read as saying: the term consisting of
``{\tt{+}}'' applied to two numerical constants may be rewritten as the constant
that represents the sum of those two numbers.

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

Projection functions select fields of constructed values:
\begin{tabbing}
\hm
\begin{tabular}[t]{lllll}
{\tt proj$_j$({\rm CN$_k$}($e_1$, $\cdots$, $e_k$))} &
    \goesto &
    $e_j$ \hmmm &
    $1 \leq j \leq k$ \hmmm &
    (Proj)
\end{tabular}
\end{tabbing}

{\em Cond\/} rules specify the behavior of conditional expressions:
\begin{tabbing}
\hm
\begin{tabular}[t]{llll}
{\tt cond(True, $e_1$, $e_2$)} &
    \goesto &
    $e_1$ \hmmmm &
    (CondT) \\
% ---
{\tt cond(False, $e_1$, $e_2$)} &
    \goesto &
    $e_2$ \hmmmm &
    (CondF) \\
\end{tabular}
\end{tabbing}

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

\subsection{Recursion}

One thing $\lambda$ calculus lacks is direct provision for recursion.
For example, we cannot write the factorial function directly, as we
might in an ordinary programming language:
\begin{tabbing}
\hm
\begin{tabular}{lcl}
{\tt fact}     &$=$&   $\lambda n .${\tt cond($n=0$, $1$, $n * $(fact ($n-1$)))}
\end{tabular}
\end{tabbing}
The problem is that {\tt fact} isn't well defined on the right hand
side of the above equation.  
Instead, we have to abstract away the recursive call to {\tt fact}:
\begin{tabbing}
\hm
\begin{tabular}{lcl}
{\tt fact}     &$=$&   {\tt fact$'$} {\tt fact}\\
{\tt fact$'$}  &$=$&   $\lambda f. \lambda n .${\tt cond($n=0$, $1$, $n * $($f$ ($n-1$)))}
\end{tabular}
\end{tabbing}
Now the {\tt fact} function we desire is the fixed point of {\tt
fact$'$}, so we can write {\tt fact} using the fixed-point combinator
$Y$:
\begin{tabbing}
\hm
\begin{tabular}{lcl}
{\tt fact}      &$=$&   $Y$ {\tt fact$'$}\\
$Y$             &$=$&   $\lambda f. (\lambda x. f\; (x\; x))(\lambda x. f\; (x\; x))$
\end{tabular}
\end{tabbing}

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

\subsection{Confluence and Equivalence}

Because $\lambda$ expressions can contain many redexes, the most
obvious question to be asked is: Is the $\lambda$ calculus confluent?
That is, if we reduce different redexes, can we eventually bring
the resulting terms back together?  The Church-Rosser Theorem says
that we can:
\begin{quote}
The $\lambda$ calculus is confluent: If $e_{1} $\goestoto\ $e_{2}$ and
$e_{1} $\goestoto\ $e_{3}$, then there exists an $e_{4}$ such that $e_{2}
$\goestoto\ $e_{4}$ and $e_{3} $\goestoto\ $e_{4}$.
\end{quote}
Unfortunately, confluence does not guarantee that we {\em will} always
reach $e_{4}$ when we reduce further; it merely states that it is
possible to do so.  Subterms may be infinitely reducible, distracting
us from useful reduction elsewhere.

\subsubsection{Normal Forms of $\lambda$ Expressions}

In functional languages like the $\lambda$ calculus, a program itself
represents the ``answer'' or ``output'' of computation.  The process
of reduction gradually transforms the initial program into a form that
more manifestly represents an answer (\eg\ the reduction of ``2+3'' to
``5'').  Note that the answer may even be infinite, such as an
infinite list of actions for the operating system to perform.  At some
intermediate point of computation, it is possible that the answer has
thus far been only partially manifested.

There are actually many possible definitions of ``answer'' even for
the pure $\lambda$ calculus.  The most obvious definition is {\em normal
form}---no further redexes exist anywhere in the expression.
Because of confluence, we know that the normal form of any expression is
unique (otherwise further reductions could be performed to bring the
distinct terms together!).  In addition, a normal-order reduction
(where the leftmost outermost redex is reduced at every step) is
guaranteed to find the normal form of a term if it exists.

However, many terms do not have a normal
form at all!  One infamous example is the term $\Omega$, which reduces
to itself:
\begin{quote}
$\Omega$ $=$ $(\lambda x. x\;x)\;(\lambda x. x\;x)$ \goesto $(\lambda
x. x\;x)\;(\lambda x. x\;x)$ \goesto $\ldots$
\end{quote}
Thus, while normal form seems to provide a convenient notion of
equality, it leaves open the question of how to treat terms which do
not possess a normal form.

More commonly used is weak head
normal form (WHNF), which can be defined syntactically (using the
category $A$ for ``answer'') as follows:
\begin{tabbing}
\begin{tabular}[t]{lcll}
$A$  & $::=$  & $V$                            & Values \\
     & $\mid$ & $P$                            & Irreducible expressions \\
$V$  & $::=$  & $\lambda x.E$                 & Abstractions \\
     & $\mid$ & CN$_0$                                         & Constants \\
     & $\mid$ & CN$_k$($E_1$,$\cdots$ $E_k$) \hmmmm
                & Constructed values, $k \geq 1$ \\
$P$  & $::=$  & $x$                             & Free variables \\
     & $\mid$ & $P\;E$                        & Applications of irreducibles
\end{tabular}
\end{tabbing}
Values, $V$, play a prominent role in the reduction rules of our later
calculi.

Unfortunately, weak head normal forms are {\em not\/} unique.  For
example, the following terms have the same normal form but are both
already in WHNF:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcl}
$\lambda x. (\lambda y. \lambda z. y)\;x\;x$ \hmm     &and \hmm&   $\lambda x.
(\lambda y. y)\;x$
\end{tabular}
\end{tabbing}
We thus still need to define equivalence between terms.

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

\section{Problems with the $\lambda$ Calculus}

\label{sec-Lambda-Problems}

There are a number of problems with the $\lambda$ calculus that
prevent it from closely mirroring the operation of an actual
programming language implementation---even a purely functional
language such as Haskell.  While the existence of the $Y$
combinator is mathematically fascinating, fixed points do not provide
a simple encapsulation of recursion.  For example, we would like to be
able to declare mutually recursive functions and data structures in
such a way that their definitions are clear and readable; the need to
re-shape such definitions as fixed points plays havoc with such an
endeavor.

More problematic is that the $\lambda$ calculus handles sharing very
poorly indeed.  The problem is in $\beta$ reduction itself.  In the
application $({\lambda}x.e_1) \; e_2$ the traditional $\beta$ rule
makes copies of the argument expression $e_2$ for each occurrence of
the formal parameter $x$.

In an effort to solve this problem, several researchers have added let
blocks to the language and replaced the $\beta$ rule with
$\beta_{G}$\cite{Ariola91a,Launchbury93,Abadi91,Ariola95b}:
\begin{tabbing}
\hm $({\lambda}x.e_1) \; e_2$ {\goesto} \{ $x'$ $=$ $e_2$ in $e_1[x'/x]$ \} 
\hmmmm \hfill ($\beta_{G}$) \\
\hm where $x'$ is a variable which does not otherwise occur.
\end{tabbing}
A central feature of the ${\beta}_G$ rule is that it performs no
substitution at all; instead we add new rules for {\em instantiating
the values of variables}.  These new rules can be designed so that
sharing of subexpressions is preserved.  This also means that the
${\beta}_G$ rule never {\em discards\/} the argument.  This will
affect the semantics of barriers and side-effects.  In short, the
${\beta}_G$ rule preserves the ``graph structure'' of the term, with
shared subterms, instead of the ``tree structure'' of the traditional
$\lambda$ calculus, with replicated subterms.  This is why we use the
subscript $G$, for ``graph.''  In the next section we will use the
$\beta_{G}$ rule as the core of a new calculus, {\LambdaLet}.


The idea of sharing subexpressions to make normal-order reduction
efficient was first tackled by Wadsworth in his D.Phil. Thesis as far
back as 1971 \cite{Wadsworth71}.  In his seminal work, which came to
be known as {\em graph reduction}, he used an explicit graph notation
instead of a textual term notation.  Since the source language was
standard $\lambda$-calculus, there was no issue of recursive or cyclic
terms---the {\em sharing\/} he obtained was just a way to avoid
duplicating the function argument when the formal parameter was used
multiple times in the $\lambda$~ body. Since then several different
let-block extensions to the $\lambda$ calculus have been presented in
the literature to model sharing.  Recently, Launchbury reformulated
Wadsworth's system without using a graph notation by introducing
``let'' expressions into the term syntax \cite{Launchbury93}.  Again,
since the source language was standard $\lambda$~calculus, there was
no issue of recursive or cyclic terms.  Launchbury did not separate
{\em calculus\/} from {\em strategy\/}---he directly gave a set of
rules to implement lazy evaluation.

In {\cite{Ariola95b}}, Ariola {\etal} presented a calculus
which did allow the definition of cyclic terms, but it was restricted
to disallow substitution of a let-bound identifier in the right-hand
side of its own binding, thus side-stepping a full treatment of cyclic
terms.  This work also did not address data structures.

In {\cite{Abadi91}}, Abadi {\etal} also presented a calculus that
dealt with cyclic terms, but it deviated quite far from traditional
$\lambda$-calculus in that it used de Bruijn notation, introduced {\em
environments\/} and a calculus of environments, \etc

The most recent work by Ariola {\cite{ariola96b}} is the first to
introduce a calculus of recursive let-expressions.  Our {\LambdaLet}
is essentially the same as Ariola's system, with some small
differences in the details of the rules of the calculus.


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

\section{{\LambdaLet}: a $\lambda$ Calculus with Letrec Blocks}

\label{sec-LambdaLet}

{\LambdaLet} extends the $\lambda$ calculus with ``letrec blocks'',
allowing us to define shared recursive bindings by binding an
expression to an identifier and then using that identifier in a number
of places.  Our plan of action for this section is as follows.  First
we present the {\LambdaLet} {\em calculus}, \ie\ the syntax of
{\LambdaLet} terms and the reduction rules that allow us to transform
terms and perform ``computation''.  We then define a notion of
printing, which captures the ``important'' information in a term.
Finally, we discuss how we might define a standard reduction strategy
which evaluates let bindings in parallel.

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

\subsection{Syntax}

\label{sec-LambdaLet-syntax}


{\LambdaLet} augments the syntax of $\lambda$ calculus with letrec blocks:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$E$  & \hm $::=$ \hm & $\cdots$                     & as before       \\
     & $\mid$ & \{ $S$ {\tt in} $E$ \}  \hmm & Letrec blocks \\
\\
$S$  & $::=$  & {\emptystmt}                 & Empty statements \\
     & $\mid$ & $x = E$                      & Bindings \\
     & $\mid$ & $S$ {\tt ;} $S$              & Parallel
\end{tabular}
\end{tabbing}
The $S$ in a Letrec block is a composition of parallel statements,
at the leaves of which are bindings and empty statements.  The
identifiers on the left-hand sides of all these bindings must be
pair-wise distinct.  The empty statement is used only as a technical
convenience in {\LambdaLet}; it will become useful in {\LambdaLetB}.
We refer to the final expression in a block as the {\em return
expression\/} of the block.

{\LambdaLet} has {\em ``letrec''\/} scope rules---any identifier on the
left-hand side of any binding in a block may be referred to in any
right-hand side, as well as in the return expression of the block.  In
other words, the collection of bindings in a block should be regarded as
simultaneous, recursive bindings.

In {\LambdaLet} we ensure that constructors are evaluated exactly
once, after which they become ``values'' and are written using an
underline.  The complete syntactic category of expressions therefore
contains these terms too:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$E$  & $::=$  & $\cdots$ \\
     & $\mid$ & \underline{CN$_k$}($E_1$,$\cdots$,$E_k$) \hmmmm & Constructor values, $k \geq 1$ \\
\end{tabular}
\end{tabbing}
Note, however, that the underlined versions of constructors never occur in
unevaluated {\LambdaLet} terms.  For the rest of this section, we
will simply appeal to the reader's intuition on the distinction between
constructors with and without underlines.

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

\subsubsection{Values and Simple Expressions}

\label{sec-LambdaLet-V-and-SE}

In our calculi, as in the $\lambda$ calculus, we need to substitute
various {\em uses\/} of an identifier with the identifier's
definition.  This is called {\em instantiation}.  The way this
operation is defined can have an impact on sharing.  Suppose we have
the following term:
\beginid
(1)        \{  x = (f a);
(2)           y = x;
           in
              w \}
\endid
Suppose we substitute the use of {\tt x} on line (2) by its
definition from line (1):
\beginid
(1)        \{  x = (f a);
(2)           y = (f a);
           in
              w \}
\endid
We now have two copies of ``\makebox{\tt f a},'' which may be an
arbitrarily complicated computation, \ie\ we have replicated the
computation, instead of {\em sharing\/} it.  In versions of the
calculus that include barriers and side-effects, this sharing is
required and not merely an issue of efficiency.

Thus, our instantiation rules must be very careful about which
expressions can be substituted.  To maintain sharing, we identify two
subsets of {\LambdaLet} terms that are substitutable---{\em values\/}
and {\em identifiers}, collectively known as {\em simple expressions}:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$SE$     & $::= $ & $x$  \hmmmm                  & Identifiers \\
         & $\mid$ & $V$                          & Values
\end{tabular}
\end{tabbing}

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

\subsection{{\LambdaLet} Equivalence Rules}

\label{sec-LambdaLet-equivalence-rules}

The first two equivalence rules are analogous to $\alpha$ renaming;
they express the idea that the particular choice of a name for a bound
variable is not important:
\begin{tabbing}
\hm  \begin{tabular}[t]{lll}
         ${\lambda}x.e$            & $\equiv$  & ${\lambda}x'.(e[x'/x])$ \\
         \{ $SC[x=e]_S$ in $e_0$ \}  & $\equiv$  & \{ $SC[x'=e]_S$ in $e_0$ \}$[x'/x]$ \\
       \makebox[0pt][l]
         {\hspace*{1em}where $x'$ does not otherwise occur in
          the program.}
     \end{tabular}
\end{tabbing}
The second set of rules states that the grouping of statements
combined with semicolons is unimportant, as is the presence or absence
of empty statements.
\begin{tabbing}
\hm  \begin{tabular}[t]{lll}
       $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$\\
       {\emptystmt} {\tt ;} $S$            & $\equiv$ & $S$
     \end{tabular}
\end{tabbing}
Recall that we regard a reduction rule to be applicable to a term if
it is applicable to any equivalent term.

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

\subsection{{\LambdaLet} Reduction Rules}

\label{sec-LambdaLet-reduction-rules}

We are now ready to look at the reduction rules themselves.  They can be divided into several groups:
\begin{tabbing}
\hm
\begin{tabular}[t]{ll}
$(1)$ & instantiation;\\
$(2)$ & function application;\\
$(3)$ & lifting; \\
$(4)$ & $\delta$ rules, conditionals, and data structures.
\end{tabular}
\end{tabbing}

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

\subsubsection{Instantiation (Substitution)}

\label{sec-LambdaLet-instantiation}
\label{sec-LambdaLet-contexts}

Given a statement that binds an identifier $x$ to a simple expression
$a$, the following rules permit a use of $x$ to be replaced by $a$.
Note that in all these rules $a$ is a {\it simple expression}, and the
$x$ is free in $C[x]$.
\begin{tabbing}
\hm
\begin{tabular}[t]{lllr}
\{ $x$ $=$ $a$ ; $S$ in $C[x]$ \} \hmm &
\goesto \hmm &
\{ $x$ $=$ $a$ ; $S$ in $C[a]$ \} \hmm &
(Inst1) \\
\\
% ----
($x$ $=$ $a$ ; $SC[x]$)           &
\goesto &
($x$ $=$ $a$ ; $SC[a]$)           &
(Inst2) \\
\\
% ----
$x$ $=$ $a$                         &
\goesto &
$x$ $=$ $C[a]$                    &
(Inst3) \\
\hm where $a = C[x]$
\end{tabular}
\end{tabbing}
The context $C[\;]$ in which instantiation takes place is an
expression with a hole (written as $[\;]$):
\begin{tabbing}
\hm
\begin{tabular}[t]{lcl}
$C[\;]$\hm  & $::=$  & $[\;]$ \hmmmm \hmm $\mid$ \hm ${\lambda}x.C[\;]$ \\
           & $\mid$ & $C[\;]$ $E$ \hmmmm\/ $\mid$ \hm $E$ $C[\;]$ \\
           & $\mid$ & \{ $S$ {\tt in} $C[\;]$ \} \hm\/\/ $\mid$ \hm \{ $SC[\;]$ {\tt in} $E$ \} \\
           & $\mid$   & PF$_k$($\ldots$, $C[\;]$, $\ldots$) \\
           & $\mid$   & CN$_k$($\ldots$, $C[\;]$, $\ldots$) \\
           & $\mid$   & \underline{CN}$_k$($\ldots$, $C[\;]$, $\ldots$)
\end{tabular}
\end{tabbing}
In this definition, $SC[\;]$ is a {\it statement\/} context for an expression;
that is, a statement with a hole in place of one of the subexpressions in it.
It is defined as follows:
\begin{tabbing}
\begin{tabular}[t]{lcl}
$SC[\;]$  & $::=$  & $x = C[\;]$ \hm $\mid$ \hm $SC[\;]$ {\tt ;} $S$
\end{tabular}
\end{tabbing}

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

\subsubsection{Function Application ($\beta$ Reduction)}

As mentioned before, a $\lambda$ expression can be applied to an
argument using the $\beta_{G}$ rule:
\begin{tabbing}
\hm $({\lambda}x.e_1) \; e_2$ {\goesto} \{ $x'$ $=$ $e_2$ in $e_1[x'/x]$ \}
\hfill \hmmmm ($\beta_{G}$) \\
\hm where $x'$ is a variable which does not otherwise occur.
\end{tabbing}

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

\subsubsection{Expression Lifting}

The following rules ``lift'' expressions that are nested in certain ways.  In
all these rules ``\{$S'$ in $e'$\}'' represents an $\alpha$-renaming of
``\{$S$ in $e$\}'' to avoid name conflicts with the surrounding scope, and the
$t$'s represent variables which do not otherwise occur.  The side
conditions $e$ {\isnotin} $SE$ prevent infinite reduction.
\begin{tabbing}
\hm
\begin{tabular}[t]{lllll}
\{ {\emptystmt} in $e$ \} &
\goesto \hm &
$e$ &
&
(Lift0) \\
% --------
$x$ $=$ \{ $S$ in $e$ \} &
\goesto &
($x$ $=$ $e'$ {\tt ;} $S'$) &
&
(Lift1) \\
% --------
\{ $S$ in $e$ \}         &
\goesto &
\{ $S$ {\tt ;} $t$ $=$ $e$ in $t$ \}  &
$e$ {\isnotin} $SE$ &
(Lift2) \\
% --------
($e$ $e_2$)              &
\goesto &
\{ $t$ $=$ $e$ in ($t$ $e_2$) \}             &
$e$ {\isnotin} $SE$ &
(Lift3) \\
% --------
($e_1$ $e$)              &
\goesto &
\{ $t$ $=$ $e$ in ($e_1$ $t$) \}             &
$e$ {\isnotin} $SE$ &
(Lift4)\\
% --------
{\tt cond($e$, $e_1$, $e_2$) } &
\goesto &
\{ $t = e$ in {\tt cond($t$, $e_1$, $e_2$)} \} &
$e$ {\isnotin} {\it SE} & (Lift5) \\
% ------------
{\tt $PF_k$($\cdots$ $e$, $\cdots$) } &
\goesto &
{\tt \{ $t = e$ in $PF_k$($\cdots$ $t$, $\cdots$) \} } &
$e$ {\isnotin} {\it SE} \hm &  (Lift6)
\end{tabular}
\end{tabbing}
The utility of these rules may be seen by considering the following example:
\beginid
\{  f = \{ $S_1$ in ${\lambda}x.e_1$ \};                                  (1)
   x = f a;                                              (2)
in
    \{ $S_2$ in ${\lambda}x.e_2$ \} $e_3$ \}                                 (3)
\endid
Without Lift1, we would not be able to substitute ${\lambda}x.e_1$ for
{\tt f} in line 2.  Similarly, without Lift2, Lift3 and Lift1, we
would not be able to apply ${\lambda}x.e_2$ to $e_3$.

\subsubsection{$\delta$ Rules, Conditionals, and Data Structures}

A rule needs to be added to turn a nonunderlined constructor into the
equivalent underlined constructor.  
\begin{tabbing}
\hm 
      CN$_k$($e_1$, $\cdots$, $e_k$)
      \goesto
      {\tt \{ $t_1$ = $e_1$; $\cdots$ ; $t_k$ = $e_k$ in
        \underline{\rm CN$_k$}($t_1$, $\cdots$, $t_k$) \}}
\end{tabbing}
The $\delta$ and conditional rules from the $\lambda$ calculus carry
over unmodified to {\LambdaLet}.  

\subsection{(Non-)Confluence}

The following theorem by Ariola and Klop \cite{ariola96a} states
that the introduction of let blocks has destroyed confluence:

\begin{Proposition}
[Ariola and Klop] {\LambdaLet} is not confluent.
\end{Proposition}
To see this, consider the following program:
\beginid
{\em Term0:}
\{ odd  = $\lambda$n. cond(n = 0, False, even(n-1));
  even = $\lambda$n. cond(n = 0, True,  odd(n-1));
in
  .. \}
\endid
Suppose we substitute {\tt odd} at its use in {\tt even}.  {\em Term0} becomes:
\beginid
{\em Term1:}
\{ odd  = $\lambda$n. cond(n = 0, False, even(n-1));
  even = $\lambda$n. cond(n = 0, True,  cond((n-1)=0, False, even((n-1)-1)));
in
  .. \}
\endid
Suppose, instead, we substitute {\tt even} at its use in {\tt odd}.  {\em Term0} becomes:
\beginid
{\em Term2:}
\{ odd  = $\lambda$n. cond(n = 0, False, cond((n-1)=0, True, odd((n-1)-1)));
  even = $\lambda$n. cond(n = 0, True,  odd(n-1));
in
  .. \}
\endid
At this point, we can see that it will never be possible to reduce
{\em Term1\/} and {\em Term2\/} to the same term.  For example, in
{\em Term1\/}, if we substitute {\tt even} into the {\tt odd}
definition, the {\tt odd} definition will still contain a call to the
{\tt even} function; this remains true no matter how may times we
repeat this substitution.  In {\tt Term2}, on the other hand, the {\tt
odd} definition has a call to the {\tt odd} function, and if we
subtitute for {\tt odd} this remains true.

This lack of confluence is true even if we permit unrestricted
instantiation, \ie\ if we allowed an identifier to be substituted by
the expression that it is bound to even though it may not be a simple
expression.  Let us call this calculus {\LambdaLetZero}.  Note that
this calculus no longer preserves sharing of computations.
\begin{Proposition}
[Ariola and Klop] {\LambdaLetZero} is not confluent.
\end{Proposition}

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

\subsection{Printable Values and the Print{\LL\RR} Function}

\label{sec-LambdaLet-printable-values}

We now wish to approach the question whether the calculus defined by
these rules makes sense; that is to say, whether there is a consistent
notion of equality which is preserved under transformation of a term
according to the rules.  We accordingly wish to develop a notion of
the observable information contained in a term.

Trying to distinguish terms by comparing their syntax is problematic,
even in the pure $\lambda$ calculus.  However, the problem gets harder
when let blocks are an integral part of the syntax. Consider the
following two terms:
\begin{tabbing}
\hm
\begin{tabular}{ll}
\{ $x=5$ in $5$ \}\hmmm &(M1)\\
\{ $x=3$; $y=2$ in $5$ \} &(M2)
\end{tabular}
\end{tabbing}
M1 and M2 behave essentially the same in all contexts and thus should
be equal but are syntactically very different. It is common to
introduce one or more ``garbage collection'' rules in the calculus to
attempt to remove the irrelevant clutter (see, for
example,{\cite{Ariola95b}}.  But even this is inadequate: as
the (non-)confluence results of Ariola and Klop ({\cite{ariola96a}})
show, there are pairs of terms which ought to be considered equal
which can never reduce to compatible syntactic forms.

We therefore introduce the concept of a ``printable value''.  This is
a rudimentary notion of value---for example, in {\LambdaLet} all
$\lambda$~abstractions are represented by the single symbol
``$\lambda$''.  It is nevertheless all we need; we consider two terms
as semantically distinct if they have different print-values, of
course; but we also consider them to be distinct, even if they have
the same print value, when there is some context that will have
different print-values depending on which of these two terms is
inserted.
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
{\it PV} \hm & ::= \hm   &  $\bot$                                  & \\
         & $\mid$ &  $\lambda$                               & \\
         & $\mid$ &  CN$_0$                                  &  \\
         & $\mid$ &  \underline{CN$_k$}(PV$_1$, $\cdots$, PV$_k$)  \hmmm & 
\end{tabular}
\end{tabbing}
We also impose an {\em ordering\/} on printable values:
\begin{tabbing}
\hm
\begin{tabular}{lllll}
$\bot$   & $\sqsubseteq$ & {\it PV}         & & \\
$\lambda$& $\sqsubseteq$ & $\lambda$        & & \\
CN$_0$   & $\sqsubseteq$ & CN$_0$           & &  \\
% ------------
\underline{CN$_k$}($v_1$, $\cdots$, $v_j$ $\cdots$, $v_k$) &
$\sqsubseteq$ &
\underline{CN$_k$}($v_1$, $\cdots$, $v_j'$ $\cdots$, $v_k$) \hm &
if $v_j \sqsubseteq v_j'$ \hmm &
$k \geq 1$ 
\end{tabular}
\end{tabbing}
In other words, $\bot$ is strictly ``less'' than everything else,
and the ordering on constructed terms is defined recursively based on
a pair-wise ordering of corresponding arguments. There is no mutual
ordering between $\lambda$-expressions, constants and constructed
terms, or between constructed terms with distinct constructors.

Print{\LL\RR} is really implemented by the Print$'${\LL\RR} function that carries
along with it a second argument, the {\em environment\/}, that remembers
all identifier bindings in the surrounding scope.  This environment argument
is a collection of bindings $x=v$.
\begin{tabbing}
\hm Print{\LL}$e${\RR} $=$ Print$'${\LL}$e${\RR} empty\_environment \\
\hm where \\
\hm
\begin{tabular}[t]{llll}
Print$'${\LL}$x${\RR} env              & $=$ & Print$'${\LL}$v${\RR} env \hmm & if {\LL}$x=v${\RR} {\isin} env \\
Print$'${\LL}${\lambda}x.e${\RR} env   & $=$ & $\lambda$             & \\
Print$'${\LL}\{ $S$ in $a$ \}{\RR} env & $=$ & Print$'${\LL}$a${\RR} env$'$     & \\
\multicolumn{4}{r}{where $a$ {\isin} $SE$ \hm and \hm env$'$ = Extend{\LL}$S${\RR} env} \\
% ------------
Print$'${\LL}CN$_0${\RR} env &
= &
CN$_0$ &
   \\
% ------------
Print$'${\LL}\underline{CN$_k$}($a_1$, $\cdots$, $a_k$) {\RR} env &
= &
\underline{CN$_k$}(\begin{tabular}[t]{l}
                     Print$'${\LL}$a_1${\RR} env, \\
                     $\vdots$           \\
                     Print$'${\LL}$a_k${\RR} env)
                   \end{tabular} &
$k \geq 1 $  \\
% ------------
{\it otherwise}               & $=$ & $\bot$                & \\
\end{tabular}
\end{tabbing}
Print$'${\LL\RR} uses the auxiliary Extend{\LL\RR} function which
augments an environment with all the bindings in a block's statement
provided that the identifiers are bound to values (we assume that
$\alpha$ renaming has been used to prevent name clashes among bindings
in the environment).
\begin{tabbing}
\hm
\begin{tabular}[t]{lllr}
Extend {\LL} $x=v$ {\RR} env                 &
$=$ &
env $+$ {\LL}$x=v${\RR} &
\\
% ----------------
Extend {\LL} ($S_1$ {\tt ;} $S_2$) {\RR} env                  &
$=$ &
Extend {\LL} $S_1$ {\RR} (Extend {\LL} $S_2$ {\RR} env) & \\
% ----------------
Extend {\LL} $\cdots$ {\RR} env &
$=$ &
env &
{\em otherwise}
\end{tabular}
\end{tabbing}

Note that being able to print a non-$\bot$ value from a term does not
mean that the term has terminated, or even that it will ever
terminate.  For example, given this term:
\beginid
\{    loop = $\lambda$x.loop x;
     bot  = loop ($\lambda$y.y);
in
     ($\lambda$z.z)  \}
\endid
we can print its value ($\lambda$), but the term as a whole will never
terminate.

The following two properties of printing are about ``monotonicity''.
The first captures the idea that as we continually reduce a term, its
information content continually increases, \ie\ printing a value
following one or more reductions will only produce a ``more defined''
value.
\begin{Proposition}
\setcounter{PrintMonotonicity}{\theDefinition}
If $e$ {\goestoto} $e_1$ then \mbox{\rm Print{\LL}$e${\RR}} $\sqsubseteq$ \mbox{\rm Print{\LL}$e_1${\RR}}
\end{Proposition}
The second expresses the notion of equality that we wanted: if one expression
reduces to another then they are print-equivalent.
\begin{Proposition}
\label{sec-LambdaLet-PrintStar-monotonicity}
If $e$ {\goestoto} $e_1$ then Print*{\LL}$e${\RR} $=$ Print*{\LL}$e_1${\RR}
\end{Proposition}
Note, as a corollary, that if $e$ is {\it convertible\/} to $e_1$ (that
is, by applying rules in either direction), then Print*{\LL}$e${\RR}
$=$ Print*{\LL$e_1$\RR}.

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

\subsection{The Power of the {\LambdaLet} Calculus}

Our instantiation rules permit instantiation of an identifier only
when it is bound to a simple expression.  The following theorm by
Ariola {\etal} \cite{ariola96b} assures us that we have not lost any
computational power due to this restriction on substitution:
\begin{Proposition}
(Fundamental theorem of graph reduction): If $e$ {\goestoto} $e_1$ in
{\LambdaLetZero}, then $\exists e_2$ such that $e$ {\goestoto} $e_2$
in {\LambdaLet}, and Print{\LL$e_1$\RR} $\sqsubseteq$ Print{\LL$e_2$\RR}.
\end{Proposition}

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

\subsection{Reduction Strategies and Standard Reduction}

When we actually sit down and perform reductions on a program, we
would like to make sure we get at least as much information as one
could get from {\em any\/} other choice of reductions:
\begin{quote}
{\bf Definition:} A {\em standard reduction strategy\/} $\sigma$
ensures that, if \mbox{$e$ {\goestoto}\ $e_1$} as a result of some
sequence of reduction rules, then  ${\exists} \; e_2$ such that
\mbox{$e$ {\goestotosigma}~$e_2$} according to the rules of
strategy $\sigma$, and
Print{\LL}$e_1${\RR}$\sqsubseteq$Print{\LL}$e_2${\RR}.
\end{quote}

Briefly, we can devise a parallel standard reduction strategy for
{\LambdaLet} in three stages.  First, we manipulate the program to put
it into kernel form---a canonical form which enables us to ignore
several of the lifting rules during the remainder of reduction.  We
then choose redexes in a fair manner, making sure that we never reduce
inside the body of a $\lambda$ or in the branches of a conditional.
Finally, we stop when we run out of candidate redexes in permitted
contexts.

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

\section{{\LambdaLetB}: Adding Barriers to {\LambdaLet}}

\label{sec-LambdaLetB}

In this section, we describe {\LambdaLetB}, which extends {\LambdaLet}
with a {\em local sequencing mechanism\/} called a {\em barrier\/},
which sequences statements in a let block.  {\LambdaLetB} remains a
purely functional language (\ie\ it has no side-effects).  The
barrier's sole effect is that a program may be {\em less defined\/}
than the corresponding program that has the barriers erased, \ie\ the
presence of barriers may prevent termination, or may even prevent
printing a non-$\bot$ value.  The barrier gets its practical
motivation from controlling side-effects like M-structures; however,
all the semantic subtlety of barriers can be studied in this simpler,
purely functional setting.

In Sections~\ref{sec-LambdaLetB-syntax},
{\ref{sec-LambdaLetB-equivalence-rules}}, and
{\ref{sec-LambdaLetB-reduction-rules}}, we present the {\LambdaLetB}
{\em calculus}, \ie\ the syntax of {\LambdaLetB} terms and the
reduction rules.  In Sect.~{\ref{sec-LambdaLetB-printable-values}}, we
briefly define the notion of printing for {\LambdaLetB}.  Finally, in
Sect.~{\ref{sec-LambdaLetB-discussion}} we provide some commentary on
{\LambdaLetB}.

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

\subsection{Syntax}

\label{sec-LambdaLetB-syntax}

{\LambdaLetB} extends the syntax of {\LambdaLet} with a new type
statement called a Barrier:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcll}
$S$  & $::=$  & $\cdots$                       & as before \\
     & $\mid$ & $S$ {\BAR}  $S$ \hmmm          & Barriers (sequential)
\end{tabular}
\end{tabbing}
The Barrier represents sequencing: the statement before the barrier is
executed to completion before the statement after the barrier; we
refer to these statements as the {\em pre-region\/} and the {\em
post-region\/} of the barrier, respectively.  The barrier is a local
sequencing construct, and only involves the two statements that are
its subterms.  A program can contain any number of barriers.

Our previous static recursive scoping rule for identifiers remains the
same---in this respect, there is no difference between barriers and
semicolons.

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

\subsubsection{Values and Simple Expressions}

\label{sec-V-and-SE}

Values and Simple Expressions remain the same in {\LambdaLetB} as in {\LambdaLet}.

Statements which bind names to actual values are treated specially
by the barrier rules.  We refer to them as ``value
statments'', $H$:
\begin{tabbing} \hm
\begin{tabular}[t]{lcl}
$H$      & $::= $ & $x = V$ \hm $\mid$ \hm  $H$ {\tt ;} $H$
\end{tabular}
\end{tabbing}

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

\subsubsection{Contexts and Renaming}

\label{sec-LambdaLetB-contexts}

Expression contexts remain the same in {\LambdaLetB} as in {\LambdaLet}.
Statement contexts for expresssions extend those in {\LambdaLet} with
new clauses for barriers:
\begin{tabbing}
\hm
\begin{tabular}[t]{lcl}
$SC[\;]$  & $::=$    & $\ldots$ \\
            & $\mid$   & $SC[\;]$ {\BAR}  $S$ \hm $\mid$ \hm $S$ {\BAR}  $SC[\;]$
\end{tabular}
\end{tabbing}

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

\subsection{{\LambdaLetB} Equivalence Rules}

\label{sec-LambdaLetB-equivalence-rules}

The $\alpha$-renaming and semicolon equivalence rules remain the same
in {\LambdaLetB} as in  {\LambdaLet}.  We add a new
rule for barriers:
\begin{tabbing}
\hm  \begin{tabular}[t]{lll}
       ($H$ {\tt ;} $S_1$) {\BAR} $S_2$ &\hm $\equiv$ \hm& $H$ {\tt ;} ($S_1$ {\BAR} $S_2$) \\
     \end{tabular}
\end{tabbing}

This rule allows value bindings to escape from the pre-regions of
barriers.  The escaped bindings may enable other instantiations in the
surrounding context.  When all such bindings can escape, the barrier
can discharge---see Sect.~{\ref{sec-LambdaLetB-discharge}} below.

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

\subsection{{\LambdaLetB} Reduction Rules}

\label{sec-LambdaLetB-reduction-rules}

The existing reduction rules remain the same.  We add a new group of
rules for barriers.

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

\subsubsection{Barrier Rules for {\LambdaLetB}}

\label{sec-LambdaLetB-discharge}

The following rules say that a barrier can be ``discharged''
(eliminated) once the pre- or post-region is empty (the first rule is
the most common in practice).
\begin{tabbing}
\hm
\begin{tabular}[t]{llll}
% ---
{\emptystmt} {\BAR} $S$         & \goesto & $S$ \hmmmm & (BAR1) \\
% ---
$S$ {\BAR} {\emptystmt}         & \goesto & $S$        & (BAR2)
\end{tabular}
\end{tabbing}
The following proposition regarding barriers states that once all
the statements in the pre-region of a barrier have terminated, the
barrier can be discharged immediately:
\begin{Proposition}

In any context, the following reduction is always correct:
\begin{tabbing}
\hmm $(H$ {\BAR} $S)$  {\goesto} $(H$ {\tt ;} $S)$
\end{tabbing}
\end{Proposition}

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

\subsection{Printable Values, and the Print{\LL\RR} Function}

\label{sec-LambdaLetB-printable-values}

Printable values, and their ordering, remain the same in {\LambdaLetB} as
in {\LambdaLet}.

In the Print{\LL\RR} function, we add one clause to the Extend{\LL\RR}
helper function for barrier terms:
\begin{tabbing}
\hm
\begin{tabular}[t]{lllr}
Extend {\LL} ($S_1$ {\BAR}  $S_2$) {\RR} env & $=$ & Extend {\LL} $S_1$ {\RR} env
\end{tabular}
\end{tabbing}
Note that it omits identifiers from the post-region.

All the Print and Print* propositions of {\LambdaLet} (in
Sect.~{\ref{sec-LambdaLet-printable-values}}) remain unchanged.
% ------------------------------------------------

\subsubsection{Stable Terms and Terminated Terms}

\label{sec-LambdaLetB-stable-terms}

As we continually reduce a term, we may reach a stage where, even
though we may continue reducing it (perhaps forever), the result of
applying Print{\LL\RR} to the term will no longer change.  We say that
the term has reached a stable state, and we capture this formally in
the following definition:
\begin{quote}
{\bf Definition:} A term $e$ is {\em stable\/} if
Print*{\LL}$e${\RR} $=$ \{ $a$ $\mid$ $a$ $\sqsubseteq$ Print{\LL}$e${\RR} \}
\end{quote}

When reduction stops the term may still contain ``computations'' (such
as applications) that are unable to make progress simply because of a
deadlock condition.  We would like to define the category of
``terminated terms'' that have not stopped for this reason, \ie\ terms
that have stopped cleanly and properly:
\begin{quote}
{\bf Definition:} {\em Terminated terms\/} are described by the following syntax: \\
\hmm \begin{tabular}[t]{lll}
         {\it ET} & $::=$  & $V$ \hm $\mid$ \hm  \{ $H$ in $SE$ \}
     \end{tabular}
\end{quote}
A terminated expression contains no applications, unless they are
inside $\lambda$ abstractions.  Note, however, the body of any
$\lambda$ expression can be an arbitrary expression.  Terminated terms
are stable:
\begin{Proposition}
If $e$ {\isin} {\it ET}, then $e$ is stable.
\end{Proposition}
Further reductions may still be possible within $\lambda$-bodies, but
this cannot affect what is printed.

Another interesting class of terms are those terms whose printed
values contain no $\bot$.
\begin{quote}
{\bf Definition:} A {\em ground-printing term\/} is a term $e$ such
that Print{\LL$e$\RR} terminates, and the printed value does not
contain $\bot$.
\end{quote}
The printed value value may be an arbitrarily deep data structure, and
this condition requires that none of the leaves are $\bot$.  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 not have terminated and which,
indeed, may even loop forever.

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

\subsection{Discussion of {\LambdaLetB}}

\label{sec-LambdaLetB-discussion}

The interaction between our ${\beta}_G$ rule for function application and
the barrier rules is subtle.  Perhaps the most surprising consequence is
that:
\begin{tabbing}
\hm ${\lambda}x.e$ \hm $\neq$ \hm \{ $t=e$ in ${\lambda}x.t$ \}
\hmmm
even if $e$ is only a free variable ($\neq x$).
\end{tabbing}

The inequality is not surprising in eager languages such as SML and
Scheme---if $e$ were a non-terminating computation, the left-hand side
would terminate and the right-hand side would not.  However, if $e$
was merely a free variable (say, $z$), then the two sides {\em
would\/} be equal in SML and Scheme, but they are still not equal in
{\LambdaLetB}.


Consider the following term (where $\bot$ is any  non-terminating term):
\beginid
    ( K = $\lambda$x.1 ;
      b = $\bot$ ;
      ( x1 = K b
        ---
        S ) )
\endid

Even though {\cf K} discards its argument, the barrier will not
discharge, as demonstrated by the following sequence of reductions
(for comparison, we also show what would happen with the traditional
$\beta$ rule):
{\cf
\begin{tabbing}
% ------------
{\goesto} \hmmmm \=
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = \{ x' = b in ($\lambda$y.y) \} \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \hmmmm \=
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = ($\lambda$y.y) \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \kill
% ------------
\mbox{} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = K b \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \\
% ------------
\\
{\goesto} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = ($\lambda$x.($\lambda$y.y)) b \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \\
% ------------
\\
{\goesto} \> {\it [using ${\beta}_G$]} \> {\it [using traditional ${\beta}$]} \\
\\
% ---
\mbox{} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = \{ x' = b in ($\lambda$y.y) \} \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = ($\lambda$y.y) \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \\
% ------------
\\
{\goesto} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = ($\lambda$y.y) ; \\
\hmm    x' = b \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  ( x1 = ($\lambda$y.y) ; \\
\hmm    S ) )
\end{tabular} \\
% ------------
\\
{\goesto} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  x1 = ($\lambda$y.y) ; \\
\hm  ( x' = b \\
\hmm    ---\\
\hmm    S ) )
\end{tabular} \>
% ---
\begin{tabular}[t]{l}
( K = $\lambda$x.($\lambda$y.y) ; \\
\hm  b = $\bot$ ; \\
\hm  x1 = ($\lambda$y.y) ; \\
\hm  S )
\end{tabular}
\end{tabbing}
}

The last term (on the left) is stuck: since {\tt b} never becomes a value,
the barrier never discharges.  This behaviour is fundamentally related to
our ${\beta}_G$ rule which does not discard the argument {\cf b} even
though the function itself does not use the argument.  In contrast, using
the traditional $\beta$ rule (on the right), the barrier does discharge.

The addition of barriers allows us to observe the {\em termination} of
any term in the calculus.  For example, the following two terms are
indistinguishable in {\LambdaLet}:
\begin{tabbing}
\hm \{ $x = 5$ in 5 \} \hmm and \hmm \{ $x = \bot$ in 5 \}
\end{tabbing}
The following context will distinguish them in {\LambdaLetB}:
\begin{tabbing}
\hm\= \{ (\=\ \=$y = [\;]$\\
\>\>      {\BAR}\\
\>\>          $z = 3$ )\\
\>     in\\
\>     \hm z \}
\end{tabbing}
It should be clear from this example that equality in {\LambdaLet} does
not imply equality in {\LambdaLetB}.  

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

\section{Conclusion}

{\LambdaLetB} is just one example of a useful extension of pure
{\LambdaLet} which enables us to study issues of termination in the
absence of other complications.  pH, the parallel dialect of Haskell
that we are designing, also has I-structures\cite{Arvind89b} and
M-structures, which add implicitly synchronized mutable storage to the
language.  In Figure~1 we show various extensions we
have formulated and studied, culminating in {\LambdaS}, which is
intended to capture all the essential semantic properties of pH
itself.  {\LambdaS} is also playing the desired role in the pH
compiler: each rule for code generation and optimization is written in
terms of {\LambdaS} constructs.

\begin{figure}
\label{fig:lattice}
\begin{center}
  \begin{picture}(200,170)(-100,0)
    \put( -10,  +0){\LambdaLet}

    \put(   0, +15){\line(0,1){25}}
    \put(   0, +15){\line(-3,1){85}}
    \put(   0, +15){\line(+3,1){85}}

    \put(-100, +50){\LambdaLetC}
    \put( -10, +50){\LambdaLetI}
    \put( +80, +50){\LambdaLetB}

    \put( +85, +65){\line(0,1){25}}
    \put( +80,+100){\LambdaLetBM}

    \put( -85, +65){\line(1,1){75}}
    \put(   0, +65){\line(0,1){75}}
    \put( +85,+115){\line(-3,1){75}}
    \put(  -5,+150){\LambdaS}

  \end{picture}
\end{center}
\caption{A taxonomy of calculi used to study pH semantics}
\end{figure}



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

\bibliography{lambda-s}

\end{document}

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

