\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{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 17, 1995}

\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
"("<primitive procedure variable> \pval_{1} \ldots")" \rulesto \pval,
\]
where \pval's are objects which have standard printable output
representations---like numbers or truth values----and primitive procedure
variables are identifiers like \Code{+}, \Code{<}, and \Code{atan} with
``built-in'' meaning in Scheme.

By repeatedly {\em applying\/} such rules, namely replacing lefthand sides
of rules with their righthand 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
truth values\/} \Code{#t}, \Code{#f}:
\begin{eqnarray*}
\Code{(< 6 7)}  & \rulesto & \Code{#t}\\
\Code{(not #f)}  & \rulesto & \Code{#t}\\
\Code{(zero? -1.414)}  & \rulesto & \Code{#f}\\
\vdots
\end{eqnarray*}
For example, applying these rules and the numerical ones above allows us
to handle:
\begin{eqnarray*}
\Code{(not (< (+ 0 1 2) \underline{(/ 3 1)}))}  & \rulesto
        & \Code{(not (< \underline{(+ 0 1 2)} 3))}\\
{}&  \rulesto & \Code{(not (< 3 3))}\\
{}&  \rulesto & \Code{(not #f)}\\
{}&  \rulesto & \Code{#t}
\end{eqnarray*}

It is easy to see that {\em it does not matter in what order the primitive
rewriting rules are applied}---the primitive value at the end will always
be the same!\footnote{Well, there's a {\em proviso\/} here: the primitive
value is unique when it is {\em possible} somehow to rewrite the
expression into one.  Some ``ill-typed'' expressions like \Code{(+ \#t 3)}
do not have values.  (What would Scheme do when such an expression is
evaluated?)} For example, we might have chosen to rewrite the example
above in another order:
\begin{eqnarray*}
\Code{(not (< \underline{(+ 0 1 2)} (/ 3 1)))}
        & \rulesto & \Code{(not (< 3 \underline{(/ 3 1)}))}\\
{}&  \rulesto & \Code{(not (< 3 3))}\\
{}&  \rulesto & \Code{(not #f)}\\
{}&  \rulesto & \Code{#t}
\end{eqnarray*}
The primitive value is unique because Scheme is {\em fully
parenthesized}---ambiguous mathematical expressions like $(3 + 2 - 4)$ are
disallowed---and because there are no primitive rules with the same
lefthand side but different righthand sides.

\subsection{Immediate Values}

In addition to the primitive values, the primitive {\em operators} like
\Code{+} or \Code{<} are themselves a kind of value called a {\em
primitive procedure variable}\footnote{We assume here that primitive
procedure variables {\em won't} be redefined!  According to the official
definition of \RFS, it is theoretically 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 construct procedures values, namely, with
{\em lambda expressions\/}. The
\begin{itemize}
\item primitive values,
\item primitive procedure variables, 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 simplification of combinations involving an arbitrary expression,
$A$, which may contain variables, as opposed merely to 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{bnf}
\begin{eqnarray*}
"(if #f "\expr_{1} \expr_{2}")" & \rulesto & \expr_{2}\\
"(if "<non-"#f" immediate value>  \expr_{1} \expr_{2}")" & \rulesto & \expr_{1}
\end{eqnarray*}
\end{bnf}

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.  Thus, in contrast to primitive
applications, the \Code{if} rule can be applied {\em without} the constraint
that $\expr_{1}$ and $\expr_{2}$ be values.

Now we can do rewriting such as
\begin{align*}
\Code{(if (lambda (a b) c) }
    &\Code{(if (not (< (+ 0 1 2) (/ 3 1))) atan (lambda (x) x)) +)}\\
{}\rulesto{} & \Code{(if (not (< (+ 0 1 2) (/ 3 1))) atan (lambda (x) x))}\\
\vdots\\
\rulesto{} & \Code{(if \#t atan (lambda (x) x))}\\
\rulesto{} & \Code{atan}
\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, it will still be the case that no matter the order that
primitive and conditional rewriting rules are applied, the same immediate
value, if any, will result.  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 definition of names and their use, as 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}

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

The variable instantiation is a basic naming rule of algebra: replace an
occurrence of a variable by the expression it names.  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 (+ 1 2)) (* x \underline{y})}}\\
{} & \rulesto & \Code{(define y 7) (define x \underline{(+ 1 2)}) (* x 7)}\\
{} & \rulesto & \Code{(define y 7) (define x 3) (* \underline{x} 7)}\\
{} & \rulesto & \Code{(define y 7) (define x 3) \underline{(* 3 7)}}\\
{} & \rulesto & \Code{(define y 7) (define x 3) 21}
\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.

\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, variables may only be instantiated with {\em immediate values},
not arbitrary expressions.  This restriction is needed to reflect
accurately Scheme's call-by-value behavior and sharing among environment
frames.  For example, unlike instantiation in algebra, Scheme's
instantiation rule does {\em not} allow
\begin{eqnarray*}
\lefteqn{\Code{(define y 7) (define x (+ y y)) (* \underline{x} 3 y )}}\\
{} & \rulesto & \Code{(define y 7) (define x (+ y y)) (* (+ y y) 3 y)}
\end{eqnarray*}
because the variable \Code{x} may not be instantiated by the non-\ival\
\Code{(+ y y)}.

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{lisp}
(define n 2)
(define add2 (lambda (m) (+ m n)))
(define add3 (lambda (n) (inc (add2 n))))
\end{lisp}
so that evaluating \Code{(add3 1)} would return \Code{4}.

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

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} for changing defined names
into ``fresh'' names.  However, there is no need for renaming, and no
problem about changed binding, as long as we obey
\begin{quote}
{\bf The Lambda Body Rewriting Restriction}: {\em Don't apply any
rewriting rule within the body of a lambda expression.}
\end{quote}
This works because in Scheme grammar, the only place definitions can occur
besides ``top level'' is within lambda bodies, so there is no possibility
of bindings being changed by instantiating ocurrrences 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 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 expressions to be manipulated in many examples.
It also will allow us to model Scheme's computational behavior much
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 usefully 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 a new
``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 lefthand side of the rule rewrites into a sequence of two
things---a definition followed by an expression.  If there were several
formal parameters instead of just \Code{x}, there would be several
definitions preceding the 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 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 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.
So in Scheme, evaluation of the following body returns the value 8, as we
would expect:
\begin{quote}
\Code{(define make-incrementer (lambda (n) (lambda (m) (+ m n))))}\\
\Code{(define add2 (\underline{make-incrementer} 2))}\\
\Code{(define add3 (lambda (n) (inc (add2 n))))}\\
\Code{(add3 5)}
\end{quote}

Let's examine in detail how our Substitution Model realizes this intended
behavior.  The only rule applicable at the start is instantiatiation for
\Code{make-incrementer} or \Code{add3}.  Scheme would work on the
definitions at the beginning first, so let's do likewise and first
instantiate the occurrrence of \Code{make-incrementer} underlined above:

\begin{quote}
\Code{\underline{(define make-incrementer (lambda (n) (lambda (m) (+ m n))))}}\\
\Code{(define add2 ((lambda (n) (lambda (m) (+ m n))) 2))}\\
\Code{(define add3 (lambda (n) (inc (add2 n))))}\\
\Code{(add3 5)}
\end{quote}

It will be easier to follow this example if we now simplify the body by
dropping the no longer referenced definition---in this case, the
underlined definition of \Code{make-incrementer}:
\begin{quote}
\Code{(define add2 \underline{((lambda (n) (lambda (m) (+ m n))) 2)})}\\
\Code{(define add3 (lambda (n) (inc (add2 n))))}\\
\Code{(add3 5)}
\end{quote}

Lambda application in the definition of \Code{add2} creates a definition
of \Code{n}:
\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{(define add3 (lambda (n) (inc (add2 n))))}\\
\Code{(\underline{add3} 5)}
\end{quote}

Now we can instantiate \Code{add3} and then drop its definition:
\begin{quote}
\Code{(define n 2)}\\
\Code{(define add2 (lambda (m) (+ m n)))}\\
\Code{\underline{((lambda (n) (inc (add2 n))) 5)}}\\
\end{quote}

Lambda application comes next, yielding:
\begin{lisp}
(define n 2)
(define add2 (lambda (m) (+ m n)))
(define n 5)
(inc (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{(inc (\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)
(inc ((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)
(inc ((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{(inc ((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, accurate statement of the {\em lambda application rule} is:
\begin{eqnarray*}
\lefteqn{\Code{((lambda (\vrbl_{1} \ldots) \defines\ \expr) \ival_{1} \ldots)}}\\
& \rulesto & \expr \hspace{3in}
\end{eqnarray*}
\begin{quote}
\noindent with the sequence
\[\Code{(define \vrbl_1 \ival_{1})}  \ldots \defines\]
placed above \expr\ in the first position where definitions may appear and
{\em with all these defined variables freshly renamed}.
\end{quote}

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

\subsection{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 dropping of
unreferenced definitions as in the previous example.  A subset $G$ of immediate definitions among the 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:
\begin{eqnarray*}
\bod_1 & \rulesto& \bod_2,\\
\mbox{where $\bod_2$ is the } & \mbox{result} & \mbox{ of erasing garbage in $\bod_1$}.
\end{eqnarray*}

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

\section{Uniqueness}

A substitution model in which rules can be used anywhere is called a {\em
Term Rewriting Model} (TRM).  That's what we have described above for
functional Scheme, because even the full set of rules shares the unique
value property of simple algebraic rules:
\begin{quote}
\noindent{\bf The Unique Value Theorem}.  {\em There is at most one
primitive value that can be reached by successively rewriting a body
applying the Scheme rewriting rules above to any subbodies in any order.}
\end{quote}

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{(fibonaaci 1000)} in:
\begin{lisp}
(if #t 1 (fibonaaci 1000))
\end{lisp}
More bad news is that immediate values which are {\em not} primitive,
namely, lambda expressions, are rarely unique.

These problems can largely be avoided by keeping to the {\em lambda body
rewriting restriction} mentioned above.  There is no problem about this
because of the
\begin{quote}
\noindent{\bf Lambda Body Safety Theorem}.  {\em If a body can be
rewritten into a primitive value by successive use of the Scheme rewrite
rules above, then it can be rewritten to a primitive value while obeying
the lambda body rewriting restriction.}
\end{quote}

Of course by the Uniqueness Theorem, rewriting under the lambda body
rewriting restriction will reach the {\em same} 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 subdiscipline of
Theoretical Computer Science which focuses on such properties.

\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 translations.}.
The \RFS\ Report describes the translations above and others for \andsf's,
\orsf's, and several further forms.

\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 very 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 variable \Code{+} (or perhaps it is the symbol ``\Code{+}'')
followed by \Code{3} and \Code{4}?  So the TRM instead ``simplifies''
lists into syntactic values which are 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.  So
\Code{(list '+ 3 4)}, which Scheme prints out as ``\Code{(+ 3 4)},''
would would be rewritten in our TRM into the 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!}, at which point a more accurate notation reflecting
  sharing in list structure would be needed.}.
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 list-oriented procedure variables 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)}.\]
We don't even have to add a rewrite rule for applications of \Code{cons}!
We do add some obvious rules for \Code{car} and \Code{cdr}:
\begin{eqnarray*}
\Code{(car (cons \ival_{1} \ival_{2}))}
& \rulesto & \ival_{1} \\
\Code{(cdr (cons \ival_{1} \ival_{2}))}
& \rulesto & \ival_{2} \\
\end{eqnarray*}
The rules for \Code{cons}, \Code{car} and \Code{cdr} resemble the
primitive procedure rules in that they require that all the operands be
\ival's before the rule can be implied.  These {\em rule-specified
procedure variables} are, like primitive procedure variables, also treated
as \ival's.

Here are the remaining important rewriting rules about lists:
\begin{gather*}
\Code{(apply $E_{0}$ (cons $E_{1} \ldots$ (cons $E_{n}$ ())\ldots ))}
\rulesto \Code{($E_{0}\ E_{1}\ldots E_{n}$)}
\\[\bigskipamount]
\begin{aligned}
\Code{(pair? (cons \ival_{1} \ival_{2}))} &\rulesto \Code{\#t}\\
\Code{(pair? \ival_{3})} &\rulesto \Code{\#f}\\
\end{aligned}\\
\text{if $\ival_{3}$ is not of the form \Code{(cons \ival_{1} \ival_{2})}}
\\[\bigskipamount]
\begin{align*}
\Code{(null? ())}   & \rulesto \Code{\#t}\\
\Code{(null? \ival)} & \rulesto \Code{\#f}\\
\mbox{if \ival}  & \mbox{ is } \mbox{not \Code{()}.}
\end{align*}\\[\bigskipamount]
\begin{align*}
\Code{(list)} & \rulesto  \Code{()}\\
\Code{(list \ival_{1} \ldots)}  & \rulesto  \Code{(cons \ival_{1}
(list \ldots))}
\end{align*}
\\[\bigskipamount]
\begin{align*}
\Code{(equal? \ival_{1} \ival_{1})} & \rulesto \Code{\#t}\\
\Code{(equal? \ival_{1} \ival_{2})} & \rulesto \Code{\#f}\\
\text{if $\ival_{1}$ and $\ival_{2}$ are not identical,}\\
\text{\em and at least one of them is printable.}
\end{align*}
\end{gather*}

The {\em printable} values are numbers, Booleans, symbols, and lists of
printable values.  Note that, the expression
\[\Code{(equal? (lambda () 2) (lambda () (+ 1 1))}\]
for example, could be rewritten to both \Code{\#t} and \Code{\#f} if we
omit the printable value restriction on the rules for \Code{equal?}.

\section{Running the Substitution Model}

There is an implementation of the Substitution Model in the 6.044 ftp
directory.  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 (dec n)))))
   (factorial 4)))
\end{lisp}
will allow you to watch how this body rewrote to \Code{24} (see
Appendix~\ref{sample}).

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.

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

\appendix
\section{Grammar for Functional Scheme}\label{grammar}

%section{Appendix

\subsection{Kernel Syntax}

\begin{bnf}
\begin{eqnarray*}
<define> &:=& "(define"\: <variable> <expression> ")"\\
<body>  &::=& <define_{1}>\ldots <expression>\\
        && {} \qquad \hbox{(Note: all defined variables must be distinct)}\\
\\
<expression> &::=& <variable> | <self-evaluating> | <symbol> | "()"\\
        && {}   | <combination> | <lambda expression> | <if>\\
\\
<self-evaluating>       &::=& <numeral> | <boolean>\\
<numeral>   &::=&   "0" | "-1" | "3.14159" | \ldots\\
<boolean>   &::=&   "#t" | "#f" \\
\\
<symbol>        &::=& "(quote " <variable> ")" | \Code{(quote $<keyword>$)}\\
\\
<combination>   &::=&   "(" <operator> <operand_{1}> \ldots ")"\\
<operator>   &::=&   <expression>\\
<operand>   &::=&   <expression>\\
\\
<lambda expression> &::=&  "(lambda ("<formals>") " <body> ")" \\
<formals>   &::=&   <variable_{1}>\ldots\\
        && {} \qquad \hbox{(Note: all \vrbl's must be distinct)}\\
\\
<if> &:=& "(if"\: <test> <consequent> <alternative> ")" \\
<test>   &::=&   <expression>\\
<consequent>   &::=&   <expression>\\
<alternative>   &::=&   <expression>\\
\\
<primitive procedure variable> &::=& "+" | "-" | "*" | "/" | "=" | "<" | "atan" | \dots\\
<rule-specified procedure variable> &::=& "null?" | "pair?" | "car" |
"cdr" | "cons" | "list" | "equal?" | "apply"\\
<keyword>   &::=& "define" | "quote" | "lambda" | "if"\\
<variable> &::=& \hbox{identifiers which are not $\bnf
        <self-evaluating>$ or $\bnf <keyword>$'s}\\
\end{eqnarray*}
\end{bnf}


\subsection{Derived Syntax}

\begin{bnf}
\begin{eqnarray*}
\expr &::=& \ldots | <derived expression>\\
<derived expression> &::=& <cond> | <let> | \ldots\\
<cond> &::=& "(cond"\: <clause_{1}> \ldots ")"\\
<clause> &::=& "(" <test> <expression>")" | "(else " \expr ")"\\
<let> &::=& "(let ("<binding_{1}> \ldots") " <body> ")" \\
<binding> &::=& "(" <variable> <init> ")"\\
<init> &::=& <expression>\\
%<begin> &::=& "(begin"\: \expr_{1} \ldots ")"\\
<define> &::=& \ \ldots\, | "(define ("<variable> <formals>")" <body>")"\\
%<primitive procedure variable> &::=& \ \ldots\, | "display" | "newline"\\
<keyword>  &::=&  \ \ldots\, | "cond" | "let" | "else" | \ldots\\
%"begin" | \ldots
\end{eqnarray*}
\end{bnf}


\subsection{Values}

\begin{bnf}
\begin{eqnarray*}
\pval &::=&  <self-evaluating> | <symbol> | "()"\\
\ival &::=& \pval | <lambda expression>\\
        && {} | <primitive procedure variable>\\
        && {} | <rule-specified procedure variable>\\
        && {} | "(cons "<immediate value>\ <immediate value>")"\\
<immediate define> &::=& "(define"\: <variable> <immediate value>")" \ldots\\
<value> &::=& <immediate define_{1}> \ldots <immediate value>\\
        && {} \qquad \hbox{(Note: all defined \vrbl's must be distinct)}\\
\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: as a formal in
the definition of \Code{make-incrementor} 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{lisp}
(define make-incrementor (lambda (n) (lambda (m) (+ m n))))
(define add2 (make-incrementor 2))
(define add3 (lambda (n_1) (inc (add2 n_1))))
(add3 5)
\end{lisp}

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 describe fresh renaming precisely, we must
first 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)
       #f)))
(define parity
  (lambda (n)
    (define even?
             (lambda (n)
               (cond ((zero? n) #t)
                     ((< n 0) (odd? (inc n)))
                     ((> n 0) (odd? (dec n))))))
    (define odd?                                ;only works on integers
             (lambda (n)
               (cond ((zero? n) #f)
                     ((< n 0) (even? (inc n)))
                     ((> n 0) (even? (dec n))))))
    (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? (inc n)))
                 ((> n 0) (odd? (dec n))))))
(define odd?
         (lambda (n)
           (cond ((zero? n) #f)
                 ((< n 0) (even? (inc n)))
                 ((> n 0) (even? (dec n))))))
(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)
       #f)))
(define parity_0
  (lambda (n_2)
    (define even?_0
             (lambda (n_0)
               (cond ((zero? n_0) #t)
                     ((< n_0 0) (odd?_0 (inc n_0)))
                     ((> n_0 0) (odd?_0 (dec n_0))))))
    (define odd?_0
             (lambda (n_1)
               (cond ((zero? n_1) #f)
                     ((< n_1 0) (even?_0 (inc n_1)))
                     ((> n_1 0) (even?_0 (dec n_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 {\em free
variables} of the body.  In the example above, the free variables are the
ones left without any number suffix: the primitive procedure variables
\Code{integer?}, \Code{zero?}, \Code{inc}, and \Code{dec}; and the
ordinary variable \Code{n}.

There is a more procedural way to define the free variables in a body.  If
the body is a


\begin{itemize}
\item number, truth value, symbol or \Code{()}: the body has no free
variables.

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

\item conditional (\Code{if}): the free variables are the variables
which are free in the test, consequent, or alternate expressions.

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

\item 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 body: the free variables are the free variables in the expression
parts of the definitions at the beginning of the body, 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{Garbage Collection in Detail}\label{garbage}
Here is a precise definition of garbage:

\begin{quote}
A subset $G$ of the \define's at the beginning of a body is {\em garbage
in the body\/} if
\begin{enumerate}

\item
none of the variables defined by the \define's in $G$ occur free in
the remaining body after $G$ is erased, and

\item\label{garbage-ival}
all the variables defined by the \define's in~$G$ are bound to
immediate values.

\end{enumerate}
\end{quote}

Condition~\ref{garbage-ival} in the definition of garbage is a
technicality needed to reflect call-by-value behavior.  For example, in
\begin{lisp}
(define spin (lambda () (spin)))
(define x (spin))
0
\end{lisp}
the definitions of \Code{spin} and \Code{x} are certainly not needed to
find the value of the expression \Code{0}, and indeed they satisfy
condition~1 in the definition of garbage.  But call-by-value means that
the values of {\em all\/} the expressions in the definitions beginning a
body must be obtained in order to find the final value of a body.  Since
\Code{(spin)} has no value, neither does the body.  Indeed, Scheme would
run forever (if we didn't interrupt it) on this body.  On the other hand,
if we erased the definitions, we would finish with the primitive value 0.
(That's what {\em call-by-name}, also called {\em normal order},
evaluation would return.)

The above definition of garbage is not very procedural.  An efficient way
to find all the garbage in a body is to identify all the variables which
are {\em needed in the body}---the rest are garbage.  Here is a precise
definition of ``needed'' which does suggest a procedure.

The variables needed in a body are defined inductively by the conditions:
\begin{enumerate}

\item
all free variables in the expression at the end of the body are needed in
the body,

\item a variable is needed in a body if it is bound by one of the
definitions at the beginning of the body to an expression which is {\em
not\/} an immediate value,

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

\item variables are needed in the body only as a consequence of the
preceding clauses~1--3.

\end{enumerate}

\section{A Sample Run}\label{sample}
\small
\begin{lisp}
(smeval
 '((define (factorial n)
     (if (= n 0)
         1
         (* n (factorial (dec n)))))
   (factorial 4)))

;==(0)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (factorial 4))

;==(1)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 ((lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))) 4))

;==(2)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (if (= n_0 0) 1 (* n_0 (factorial (dec n_0)))))

;==(3)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (if (= 4 0) 1 (* n_0 (factorial (dec n_0)))))

;==(4)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (if () 1 (* n_0 (factorial (dec n_0)))))

;==(5)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (* n_0 (factorial (dec n_0))))

;==(6)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (* n_0 (factorial (dec 4))))

;==(7)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (* n_0 (factorial 3)))

;==(8)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (* n_0 ((lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))) 3)))

;==(9)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (if (= n_1 0) 1 (* n_1 (factorial (dec n_1))))))

;==(10)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (if (= 3 0) 1 (* n_1 (factorial (dec n_1))))))

;==(11)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (if () 1 (* n_1 (factorial (dec n_1))))))

;==(12)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (* n_1 (factorial (dec n_1)))))

;==(13)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (* n_1 (factorial (dec 3)))))

;==(14)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (* n_1 (factorial 2))))

;==(15)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (* n_0 (* n_1 ((lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))) 2))))

;==(16)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (if (= n_2 0) 1 (* n_2 (factorial (dec n_2)))))))

;==(17)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (if (= 2 0) 1 (* n_2 (factorial (dec n_2)))))))

;==(18)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (if () 1 (* n_2 (factorial (dec n_2)))))))

;==(19)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (* n_2 (factorial (dec n_2))))))

;==(20)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (* n_2 (factorial (dec 2))))))

;==(21)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (* n_0 (* n_1 (* n_2 (factorial 1)))))

;==(22)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (*
  n_0
  (* n_1 (* n_2 ((lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))) 1)))))

;==(23)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (if (= n_3 0) 1 (* n_3 (factorial (dec n_3))))))))

;==(24)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (if (= 1 0) 1 (* n_3 (factorial (dec n_3))))))))

;==(25)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (if () 1 (* n_3 (factorial (dec n_3))))))))

;==(26)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (* n_3 (factorial (dec n_3)))))))

;==(27)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (* n_3 (factorial (dec 1)))))))

;==(28)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (* n_0 (* n_1 (* n_2 (* n_3 (factorial 0))))))

;==(29)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (*
  n_0
  (*
   n_1
   (* n_2 (* n_3 ((lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))) 0))))))

;==(30)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (define n_4 0)
 (*
  n_0
  (* n_1 (* n_2 (* n_3 (if (= n_4 0) 1 (* n_4 (factorial (dec n_4)))))))))

;==(31)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (define n_4 0)
 (* n_0 (* n_1 (* n_2 (* n_3 (if (= 0 0) 1 (* n_4 (factorial (dec n_4)))))))))

;==(32)==>
((define factorial (lambda (n) (if (= n 0) 1 (* n (factorial (dec n))))))
 (define n_0 4)
 (define n_1 3)
 (define n_2 2)
 (define n_3 1)
 (define n_4 0)
 (* n_0 (* n_1 (* n_2 (* n_3 (if #t 1 (* n_4 (factorial (dec n_4)))))))))

;==(33)==>
((define n_0 4) (define n_1 3) (define n_2 2)
 (define n_3 1) (* n_0 (* n_1 (* n_2 (* n_3 1)))))

;==(34)==>
((define n_0 4) (define n_1 3) (define n_2 2) (* n_0 (* n_1 (* n_2 (* 1 1)))))

;==(35)==>
((define n_0 4) (define n_1 3) (define n_2 2) (* n_0 (* n_1 (* n_2 1))))

;==(36)==>
((define n_0 4) (define n_1 3) (* n_0 (* n_1 (* 2 1))))

;==(37)==>
((define n_0 4) (define n_1 3) (* n_0 (* n_1 2)))

;==(38)==>
((define n_0 4) (* n_0 (* 3 2)))

;==(39)==>
((define n_0 4) (* n_0 6))

;==(40)==>
(* 4 6)

;==(41)==>
24
;Value 1: "Syntactic Value was returned"

\end{lisp}



\end{document}
