\documentclass[11pt]{handout}
\usepackage{6044}
%\documentclass[11pt]{article}
%\usepackage{6001}
\usepackage{time,fullpage}
\usepackage{amsmath}

\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

\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}

\makeatletter


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


\begin{document}
\handout{rewriting-model-1}{A Term Rewriting Model for Scheme\\
I. The Functional Kernel}%
{September 4, 1996; revised$^{4}$ October 30, 1996}

\section{Rewrite Rules}\label{rewrite-rules}

\subsection{Primitive Application Rules}

A useful way to think about computation in Scheme is as {\em algebraic
simplification\/} aimed at computing the {\em value\/} of an expression.

Let's start by considering a simple arithmetic combination of numbers in
Scheme notation:
\[\Code{(+ 0 1 (- 2 3) (* 4 5 (* -6 -7)))}.\]
We take for granted an infinite set of {\em primitive application\/} rules
for rewriting such expressions, for example,
\begin{eqnarray*}
\Code{(- 2 3)}  & \rulesto & \Code{-1}\\
\Code{(* 4 5 42)}  & \rulesto & \Code{840}\\
\vdots
\end{eqnarray*}
In general, a primitive application rule is of the form
\[\bnf
"("\ppridfr\ \pval_{1} \ldots")" \rulesto \pval,
\]
where \pval's are atomic expressions like numbers or truth values, and
primitive procedure identifiers are names like \Code{+}, \Code{<}, and
\Code{atan}, etc., which in Scheme are bound to ``built-in'' procedures
applicable to primitive values.

By repeatedly replacing left hand sides of rules with their right hand
sides, we can eventually rewrite the expression above to its numerical
value.  As an aid in reading the calculation, we underline the successive
subexpressions which are to be rewritten:
\begin{eqnarray*}
\Code{(+ 0 1 (- 2 3) (* 4 5 \underline{(* -6 -7)}))}
        & \rulesto & \Code{(+ 0 1 \underline{(- 2 3)} (* 4 5 42))}\\
{}&  \rulesto & \Code{(+ 0 1 -1 \underline{(* 4 5 42)})}\\
{}&  \rulesto & \Code{(+ 0 1 -1 840)}\\
{}&  \rulesto & \Code{840}
\end{eqnarray*}

Another familiar set of primitive application rules result in the {\em
Booleans} \Code{#t}, \Code{#f}:
\begin{eqnarray*}
\Code{(< 6 7)}  & \rulesto & \Code{#t}\\
\Code{(zero? -1.414)}  & \rulesto & \Code{#f}\\
\vdots
\end{eqnarray*}
For example, using these rules and the numerical ones above allows us to
handle:
\begin{eqnarray*}
\Code{(< (+ 0 1 2) \underline{(/ 3 1)})}  & \rulesto
        & \Code{(< \underline{(+ 0 1 2)} 3)}\\
{}&  \rulesto & \Code{(< 3 3)}\\
{}&  \rulesto & \Code{#f}
\end{eqnarray*}

Note that there is no specified order or location for applying the rules.
We might have chosen to rewrite the example above using the rules in
another order:
\begin{eqnarray*}
\Code{(< \underline{(+ 0 1 2)} (/ 3 1))}
        & \rulesto & \Code{(< 3 \underline{(/ 3 1)})}\\
{}&  \rulesto & \Code{(< 3 3)}\\
{}&  \rulesto & \Code{#f}
\end{eqnarray*}

An expression to which no rules can be applied is called {\em terminated}.
Primitive rewriting has two familiar, important properties:
\begin{itemize}
\item {\bf Termination}.  No matter in what order the rewriting rules are
applied, a terminated expression\footnote{We usually expect the terminated
expression to be a primitive value, but some ``ill-typed'' expressions
like \Code{(+ \#t 3)} are terminated but do not have values.  (What would
Scheme do when such an expression is evaluated?)} will eventually be
reached.

\item {\bf Uniqueness}. No matter in what order the rewriting rules
are applied, the terminated expression arrived at is the same!
\end{itemize}

The Termination property is obvious because primitive applications always
shorten an expression.  We'll say more about Uniqueness below.

\subsection{Immediate Values}

In addition to the primitive values, procedure identifiers like \Code{+}
or \Code{<} are themselves a kind of value\footnote{We assume here that
procedure identifiers {\em won't} be redefined!  Note that according to
the official definition of \RFS, these identifiers {\em are} treated as
variables and it is possible to redefine them.  As a matter of fact, in
6.001 Scheme, the arithmetic operators do get redefined slightly from
general MIT Scheme---so that novice users don't unexpectedly generate the
huge quotients possible from Scheme's infinite-precision rational number
operations.}.  Scheme also provides a means to {\em construct} procedures
values, namely, with {\em lambda expressions\/}. The
\begin{itemize}
\item primitive values,
\item procedure identifiers, and
\item lambda expressions,
\end{itemize} are called {\em immediate values}.

\subsection{Conditional Rules} Other familiar algebraic rules like
\begin{eqnarray*}
(1 \cross A) & = & A\\
(A + 0)  & = & A\\
(A \cross 0)  & = & 0\\
\vdots
\end{eqnarray*}
allow simplifications of arbitrary subexpressions, $A$, which may contain
variables, as opposed to just combinations of constants as above.

Scheme's rules for \Code{if} expressions, also called {\em conditionals},
resemble this sort of algebraic rule.  There are only two rewrite rules
for an \Code{if} expression:
\[\begin{array}{l}
\Code{(if \#f $\expr_{1}$ $\expr_{2}$)} \rulesto \expr_{2},\\
\Code{(if $V$ $\expr_{1}$ $\expr_{2}$)} \rulesto \expr_{1},\\
\mbox{when $V$ is an \ival\ not equal to \Code{\#f}}.
\end{array}\]

Simple as they are, these two rules differ significantly from the
primitive application rules because $\expr_{1}$ and $\expr_{2}$ may be
{\em any\/} Scheme expressions, not just immediate values as with
primitive applications.

Now we can do rewriting such as
\begin{align*}
{}  & \Code{\underline{(if (lambda (a b) c)
        (if (< (+ 0 1 2) (/ 3 1)) atan (lambda (x) x)) +)}}\\
{}\rulesto{} & \Code{(if (< (+ 0 1 2) \underline{(/ 3 1)}) atan (lambda (x) x))}\\
\vdots\\
\rulesto{} & \Code{\underline{(if \#f atan (lambda (x) x))}}\\
\rulesto{} & \Code{(lambda (x) x)}
\end{align*}

As long as we restrict to a {\em functional} subset of
Scheme\footnote{Appendix~\ref{grammar} contains a grammar for the
functional part of Scheme we consider.}, i.e., Scheme without
side-effects, the termination and uniqueness properties still hold for
rewritings using both primitive applications and conditional rules.
In particular, although rewriting the second or third expressions (called
the {\em consequent\/} and the {\em alternative\/} of the conditional)
before simplifying the first expression (called the {\em test\/}) may
waste some effort, or may even cause an error, it will never result in a
different value than the obvious strategy of first rewriting the test into
an immediate value.

\problem The algebraic rules above do {\em not} accurately reflect Scheme
behavior.
\begin{subproblems}
\item Describe a definition of \Code{x} such that evaluation of \Code{(* 1 x)}
does not return the value of \Code{x}.
\item Describe a simple Scheme expression, $A$, such that evaluation of
\Code{(* $A$ 0)} neither returns \Code{0} nor interrupts with an error.
\end{subproblems}

\section{Substitution Models}

Another familiar part of algebra is the use of names for expressions, for
example, the names ``$p$,'' ``$p_{1}$,'' and ``$p_{2}$'' in:
\begin{quote}
Let $p(x) = x^{2}-1$.  The polynomial $p$ factors into $p_{1}\cdot p_{2}$,
where $p_{1}(x) = x + 1$ and $p_{2}(x) = x - 1$.
\end{quote}

{\em Variable instantiation} is a basic naming rule of algebra: substitute
an expression for an occurrence of its name.  For example, using
instantiation and primitive applications in Scheme, we can carry out the
following calculation:
\begin{eqnarray*}
\lefteqn{\Code{(define y 7) (define x <) (x (+ 1 2) \underline{y})}}\\
{} & \rulesto & \Code{(define y 7) (define x <) (x \underline{(+ 1 2)} 7)}\\
{} & \rulesto & \Code{(define y 7) (define x <) (\underline{x} 3 7)}\\
{} & \rulesto & \Code{(define y 7) (define x <) \underline{(< 3 7)}}\\
{} & \rulesto & \Code{(define y 7) (define x 3) \#t}
\end{eqnarray*}

A system of rules which explain Scheme computation in terms of symbolic
manipulation of Scheme expressions and definitions is called a {\em
Substitution Model} for Scheme.

For ordinary algebra, naming rules are not much emphasized.  In contrast,
for nearly all programming languages, rules for handling names and their
definitions play a key role---arguably a more important one than the
ordinary algebraic simplification rules described in
Section~\ref{rewrite-rules}.

\subsection{Instantiation}
The Scheme version of the {\em variable instantiation rule\/} is:
\[\vrbl \rulesto \ival\]
\begin{quote}
\noindent when \vrbl\ is bound to \ival\ and no variable binding is
changed by the rewriting.
\end{quote}

There are three aspects of this rule which need to be explained.

First, we need to specify which, if any, definitions {\em bind} which
occurrences of variables, in order to know which immediate value to
substitute where---after all, there may be different definitions of the
same variable in different parts of an expression.  Scheme's binding rule
is quite simple: starting at the occurrence of the variable to be
instantiated, search back through the enclosing subexpressions until
arriving at a definition of that variable.\footnote{A more precise
specification of Scheme's binding (also called {\em scoping}) rules, is
given in Appendix~\ref{scope}.}

Second, we note that variables are only instantiated with {\em immediate values},
not arbitrary expressions, because in our kernel Scheme, definitions may
only bind variables to immediate values.  For example, a definition such as
\[\Code{(define y (+ 1 2)) (* y y)}\]
is not part of the functional kernel.\footnote{Such non-immediate
definitions will be handled later when we extend our model to include
assignment statements, i.e., Scheme's special form \Code{set!}.}

Third is the condition that variable binding not be changed by
instantiation.  For example, in Scheme we could define \Code{add2} and
\Code{add3} procedures as follows:
\[\begin{array}{l}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{(define add3 (lambda (n) (+ 1 (\underline{add2} n))))}
\end{array}\]
so that evaluating \Code{(add3 5)} would return \Code{8}.

But suppose we {\bf naively} instantiate the underlined occurrence of
\Code{add2}, obtaining:
\begin{lisp}
(define n 2)
(define add2 (lambda (m) (+ m n)))
(define add3 (lambda (n) (+ 1 ((lambda (m) (+ m n)) n))))
\end{lisp}
Now, evaluating \Code{(add3 5)} would return \Code{11}!

The problem is that the occurrence of \Code{n} is bound to \Code{2} in the
definition of \Code{add2}, but in the instantiated copy of \Code{add2}'s
value, the copied occurrence of \Code{n} has become bound by the
\Code{lambda (n)} in the definition of \Code{add3}.  This change in
\Code{n}'s binding is what has to be prevented in order to reflect
Scheme's static scoping discipline.

Instantiation at arbitrary positions will be possible after we describe
some additional rules in Section~\ref{renaming} and Appendix~\ref{scope}
for changing defined names into ``fresh'' names.  However, there is no
need for renaming, and no problem about changed bindings, as long as we
obey
\begin{quote}
{\bf The Lambda Body Rewriting Restriction}: {\em Don't rewrite any
expression within the body of a lambda expression.}
\end{quote}
This works because in Scheme grammar, the only place definitions can occur
is at ``top level'' or at the beginning of lambda bodies.  So there is no
possibility of bindings being changed by instantiating occurrences of
variables outside lambda bodies.  Real Scheme evaluates in an order
obeying the lambda body restriction.

\problem Describe a simple Scheme expression, $M$, such that evaluation of
$M$ returns 0 but evaluation of $N$ returns 1, where $N$ is the expression
which results from a naive instantiation (without renaming) inside some
lambda body in $M$.

\subsection{Lambda Applications} The Substitution Model sketched in 6.001
handled procedure applications with a {\em substitution rule} rule of the
form:
\begin{quote}
Rewrite ``\Code{((lambda ($x$) $B$) $V$)}'' as ``$B$ with $V$ substituted
for $x$,''\\
where $V$ is an immediate value.
\end{quote}

In these notes we describe a slightly different rule for procedure
application.  Using this new rule dramatically
shortens the size of rewritten
expressions in many examples.
It also will allow us to model Scheme's computational behavior
more accurately.\footnote{The Substitution Model in 6.001 is
  sketchily described (on purpose, to avoid distracting beginners with
  details).  The most straightforward ways of spelling out the details
  lead to models which have to be abandoned in favor of the 
  {\em environment model} in order to explain side-effects.
  The Substitution Model described in these
  notes extends to handle side-effects quite well.  In
  fact, the environment model can be understood as a way to
  {\em implement} the present Substitution Model efficiently.}

We'll simply call the new rule the {\em lambda application rule}.  A
simplified example of this rule is:
\begin{quote}
Rewrite ``\Code{((lambda ($x$) $B$) $V$)}'' as ``$B$,''\\
while adding the definition ``\Code{(define $x$ $V$)}.''
\end{quote}
Of course to use this rule, we'll need to specify where and how to ``add''
definitions.

It's helpful to realize that the new lambda application rule could be used
to simulate the old 6.001 rule: starting with \Code{((lambda ($x$) $B$)
$V$)}, use the lambda application rule.  This gives $B$ along with the
definition \Code{(define $x$ $V$)}.  Then, by successively instantiating
all the $x$'s in $B$ by copies of $V$, we arrive at the same result as the
substitution rule.  Well almost---we still have the definition of $x$
hanging around.  But since we instantiated all the $x$'s, this definition
no longer refers to anything and is not needed.  So we will apply an
additional ``garbage collection'' rule which allows us to remove
unreferenced definitions.

\subsubsection{Bodies}
Note that we might have tried expressing the rule above as
\begin{eqnarray*}
\lefteqn{\Code{((lambda ($x$) $B$) $V$)}}\\ &\rulesto& \Code{(define $x$ $V$) $B$}.
\end{eqnarray*}
This version introduces a slight grammatical complication: the expression
on the left hand side of the rule rewrites into a sequence of two
things---a definition followed by the body, $B$, of the lambda expression.
If there were several formal parameters instead of just $x$, there
would be several definitions preceding $B$.  What's more, $B$ itself might
be a sequence of definitions followed by an expression.
\begin{quote}
A sequence of zero or more definitions followed by an expression at the
end is called a {\em body}.
\end{quote}
The only place Scheme grammar allows definitions to appear is at the
beginning of bodies.  Moreover, bodies which begin with definitions can
only appear by themselves at ``top-level,'' or as the bodies of lambda
expressions (cf.~Appendix~\ref{grammar}).

The lambda application rule deals with this by directing that the newly
created definitions be inserted someplace that is grammatical.
Definitions at the beginning of a lambda body may also have to be moved
after the lambda disappears.  For example, using the rule expressed above,
\begin{quote}
\Code{(if (zero? \underline{((lambda (n) (define m 2) (+ m n)) 3)}) 4 5)}
\end{quote}
would rewrite to
\begin{quote}
\Code{(if (zero? (define n 3) (define m 2) (+ m n)) 4 5)}
\end{quote}
which is not grammatical because the operand of \Code{zero?} is a body
with defines.  Proper use of the lambda application rule instead rewrites
this conditional as a body:
\begin{quote}
\Code{(define n 3) (define m 2) (if (zero? (+ m n)) 4 5)}
\end{quote}

\subsubsection{Fresh Renaming}\label{renaming}

With lambda application, however, there is a naming problem we cannot
avoid.  For example, in the definitions below, \Code{add2} is defined as a
procedure that adds two to its operand; similarly, \Code{add3} adds three.
\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{(define add3 (lambda (n) (+ 1 (add2 n))))}\\
\Code{(\underline{add3} 5)}
\end{quote}
So in Scheme, evaluation of the following body returns the value 8, as we
would expect.  Let's examine the steps in this computation.  We begin by
instantiating the underlined occurrence of \Code{add3}:
\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{\underline{(define add3 (lambda (n) (+ 1 (add2 n))))}}\\
\Code{((lambda (n) (+ 1 (add2 n))) 5)}\\
\end{quote}

It will be easier to follow this example if we now ``garbage
collect''---that is, erase---the underlined definition of \Code{add3}
since it is no longer referenced.  This leaves:

\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{\underline{((lambda (n) (+ 1 (add2 n))) 5)}}\\
\end{quote}

Now the only possible rewriting is lambda application, yielding:
\begin{lisp}
(define n 2)
(define add2 (lambda (m) (+ m n)))
(define n 5)
(+ 1 (add2 n))
\end{lisp}

Here we have an obvious problem: two definitions of \Code{n} at the
beginning of the block.  This is ambiguous, and indeed violates the Scheme
grammatical rule that a sequence of definitions may contain only one
definition per variable.  We handle this by renaming the newly defined
\Code{n} and the occurrences it binds, to some ``fresh'' name, say
\Code{n\_1}:
\begin{quote}
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{(define n 2)}\\
\Code{(define n\_1 5)}\\
\Code{(+ 1 (\underline{add2} n\_1))}
\end{quote}

This expression is grammatical again, and now it is safe to instantiate
and garbage-collect \Code{add2}:
\begin{lisp}
(define n 2)
(define n_1 5)
(+ 1 ((lambda (m) (+ m n)) n_1))
\end{lisp}

Notice that if we had not renamed \Code{n} to \Code{n\_1} in this way, we
would have rewritten to
\begin{lisp}
(define n 2)
(define n 5)
(+ 1 ((lambda (m) (+ m n)) n))
\end{lisp}
and the ambiguity of which occurrence of \Code{n} is defined to be which
value becomes unresolvable.\footnote{Actually, until the mid-1970's, all
Lisp dialects resolved the ambiguity by choosing the ``nearest'' value of
\Code{n}, so that this example would have rewritten to \Code{(+ 1 ((lambda
(m) (+ m 5)) 5))} and resulted in the value 11 instead of 8.  This method
of name management is called ``dynamic scope.''}

So the final, general formulation of the {\em lambda application rule} is:
\begin{eqnarray*}
\lefteqn{\Code{((lambda (\vrbl_{1} \ldots) $\define^*$ \expr) \ival_{1} \ldots)}}\\
& \rulesto & \expr \hspace{3in}
\end{eqnarray*}
\begin{quote}
\noindent with the sequence
\[\Code{(define \vrbl_1 \ival_{1})}  \ldots \define^*\]
placed above \expr\ in the first position where definitions may appear and
{\em with all these defined variables freshly renamed}.
\end{quote}

Here is an example illustrating this general form of the rule.

\begin{example}
\begin{eqnarray*}
\lefteqn{\Code{(define f (lambda (x) (+ x 2)))}}\\
\lefteqn{\Code{(if (zero? \underline{((lambda (g x) (define f (lambda (x) (* x x))) (f (g x)))}}}\\
\lefteqn{\Code{\qquad\qquad\qquad \underline{(lambda (x) (f (- x 2)))}}}\\
\lefteqn{\Code{\qquad\qquad\qquad \underline{-1)}}}\\
\lefteqn{\Code{\qquad 3}}\\
\lefteqn{\Code{\qquad 4)}}\\
& \rulesto & \Code{(define f (lambda (x) (+ x 2)))}\\
& & \Code{(define g\_0 (lambda (x) (f (- x 2))))}\\
& & \Code{(define x\_0 -1)}\\
& & \Code{(define f\_1 (lambda (x) (* x x)))}\\
& & \Code{(if (zero? (f\_1 (g\_0 x\_0)))}\\
& & \Code{\qquad 3}\\
& & \Code{\qquad 4)}
\end{eqnarray*}
\end{example}

A more detailed discussion of fresh renaming appears in
Appendix~\ref{scope}.

\subsection{Garbage Collection}\label{garbage-collection}

``Garbage collection'' refers to the process whereby Lisp-like systems
identify and recapture previously used, but no longer accessible, storage
cells.  The corresponding process in our substitution model is erasure of
unreferenced definitions, as in the previous example.

So, a subset $G$ of the immediate definitions occurring at the beginning
of a body is said to be {\em garbage in the body}, if none of the
variables left in the body after $G$ is erased were defined by $G$.  The
Substitution Model {\em garbage collection rule} is: {\em erase garbage}.

For example, in
\begin{lisp}
(define a (lambda () b))
(define b 3)
(define c (lambda () (* b d)))
(define d 4)
(+ 1 (a))
\end{lisp}
The definitions of \Code{c} and \Code{d} are {\em garbage} because
\Code{c}'s and \Code{d}'s don't occur anywhere outside their own
definitions.  The body can be garbage collected to be:
\begin{lisp}
(define a (lambda () b))
(define b 3)
(+ 1 (a))
\end{lisp}

More details of garbage collection are given in Appendix~\ref{garbage-proc}.

\section{Uniqueness}

A substitution model in which rules can be used anywhere is called a {\em
Term Rewriting Model} (TRM).  That's essentially what we have described
above for functional Scheme.  We need not specify where or in what order
to apply rewrite rules because even the full set of rules shares the
unique value property of simple algebraic rules.

\begin{definition}
We use the notation $B_{1} \rulesto^{*} B_{2}$ to indicate that body
$B_{1}$ can be rewritten to body $B_{2}$ by successively applying the
Scheme rewriting rules above zero or more times.
\end{definition}

\begin{quote}
\noindent{\bf The Unique Primitive Value Theorem}.  {\em If Scheme body
$B_{1}$ can be rewritten to some {\em primitive} value, $p$, then $p$ is
the only immediate value of any kind to which it can rewritten.}
\end{quote}

In other words, if $B_{1} \rulesto^{*} p$ and also $B_{1} \rulesto^{*} V$
for some \ival, $V$, then $V = p$.

That's the good news.  The bad news is that the order in which rules are
applied {\em does} matter to avoid wasted time and space---even infinite
waste if rules are applied forever in useless places.  For example, one
could waste a lot of time uselessly rewriting the
subexpression \Code{(Fibonacci 1000)} in:
\begin{lisp}
(if #t 1 (Fibonacci 1000))
\end{lisp}

More bad news is that an expression may rewrite to many distinct immediate
values none of which are terminated, for example,

\begin{eqnarray*}
&&\Code{(lambda (x) (define y (lambda (z) (+ x (y z)))) (y 1))}\\
{} & \rulesto^{*} & \Code{(lambda (x) (define y (lambda (z) (+ x
(y z)))) (+ x (y 1)))}\\
{} & \rulesto^{*} & \Code{(lambda (x) (define y (lambda (z) (+ x
(y z)))) (+ x (+ x (y 1))))}\\
{} & &\qquad\vdots
\end{eqnarray*}

This last example also illustrates that the full set of TRM rules do not have
the Termination property.

These non-uniqueness problems can largely be avoided by keeping to the
Lambda Body Rewriting Restriction mentioned above.  In the functional
case, this restriction never prevents rewriting to some value:
\begin{quote}
\noindent{\bf Lambda Body Safety Theorem}.  {\em If a body can be
rewritten into a value by successive use of the functional Scheme rewrite
rules above, then it can be rewritten to a value while obeying the Lambda
Body Rewriting Restriction.}
\end{quote}

Of course by the Uniqueness Theorem, rewriting according to the Lambda
Body Restriction will reach the same {\em primitive} value, if any, as any
other way of applying the rules.

The Uniqueness and Safety Theorems are by no means obvious.  (Their proof
is sometimes covered in the graduate course 6.840 on Semantics of
Programming Languages.)  Term Rewriting Theory is a sub-discipline of
Theoretical Computer Science which focuses on such properties.


\section{Rule-specified Procedures}

Since the built-in Scheme procedure \Code{not} may be applied to any
value, not just primitive values, we have to go beyond primitive
application rules to describe its behavior.  So we provide specific rules
for applying \Code{not}:
\[\begin{array}{l}
\Code{(not \#f)} \rulesto \Code{#t},\\
\Code{(not $V$)} \rulesto \Code{#f},\\
        \mbox{when } V \mbox{ is an } \ival \mbox{ not equal to } \Code{\#f}.
\end{array}\]

Notice that in order to use \Code{not} as an operator, the rules require
that its operand be an \ival.  This is the essential property of
procedures in a call-by-value language like Scheme, and so we classify
\Code{not} as a {\em rule-specified} procedure identifier.

Another such rule-specified procedure identifier is, for example,
\Code{integer?} with rules:
\[\begin{array}{l}
\Code{(integer? $V$)}  \rulesto \Code{#t}\\
\mbox{when } V \mbox{ is the numeral for an integer,}
\\
\Code{(integer? $V$)}  \rulesto \Code{#f}\\
\mbox{when } V \mbox{ is an } \ival \mbox{ other than a numeral for an integer.}
\end{array}\]

Rule-specified procedure identifiers are, like primitive procedure
identifiers, also counted as immediate values.

\section{Derived Expressions}

We have described above a ``kernel'' of Scheme which omits many familiar,
convenient Scheme constructs.  For example, we want to handle \Code{cond}
and \Code{let}.  One approach is to add rewrite rules to handle these
special forms directly.  Another approach is to think of these extensions
as abbreviations, or ``syntactic sugar,'' for kernel expressions.  For
example,
\[
\Code{(let (($\vrbl_1$ $\init_1$)$\ldots\,$) \bod)}
\]
can be understood as an abbreviation for
\[
\Code{((lambda ($\vrbl_1\cdots\,$) \bod) $\init_1 \ldots\,$).}
\]
and
\begin{eqnarray*}
\Code{(cond } & \Code{($\test_{1}$ $\expr_{1}$)} \\*
              & \Code{($\test_{2}$ $\expr_{2}$)} \\*
              & \vdots \\*
              & \Code{(else $\expr_{n}$))} 
\end{eqnarray*}
can be understood as an abbreviation for
\[
    \setlength{\arraycolsep}{0pt}
    \begin{array}{lllllllllllll}
    \Code{(if } & \rlap{\test_{1}} \\
                & \rlap{\expr_{1}} \\
                & \Code{(if } & \test_{2} \\
                &             & \rlap{\expr_{2}} \\
                &             & \vdots \\
                &             & \qquad \Code{(if } & \test_{n-1} \\
                &             &                    & \expr_{n-1} \\
                &             &                    & \expr_{n}\Code{)\ldots))}.
    \end{array}
\]
So we can specify the computations of $\bnf<derived expression>$'s by
translating, or ``desugaring,'' them into kernel \expr's.\footnote{These
translations are generally linear-time, one-pass, and yield a
kernel-\expr\ of size proportional to the original extended-\expr.  Real
Scheme interpreters and compilers typically carry out such ``source to
source'' translations.} The \RFS\ Report describes the translations above
and others for \andsf's, \orsf's, and several further forms.

\problem The procedure \Code{not} could have been treated as sugar instead
of as a rule-defined procedure.  Describe a simple translation of
\Code{not} into kernel Scheme.

\section{Lists and Symbols}

Scheme output notation for lists and symbols makes them look just like
expressions.  Using this notation in our Term Rewriting Model presents a
problem: how do we tell the difference between lists and
combinations?\footnote{The fact that lists print out looking like
expressions is generally considered a valuable feature in Lisp.  On
the other hand, at least one famous contemporary Computer Scientist has
protested publicly that because of this he couldn't learn Lisp---he could
never figure out when to stop evaluating expressions.} For example, is
``\Code{(+ 3 4)}'' a combination---which should be rewritten to the
syntactic value \Code{7}---or is it a list of three elements---the
procedure identifier \Code{+} (or perhaps it is the symbol ``\Code{+}'')
followed by \Code{3} and \Code{4}?  To avoid any confusion, the TRM
instead rewrites lists into nested \Code{cons}'s of list elements.  For
example, the expression \Code{(list + 3 4)}, which Scheme prints out as
``\Code{([compiled arithmetic procedure +] 3 4)},'' would be rewritten in
our TRM into the expression
\[\Code{(cons + (cons 3 (cons 4 ())))}.\]
Similarly, {\em symbols\/} which print out as \Code{a} or \Code{+} would
be described in the TRM by the expressions \Code{(quote a)} or
\Code{(quote +)} to avoid confusing them with variables or procedure
identifiers.  So \Code{(list '+ 3 4)}, which Scheme prints out as
``\Code{(+ 3 4)},'' would would be rewritten in our TRM into the
terminated expression
\[\Code{(cons (quote +) (cons 3 (cons 4 ())))}.\]

With these notational conventions, it is a straightforward to handle list
structures in the TRM\footnote{This way of handling list works usefully
until we begin mutating lists with \Code{set-car!} and \Code{set-cdr!}.
Then we will need a notation which more accurately reflects sharing in
list structures.}.  Namely, we specify that {\em symbol expressions} of
the form
\[\bnf\Code{(quote \idfr)}\]
and the {\em nil expression} \Code{()} are also primitive values, we
introduce new rule-specified procedure identifiers for list operations such
as \Code{cons}, \Code{car} and \Code{cdr}, and we extend the definitions
of \ival\ to include all expressions of the form
\[\bnf\Code{(cons \ival\ \ival)}.\]
Now it turns out that the behavior of \Code{cons} is specified by
having no rewrite rule for it at all!
We do add some obvious rules for \Code{car} and \Code{cdr}:
\begin{eqnarray*}
\Code{(car (cons $V_{1}$ $V_{2}$))}
& \rulesto & V_{1} \\
\Code{(cdr (cons $V_{1}$ $V_{2}$))}
& \rulesto & V_{2} \\
\end{eqnarray*}

Here are the remaining important rewriting rules about lists:
\begin{gather*}
\Code{(apply $V_{0}$ (cons $V_{1} \ldots$ (cons $V_{n}$ ())\ldots ))}
\rulesto \Code{($V_{0}\ V_{1}\ldots V_{n}$)}
\\[\bigskipamount]
\begin{aligned}
\Code{(pair? (cons $V_{1}$ $V_{2}$))} &\rulesto \Code{\#t}\\
\Code{(pair? $V_{3}$)} &\rulesto \Code{\#f},\\
\end{aligned}\\
\text{if $V_{3}$ is not of the form \Code{(cons $V_{1}$ $V_{2}$)}.}
\\[\bigskipamount]
\begin{align*}
\Code{(null? ())}   & \rulesto \Code{\#t}\\
\Code{(null? $V$)} & \rulesto \Code{\#f},\\
\mbox{if } V & \mbox{ is } \mbox{not \Code{()}.}
\end{align*}
\\[\bigskipamount]
\begin{align*}
\Code{(eq? (quote $I$) (quote $I$))}   & \rulesto \Code{\#t}\\
\Code{(eq? (quote $I$) (quote $J$))} & \rulesto \Code{\#f},\\
\mbox{if } I \mbox{ and } J & \mbox{are distinct \idfr's.}
\end{align*}
\\[\bigskipamount]
\begin{align*}
\Code{(list)} & \rulesto  \Code{()}\\
\Code{(list $V_{1}$ \ldots)}  & \rulesto  \Code{(cons $V_{1}$
(list \ldots))}
\end{align*}
\end{gather*}


\section{Running the Substitution Model}

There is an implementation of the Substitution Model available through the
6.044 WWW page.  It may help you understand how Scheme processes behave,
and it can also serve as a simple debugging aid.  Of course it is about
four orders of magnitude slower than Scheme, so don't expect it to be
useful on compute-intensive examples.

The order in which rewrite rules are applied in the implementation
reflects Scheme evaluation order fairly accurately.  To generate the list
of expressions to which an input expression rewrites, apply the procedure
\Code{smeval} to the quoted expression.

For example, evaluate
\begin{lisp}
(smeval '((lambda (n) (+ 2 n)) 3))
\end{lisp}
to see the successive expressions as this lambda application rewrites to
\Code{5}.

A body beginning with one or more definitions is represented as a list of
the definitions with an expression at the end.  So evaluating,
\begin{lisp}
(smeval
 '((define (factorial n)
     (if (= n 0)
         1
         (* n (factorial (- n 1)))))
   (factorial 4)))
\end{lisp}
will allow you to watch how this body rewrote to \Code{24}.

An expression printed out by \Code{smeval} at any point is a well-formed
Scheme expression which can be evaluated in Scheme and will give the same
final result as \Code{smeval}---at least if the final result is a number
or truth value\footnote{To evaluate a {\em body} printed by \Code{smeval}
when the body begins with definitions, it has to be made into a Scheme
expression.  If the body printed out is
\[\bnf \Code{(}\define_{1} \ldots \expr \Code{)}, \]
then in Scheme evaluate
\[\bnf \Code{((lambda () } \define_{1} \ldots \expr\Code{))}.\]}.

Our TRM does not model Scheme's ability to remember definitions from one
evaluation to the next.  For example, evaluating
\begin{lisp}
(define (square n) (* n n))
\end{lisp}
in Scheme will return an unspecified value, after which evaluating
\begin{lisp}
(square 3)
\end{lisp}
will return \Code{9}.  But if you try
\begin{lisp}
(smeval '(define (square n) (* n n)))
\end{lisp}
you will get some (probably uninformative) error message.  The reason for
the error is that \Code{smeval} expects a {\em body} as an argument, and a
definition by itself is not a body.  Instead, you should have typed
\begin{lisp}
(smeval
 '((define (square n) (* n n))
   (square 3)))
\end{lisp}


\subsection{Controlling Printout}

There are several utilities to control the output printed by \Code{smeval}.

The value returned by a call to \Code{smeval} is the \val\ at
which it successfully stops, or else an error message.

The procedure \Code{print-this-step?} determines which steps get saved on
the list generated by \Code{smstep-list} for printing by \Code{smeval}.
The default is to print every step.

The procedure \Code{garbage-collect-this-step?} can be used to control the
frequency of garbage collection.  Its default is to garbage-collect at
every step (which can slow things down a bit).  To postpone all garbage
collection until the last step, evaluate
\begin{lisp}
(define (garbage-collect-this-step? step-number body) #f)
\end{lisp}

The procedure \Code{interrupt-smeval?} limits the number of rewriting
steps in an evaluation.  Its default is to abort evaluation after 600
steps.  You may want to do shorter runs.  For example, to set
\Code{smeval} to stop after 100 rewriting steps, evaluate
\begin{lisp}
(define (interrupt-smeval? step-number body) (> step-number 100))
\end{lisp}

{\bf Warnings}:
The code for the TRM implementation is written to be readable by
(ambitious) beginning 6.001 students, with major sacrifices in speed and
resilience for the sake of clarity.  As a consequence, \Code{smeval}
typically runs forever or crashes gracelessly on ungrammatical inputs.  It
is a good idea to test expressions by evaluating them in Scheme before
\Code{smeval}'ing them.

Edwin itself wedges horribly if the \Code{*scheme*} buffer overflows
(which may happen when its size is within a small factor of 100K
characters).  You don't want this to happen!  So be careful about doing
\Code{smeval} for long computations; instead save the list generated by
procedure \Code{smstep-list} and view it selectively.

\iffalse
\subsection{Bugs}

We don't know of any now, but there likely are some.  Gratitude and lots
of 6.044 brownie points for bug reports---email them to
\Code{6044-lecturer@theory.lcs.mit.edu}.
\fi

\appendix
\section{Grammar for Functional Scheme}\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>\\
\\
<self-evaluating>       &::=& <numeral> | <boolean>\\
<numeral>   &::=&   "0" | "-1" | "3.14159" | \ldots\\
<boolean>   &::=&   "#t" | "#f"
\end{eqnarray*}
\end{bnf}

\begin{bnf}
\begin{eqnarray*}
\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\qquad
                        \hbox{(Note: all \vrbl's must be distinct.)}\\
\\
<if> &:=& "(if"\: <test> <consequent> <alternative> ")" \\
<test>   &::=&   <expression>\\
<consequent>   &::=&   <expression>\\
<alternative>   &::=&   <expression>\\
\\
<keyword>   &::=& "define" | "quote" | "lambda" | "if"\\
<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>")"\\
\expr &::=& \ldots | <derived expression>\\
<derived expression> &::=& <cond> | <let> \\
\\
<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>\\
<keyword>  &::=&  \ \ldots\, | "cond" | "let" | "else"
\end{eqnarray*}
\end{bnf}


\section{Renaming Variables for Static Scope}\label{scope}

The scope, or binding, rules of a language determine how names are
associated with things named.  Scheme is a {\em statically} scoped
language (also called {\em lexically} scoped).  The purpose of this
scoping discipline is to ensure that formals or defined variables within
an expression can be ``kept private'' and behave independently of
occurrences of names outside the expression.  In this way, a programmer
can choose names within a program without concern for whether or how the
same names may have been used elsewhere.

Correctly managing names is a problem only when the same variable is bound
in more than one way in a body.  In the example in Section~\ref{renaming},
there were initially two places where \Code{n} was bound: by the initial \define
the definition of \Code{} and as a formal in the
definition of \Code{add3}.  There would have been no problem if these different
bindings used different names in the first place, as in:
\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{(define add3 (lambda (n) (+ 1 (add2 n))))}\\
\Code{(\underline{add3} 5)}
\end{quote}

The lambda application rule specifies that such fresh renaming of \Code{n}
to \Code{n\_1} should be done as definitions are created and/or moved to
the beginning of a block. To understand fresh renaming precisely, we must
understand exactly how to determine which occurrences of variables are
bound where.  So we will now carefully spell out the scoping rules for
Scheme.

An occurrence of a variable in a body is a {\em binding occurrence} if it
occurs as a formal of a lambda expression or as the variable part of a
definition.  Associated with every binding occurrence is a subbody called
the {\em scope} of the binding.
\begin{itemize}
\item The scope of a formal of a lambda expression is the body of the
lambda expression.

\item The scope of the variable part of a given definition is the subbody
consisting of the {\em entire sequence} of definitions in which the given
definition appears, as well as the expression at the end of the sequence.
\end{itemize}

For example, consider the following body beginning with two definitions:
\begin{lisp}
(define odd?                                     ;works on any numbers
  (lambda (n)
   (if (integer? n)
       (= (parity n) 1)
       false)))
(define parity
  (lambda (n)
    (define even?
             (lambda (n)
               (cond ((zero? n) #t)
                     ((< n 0) (odd? (+ 1 n)))
                     ((> n 0) (odd? (- n 1))))))
    (define odd?                                ;only works on integers
             (lambda (n)
               (cond ((zero? n) false)
                     ((< n 0) (even? (+ 1 n)))
                     ((> n 0) (even? (- n 1))))))
    (if (even? n) 1 0)))
(odd? (+ n 0.3))
\end{lisp}

In this example, there is only one binding occurrence of \Code{parity},
namely as the variable in the second definition in the body.  The scope of
this binding occurrence is the {\em whole} body.  There are two binding
occurrences of \Code{odd?}.  The first is as the variable in the second
definition in the subbody:
\begin{lisp}
(define even?
         (lambda (n)
           (cond ((zero? n) #t)
                 ((< n 0) (odd? (+ 1 n)))
                 ((> n 0) (odd? (- n 1))))))
(define odd?
         (lambda (n)
           (cond ((zero? n) false)
                 ((< n 0) (even? (+ 1 n)))
                 ((> n 0) (even? (- n 1))))))
(if (even? n) 1 0)
\end{lisp}
and its scope is this whole subbody.  The second binding occurrence of
\Code{odd?} is as the variable in the definition at the beginning of the
whole body, and its scope is the whole body.  There are four binding
occurrences of \Code{n} as the formal of four different lambda expressions
within the body.

Any occurrence of a variable which is not a binding occurrence and which
is inside the scope of a binding occurrence of that variable, is called a
{\em bound occurrence} of that variable.  The bound occurrence is said to
be {\em bound to} the binding occurrence with the smallest scope which
includes it.  We can illustrate which bound occurrences are bound to which
binding occurrences by attaching the same numerical suffix to binding
occurrences and occurrences bound to them:
\begin{lisp}
(define odd_1?
  (lambda (n_3)
   (if (integer? n_3)
       (= (parity_0 n_3) 1)
       false)))
(define parity_0
  (lambda (n_2)
    (define even?_0
             (lambda (n_0)
               (cond ((zero? n_0) #t)
                     ((< n_0 0) (odd?_0 (+ 1 n_0)))
                     ((> n_0 0) (odd?_0 (- n 1_0))))))
    (define odd?_0
             (lambda (n_1)
               (cond ((zero? n_1) false)
                     ((< n_1 0) (even?_0 (+ 1 n_1)))
                     ((> n_1 0) (even?_0 (- n 1_1))))))
    (if (even?_0 n_2) 1 0)))
(odd_1? (+ n 0.3))
\end{lisp}

Notice that the first occurrence of the variable \Code{parity\_0} actually
occurs {\em before} the definition which binds it!

The occurrences in a body which are neither binding nor bound are called
{\em free}.  Variables with free occurrences are called the free variables
of the body.  In the example above, the free variables are the ones left
without any number suffix: namely \Code{false} and \Code{n}.  (Note that
\Code{integer?} and \Code{zero?} don't count as free variables because
they are procedure identifiers.)

There is a more procedural way to define the {\em free variables in a
body}.  If the body is
\begin{itemize}
\item $\bnf <primitive value> \mbox{ or } <procedure identifier>$: the
body has no free variables.

\item a variable $x$: the body has $x$ as its only free variable.

\item a conditional: the free variables are the variables which are free in
either the test, consequent, or alternate expressions.

\item a combination: the free variables are the variables which are free in
operator or operands.

\item a lambda expression: the free variables are the free variables of the
body of the lambda expression {\em excluding} the variables which are
formals of the lambda expression.

\item a body beginning with one or more definitions: the free variables
are the free variables in the immediate value parts of the definitions at
the beginning, plus the free variables of the expression at
the end of the body, {\em excluding} the variables defined at the
beginning of the body.
\end{itemize}

\section{A Garbage Collection Procedure}\label{garbage-proc}

The definition of ``garbage in the body'' we gave in
Section~\ref{garbage-collection} was accurate, but not very procedural.
An efficient way to find all the garbage in a body is to identify all the
variables which are needed in the body---the rest are garbage.  Here is an
inductive definition of the {\em variables needed in a body} which
effectively specifies a procedure for finding all the garbage.

\begin{itemize}
\item
All free variables of the expression at the end of the body are needed in
the body.

\item If $x$ is a variable needed in a body and \Code{(define $x\ V$)} is
one of the defines at the beginning of the body, then all the free
variables of $V$ are also needed in the body.

\end{itemize}

\end{document}
