\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}}}}
\newcommand{\obscong}{\fortext{\mathrel{\cong}}}
\newcommand{\retcong}{\underset{\rm ret}{\cong}}
\newcommand{\meas}[1]{\fortext{\mu(#1)}}

\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{ps4}{Problem Set 4}{11 October, 1996}

\due 18 October, 1996.

\medskip


\problem  The procedure for ``flattening'' arithmetic expressions suggested
in Handout 3 can be described by rewrite rules, the main ones being
``directed'' distributivity:
\begin{eqnarray*}
\Code{($e$ * ($f$ + $g$))} &\rulesto& \Code{(($e$ * $f$) + ($e$ * $g$))},\\
\Code{(($f$ + $g$) * $e$)} &\rulesto& \Code{(($f$ * $e$) + ($g$ * $e$))}.
\end{eqnarray*}

\subproblem 
Suppose $h$ is an arithmetic expression whose only operators are \Code{+}
and \Code{*}---no \Code{-} operator.
Starting from $h$ and successively applying the
directed distributivity rules to ``innermost'' subexpressions, i.e.,
subexpressions which do not have subsubexpressions to which the rule is
also applicable, will eventually rewrite $h$ to a ``flattened''
expression, namely, an expression with no subexpressions to which the rule
applies.  Give a simple justification for this claim.

\subproblem The directed distributivity rules are actually terminating:
starting with $h$, {\em no matter where the rule is successively applied},
a flattened expression will be reached.  This fact is not obvious because
if $e$ is a ``large'' subexpression, then the righthand side of the rule
with two occurrences of $e$ may be larger, have more redexes, etc., than
the lefthand side with only one $e$.

There is an ingenious, simple way to verify this termination
claim.  Define the measure, \meas{h}, of an arithmetic expression
$h$, by induction:
\begin{itemize}
\item $\meas{h} = 2$ if $h$ is \Code{0}, \Code{1}, or a variable.
\item $\meas{\Code{($e$ + $f$)}} = \meas{e} + \meas{f} + 1$.
\item $\meas{\Code{($e$ * $f$)}} = \meas{e} \times \meas{f}$.
\end{itemize}

Then termination follows immediately from the observation that if $h
\byrule{dir-dist} h'$, then $\meas{h'} < \meas{h}$.  Prove this fact.
\hint You should of course verify that $\meas{(e * f) + (e * g)} < \meas{e
* (f + g)}$, but termination does not follow {\em solely} from this fact,
since the subexpression $e * (f + g)$ which gets rewritten may not the
whole of $h$.

\subproblem  Now we extend the directed distributivity rule to handle
arithmetic expressions with the unary negation operator, \Code{-}, as
well:
\begin{eqnarray*}
-(-e) & \rulesto & e\\
-(f + g) & \rulesto & (-f) + (-g)\\
-(f *  g) & \rulesto & (-f) * g
\end{eqnarray*}
Verify that the rewrite system consisting of the directed distributivity
rules and the three rules above is terminating on all arithmetic
expressions.

\problem In Handout 2, we treated Scheme's \Code{let} as a derived
construct, i.e., ``syntactic sugar.''  There are some technical benefits
to treating \Code{let} instead as a legitimate ``functional kernel''
construct, with specific rewrite rules defining its computational
behavior.  Describe such a set of rewrite rules for \Code{let}.


\problem 

\begin{definition*}
The {\em printable values} are defined inductively to be: booleans,
numbers, the empty list \Code{()}, and \Code{cons}'s of printable values.
\end{definition*}

So lambda expressions are {\em not} printable values, and neither is a
list any of whose members are not printable.

\begin{definition*}
Two Scheme bodies are \emph{observationally distinguishable} iff one
rewrites to a printable value, and the other does not evaluate to exactly
that printable value.

A \emph{context} is a Scheme body with a single occurrence
of a free variable, \hole, called the \emph{hole}.  If $C$ is a context
and $M$ is an expression, then $C[M]$ denotes the result of
literally replacing---without any renaming---the hole in $C$ by $M$.

Two bodies $M$, $N$ are \emph{observationally congruent}, in symbols,
$M \obscong N$ iff there is {\em no} Scheme context, $C$, such that $C[M]$
and $C[N]$ are observationally distinguishable.
\end{definition*}

\subproblem  Say that two two bodies are {\em return-distinguishable} iff
{\em exactly one} of them can rewrite to a value (cf. Handout 2, \S~A.3).

Two bodies $M$, $N$ are \emph{return congruent}, in symbols,
$M \retcong N$ iff there is {\em no} Scheme context, $C$, such that $C[M]$
and $C[N]$ are return-distinguishable.

Prove that $M \retcong N$ iff $M \obscong N$.

\subproblem Carefully prove that
\[\Code{(+ $M$ $N$)} \obscong \Code{(+ $N$ $M$)}.\]
\hint A handwaving argument that this follows immediately because addition
is commutative is not acceptable.  For example, you will have to appeal to
facts specific to the functional kernel of Scheme we have considered thus
far in the course, since this observational congruence no longer holds
when we extend Scheme to include \Code{set!} or \Code{error} expressions.

\end{document}




\iffalse

rules for LET

extend simple expressions with LET and discuss (not prove)

terminated value must be ival.

use smeval

newman's lemma, local confluence (fails in Scheme with def's--spurious
failure up to def permutation, and real failure).

prove that in functional scheme (e + f) is obs cong to (f + e)

printable value congruent iff output ``1'' congruent iff returns-value-(ie
halts)-congruent.

R[(error V)] ---> V

termination of directed distributive law
\fi
