\documentclass[11pt]{handout}
\usepackage{6044}
\usepackage{time,fullpage}
\usepackage{amsmath}
\usepackage{prooftree}

\textheight 8in

\oddsidemargin 11pt
\evensidemargin \oddsidemargin
\marginparwidth 0.5in

\advance\textwidth by -2\oddsidemargin

\newdimen\tablewidth
\tablewidth=\textwidth
\advance \tablewidth by -11pt

\parindent 0.0in
\parskip \medskipamount

\newcommand\Atop{\genfrac{}{}{0pt}0}
\newcommand\Over{\genfrac{}{}{}0}
%\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}

\newcommand{\fcte}{\underset{\rm ftc}{=}}

\def\halts{\cal Halts}
\def\nhalts{${\overline{\halts}}$}

\newenvironment{btable}{%
    \begin{center}
    \begin{tabular*}{.8\textwidth}{@{}l@{\extracolsep{\fill}}l@{}}
}{%
    \end{tabular*}
    \end{center}
}

\newenvironment{bnfarray}{%
    \bnf
    \begin{eqnarray*}%
}{%
    \end{eqnarray*}%
}

\let\to\rightarrow
\let\union\cup
\let\cross\times

\def\SI{\mbox{Scheme-Integer}}
\def\SNI{\mbox{Scheme-Nonneg-Integer}}
\def\SN{\mbox{Sch-\-Num}}
\def\SB{\mbox{Sch-Bool}}
\def\Empty{\mbox{Empty}}
\def\SI{\mbox{Sch-Int}}
\def\SNI{\mbox{Sch-Nonneg-Int}}

\makeatletter

\def\DefineBNFAbbrev#1#2{%
    \expandafter\newcommand\expandafter{\csname#1\endcsname}{\@bnfabbrev{#2}}%
}

\def\@bnfabbrev#1{%
    \@ifnextchar _{\@subabbrev{#1}}{\@plainabbrev{#1}}%
}

\def\@subabbrev#1_#2{\hbox{\normalfont$\langle\mbox{#1}_{#2}\rangle$}}

\def\@plainabbrev#1{\hbox{\normalfont$\langle\mbox{#1}\rangle$}}

% \def\exp{\hbox{$\bnf <expression>$}}

\DefineBNFAbbrev{idfr}{identifier}
\DefineBNFAbbrev{expr}{expression}
\DefineBNFAbbrev{define}{define}
%\DefineBNFAbbrev{defines}{defines}
\DefineBNFAbbrev{vrbl}{variable}
\DefineBNFAbbrev{bod}{body}
\DefineBNFAbbrev{init}{init}
\DefineBNFAbbrev{val}{value}
\DefineBNFAbbrev{pval}{primitive\ value}
\DefineBNFAbbrev{ival}{immediate\ value}
\DefineBNFAbbrev{test}{test}
\DefineBNFAbbrev{orsf}{or}
\DefineBNFAbbrev{andsf}{and}
\DefineBNFAbbrev{pridfr}{procedure\ identifier}
\DefineBNFAbbrev{rspidfr}{rule-specified\ procedure\ id}
\DefineBNFAbbrev{ppridfr}{primitive\ procedure\ id}
\DefineBNFAbbrev{lamexp}{lambda\ expression}

\DefineBNFAbbrev{beginsf}{begin}
\DefineBNFAbbrev{cntxt}{context}
\DefineBNFAbbrev{deflimcntxt}{definition-limiting\ context}
\DefineBNFAbbrev{nondefcntxt}{non-definition\ context}
\DefineBNFAbbrev{nondefhole}{non-def\ or\ hole}
\DefineBNFAbbrev{evcntxt}{eval\ context}
\DefineBNFAbbrev{dcntxt}{definition\ context}
\DefineBNFAbbrev{idef}{immediate\ define}
\DefineBNFAbbrev{ccntxt}{control\ context}

\newcommand{\undefv}{\formath{undefined-flag}}
\newcommand{\setbv}{\Code{(quote set!-value)}}

\makeatletter

\def\fbox#1{%
  \vtop{\vbox{\hrule%
     \hbox{\vrule\kern3pt%
 \vtop{\vbox{\kern3pt#1}\kern3pt}%
 \kern3pt\vrule}}%
 \hrule}}


\begin{document}
\handout{rewriting-model-2}{Scheme Rewriting Model\\
II. Side-Effects}%
{30 October, 1996}

\section{Assignment Statements}

Scheme's {\em assignment statement} has the form
\[\Code{(set! \vrbl\ \expr)}.\]
Its computational behavior is explained in part by a rewrite rule:
\[\begin{array}{l}
\Code{(set! $x$ $V$)}  \rulesto  \setbv\\
\text{where $V$ is an immediate value and the occurrence of $x$}\\
\text{is bound by some definition.  This definition gets replaced}\\
\text{by \Code{(define $x$ $V$)}.}
\end{array}\]

The value of a \Code{set!} expression is not very interesting, since it is
always just the symbol \setbv.  What is important about an assignment is
its {\em side-effect}: changing the binding of a defined variable.

With side-effects in the language, the {\em order} in which subexpressions
are evaluated plays a central role.  For example, if the operands of
combinations are evaluated in left to right order, then evaluation of the
body
\begin{lisp}
(define x 0)
((lambda (dummy1 dummy2) x) (set! x 1) (set! x 2))
\end{lisp}
returns the value \Code{2}, but if evaluation proceeds right to left, it
returns the value \Code{1}.  This is strikingly different from functional
Scheme, where we have seen that a primitive value of a functional
expression is independent of evaluation order.

So in a substitution model for Scheme with side-effects, we will have to
specify when and where to apply rewrite rules.

\section{Contexts}

To be able to specify {\em where} to do a rewriting, we need a precise way
to indicate a desired subphrase of any expression.  For this purpose we
introduce {\em contexts}.

\begin{definition}
Let $\bnf{<phrase>}$ be one of the phrase types appearing in the grammar
of Scheme, e.g., $\bnf <phrase>$ might by $\bnf <variable>$, $\bnf
<formals>$, $\bnf <binding>$.  A \emph{$\bnf{<phrase>}$-context} is a
syntactic object, $C$, with a single occurrence of a variable, \hole,
called the \emph{hole}, such that $C$ would parse as a Scheme body if the
hole was parsed as a $\bnf{<phrase>}$.  If $C$ is a $\bnf
<phrase>$-context and $P$ is a $\bnf <phrase>$, then $C[P]$ denotes the
result of literally replacing---without any renaming---the hole in $C$ by
$P$.
\end{definition}

\begin{example}

The expression
\[\Code{(if (= -6 ((lambda (y) (* 2 y) ((lambda (x) (x 3)) -)))) 5 6)}\]
has a subexpression which matches the left hand side of the lambda
application rule at the $\bnf <expression>$-contexts $C_{1}, C_{2}$ where
\begin{eqnarray*}
C_{1} & = & \Code{(if (= -6 \hole) 5 6)},\\
C_{2} & = & \Code{(if (= -6 ((lambda (y) (* 2 y) \hole))) 5 6)}
\end{eqnarray*}

The body
\begin{lisp}
(define x ())
( (lambda (x y) ( (lambda (dummy) x) (set! x (cons y x)) ))
  x
  4 )
\end{lisp}
has two binding occurrences of \Code{x} at the $\bnf <variable>$-contexts
\[\begin{array}{l}
\Code{(define \hole ())}\\
\Code{( (lambda (x y) ( (lambda (dummy) x) (set! x (cons y x)) ))}\\
  \Code{  x}\\
  \Code{  4 )}\\
\end{array}\]
and 
\[\begin{array}{l}
\Code{(define x ())}\\
\Code{( (lambda (\hole\: y) ( (lambda (dummy) x) (set! x (cons y x)) ))}\\
  \Code{x}\\
  \Code{4} )\\
\end{array}\]
\end{example}

One technicality of Scheme grammar which we will use later is that a
Scheme body must parse as a sequence of zero or more definitions of
distinct variables followed by an expression.  The Scheme grammar does
{\em not} allow a body beginning with two or more definitions to be parsed
as a definition followed by a body beginning with one or more definition.
So
\begin{example}
\[
\begin{array}{l}
\Code{(define x 1)}\\
\hole
\end{array}
\]
is an $\bnf <expression>$-context, but {\em not} a $\bnf <body>$-context.

\[
\Code{(list (quote \hole) (quote a) 3)}
\]
is a $\bnf <variable>$-context (as well as a \pridfr- and $\bnf
<keyword>$-context), but {\em not} an \expr-context.
\end{example}
When the phrase type of the hole in a $\bnf <phrase>$-context, $C$, is
unambiguous, we drop the prefix and simply call $C$ a ``context.''

\section{Redexes and Contracta}

Applicability of the functional rewrite rules P, C, I, L and the
\Code{set!} rule, S, is determined by the expressions which appear on the
left hand sides of our descriptions of the rewrite rules:
\[
\begin{array}{lll}
\mbox{(P)} & \Code{(\mbox{prvar} $v_{1}\dots v_{n}$)} &
        \mbox{where prvar is a \ppridfr}\\
        &       & \mbox{ and the $v_{i}$ are \pval's.}\\
\mbox{(C)} & \Code{(if $V$ $M$ $N$)} &\mbox{where $V$ is an \ival.}\\
\mbox{(I)} & x          & \mbox{where $x$ is a variable.}\\
\mbox{(L)} & \Code{( (lambda ($x_{1}\dots x_{n}$) $B$) $V_{1}\dots V_{n}$
)}
 &\mbox{ where the $x_{i}$ are variables and the}\\
        &&       \mbox{ $V_{i}$ are \ival's.}\\
\mbox{(S)} & \Code{(set! $x$ V)} & \mbox{where $x$ is a variable and $V$}\\
        &&       \mbox{ is an \ival.}
\end{array}
\]

We will refer to these expressions as {\em redex-triggers}.  Informally we
have said that rewriting consists of replacing left hand sides of rules by
right hand sides.  For the P and C rules, the redex-triggers above really
are the complete left hand sides.  However, this is not the case for I, L,
and S because more information about the context in which the triggers
appear is needed in order to determine how the rewriting should be carried
out, or even whether the rule is applicable.

For example, consider the Instantiation Rule applied to the last
occurrence of the I-trigger, i.e., variable, \Code{k-to-the} in the
expression $M$:
\begin{lisp}
( (lambda (n)
    (define k n)
    (define k-to-the
      (lambda (n) (if (zero? n) 1 (* k (k-to-the (- n 1))))))
    (lambda (k) (k-to-the
                 (* k k))))
  2 )
\end{lisp}

In order to instantiate at all, we must know that this occurrence of
\Code{k-to-the} is bound by the definition two lines above.  Not only
that, but in doing the instantiation, we actually have to do more than
replace the occurrence of \Code{k-to-the} by the lambda-expression to
which it is bound.  To avoid improper binding, we also have to rename some
of the occurrences of \Code{k}: the body $M$ actually rewrites to
\begin{lisp}
( (lambda (n)
    (define k n)
    (define k-to-the
      (lambda (n) (if (zero? n) 1 (* k (k-to-the (- n 1))))))
    (lambda (k_1) ((lambda (n) (if (zero? n) 1 (* k (k-to-the (- n 1)))))
                   (* k_1 k_1))))
  2 )
\end{lisp}

So to describe the complete left hand side of the instantiation rule to
include {\em all} the information needed to apply the rule and all the
parts of the expression which change as a result of the rewriting, we must
take the left hand side to be $D[C_1[\Code{k-to-the}]]$, where
$D$ is
\begin{lisp}
(define k n)
(define k-to-the
  (lambda (n) (if (zero? n) 1 (* k (k-to-the (- n 1))))))
[],
\end{lisp}
$C_1$ is \Code{(lambda (k) (\hole\ (* k k)))},
and the right hand side is
\[D[C_1'[\Code{(lambda (n) (if (zero? n) 1 (* k (k-to-the (- n 1)))))}]]\]
where $C_1'$ was obtained by freshly renaming the bound variables in
$C_1$.  Moreover, the replacement of this right hand side by this left hand
side occurred {\em at} the context
\[\Code{( (lambda (n) \hole) 2)} .\]

\begin{definition}
The complete left hand side of a rule is called its {\em redex}, and its
complete right hand side is its {\em contractum}.
\end{definition}

So for rules P and C, the redex-triggers are the redexes of the rules.
For instantiation we have
\begin{definition}
A {\em definition context} is an \expr-context which is a sequence of one
or more immediate definitions followed by a hole.  An {\em instantiation
redex} is a body of the form $D[C[x]]$ for some definition context, $D$,
variable, $x$, and \expr-context, $C$, such that \Code{(define $x$ $V$)}
is one of the definitions in $D$, and the occurrence of $x$ at the hole in
$C$ is free.  The {\em contractum} of the instantiation rule with this
redex is $D[C'[V]]$ where $C'$ is the result of freshly renaming the bound
variables\footnote{Less drastic renamings would work in many
cases.} in $C$.
\end{definition}

\problem Give a precise definition of whether a variable, $x$, has {\em a
free occurrence at the hole in a $\bnf <variable>$-context $C$.} \hint By
structural induction on $C$.

There is another form of instantiation redex for the case of instantiation
of a variable within a definition context in which it is defined.  A
similar definition can also be given for the redexes and contracta of the
Lambda application rule.  We omit these general definitions.  In the next
section we give the special case of these rules when rewriting in
evaluation order.

\problem
Give a precise definition for the form of instantiation redex applicable
for instantiating a variable within a definition context in which it is
defined.

\problem
Give a precise definition for the redexes and contracta of the Lambda
application rule.

\section{Order of Evaluation}

The order in which the parts of a Scheme body are supposed to be evaluated
can be described informally as follows:

\begin{itemize}
\item If the whole body is a redex, rewrite it into the corresponding
contractum.

\item If the body is a conditional, do an evaluation-rewrite on its test.

\item If the body is a combination, do an evaluation-rewrite on the
rightmost\footnote{This specifies right-to-left order of evaluation.  The
official Scheme definition allows each implementation to specify its own
orders for evaluation of the components of a combination.} operand or
operator which is not an \ival.

\item If the body is an assignment, do an evaluation-rewrite on its
expression part.

\item If none of the above cases apply, evaluation is complete.
\end{itemize}

An \emph{evaluation context} is a special kind of context which we will
use to formally specify where to use rules in an evaluation.  We define
them with a grammar which corresponds directly to the cases above:

\begin{definition}
An {\em evaluation context} is a context of the form $D[C]$, where $D$ is
a {\em definition context} and $C$ is a {\em control context}.  Control
contexts are \expr-contexts defined by the grammar:
\begin{bnfarray}
\ccntxt ::= \hole\\
    &|& \Code{(if\ \ccntxt\ \expr\ \expr)}\\
    &|& \Code{(${\expr}^{*}$ \ccntxt\ ${\ival}^{*}$)}\\
    &|& \Code{(set! $<var>$ \ccntxt)}
\end{bnfarray}
\end{definition}

We now specify ``evaluation'' versions of the rewriting rules:
\begin{definition}

A {\em Primitive application evaluation rule} has a redex of the form
$E[T]$ and a corresponding contractum $E[b]$, where $E$ is an evaluation
context, $T$ is a P-trigger and $b$ is the \pval\ determined by the
trigger.

A {\em Conditional evaluation rule} has a redex of the form $E[T]$ and a
corresponding contractum $E[M]$, where $E$ is an evaluation context, $T$
is a C-trigger, and $M$ is the alternative (resp. consequent) branch of $T$
if the test is \Code{\#f} (resp. an \ival\ other than \Code{\#f}).

An {\em Instantiation evaluation rule} has a redex of the form $D[C[x]]$
for some {\em control} context, $C$, variable, $x$, whose occurrence at
the hole in $C$ is free, and definition context, $D$, such that
\Code{(define $x$ $V$)} is one of the definitions in $D$.  The
corresponding {\em contractum} is $D[C[V]]$.

A {\em Lambda application evaluation rule} has a redex of the form
$D[C[T]]$ where $C$ is a {\em control} context, $D$ is a definition
context or hole, and $T$ is an L-trigger.  Suppose $T$ is of the form
\[
\Code{( (lambda ($x_{1} \dots x_{n}$) $D_{1}[M]$) $V_{1} \dots V_{n}$ )}
\]
where $D_1$ is a definition context or hole, $M$ is an \expr, $V_{1} \dots
V_{n}$ are \ival's, and $x_{1} \dots x_{n}$ are variables, for some $n
\geq 0$.  Let $x'_{1} \dots x'_{n}$ be ``fresh'' variables (i.e.,
variables which do not occur in the redex).  Then the corresponding
contractum is $D[D_0[D'_1[C[M']]]]$ where $D_0$ is
\[\Code{(define $x'_{1}$ $V_{1}$)}\dots
        \Code{(define $x'_{n}$ $V_{n}$)}\hole
\]
and $D'_1[M']$ is the result of first freshly renaming the bound variables
in $D_1[M]$ (this is to avoid improper binding of free variables in $C$)
and then replacing free occurrences of $x_i$ by $x'_i$.

A {\em \Code{set!} evaluation rule} has a redex of the form
$D[C[\Code{(set! $x$ $V$)}]]$ where $x$ is a variable, $V$ is an \ival,
$C$ is a control context, and $D$ is a definition context which includes a
definition of $x$.  The corresponding contractum is $D'[C[\setbv]]$ where
$D'$ is the same as $D$ except that the definition of $x$ is replaced by
\Code{(define $x$ $V$)}.

A {\em Garbage collection evaluation rule} is $D[M] \rulesto D'[M]$ where
$D$ is a definition context and $D'$ is the result of deleting definitions
which are garbage in $D[M]$.

The evaluation rewrite rules other than garbage collection rules are
called {\em active} rules.

A body $B_{1}$ {\em evaluates in one step} to body $B_{2}$, in symbols
$B_{1} \eval1 B_{2}$, iff $B_{1} \rulesto B_{2}$ is an active evaluation
rewrite rule.  $B_{1}$ {\em evaluates through} body $B_2$, written $B_{1}
\evalss B_2$, iff $B_{1}$ can be rewritten to $B_{2}$ by a series of zero
or more rewritings each of which is one evaluation step {\em or} an
application of the Garbage Collection rule.
\end{definition}

\begin{lemma}\label{determinism} ({\bf Determinism})
For any scheme body, $B$, there is at most one evaluation context, $E$,
and active trigger, $T$, such that $B$ is of the form $E[T]$.  Hence, for
any Scheme body, $B$, there is (up to fresh renaming) at most one body
$B'$ such that $B \eval1 B'$.
\end{lemma}

\problem Prove Lemma~\ref{determinism}.

\begin{definition}
A Scheme \emph{value} is a body of the form:
\[\bnf
    <immediate define>^* <immediate value>.
\]
\end{definition}

\begin{lemma}\label{value-terminated}
If $V$ is a value, then $V$ does not evaluate in one step to anything.
\end{lemma}

\problem Prove Lemma~\ref{value-terminated}.

One of the virtues of a language like Scheme with automatic
``garbage-collection'' is that a programmer can ignore most aspects of
memory allocation.  This is reflected in our substitution model by the
fact that, even with side-effects, garbage collection rules may be applied
at any time:

\begin{lemma}
Rule G commutes with the active rules.  See Problem Set 2, problem 4.
\end{lemma}

The Lemmas above directly imply:

\begin{theorem} ({\bf Uniqueness})
For every Scheme body, $B$, there is (up to freshly renaming bound
variables) at most one garbage-free value, $V$, such that $B \evalss V$.
\end{theorem}

\begin{definition}
For a Scheme body, $B$, the unique garbage-free value $V$, if any, such
that $B \evalss V$ is called the \emph{evaluation-value} of $B$, written
\valof{B}.  $B$ is said to {\em halt} iff $valof{B}$ is defined.
\end{definition}

Bodies may not have values because they successively evaluate in one step
forever, or because they get stuck after some number of evaluation steps
at a \emph{non}value expression, which does not evaluate further.  Such
``stuck'' expressions, correspond to errors which would be reported by
real Scheme.

\begin{example}
The body
\begin{lisp}
(define f (lambda (x) (+ x (f x))))
(f 1)
\end{lisp}
evaluates through an infinite sequence of bodies of the form
\begin{lisp}
(define f (lambda (x) (+ x (f x))))
(+ 1 (+ 1 (+ 1 ... (+ 1 (f 1)))))
\end{lisp}
and never reaches a value; evaluation in real Scheme would eventually
cause a ``stack overflow'' error.

The body
\begin{lisp}
(define f (lambda (x) (f x)))
(f 1)
\end{lisp}
evaluates to itself in three steps and a garbage collection; in real
Scheme it simply keeps evaluating until it gets interrupted.

The expression
\[\Code{(if (< 3 4) f 7)}\]
gets stuck at the variable \Code{f} after two evaluation steps; evaluation
in real Scheme causes an ``\Code{unbound variable f}'' error.

The expression
\[\Code{((lambda (x y) (+ x y)) (* 3 4))}\]
gets stuck after one step; real Scheme reports a ``\Code{compound}
\Code{procedure} \Code{called} \Code{with 1} \Code{argument;} \Code{it}
\Code{requires} \Code{exactly 2} \Code{arguments}'' error.

\end{example}

Another important general property of evaluation is that in the functional
case, evaluation rewriting does as well at getting to some value as any
possible way of rewriting:

\begin{theorem} {\bf Value-safety}.  For any body, $B$, in the functional
kernel of Scheme, the following are equivalent
\begin{itemize}
\item there is a way to rewrite $B$ into a value by successive use of the
functional Scheme rewrite rules,
\item $B$ evaluates through some value,
\item $B$ halts.
\end{itemize}
\end{theorem}

Proving this theorem requires a more elaborate development of facts about
term rewriting than we can undertake in 6.044.

Note that our definition of evaluation contexts implies that combinations
get evaluated in right-to-left order.  This was an arbitrary choice; a
left-to-right or other evaluation order for combinations could have been
specified.  As we saw above, the values of particular expressions will not
be the same using another order than ours, but the general properties of
evaluation such as uniqueness and value-safety remain the same.

\problem Explain how to modify the definition of evaluation context to
reflect left-to-right order for the operator and operands of combinations.

\section{Non-immediate Definitions}

With \Code{set!} in the kernel, we can handle non-immediate definitions as
sugar.  For example, we can translate the body
\[\begin{array}{l}
\Code{(define x $\expr_{1}$)}\\
$\expr_{2}$
\end{array}\]
into
\[\begin{array}{l}
\Code{(define x \undefv)}\\
\Code{(begin (set! x $\expr_{1}$) $\expr_{2}$)}
\end{array}\]
where \undefv\ is some designated\footnote{In real Scheme, an attempt to
evaluate \undefv\ causes an error.} \ival, and
\[\Code{(begin\ $\expr_{0}$\ $\expr_{1}$)}\]
is itself sugar for
\[\Code{((lambda ($\mbox{fresh}$) $\expr_{1}$) $\expr_{0}$)}.\]

\section{Other Side-effects}
In this section we briefly indicate how our substitution model could be
extended to include list mutation and input-output.

So far we have modeled Scheme solely by rewriting Scheme bodies.  That is,
if $B_{1}$ parses as a Scheme body according to our given grammar for
Scheme, and $B_{1} \eval1 B_{2}$, then $B_{2}$ also parses as a body.

We were able to stick to Scheme bodies to reflect the side-effects of
assigments because we could represent the results of such side-effects by
changes in the \define's in a body.  It would be nice to model the
procedures \Code{set-car!} or \Code{set-cdr!} which cause side-effects on
lists in the same way.  However, so far no satisfactory way has been found
to model list side-effects while staying strictly within Scheme grammar.
So we extend Scheme with new self-evaluating tokens \Code{\#cell-0},
\Code{\#cell-1}, \dots, called {\em cell-values}.  The idea is that
cell-values correspond to the cons-cells in the standard internal
representation of list structure maintained by Scheme implementations.
Cell-values get created by new rewriting rules for list expressions, and
they can be {\em declared} within a new \Code{shared} special form.  For
example, the value of
\begin{center}
\begin{lisp}
(define a (list 1 2 3))
(list a (cdr a))
\end{lisp}
\end{center}
would print out in real Scheme as
\begin{center}
\begin{lisp}
((1 2 3) (2 3))
\end{lisp}
\end{center}
and rewrite in our Scheme TRM to the immediate value:
\begin{center}
\begin{lisp}
(cons
 (cons 1 (cons 2 (cons 3 ())))
 (cons (cons 2 (cons 3 ()))
       ())) .
\end{lisp}
\end{center}
But in the model with the sharing extension, this value will rewrite to a list
representation which reflects the fact that the two occurrences of
\Code{(cons 2 (cons 3 ()))} above correspond to the {\em same} list:
\begin{center}
\begin{lisp}
(shared ((#cell-0 (cons 2 (cons 3 ()))))
 (cons
  (cons 1 #cell-0)
  (cons #cell-0
       ())) .
\end{lisp}
\end{center}

The Donkey interpreter in the DrScheme system at Rice University,
available on the WWW at
\begin{center}
\Code{http://www.cs.rice.edu/CS/PLT/packages/drscheme/}
\end{center}
supports \Code{shared} declarations.

\iffalse
\footnote{The extension of the Scheme kernel grammar to include shared
declarations is:
\begin{bnf}
\begin{eqnarray*}
<expression> &::=& \dots | <shared>\\
<self-evaluating> &::=& \dots | <cell-value>\\
<cell-binding> &::=& \Code{(} <cell-value> \ival \Code{)}\\
<shared> &::=& \Code{(shared (}<cell-binding>*\Code{)}\ <body> \Code{)} \\
    && {} \qquad \hbox{(Note: all \Code{<shared>}-bound cell-values must be distinct.)}\\
<cell-value>\ &::=& \Code{\#cell-0} | \Code{\#cell-1} | \dots\\
<keyword>  &::=&  \ \dots\, | \Code{shared}\\
\end{eqnarray*}
\end{bnf}}
\fi

Scheme's \Code{read} and \Code{display} procedures can be modeled with
rewriting by explicitly defining variables \Code{read-list} and
\Code{display-list} to be lists of values to be read and displayed.  Then,
the procedure variable \Code{read} can be regarded as sugar for
\begin{center}
\begin{lisp}
(lambda ()
 (let ((value (car read-list)))
  (set! read-list (cdr read-list))
  value))
\end{lisp}
\end{center}
and \Code{display} as sugar for
\begin{center}
\begin{lisp}
(lambda (output)
 (set! display-list (cons output display-list)))
\end{lisp}
\end{center}

\iffalse
\section{Control abstractions}

Scheme's \Code{error} procedure is an example of a new class of {\em
control procedures} whose significance comes neither from the values they
return nor their side-effects.  
Rewriting provides a simple way to understand Scheme's control procedures,
including Sheme's murky and controversial
\[\Code{call-with-current-continuation}\]
procedure, \Code{call/cc} for short.
\fi


\appendix \section{Grammar for Scheme with Side-Effects}\label{grammar}

In the following grammars, superscript ``$*$'' indicates zero or more
occurrences of a grammatical phrase.

\subsection{Kernel Syntax}

\begin{bnf}
\begin{eqnarray*}
<define> &:=& <immediate define>\\
<immediate define> &:=& "(define"\: <variable> \ival")"\\
\\
<body>  &::=& \define^* <expression>\\
        && {} \qquad \hbox{(Note: all defined variables must be distinct.)}\\
<expression> &::=& <variable> | <self-evaluating>  | <procedure identifier>\\
        && {}  | <symbol> | "()" | <combination> | <lambda expression>\\
        && {} | <if> | <assignment>\\
\end{eqnarray*}
\end{bnf}

\begin{bnf}
\begin{eqnarray*}
<assignment> &::=& "(set!"\: \vrbl\: \expr")"\\
\\
<self-evaluating>       &::=& <numeral> | <boolean>\\
<numeral>   &::=&   "0" | "-1" | "3.14159" | \ldots\\
<boolean>   &::=&   "#t" | "#f" \\
\\
\pridfr  &::=& \ppridfr | \rspidfr\\
\ppridfr &::=& "+" | "-" | "*" | "/" | "=" | "<" |
        "atan" | "zero?" | \dots\\
\rspidfr &::=& "not" | "boolean?" | "integer?" | "number?" | "null?" | "pair?"\\
        && {}  | "symbol?" | "procedure?" | "car" | "cdr" | "cons" | "list"\\
        && {}  | "apply"| "eq?"\\
\\
<symbol>        &::=& "(quote"\: \vrbl")" | "(quote"\: \pridfr")"\\
        && {}  | "(quote"\: <keyword>")"\\
\end{eqnarray*}
\end{bnf}

\begin{bnf}
\begin{eqnarray*}
<combination>   &::=&   "("<operator> <operand>^{*}")"\\
<operator>   &::=&   <expression>\\
<operand>   &::=&   <expression>\\
\\
<lambda expression> &::=&  "(lambda ("<formals>")" <body>")"\\
<formals>   &::=&   <variable>^{*}  \qquad
                        \hbox{(Note: all \vrbl's must be distinct.)}\\
\\
<if> &:=& "(if"\: <test> <consequent> <alternative> ")" \\
<test>   &::=&   <expression>\\
<consequent>   &::=&   <expression>\\
<alternative>   &::=&   <expression>\\
\\
<keyword>   &::=& "define" | "lambda" | "if" | "quote" | "set!"\\
<variable> &::=& \hbox{identifiers which are not $\bnf <self-evaluating>,$}\\
      & &   {} \quad \hbox{\pridfr's or $<keyword>$'s}
\end{eqnarray*}
\end{bnf}

\subsection{Values}

\begin{bnf}
\begin{eqnarray*}
\pval &::=&  <self-evaluating> | <symbol> | "()"\\
\ival &::=& \pval | <procedure identifier> | <lambda expression>\\
        && {} | "(cons "\ival\: \ival")"\\
<value> &::=& <immediate define>^{*} \ival\\
        && {} \quad \hbox{(Note: all defined \vrbl's must be distinct.)}\\
\end{eqnarray*}
\end{bnf}

\subsection{Derived Syntax}

\begin{bnf}
\begin{eqnarray*}
\define &::=& \ldots | "(define ("<variable> <formals>")" <body>")"\\
        && {} | "(define " \vrbl\: \expr")"\\
\expr &::=& \ldots | <derived expression>\\
<derived expression> &::=& <cond> | <let> | <begin>\\
% | <quoted> \\
\\
<begin> &::=& "(begin"\: \expr\: \expr^{*}")"\\
\\
%<quoted> &::=& "(quote"\: <s-expression>")"\\
%<s-expression> &::=& \idfr | "("<s-expression>^*")"\\
%\\
<cond> &::=& "(cond"\: <clause> <clause>^{*}")"\\
<clause> &::=& "("<test> <expression>")" | "(else"\: \expr")"\\
\\
<let> &::=& "(let ("<binding>^{*}") "<body>")"\\
        && {} \qquad \hbox{(Note: all \Code{let}-bound variables must be distinct.)}\\
<binding> &::=& "("<variable> <init>")"\\
<init> &::=& <expression>\\
\\
%\ppridfr &::=& \ \dots\, | "display" | "newline"\\
<keyword>  &::=&  \ \dots\, | "cond" | "let" | "else" | "begin"
\end{eqnarray*}
\end{bnf}

\end{document}
