%!TEX root = r6rs.tex

This appendix presents a non-normative, formal, operational semantics for Scheme, that is based on an earlier semantics~\cite{mf:scheme-op-sem}. It does not cover the entire language. The notable missing features are the macro system, I/O, and the numerical tower. The precise list of features included is given in section~\ref{sec:semantics:grammar}.

The core of the specification is a single-step term rewriting relation that indicates how an (abstract) machine behaves. In general, the report is not a complete specification, giving implementations freedom to behave differently, typically to allow optimizations. This underspecification shows up in two ways in the semantics. 

The first is reduction rules that reduce to special ``\textbf{unknown:} \textit{string}'' states (where the string provides a description of the unknown state). The intention is that rules that reduce to such states can be replaced with arbitrary reduction rules. The precise specification of how to replace those rules is given in section~\ref{sec:semantics:underspecification}.

The other is that the single-step relation relates one program to
multiple different programs, each corresponding to a legal transition
that an abstract machine might take. Accordingly we use the transitive
closure of the single step relation $\rightarrow^*$ to define the
semantics, \calS, as a function from programs (\calP)
to sets of observable results (\calR):
\begin{center}
\begin{tabular}{l}
$\calS : \calP \longrightarrow 2^{\calR}$ \\
$\calS(\calP) = \{ \scrO(\calA) \mid \calP \rightarrow^* \calA \}$
\end{tabular}
\end{center}
where the function $\scrO$ turns an answer ($\calA$) from the semantics into an observable result. Roughly, $\scrO$ is the identity function on simple base values, and returns a special tag for more complex values, like procedure and pairs.

So, an implementation conforms to the semantics if, for every program $\calP$, the implementation produces one of the results in $\calS(\calP)$ or, if the implementation loops forever, then there is an infinite reduction sequence starting at $\calP$, assuming that the reduction relation $\rightarrow$ has been adjusted to replace the \textbf{unknown:} states.

The precise definitions of $\calP$, $\calA$, $\calR$, and $\scrO$ are also given in section~\ref{sec:semantics:grammar}.

To help understand the semantics and how it behaves, we have
implemented it in PLT Redex. The implementation is available at the
report's website: \url{http://www.r6rs.org/}. All of the reduction
rules and the metafunctions shown in the figures in this semantics
were generated automatically from the source code.

\section{Background}

We assume the reader has a basic familiarity with context-sensitive
reduction semantics. Readers unfamiliar with this system may wish to
consult Felleisen and Flatt's monograph~\cite{ff:monograph} or Wright
and Felleisen~\cite{wf:type-soundness} for a thorough introduction,
including the relevant technical background, or an introduction to PLT
Redex~\cite{mfff:plt-redex} for a somewhat lighter one.

As a rough guide, we define the operational semantics of a language
via a relation on program terms, where the relation corresponds to a
single step of an abstract machine. The relation is defined using
evaluation contexts, namely terms with a distinguished place in them,
called \emph{holes}\index{hole}, where the next step of evaluation
occurs. We say that a term $e$ decomposes into an evaluation
context $E$ and another term $e'$ if $e$ is the
same as $E$ but with the hole replaced by $e'$. We write
$E[e']$ to indicate the term obtained by replacing the hole in
$E$ with $e'$.

For example, assuming that we have defined a grammar containing
non-terminals for evaluation contexts ($E$), expressions
($e$), variables ($x$), and values ($v$), we
would write:
%
\begin{displaymath}
  \begin{array}{l}
    E_1[\texttt{((}\sy{lambda}~\texttt{(}x_1 \cdots{}\texttt{)}~e_1\texttt{)}~v_1~\cdots\texttt{)}] \rightarrow
    \\
    E_1[\{ x_1 \cdots \mapsto v_1 \cdots \} e_1] ~~~~~ (\#x_1 = \#v_1)
  \end{array}
\end{displaymath}
%
to define the $\beta_v$ rewriting rule (as a part of the $\rightarrow$
single step relation). We use the names of the non-terminals (possibly
with subscripts) in a rewriting rule to restrict the application of
the rule, so it applies only when some term produced by that grammar
appears in the corresponding position in the term. If the same
non-terminal with an identical subscript appears multiple times, the
rule only applies when the corresponding terms are structurally
identical (nonterminals without subscripts are not constrained to
match each other). Thus, the occurrence of $E_1$ on both the
left-hand and right-hand side of the rule above means that the context
of the application expression does not change when using this rule.
The ellipses are a form of Kleene star, meaning that zero or more
occurrences of terms matching the pattern proceeding the ellipsis may
appear in place of the the ellipsis and the pattern preceding it. We
use the notation $\{ x_1 \cdots \mapsto v_1 \cdots \} e_1$ for
capture-avoiding substitution; in this case it means that each
$x_1$ is replaced with the corresponding $v_1$ in
$e_1$. Finally, we write side-conditions in parentheses beside
a rule; the side-condition in the above rule indicates that the number
of $x_1$s must be the same as the number of $v_1$s.
Sometimes we use equality in the side-conditions; when we do it merely
means simple term equality, i.e., the two terms must have the
same syntactic shape.


\addtocounter{figure}{1} % get the figure counter in sync with the section counter
\subfigurestart{}
\beginfig
\input{r6-fig-grammar-parti.tex}
\caption{Grammar for programs and observables}\label{fig:grammar}
\endfig

Making the evaluation context $E$ explicit in the rule allows
us to define relations that manipulate their context. As a simple
example, we can add another rule that signals a violation when a
procedure is applied to the wrong number of arguments by discarding
the evaluation context on the right-hand side of a rule:
%
\begin{displaymath}
  \begin{array}{l}
    E[\texttt{((}\sy{lambda}~\texttt{(}x_1 \cdots\texttt{)}~e\texttt{)}~v_1~\cdots\texttt{)}] \rightarrow
    \\
    \textrm{\textbf{violation:} wrong argument count} ~~~~~ (\#x_1 \neq \#v_1)
  \end{array}
\end{displaymath}
%
Later we take advantage of the explicit evaluation context in more
sophisticated ways.



\section{Grammar}\label{sec:semantics:grammar}

\beginfig
\subfigureadjust{}
\input{r6-fig-grammar-partii.tex}
\caption{Grammar for evaluation contexts}\label{fig:ec-grammar}
\endfig
\subfigurestop{}

Figure~\ref{fig:grammar} shows the grammar for the subset of the
report this semantics models. Non-terminals are written in
\textit{italics} or in a calligraphic font ($\calP$
$\calA$, $\calR$, and $\calRv$) and literals are 
written in a \texttt{monospaced} font.

The $\calP$ non-terminal represents possible program states. The
first alternative is a program with a store and an expression. 
The second alternative is an uncaught exception, and the third is
used to indicate a place where the model does not completely specify
the behavior of the primitives it models (see section~\ref{sec:semantics:underspecification} for details of those situations). 
The $\calA$ non-terminal
represents a final result of a program. It is just like $\calP$
except that expression has been reduced to some sequence of values.

The $\calR$ and $\calRv$ non-terminals specify the observable results of a program. Each $\calR$ is either a sequence of values that correspond to the values produced by the program that terminates normally, or a tag indicating an uncaught exception was raised, or \sy{unknown} if the program encounters a situation the semantics does not cover. The $\calRv$ non-terminal specifies what the observable results are for a particular value: a pair, the empty list, a symbol, a self-quoting value (\schtrue, \schfalse, and numbers), a condition, or a procedure.

The \nt{sf} non-terminal generates individual elements of the
store. The store holds all of the mutable state of a program. It is
explained in more detail along with the rules that manipulate it.

Expressions ($\mathit{es}$) include quoted data, \sy{begin} expressions, \sy{begin0} expressions%
\footnote{ \sy{begin0} is not part of the standard, but we include it
  to make the rules for \va{dynamic-wind} and \va{letrec} easier to read. Although
  we model it directly, it can be defined in terms of other forms we
  model here that do come from the standard:
\begin{displaymath}
  \begin{array}{rcl}\tt
    \texttt{(}\sy{begin0}~e_1~e_2~\cdots\texttt{)} &=&
    \begin{array}{l}
      \texttt{(}\va{call\mbox{-}with\mbox{-}values}\\
      ~\texttt{(}\sy{lambda}~\texttt{()}~e_1\texttt{)}\\
      ~\texttt{(}\sy{lambda}~x\\
      ~~~e_2~\cdots\\
      ~~~\texttt{(}\va{apply}~\va{values}~x\texttt{)))}
    \end{array}
  \end{array}
\end{displaymath}
}, application expressions, \sy{if} expressions, \sy{set!}
expressions, variables, non-procedure values (\nt{nonproc}), primitive
procedures (\nt{pproc}), lambda expressions, \sy{letrec} and \sy{letrec*} expressions. 

The last few expression forms are only generated for intermediate states (\sy{dw} for \sy{dynamic-wind}, \sy{throw} for continuations, \sy{unspecified} for the result of the assignment operators, \sy{handlers} for exception handlers, and \sy{l!} and \sy{reinit} for \sy{letrec}), and should not appear in an initial program. Their use is described in the relevant sections of this appendix.

The \nt{f} non-terminal describes the formals for \sy{lambda} expressions. (The \sy{dot} is used instead of a period for procedures that accept an arbitrary number of arguments, in order to avoid meta-circular confusion in our PLT Redex model.) 

The \nt{s} non-terminal covers all datums, which can be either non-empty sequences (\nt{seq}), the empty sequence, self-quoting values (\nt{sqv}), or symbols. Non-empty sequences are either just a sequence of datums, or they are terminated with a dot followed by either a symbol or a self-quoting value. Finally the self-quoting values are numbers and the booleans \semtrue{} and \semfalse{}.

The \nt{p} non-terminal represents programs that have no quoted
data. Most of the reduction rules rewrite \nt{p} to \nt{p},
rather than $\calP$ to $\calP$, since quoted data is first
rewritten into calls to the list construction functions before
ordinary evaluation proceeds. In parallel to \nt{es}, \nt{e} represents
expressions that have no quoted expressions.

\beginfig
\begin{center}
\input{r6-fig-Quote.tex}

\input{r6-fig-QtocQtoic.tex}
\end{center}
\caption{Quote}\label{fig:quote}
\endfig

The values ($v$) are divided into four categories:
%
\begin{itemize}
\item Non-procedures (\nt{nonproc}) include pair pointers
  (\va{pp}), the empty list (\va{null}), symbols, self-quoting values
  (\nt{sqv}), and conditions. Conditions represent
  the report's condition values, but here just contain a message and
  are otherwise inert.
\item User procedures (\texttt{(}\sy{lambda} \nt{f} \nt{e} \nt{e} $\cdots$\texttt{)}) include multi-arity lambda expressions and lambda expressions with dotted parameter lists,
\item Primitive procedures (\nt{pproc}) include

\begin{itemize}
\item
 arithmetic procedures
  (\nt{aproc}): \va{+}, \va{-}, \va{/}, and \va{*}, 
\item 
  procedures of one
  argument (\nt{proc1}): \va{null?}, \va{pair?}, \va{car}, \va{cdr},
  \va{call/cc}, \va{procedure?}, \va{condition?}, \va{unspecified?}, \va{raise}, and \va{raise-continuable}, 
  \item
  procedures of
  two arguments (\nt{proc2}): \va{cons}, \va{set-car!}, \va{set-cdr!}, \va{eqv?},
  and \va{call-with-values}, 
  \item as well as \va{list}, \va{dynamic-wind},
  \va{apply}, \va{values}, and \va{with-exception-handler}.
\end{itemize}
\item Finally, continuations are represented as \sy{throw} expressions
  whose body consists of the context where the continuation was
  grabbed.
\end{itemize}
%
The next three set of non-terminals in figure~\ref{fig:grammar} represent pairs (\nt{pp}), which are divided into immutable pairs (\nt{ip}) and mutable pairs (\nt{mp}). The final set of non-terminals in figure~\ref{fig:grammar}, \nt{sym},
\nt{x}, and $n$ represent symbols, variables, and
numbers respectively. The non-terminals \nt{ip}, \nt{mp}, and \nt{sym} are all assumed to all be disjoint. Additionally, the variables $x$ are assumed not to include any keywords or primitive operations, so any program variables whose names coincide with them must be renamed before the semantics can give the meaning of that program.

\beginfig
\begin{center}
\input{r6-fig-Multiple--values--and--call-with-values.tex}
\end{center}
\caption{Multiple values and call-with-values}\label{fig:Multiple--values--and--call-with-values}
\endfig

The set of non-terminals for evaluation contexts is shown in
figure~\ref{fig:ec-grammar}. The \nt{P} non-terminal controls where
evaluation happens in a program that does not contain any quoted data.
The $E$ and $F$ evaluation contexts are for expressions.  They are factored in
that manner so that the \nt{PG}, \nt{G}, and \nt{H} evaluation contexts can
re-use \nt{F} and have fine-grained control over the context to support
exceptions and \va{dynamic-wind}. The starred and circled variants,
\Estar{}, \Eo{}, \Fstar{}, and \Fo{} dictate where a single value is
promoted to multiple values and where multiple values are demoted to a
single value. The \nt{U} context is used to manage the report's underspecification of the results of \sy{set!}, \va{set-car!}, and \va{set-cdr!} (see section~\ref{sec:semantics:underspecification} for details). Finally, the \nt{S} context is where quoted expressions can be simplified. The precise use of the evaluation contexts is explained along with the relevant rules.

To convert the answers ($\calA$)  of the semantics into observable results, we use these two functions:
\input{r6-fig-observable}
\input{r6-fig-observable-value}
They eliminate the store, and replace complex values with simple tags that indicate only the kind of value that was produced or, if no values were produced, indicates that either an uncaught exception was raised, or that the program reached a state that is not specified by the semantics.

\section{Quote}\label{sec:semantics:quote}

The first reduction rules that apply to any program is the 
rules in figure~\ref{fig:quote} that eliminate quoted expressions. 
The first two rules erase the quote for quoted expressions that do not introduce any pairs.
The last two rules lift quoted datums to the top of the expression so
they are evaluated only once, and turn the datums into calls to either \va{cons} or \va{consi}, via the metafunctions $\mathscr{Q}_i$ and $\mathscr{Q}_m$.

Note that the left-hand side of the \rulename{6qcons} and \rulename{6qconsi} rules are identical, meaning that if one rule applies to a term, so does the other rule. 
Accordingly, a quoted expression may be lifted out into a sequence of \va{cons} expressions, which create mutable pairs, or into a sequence of \va{consi} expressions, which create immutable pairs (see section~\ref{sec:semantics:lists} for the rules on how that happens).

These rules apply before any other because of the contexts in which they, and all of the other rules, apply. In particular, these rule applies in the
\nt{S} context. Figure~\ref{fig:ec-grammar} shows that the
\nt{S} context allows this reduction to apply in
any subexpression of an \nt{e}, as long as all of the
subexpressions to the left have no quoted expressions in them,
although expressions to the right may have quoted expressions.
Accordingly, this rule applies once for each quoted expression in the
program, moving out to the beginning of the program.
The rest of the rules apply in contexts that do not contain any quoted
expressions, ensuring that these rules convert all quoted data
into lists before those rules apply.

Although the identifier \nt{qp} does not have a subscript, the semantics of PLT Redex's ``fresh'' declaration takes special care to ensures that the \nt{qp} on the right-hand side of the rule is indeed the same as the one in the side-condition.

\beginfig
\begin{center}
\input{r6-fig-Exceptions}
\end{center}
\caption{Exceptions}\label{fig:Exceptions}
\endfig

\section{Multiple values}

The basic strategy for multiple values is to add a rule that demotes
$(\va{values}~v)$ to $v$ and another rule that promotes
$v$ to $(\va{values}~v)$. If we allowed these rules to apply
in an arbitrary evaluation context, however, we would get infinite
reduction sequences of endless alternation between promotion and
demotion. So, the semantics allows demotion only in a context
expecting a single value and allows promotion only in a context
expecting multiple values. We obtain this behavior with a small
extension to the Felleisen-Hieb framework (also present in the
operational model for R$^5$RS~\cite{mf:op-r5rs}).
We extend the notation so that
holes have names (written with a subscript), and the context-matching
syntax may also demand a hole of a particular name (also written with
a subscript, for instance $E[e]_{\star}$).  The extension
allows us to give different names to the holes in which multiple
values are expected and those in which single values are expected, and
structure the grammar of contexts accordingly.

To exploit this extension, we use three kinds of holes in the
evaluation context grammar in figure~\ref{fig:ec-grammar}. The
ordinary hole \hole{} appears where the usual kinds of
evaluation can occur. The hole \holes{} appears in contexts that
allow multiple values and \holeone{} appears in
contexts that expect a single value. Accordingly, the rule
\rulename{6promote} only applies in \holes{} contexts, and 
\rulename{6demote} only applies in \holeone{} contexts.

To see how the evaluation contexts are organized to ensure that
promotion and demotion occur in the right places, consider the \nt{F},
\Fstar{} and \Fo{} evaluation contexts. The \Fstar{} and \Fo{}
evaluation contexts are just the same as \nt{F}, except that they allow
promotion to multiple values and demotion to a single value,
respectively. So, the \nt{F} evaluation context, rather than being
defined in terms of itself, exploits \Fstar{} and \Fo{} to dictate
where promotion and demotion can occur. For example, \nt{F} can be
$\texttt{(}\sy{if}~\Fo{}~e~e\texttt{)}$ meaning that demotion from
$\texttt{(}\va{values}~v\texttt{)}$ to
$v$ can occur in the test of an \sy{if} expression.
Similarly, $F$ can be $\texttt{(}\sy{begin}~\Fstar{}~e~e~\cdots\texttt{)}$ meaning that
$v$ can be promoted to $\texttt{(}\va{values}~v\texttt{)}$ in the first subexpression of a \sy{begin}.

In general, the promotion and demotion rules simplify the definitions
of the other rules. For instance, the rule for \sy{if} does not
need to consider multiple values in its first subexpression.
Similarly, the rule for \sy{begin} does not need to consider the
case of a single value as its first subexpression.

\beginfig
\begin{center}
\input{r6-fig-Arithmetic.tex}
\input{r6-fig-Basic--syntactic--forms.tex}
\end{center}
\caption{Arithmetic and basic forms}\label{fig:Arithmetic}
\endfig

The other two rules in
figure~\ref{fig:Multiple--values--and--call-with-values} handle
\va{call-\hp{}with-\hp{}values}. The evaluation contexts for
\va{call-with-values} (in the $F$ non-terminal) allow
evaluation in the body of a procedure that has been passed as the first
argument to \va{call-with-values}, as long as the second argument
has been reduced to a value. Once evaluation inside that procedure
completes, it will produce multiple values (since it is an \Fstar{}
position), and the entire \va{call-with-values} expression reduces
to an application of its second argument to those values, via the rule
\rulename{6cwvd}. Finally, in the
case that the first argument to \va{call-with-values} is a value,
but is not of the form $\texttt{(}\sy{lambda}~\texttt{()}~e\texttt{)}$, the rule
\rulename{6cwvw} wraps it in a thunk to trigger evaluation.

\beginfig
\begin{center}
\input{r6-fig-Cons.tex}
\end{center}
\caption{Lists}\label{fig:Cons}
\endfig

\section{Exceptions}

The workhorses for the exception system are $$\texttt{(}\sy{handlers}~\nt{proc}~\cdots{}~\nt{e}\texttt{)}$$ expressions and the \nt{G} and \nt{PG} evaluation contexts (shown in figure~\ref{fig:ec-grammar}). 
The \sy{handlers} expression records the
active exception handlers (\nt{proc} $\cdots$) in some expression (\nt{e}). The
intention is that only the nearest enclosing \sy{handlers} expression
is relevant to raised exceptions, and the $G$ and \nt{PG} evaluation
contexts help achieve that goal. They are just like their counterparts
\nt{E} and \nt{P}, except that \sy{handlers} expressions cannot occur on the
path to the hole, and the exception system rules take advantage of
that context to find the closest enclosing handler.

To see how the contexts work together with \sy{handler}
expressions, consider the left-hand side of the \rulename{6xunee}
rule in figure~\ref{fig:Exceptions}.
It matches expressions that have a call to \va{raise} or
\va{raise-continuable} (the non-terminal \nt{raise*} matches
both exception-raising procedures) in a \nt{PG}
evaluation context. Since the \nt{PG} context does not contain any
\sy{handlers} expressions, this exception cannot be caught, so
this expression reduces to a final state indicating the uncaught
exception. The rule \rulename{6xuneh} also signals an uncaught
exception, but it covers the case where a \sy{handlers} expression
has exhausted all of the handlers available to it. The rule applies to
expressions that have a \sy{handlers} expression (with no
exception handlers) in an arbitrary evaluation context where a call to
one of the exception-raising functions is nested in the
\sy{handlers} expression. The use of the \nt{G} evaluation
context ensures that there are no other \sy{handler} expressions
between this one and the raise.

The next two rules cover call to the procedure \va{with-exception-handler}.
The \rulename{6xwh1} rule applies when there are no \sy{handler}
expressions. It constructs a new one and applies $\nt{v}_2$ as a
thunk in the \sy{handler} body. If there already is a handler
expression, the \rulename{6xwhn} applies. It collects the current
handlers and adds the new one into a new \sy{handlers} expression
and, as with the previous rule, invokes the second argument to
\va{with-exception-handlers}.

The next two rules cover exceptions that are raised in the context of
a \sy{handlers} expression. If a continuable exception is raised,
\rulename{6xrc} applies. It takes the most recently installed
handler from the nearest enclosing \sy{handlers} expression and
applies it to the argument to \va{raise-continuable}, but in a
context where the exception handlers do not include that latest
handler. The \rulename{6xr} rule behaves similarly, except it
raises a new exception if the handler returns. The new exception is
created with the \sy{make-cond} special form.

\beginfig
\begin{center}
\input{r6-fig-Eqv.tex}
\end{center}
\caption{Eqv}\label{fig:Eqv}
\endfig

The \sy{make-cond} special form is a stand-in for the report's
conditions. It does not evaluate its argument (note its absence from
the $E$ grammar in figure~\ref{fig:ec-grammar}). That argument
is just a literal string describing the context in which the exception
was raised. The only operation on conditions is \va{condition?},
whose semantics are given by the two rules \rulename{6ct} and
\rulename{6cf}.

Finally, the rule \rulename{6xdone} drops a \sy{handlers} expression
when its body is fully evaluated, and the rule \rulename{6weherr}
raises an exception when \va{with-exception-handler} is supplied with
incorrect arguments.

\section{Arithmetic and basic forms}

This model does not include the report's arithmetic, but does include
an idealized form in order to make experimentation with other features
and writing test suites for the model simpler.
Figure~\ref{fig:Arithmetic} shows the reduction rules for the
primitive procedures that implement addition, subtraction,
multiplication, and division. They defer to their mathematical
analogues. In addition, when the subtraction or divison operator are
applied to no arguments, or when division receives a zero as a
divisor, or when any of the arithmetic operations receive a
non-number, an exception is raised.

The bottom half of figure~\ref{fig:Arithmetic} shows the rules for
\sy{if}, \sy{begin}, and \sy{begin0}. The relevant
evaluation contexts are given by the $F$ non-terminal.

The evaluation contexts for \sy{if} only allow evaluation in its
test expression. Once that is a value, the rules reduce
an \sy{if} expression to its consequent if the test is not
\semfalse{}, and to its alternative if it is \semfalse{}.

The \sy{begin} evaluation contexts allow evaluation in the first
subexpression of a begin, but only if there are two or more
subexpressions. In that case, once the first expression has been fully
simplified, the reduction rules drop its value. If there is only a
single subexpression, the \sy{begin} itself is dropped.

\subfigurestart{}
\beginfig
\begin{center}
\input{r6-fig-Procedure--application.tex}
\end{center}
\caption{Procedures \& application}\label{fig:Procedure--application}
\endfig

Like the \sy{begin} evaluation contexts, the \sy{begin0}
evaluation contexts allow evaluation of the first subexpression of a
\sy{begin0} expression when there are two or more subexpressions.
The \sy{begin0} evaluation contexts also allow evaluation in the
second subexpression of a \sy{begin0} expression, as long as the first
subexpression has been fully simplified. The \rulename{6begin0n} rule for
\sy{begin0} then drops a fully simplified second subexpression.
Eventually, there is only a single expression in the \sy{begin0},
at which point the \rulename{begin01} rule fires, and removes the
\sy{begin0} expression.

\section{Lists}\label{sec:semantics:lists}

The rules in figure~\ref{fig:Cons} handle lists. The first two rules handle \va{list} by reducing it to a succession of calls to \va{cons}, followed by \va{null}.

The next two rules, \rulename{6cons} and \rulename{6consi}, allocate new \va{cons} cells.
They both move $\texttt{(}\va{cons}~v_1~v_2\texttt{)}$ into the store, bound to a fresh
pair pointer (see also section~\ref{sec:semantics:quote} for a description of ``fresh''). 
The \rulename{6cons} uses a \nt{mp} variable, to indicate the pair is mutable, and the \rulename{6consi} uses a \nt{ip} variable to indicate the pair is immutable.

The rules \rulename{6car} and \rulename{6cdr} extract the components of a pair from the store when presented with a pair pointer (the \nt{pp} can be either \nt{mp} or \nt{ip}, as shown in figure~\ref{fig:grammar}).

The rules \rulename{6setcar} and \rulename{6setcdr} handle assignment of mutable pairs. 
They replace the contents of the appropriate location in the store with the new value, and reduce to \va{unspecified}. See section~\ref{sec:semantics:underspecification} for an explanation of how \va{unspecified} reduces.

\beginfig
\subfigureadjust{}
\begin{center}
\input{r6-fig-Var-set!d_.tex}
\end{center}
\caption{Variable-assignment relation}\label{fig:varsetd}
\endfig

The next four rules handle the \va{null?} predicate and the \va{pair?} predicate, and the final four rules raise exceptions when \va{car}, \va{cdr}, \va{set-car!} or \va{set-cdr!} receive non pairs.

\section{Eqv}

The rules for \va{eqv?} are shown in figure~\ref{fig:Eqv}. The first two rules cover most of the behavior of \va{eqv?}. 
The first says that when the two arguments to \va{eqv?} are syntactically identical, then \va{eqv?} produces \semtrue{} and the second says that when the arguments are not syntactically identical, then \va{eqv?} produces \semfalse{}. 
The structure of \nt{v} has been carefully designed so that simple term equality corresponds closely to \va{eqv?}'s behavior. 
For example, pairs are represented as pointers into the store and \va{eqv?} only compares those pointers.

The side-conditions on those first two rules ensure that they do not apply when simple term equality does not match the behavior of \va{eqv?}. There are two situations where it does not match: comparing two conditions and comparing two procedures. For the first, the report does not specify \va{eqv?}'s behavior, except to say that it must return a boolean, so the remaining two rules (\rulename{6eqct}, and \rulename{6eqcf}) allow such comparisons to return \semtrue{} or \semfalse{}. Comparing two procedures is covered in section~\ref{sec:semantics:underspecification}. 

\section{Procedures and application}

In evaluating a procedure call, the report leaves
unspecified the order in which arguments are evaluated. So, our reduction system allows multiple, different reductions to occur, one for each possible order of evaluation.

To capture unspecified evaluation order but allow only evaluation that
is consistent with some sequential ordering of the evaluation of an
application's subexpressions, we use non-deterministic choice to first pick
a subexpression to reduce only when we have not already committed to
reducing some other subexpression. To achieve that effect, we limit
the evaluation of application expressions to only those that have a
single expression that is not fully reduced, as shown in the
non-terminal $F$, in figure~\ref{fig:ec-grammar}. To evaluate
application expressions that have more than two arguments to evaluate,
the rule \rulename{6mark} picks one of the subexpressions of an
application that is not fully simplified and lifts it out in its own
application, allowing it to be evaluated. Once one of the lifted
expressions is evaluated, the \rulename{6appN} substitutes its value
back into the original application.

The \rulename{6appN} rule also handles other applications whose
arguments are finished by substituting the first argument for
the first formal parameter in the expression. Its side-condition uses
the relation in figure~\ref{fig:varsetd} to ensure that there are no
\sy{set!} expressions with the parameter $x_1$ as a target.
If there is such an assignment, the \rulename{6appN!} rule applies (see also section~\ref{sec:semantics:quote} for a description of ``fresh'').
Instead of directly substituting the actual parameter for the formal
parameter, it creates a new location in the store, initially bound the
actual parameter, and substitutes a variable standing for that
location in place of the formal parameter. The store, then, handles
any eventual assignment to the parameter. Once all of the parameters
have been substituted away, the rule \rulename{6app0} applies and
evaluation of the body of the procedure begins.

At first glance, the rule \rulename{6appN} appears superfluous, since it seems like the rules could just reduce first by \rulename{6appN!} and then look up the variable when it is evaluated. 
There are two reasons why we keep the \rulename{6appN}, however. 
The first is purely conventional: reducing applications via substitution is taught to us at an early age and is commonly used in rewriting systems in the literature.
The second reason is more technical:  the
\rulename{6mark} rule requires that \rulename{6appN} be applied once $\nt{e}_i$ has been reduced to a value. \rulename{6appN!} would
lift the value into the store and put a variable reference into the application, leading to another use of \rulename{6mark}, and another use of \rulename{6appN!}, which continues forever.

The rule \rulename{6$\mu$app} handles a well-formed application of a function with a dotted parameter lists. 
It such an application into an application of an
ordinary procedure by constructing a list of the extra arguments. Similarly, the rule \rulename{6$\mu$app1} handles an application of a procedure that has a single variable as its parameter list.

The rule \rulename{6var} handles variable lookup in the store and \rulename{6set} handles variable assignment.

The next two rules \rulename{6proct} and \rulename{6procf} handle applications of \va{procedure?}, and the remaining rules cover applications of non-procedures and arity violations.

\beginfig
\subfigureadjust{}
\begin{center}
\input{r6-fig-Apply.tex}
\input{r6-fig-circular_.tex}
\end{center}
\caption{Apply}\label{fig:Apply}
\endfig
\subfigurestop{}

The rules in figure~\ref{fig:Apply} 
cover \va{apply}. 
The first rule, \rulename{6applyf}, covers the case where the last argument to
\va{apply} is the empty list, and simply reduces by erasing the
empty list and the \va{apply}. The second rule, \rulename{6applyc}
covers a well-formed application of \va{apply} where \va{apply}'s final argument is a pair. It
reduces by extracting the components of the pair from the store and
putting them into the application of \va{apply}. Repeated
application of this rule thus extracts all of the list elements passed
to \va{apply} out of the store. 

The remaining five rules cover the
various violations that can occur when using \va{apply}. The first one covers the case where \va{apply} is supplied with a cyclic list. The next four cover applying a
non-procedure, passing a non-list as the last argument, and supplying
too few arguments to \va{apply}.

\section{Call/cc and dynamic wind}

\beginfig
\begin{center}
\input{r6-fig-Call-cc--and--dynamic-wind.tex} \\
\input{r6-fig-TrimpRepoSt.tex}
\end{center}
\caption{Call/cc and dynamic wind}\label{fig:Call-cc--and--dynamic-wind}
\endfig

The specification of \va{dynamic-wind} uses 
$\texttt{(}\sy{dw}~x~e~e~e\texttt{)}$
expressions to record which dynamic-wind \var{thunk}s are active at
each point in the computation. Its first argument is an identifier
that is globally unique and serves to identify invocations of
\va{dynamic-wind}, in order to avoid exiting and re-entering the
same dynamic context during a continuation switch. The second, third,
and fourth arguments are calls to some \var{before}, \var{thunk}, and
\var{after} procedures from a call to \va{dynamic-wind}. Evaluation only
occurs in the middle expression; the \sy{dw} expression only
serves to record which \var{before} and \var{after} procedures need to be run during a
continuation switch. Accordingly, the reduction rule for an
application of \va{dynamic-wind} reduces to a call to the
\var{before} procedure, a \sy{dw} expression and a call to the
\var{after} procedure, as
shown in rule \rulename{6wind} in
figure~\ref{fig:Call-cc--and--dynamic-wind}. The next two rules cover
abuses of the \va{dynamic-wind} procedure: calling it with
non-procedures, and calling it with the wrong number of arguments. The
\rulename{6dwdone} rule erases a \sy{dw} expression when its second
argument has finished evaluating.

The next two rules cover \va{call/cc}. The rule
\rulename{6call/cc} creates a new continuation. It takes the context
of the \va{call/cc} expression and packages it up into a
\sy{throw} expression that represents the continuation. The
\sy{throw} expression uses the fresh variable $x$ to record
where the application of \va{call/cc} occurred in the context for
use in the \rulename{6throw} rule when the continuation is applied.
That rule takes the arguments of the continuation, wraps them with a
call to \va{values}, and puts them back into the place where the
original call to \va{call/cc} occurred, replacing the current
context with the context returned by the $\mathscr{T}$ metafunction.

The $\mathscr{T}$ (for ``trim'') metafunction accepts two $D$ contexts and
builds a context that matches its second argument, the destination
context, except that additional calls to the \var{before} and
\var{after} procedures
from \sy{dw} expressions in the context have been added.

The first clause of the $\mathscr{T}$ metafunction exploits the
$H$ context, a context that contains everything except
\sy{dw} expressions. It ensures that shared parts of the
\va{dynamic-wind} context are ignored, recurring deeper into the
two expression contexts as long as the first \sy{dw} expression in
each have matching identifiers ($x_1$). The final rule is a
catchall; it only applies when all the others fail and thus applies
either when there are no \sy{dw}s in the context, or when the
\sy{dw} expressions do not match. It calls the two other
metafunctions defined in figure~\ref{fig:Call-cc--and--dynamic-wind} and
puts their results together into a \sy{begin} expression.

The $\mathscr{R}$ metafunction extracts all of the \var{before}
procedures from its argument and the $\mathscr{S}$ metafunction extracts all of the \var{after} procedures from its argument. They each construct new contexts and exploit
$H$ to work through their arguments, one \sy{dw} at a time.
In each case, the metafunctions are careful to keep the right
\sy{dw} context around each of the procedures in case a continuation
jump occurs during one of their evaluations. 
Since $\mathscr{R}$,
receives the destination context, it keeps the intermediate
parts of the context in its result.
In contrast
$\mathscr{S}$ discards all of the context except the \sy{dw}s,
since that was the context where the call to the
continuation occurred.

\section{Letrec}

\beginfig
\begin{center}
\input{r6-fig-Letrec.tex}
\end{center}
\caption{Letrec and letrec*}
\label{fig:Letrec}
\endfig

Figre~\ref{fig:Letrec} shows the rules that handle \sy{letrec} and \sy{letrec*} and the supplementary expressions that they produce, \sy{l!} and \sy{reinit}. As a first approximation, both \va{letrec} and \va{letrec*} reduce by allocating locations in the store to hold the values of the init expressions, initializing those locations to \sy{bh} (for ``black hole''), evaluating the init expressions, and then using \va{l!} to update the locations in the store with the value of the init expressions. They also use \va{reinit} to detect when an init expression in a letrec is reentered via a continuation.

Before considering how \sy{letrec} and \sy{letrec*} use \sy{l!} and \sy{reinit}, first consider how \sy{l!} and \sy{reinit} behave. The first two rules in figure~\ref{fig:Letrec} cover \sy{l!}. It behaves very much like \sy{set!}, but it initializes both ordinary variables, and variables that are current bound to the black hole (\sy{bh}).

The next two rules cover ordinary \sy{set!} when applied to a variable
that is currently bound to a black hole. This situation can arise when
the program assigns to a variable before letrec initializes it, eg
\verb|(letrec ((x (set! x 5))) x)|. The report specifies that either
an implementation should perform the assignment, as reflected in the
\rulename{6setdt} rule or it raise an exception, as reflected in the \rulename{6setdte} rule.

The \rulename{6dt} rule covers the case where a variable is referred
to before the value of a init expression is filled in, which must
always raise an exception.

A \va{reinit} expression is used to detect a program that captures a continuation in an initialization expression and returns to it, as shown in the three rules \rulename{6init}, \rulename{6reinit}, and \rulename{6reinite}. The \va{reinit} form accepts an identifier that is bound in the store to a boolean as its argument. Those are identifiers are initially \semfalse{}. When \va{reinit} is evaluated, it checks the value of the variable and, if it is still \semfalse{}, it changes it to \semtrue{}. If it is already \semtrue{}, then \va{reinit} either just does nothing, or it raises an exception, in keeping with the two legal behaviors of \va{letrec} and \va{letrec*}. 

The last two rules in figure~\ref{fig:Letrec} put together \sy{l!} and \sy{reinit}. The \rulename{6letrec} rule reduces a \sy{letrec} expression to an application expression, in order to capture the unspecified order of evaluation of the init expressions. Each init expression is wrapped in a \sy{begin0} that records the value of the init and then uses \sy{reinit} to detect continuations that return to the init expression. Once all of the init expressions have been evaluated, the procedure on the right-hand side of the rule is invoked, causing the value of the init expression to be filled in the store, and evaluation continues with the body of the original \sy{letrec} expression.

The \rulename{6letrec*} rule behaves similarly, but uses a \sy{begin} expression rather than an application, since the init expressions are evaluated from left to right. Moreover, each init expression is filled into the store as it is evaluated, so that subsequent init expressions can refer to its value.

\section{Underspecification}\label{sec:semantics:underspecification}

\beginfig
\begin{center}
\input{r6-fig-Underspecification.tex}
\end{center}
\caption{Explicitly unspecified behavior}\label{fig:Underspecification}
\endfig

The rules in figure~\ref{fig:Underspecification} cover aspects of the
semantics that are explicitly unspecified. Implementations can replace
the rules \rulename{6ueqv}, \rulename{6uval} and with different rules that cover the left-hand sides and, as long as they follow the informal specification, any replacement is valid. Those three situations correspond to the case when \va{eqv?} applied to two procedures and when multiple values are used in a single-value context.

The remaining rules in figure~\ref{fig:Underspecification} cover the results from the assignment operations, \sy{set!}, \va{set-car!}, and \va{set-cdr!}. An implementation does not adjust those rules, but instead renders them useless by adjusting the rules that insert \va{unspecified}: \rulename{6setcar}, \rulename{6setcdr}, \rulename{6set}, and \rulename{6setd}. Those rules can be adjusted by replacing \va{unspecified} with any number of values in those rules.

So, the remaining rules just specify the minimal behavior that we know that a value or values must have and otherwise reduce to an \textbf{unknown:} state. The rule \rulename{6udemand} drops \va{unspecified} in the \sy{U} context. See figure~\ref{fig:ec-grammar} for the precise definition of \sy{U}, but intuitively it is a context that is only a single expression layer deep that contains expressions whose value depends on the value of their subexpressions, like the first subexpression of a \sy{if}. Following that are rules that discard \va{unspecified} in expressions that discard the results of some of their subexpressions. The \rulename{6ubegin} shows how \sy{begin} discards its first expression when there are more expressions to evaluate. The next two rules, \rulename{6uhandlers} and \rulename{6udw} propagate \va{unspecified} to their context, since they also return any number of values to their context. Finally, the two \va{begin0} rules preserve \va{unspecified} until the rule \rulename{6begin01} can return it to its context.

%\section*{Acknowledgments}
%Thanks to Michael Sperber for many helpful discussions of specific points in the semantics, for spotting many mistakes and places where the formal semantics diverged from the informal semantics, and for generally making it possible for us to keep up with changes to the informal semantics as it developed. Thanks also to Will Clinger for a careful reading of the semantics and its explanation.

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "r6rs"
%%% End: 
