\documentclass[11pt]{handout}

\usepackage{6044}
\usepackage{time}
%,fullpage}
\usepackage{amsmath}

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

\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}
\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}}

\DefineBNFAbbrev{simpexp}{simple expression}
%\def\mult{\cross}

\begin{document}
\handout{ps3}{Problem Set 3}{27 September 1996}

\due 4 October, 1996.

\reminder {\bf QUIZ 1} in class on 4 October.

\medskip

\reading Revised (27 September) version of Handout 2, ``A Term
Rewriting Model for Scheme, I.''

\medskip

\problem We consider applying the garbage-collection rule to the body
\begin{lisp}
(define u (lambda () (* 2 x)))
(define v 4)
(define w (+ 1 (u)))
(define x (+ 1 v))
(define y (lambda () x))
(define z (lambda () y))
(cons v x)
\end{lisp}
For each of the subproblems below, briefly explain how you arrived at your
answer.

\subproblem Indicate which definitions can be garbage-collected
``immediately'', that is, by one application of the garbage-collection
rule to this body.

\subproblem Indicate which of the above definitions get garbage-collected
when this body is rewritten to a value while obeying the Lambda Body
Restriction.

\subproblem Indicate which of the above definitions can be
garbage-collected when this body is rewritten to a value with unrestricted
application of rewrite rules.

\problem We define {\em simple expressions} to be those expressions of
kernel Scheme (cf. Handout 2, Appendix A) which do not contain lambda
expressions or $\bnf <symbol>$'s, and whose {\em only} occurrences of
variables are the primitive procedure variables \Code{+}, \Code{-},
\Code{*}, \Code{<}, and \Code{=}.  (So simple expressions can't contain
\define's either, since procedure variables can't be redefined in our
TRM).  We also require that if one of these procedure variables occurs as
the operator of a combination, then the combination has exactly two
operands.

\subproblem  Give a grammatical description of \simpexp's in the style of
Appendix A of Handout 2.

\medskip The set of {\em simple values} is defined to be the integers and
truth values along with three functions from pairs of integers to
integers, namely, addition, subtraction and multiplication, and also with
two binary relations on the integers, namely, equality and $<$.  (Warning:
A simple value is an abstract {\em mathematical} object.  A \pval\ or a
\prvar\ is a {\em syntactic} token.  Don't confuse them.)

We regard any simple expression, $s$, as describing some simple value
which we call the {\em meaning of $s$}, written \mean{s}, except that not
every \simpexp\ is meaningful.  For example, \Code{(+ \#t <)} is
meaningless because it makes no sense to add a truth-value to a relation.
Similarly, \Code{(- 7 (+ \#t <))} is meaningless because it makes no sense
to subtract something meaningless from the integer seven.  On the other
hand, it makes sense to declare \mean{\Code{(if \#f (- 7 (+ \#t <)) =)}}
to be the same as \mean{\Code{=}}, namely, the integer equality relation,
even though the first branch of this conditional is meaningless.

\subproblem We can regard ``meaning'' as a partial function, \mean{\cdot},
from simple expressions to simple values.  Give a definition of this
partial function in the style used in Handout 3 to define the meaning of
arithmetic expressions---namely, by structural induction on \simpexp's.

\subproblem Prove that if $s_{1}$ and $s_{2}$ are simple expressions and
$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}}$.

\subproblem Prove the following version of a Unique Value Theorem for
Simple Expressions:
\begin{theorem*}
If a simple expression is meaningful, then it rewrites
to a {\em unique} \ival.
\end{theorem*}
\hint Use structural induction on \simpexp's.  You will need a stronger
induction hypothesis than this theorem itself.  It will help to note that
for every simple value, $v$, there is a unique simple expression, call it
$\hat{v}$, which is an \ival\ such that $\mean{\hat{v}} = v$.

\subproblem Prove that every simple expression, meaningful or not,
rewrites to a {\em unique, terminated} simple expression.

\problem Two Scheme expressions or bodies are said to be {\em equivalent
up to renaming} iff they can be made syntactically identical by freshly
renaming their bound variables.  Equivalence up to renaming is often
called {\em $\alpha$-equivalence} in the research literature and is
written \aeqv.

\subproblem Describe (in English or in Scheme) a procedure {\it replace}
such that for any Scheme body, $B$, and variables $x,y$, applying {\it
replace} to the arguments $B,x,y$ yields $B$ with all {\em free}
occurrences of $x$ replaced by $y$.

\subproblem Describe (in English or in Scheme) a procedure which
determines whether two Scheme bodies are \aeqv.

\hint Suppose $B_{1}$ is a body of the form \Code{(lambda (a b) $C_{1}$)}.
Then $B_{2}\aeqv B_{1}$ iff $B_{2}$ is of the form \Code{(lambda (c d)
$C_{2}$)}, and there are variables $v_{1} \neq v_{2}$ which do not occur
in either of $B_{1}$ or $B_{2}$ such that
\[{\it replace}({\it replace}(C_{1}, \Code{a}, v_{1}), \Code{b}, v_{2}) \aeqv
{\it replace}({\it replace}(C_{2}, \Code{c}, v_{1}), \Code{d}, v_{2}).\]

\subproblem {\em optional:}  Prove that \aeqv\ is an equivalence relation on Scheme
bodies.


\problem Suppose $B_{1}, B_{2}$ are Scheme bodies such that $B_{1} \aeqv
B_{2}$.

\subproblem Suppose $B_{1} \rulesto C_{1}$.  Verify that there must be a
$C_{2} \aeqv C_{1}$ such that $B_{2} \rulesto C_{2}$.

\subproblem Suppose $B_{1}$ can be rewritten to the numeral \Code{13}
using our Scheme Term Rewriting Model (TRM).  Conclude that $B_{2}$ also
can be rewritten to \Code{13}.

\problem Show that the Unique Primitive Value Theorem would fail if we
tried to specify the Scheme procedure \Code{equal?} by adding the
following rewrite rules to our TRM for functional Scheme:
\[\begin{array}{l}
\Code{(equal? \ival_{1} \ival_{2})} \rulesto \Code{\#t},\\
\text{\qquad if $\ival_{1}$ and $\ival_{2}$ are \aeqv.}\\
\\
\Code{(equal? \ival_{1} \ival_{2})} \rulesto \Code{\#f},\\
\text{\qquad if $\ival_{1}$ and $\ival_{2}$ are not \aeqv.}
\end{array}\]


\end{document}
