\documentclass[11pt]{handout}

\usepackage{6044}
\usepackage{time}
\usepackage[fleqn]{amsmath}

\setlength{\textheight}{8in}
\setlength{\textwidth}{5.5in}
\setlength{\oddsidemargin}{.4in} 
\setlength{\evensidemargin}{0in} 
\parindent0in
\parskip\medskipamount

\newcommand{\ple}{\ensuremath{\vdash_\le\,}}

\def\f={\mathop{\Code{=}}}
\newcommand{\eqtn}[2]{\Code{( #1 = #2 )}}
\newcommand{\peqtn}[2]{\fortext{\proves \eqtn{#1}{#2}}}
\newcommand{\etrm}[1]{\Code{ = #1}}
\newcommand{\leqtn}[2]{\Code{( #1 <= #2 )}}
\newcommand{\aeqv}{\fortext{\mathrel{=_{\alpha}}}}

\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{prvar}{procedure\ variable}
\DefineBNFAbbrev{rspvar}{rule-specified\ procedure\ variable}
\DefineBNFAbbrev{pprvar}{primitive\ procedure\ variable}
\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}}

\makeatletter
\renewenvironment{description}
               {\list{}{\labelwidth\z@
                        \leftmargin1em
                        \itemindent-\leftmargin
                        \let\makelabel\descriptionlabel}}
               {\endlist}
\makeatother

\renewcommand*\descriptionlabel[1]{\hspace\labelsep
                                {\normalfont\bfseries #1}:}


\begin{document}
\handout{ps3-soln}{Problem Set 3 Solutions}{4 October 1996}

\reminder {\bf QUIZ 1} in class on Monday, 7 October.

\medskip

\subsubsection*{Problem 1} (a) \Code{v}, \Code{x} are free in the
expression at the end of the body, so are needed.  The definition of
\Code{w} is not immediate, so \Code{w} is needed, and \Code{w} needs
\Code{u}.  This leaves \Code{y} and \Code{z} available for garbage
collection at the first step.

(b) All the definitions get garbage collected by the end, even with the
Lambda Body Restriction.  (To see how, run the body using the \Code{smeval}
procedure from the rewriting interpreter described in Handout 2.)

(c) ---so they certainly all get garbage collected when the restriction is
relaxed.

\subsubsection*{2(a)}
\begin{bnf}
\begin{eqnarray*}
<simple expression> &::=& <self-evaluating> | <primitive procedure variable>\\
        && {} | <combination> | <if>\\
\\
<self-evaluating>       &::=& <numeral> | <boolean>\\
<numeral>   &::=&   "0" | "1" | "-1" | "2" | "-2" | \dots\\
<boolean>   &::=&   "#t" | "#f" \\
<primitive procedure variable> &::=& "+" | "-" | "*" | "=" | "<"\\
\\
<combination>   &::=&   "(" <operator> <operand_{1}> <operand_{2}> ")"\\
<operator>   &::=&   <simple expression>\\
<operand>   &::=&   <simple expression>\\
\\
<if> &:=& "(if"\: <test> <consequent> <alternative> ")" \\
<test>   &::=&   <simple expression>\\
<consequent>   &::=&   <simple expression>\\
<alternative>   &::=&   <simple expression>\\
\end{eqnarray*}
\end{bnf}

\subsubsection*{2(b)}
\begin{definition*}
The {\em meaning}, \mean{s}, of a simple expression, $s$, is defined by
structural induction on $\bnf <simple expression>$'s as follows:
\begin{itemize}

\item
\begin{eqnarray*}
\mean{\mbox{\bf n}} & = & n \qquad \mbox{if {\bf n} is the numeral for the number $n$,}\\
\mean{\Code{\#t}} & = & {\it true},\\
\mean{\Code{\#f}} & = & {\it false}.
\end{eqnarray*}

\item
$\mean{\it op} = \circ$ when {\it op} is \Code{+}, \Code{-}, \Code{*},
\Code{=}, or \Code{<}, and $\circ$ is the binary arithmetic operation $+,
-, *, =$, or $<$, respectively.  (We treat the binary relations $=$ and
$<$ on numbers as binary operations from numbers to Boolean values).

\item
$\mean{\Code{({\it op} $s_{1}$ $s_{2}$)}} = \mean{s_{1}} \circ
\mean{s_{2}}$, providing \mean{s_{1}} and \mean{s_{2}} are both defined to
be numbers, {\it op} is a $\bnf <primitive procedure variable>$ and
$\mean{\it op} = \circ$.

\item
$\mean{\Code{(if $s_{1}$ $s_{2}$ $s_{3}$)}}=\left\{\begin{array}{ll}
\mean{s_{2}}    & \mbox{if $\mean{s_{1}}={\it true}$ and \mean{s_{2}} is defined,}\\
\mean{s_{3}}    & \mbox{if $\mean{s_{1}}={\it false}$ and \mean{s_{3}} is defined,}\\
\mbox{undefined}       & \mbox{otherwise.}
\end{array}
\right. $

\item if $s$ is not of one of the forms above, then \mean{s} is undefined.
\end{itemize}

\end{definition*}

\subsubsection*{2(c)} If $s_{1} \rulesto s_{2}$, then $s_{2}$ is a simple
expression, and either both of $s_{1}$ and $s_{2}$ are meaningless, or
else $\mean{s_{1}} = \mean{s_{2}}$.

\begin{proof}
By structural induction on $s_{1}$.

\begin{description}

\item[$s_{1}$ is $\bnf <self-evaluating>$ or a $\bnf <primitive\ procedure\
variable>$]  No rule applies to $s_{1}$, so there is nothing to prove.

\item[$s_{1}$ is of the form \Code{({\it op} $s_{3}$ $s_{4}$)}]  There are three
subcases to consider.
\begin{enumerate}

\item  $s_{1}$ is itself the redex of a rule.

This is possible only if {\it op} is a $\bnf <procedure variable>$ and
$s_{3}, s_{4}$ are both numerals, in which case $s_{2}$ must be $\bnf
<self-evaluating>$ and $s_{1} \rulesto s_{2}$ by a primitive application
rule.  Then $\mean{s_{1}} = \mean{s_{2}}$ since the left and righthand
sides of primitive application rules obviously have the same meaning.

\item

$s_{2}$ is of the form \Code{({\it op} $s'_{3}$ $s_{4}$)} where $s_{3}
\rulesto s'_{3}$.

If $\mean{s_{3}}$ is undefined, then by definition, so is \mean{s_{1}} .
But then by induction, $\mean{s'_{3}}$ is also undefined, and by
definition, so is \mean{s_{2}}.  Thus both \mean{s_{1}} and \mean{s_{2}}
are undefined.

If $\mean{s_{3}}$ is defined, then by induction, $\mean{s_{3}} =
\mean{s'_{3}}$.  If \mean{s_{3}} is not a number, then both \mean{s_{1}}
and \mean{s_{2}} are undefined by definition.  If \mean{s_{3}} is a
number, then
\[\mean{s_{1}} = \mean{s_{3}} \circ \mean{s_{4}} = 
\mean{s'_{3}} \circ \mean{s_{}{4}} = \mean{s_{2}},\]
where $\mean{\it op} = \circ$.

\item
$s_{2}$ is of the form \Code{({\it op} $s_{3}$ $s'_{4}$)} where $s_4
\rulesto s'_{4}$.  As in the previous subcase.
\end{enumerate}

\item[$s_{1}$ is of the form \Code{(if $s_{3}$ $s_{4}$ $s_{5}$)}]  This
time there are four subcases.

\begin{enumerate}
\item

$s_{1}$ is itself the redex of a rule.  This is possible if $s_{3}$ is
\Code{\#t} and $s_{2}$ is $s_{4}$, in which case the meanings of $s_{1}$ and
$s_{2}$ are both undefined or are equal by the definition of
$\mean{s_{1}}$.  The only other way $s_{1}$ can be a redex is if $s_{3}$
is \Code{\#f}, and we similarly conclude that $\mean{s_{1}}$ and
$\mean{s_{2}}$ are both undefined or equal.

\item

$s_{2}$ is of the form \Code{(if $s'_{3}$ $s_{4}$ $s_{5}$)} where $s_{3}
\rulesto s'_{3}$.

If $\mean{s_{3}}$ is undefined, then by definition, so is \mean{s_{1}} .
But then by induction, $\mean{s'_{3}}$ is also undefined, and by
definition, so is \mean{s_{2}}.  Thus both \mean{s_{1}} and \mean{s_{2}}
are undefined.

If $\mean{s_{3}}$ is defined, then by induction, $\mean{s_{3}} =
\mean{s'_{3}}$.  If \mean{s_{3}} is not a Boolean value, then both
\mean{s_{1}} and \mean{s_{2}} are undefined by definition.  Finally, if
\mean{s_{3}} is a Boolean, then by definition of the meaning of a
conditional, the meanings of $s_{1}$ and $s_{2}$ are both undefined or are
equal.

\item $s_{2}$ is of the form \Code{(if $s_{3}$ $s'_{4}$ $s_{5}$)} where $s_{4}
\rulesto s'_{4}$.  Similar to the previous case.

\item $s_{2}$ is of the form \Code{(if $s_{3}$ $s_{4}$ $s'_{5}$)} where $s_{5}
\rulesto s'_{5}$.  Similar to the previous case.
\end{enumerate}
\end{description}
\end{proof}

\subsubsection*{2(d)}

Define the {\em unit} expressions to be $\bnf <self-evaluating>$ or $\bnf
<primitive procedure variable>$'s.  We first prove that the only
terminated simple expressions whose meaning is defined are unit
expressions.  In other words, if $s_{1}$ is a meaningful simple expression
which is {\em not} a unit, then $s_{1}$ will contain a redex of a
rewriting rule.  (The redex may be $s_{1}$ itself.)  The proof is by
structural induction on $s_{1}$.

If $s_{1}$ is a unit, there is nothing to prove.

Suppose $s_{1}$ is of the form \Code{(if $s_{3}$ $s_{4}$ $s_{5}$)}.  In
this case, since $s_{1}$ is meaningful, \mean{s_{3}} must be defined to be
Boolean value.  If $s_{3}$ is not a unit, then by induction, $s_{3}$
contains a redex, hence so does $s_{1}$.  Otherwise, $s_{3}$ must be
\Code{\#t} or \Code{\#f}, since these are only units with Boolean values,
and in that case $s_{1}$ itself is a redex.

The final case, when $s_{1}$ is a combination, follows similarly.

Now by 2(c), rewriting preserves simplicity of expressions.  Moreover, the
only rewrite rules applicable to simple expressions are primitive
applications and conditional rules, and these rules always {\em decrease}
the size of the rewritten expression.  So it is impossible to successively
rewrite a simple expression more times than the length (number of
syntactic tokens) of the expression.  Hence, every simple expression
eventually rewrites to a terminated expression.

Also, by 2(c), rewriting preserves meaning of simple expressions.  So a
meaningful simple expression must eventually rewrite to a unit with the
same meaning.  Since distinct units have different meanings, we conclude
that every meaningful simple expression must eventually rewrite to a {\em
unique} unit.

\subsubsection*{2(e)} We claim that simple expressions satisfy the {\em
strong diamond property}: If an expression $s$ can rewrite in one
step to $s_{1}$, in symbols, $s \rulesto s_{1}$; and also $s \rulesto
s_{2}$, then there is an $s_{3}$ such that $s_{1}$ and $s_{2}$ can both be
rewritten to $s_{3}$ in {\em at most} one step.  We saw in class that
strong diamond implies unique termination.

We prove the strong diamond property by structural induction on $s$.
Suppose $s$ $s \rulesto s_{1}$ and $s \rulesto s_{2}$ with $s_{1} \neq
s_{2}$.  Since a rewrite rule applies to $s$, it must be a combination or
a conditional.

If $s$ is a conditional, it is of the form \Code{(if $s_{4}$ $s_{5}$
$s_{6}$)}.  Now we have three subcases.
\begin{enumerate}
\item $s_{1}$ and $s_{2}$ arise from applying rules to redexes in
different components of the conditional.  For example, $s_{1} = \Code{(if
$s'_{4}$ $s_{5}$ $s_{6}$)}$ because the test, $s_{4}$ rewrites to
$s'_{4}$, and $s_{2} = \Code{(if $s_{4}$ $s_{5}$ $s'_{6}$)}$ because the
alternate branch, $s_{6}$ rewrites to $s'_{6}$.  Then we can let $s_{3}$
be \Code{(if $s'_{4}$ $s_{5}$ $s'_{6}$)}.

\item $s_{1}$ and $s_{2}$ arise from applying rules to redexes in the same
component of the conditional.  For example, $s_{1} = \Code{(if $s'_{4}$
$s_{5}$ $s_{6}$)}$ because the test, $s_{4}$ rewrites to $s'_{4}$, and
$s_{2} = \Code{(if $s''_{4}$ $s_{5}$ $s_{6}$)}$ because the test also
rewrites to $s''_{4}$.  Then by induction there is an $s_{7}$ such that
$s'_{4}$ and $s''_{4}$ each rewrite to $s_{7}$ in at most step.  Then we
can let $s_{3}$ be \Code{(if $s_{7}$ $s_{5}$ $s_{}{6}$)}.

\item $s_{1}$ arises from applying a rule with all of $s$ as the redex.
This means the test, must be a $\bnf <boolean>$, say \Code{\#t}, and $s$
is of the form \Code{(if \#t $s_{1}$ $s_{6}$)}.  Also, $s_{2}$ must arise
from applying a rule to a branch of $s$.  If $s_{2}$ arose from rewriting
a redex in the other branch, then $s_{2}$ is of the form \Code{(if \#t
$s_{1}$ $s'_{6}$)} where $s_{6} \rulesto s'_{6}$.  So we let $s_{3}$ be
$s_{1}$ since $s_{2}\rulesto s_{1}$.  If $s_{2}$ arose from a redex in the
branch $s_{1}$, then $s_{2}$ is \Code{(if \#t $s'_{1}$ $s_{6}$)} where
$s_{1} \rulesto s'_{1}$.  Then let $s_{3}$ be $s'_{1}$.
\end{enumerate}


\subsubsection*{3(a)} The function ${\it replace}(B, x, y)$ is defined by
structural induction on the Scheme body $B$.

Suppose $B$ is of the form
\[\Code{(define $v_{1}$ $V_{1}$) \dots (define $v_{n}$ $V_{n}$) $M$},\]
where $M$ is an expression.   If $x \in \{v_{1}, \dots, v_{n}\}$, then 
${\it replace}(B, x, y) = B$, otherwise
\[{\it replace}(B, x, y) =
\Code{(define $v_{1}$ $V'_{1}$) \dots (define $v_{n}$ $V'_{n}$) $M'$}\]
where $V'_{i} = {\it replace}(V_{i}, x, y)$, and $M' = {\it replace}(M, x, y)$.

Suppose $B$ is of the form $\Code{($M_{1}$ \dots $M_{n}$)}$.  Then ${\it
replace}(B, x, y) = \Code{($M'_{1}$ \dots $M'_{n}$)},$ where $M'_{i} =
{\it replace}(M_{i}, x, y).$

The other cases are similar.

\subsubsection*{3(b)}
The decision procedure for $\alpha$-equivalence is defined by structural
induction on $B_{1}$.

The case for $B_{1}$ a lambda expression was given in the hint for
expressions with two formals; the extension to an arbitrary number of
formals is straightforward.

Suppose $B_{1}$ of the form
\[\Code{(define $v_{1}$ $V_{1}$) \dots (define $v_{n}$ $V_{n}$) $M$}.\]
Let $u_{1}, \dots, u_{n}$ be distinct ``fresh'' variables, i.e., variables
which do not occur in $B_{1}, B_{2}$.  Let
\[r_{1}(N) = {\it replace}({\it replace}(\dots ({\it replace}(N, v_{1},
u_{1}), v_{2}, u_{2})\dots v_{n-1}, u_{n-1}), v_{n}, u_{n}),\]
Then $B_{1}$ and $B_{2}$ are \aeqv\ iff $B_{2}$ is of the form
\[\Code{(define $v'_{1}$ $V'_{1}$) \dots (define $v'_{n}$ $V'_{n}$) $M'$},\]
$r_{1}(M) \aeqv r_{2}(M')$
and $r_{1}(V_{i}) \aeqv r_{2}(V'_{i})$ for $i=1,\dots,n$, where
\[r_{2}(N) = {\it replace}({\it replace}(\dots ({\it replace}(N, v'_{1},
u_{1}), v'_{2}, u_{2})\dots v'_{n-1}, u_{n-1}), v'_{n}, u_{n}).\]

The other cases are similar.

\subsubsection*{Problem 5}
By these rules,
\[\Code{(equal? (lambda (x) (+ 1 2)) (lambda (x) (+ 1 2))) $\rulesto$ \#t}.\]
But also,
\begin{eqnarray*}
\lefteqn{\Code{(equal? (lambda (x) (+ 1 2)) (lambda (x) (+ 1 2)))}}\\
{} & \rulesto & \Code{(equal? (lambda (x) (+ 1 2)) (lambda (x) 3))}\\
{} & \rulesto & \Code{\#f}
\end{eqnarray*}

\end{document}


