\documentclass{handout}
\usepackage{6044}
%\documentclass[11pt]{article}
%\usepackage{6001}
\usepackage{time,fullpage}
\usepackage{amsmath}
%\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}
%\newcommand{\subst}[3]{#1[#2 := #3]}
%\newcommand{\patch}[3]{#1[#2 \leftarrow #3]}
\begin{document}
\handout{ps4}{Problem Set 4}{19 October 1998}
\due Friday 23 October.
\medskip
\problem Consider the following versions for inequalities of the two
substitution rules for equality:
\[
\mbox{(1)}\qquad \models f \leq g \mbox{ implies } \models\ \subst{e}{x}{f} \leq
\subst{e}{x}{g}.
\]
\[
\mbox{(2)} \qquad \models e \leq g \mbox{ implies } \models\ \subst{e}{x}{f} \leq
\subst{g}{x}{f}.
\]
Only one of these assertions is true. Prove the one which is true, and
give a simple counterexample to the other one.
You may assume from lecture the
\begin{lemma*}
$\mean{\subst{e}{x}{f}}V = \mean{e}(\patch{V}{x}{\mean{f}V})$,
\end{lemma*}
where for any function, $F$, and elements $a,b$, we define $\patch{F}{a}{b}$
to be the function $G$ such that
\[G(u) = F(u) \mbox{ for } u \neq a,\mbox{ and } G(a) = b.\]
\bigskip
Download the latest version of the pattern matching code and the
Substitution Model interpreter for Scheme from the course website.
The file \texttt{match.scm} is a slightly updated version of the "context"
pattern matcher from the file \texttt{pattern.scm} used in a previous
assignment. The file \texttt{deriv-simplify-rules.scm} contains a set of
rewrite rules for putting arithmetic expressions in standard
sum-of-products form.
\problem Load the files \texttt{match.scm} and
\texttt{deriv-simplify-rules.scm} into Scheme. Simplify some example
arithmetic expressions to see what happens; there are some examples at the
end of \texttt{deriv-simplify-rules.scm}.
\subproblem Examine the \texttt{simplify-rules} defined in
\texttt{deriv-simplify-rules.scm}. Give an example showing that the order
in which the rules appear in the list \texttt{simplify-rules} matters: a
search for a final form by either of the procedures
\texttt{one-rules-application} or \texttt{apply-rules} in
\texttt{match.scm} may run forever if the rules are reordered.
\medskip
Rules closer to the beginning of the \texttt{simplify-rules} list have
priority in being applied by the rule application procedures. The rules
really accomplish rewriting in a series of stages: first they ``flatten''
an expression by repeated use of distributivity, then all sums and
nonnumeric products are right-associated, then products and then sums are
sorted, and throughout numerical operations are performed whenever
possible.
For ``staged'' rules like this, it's somewhat inefficient to keep one big
rule list: at later stages all the higher-priority rules are tried first
even though they will no longer be applicable. So there can be a small
gain in efficiency if the rules are grouped to reflect the intended stages
of the simplification process, and then final forms are found successively
for each group.
A more significant gain in efficiency can be achieved by noticing that
final forms for several rule-groups can be found using the
\texttt{one-topdown-final-form} or \texttt{one-bottomup-final-form}
procedures, instead of the very inefficient
\texttt{one-everywhere-final-form} procedure (all from the file
\texttt{match.scm}).
\subproblem Figure out a useful way to group the rules, and in several
cases to use bottomup or topdown rewriting, to find the final form of
arithmetic expressions. (Some rules may appear in several groups.) Then
define a procedure
\begin{lisp}
(define (one-arithmetic-final-form expr)
(one--final-form
last-rule-group
(one--final-form
next-to-last-rule-group
(one-...
.
.
.
(one--final-form
first-rule-group
expr)))))
\end{lisp}
Briefly justify any uses you made of bottomup or topdown final form search
in your procedure definition. Turn in some examples illustrating the
correctness of your procedure -- it should return the same final form as
\begin{lisp}
(one-everywhere-final-form simplify-rules expr)
\end{lisp}
If possible, submit timing information comparing these two procedures on
various expressions. In MIT scheme, a useful utility for timing
evaluations is
\begin{lisp}
(define (timed f . args)
(let ((init (runtime)))
(let ((v (apply f args)))
(write-line (list 'time: (- (runtime) init)))
v)))
\end{lisp}
\problem The file \texttt{sm.scm} includes many rules for "desugaring"
more general Scheme expressions into a small "kernel" of Scheme. For
example \texttt{drules:quote} are two simple rules for desugaring
expressions with quoted lists into expression in which quotes are only
used to describe symbols.
With these quote desugaring rules, the \texttt{one-everywhere-final-form}
procedure is not only inefficient, but depends for its correct handling of
quoted expressions on the details of how the \texttt{match} procedure
searches for context-pattern matches. So it would not work with several
correct, alternative versions of a \texttt{match} procedure.
\subproblem Give a simple example of an expression \texttt{expr} such that
\begin{lisp}
(one-bottomup-final-form drules:quote expr)
\end{lisp}
\emph{incorrectly} desugars \texttt{expr}.
\subproblem
Explain why
\begin{lisp}
(one-topdown-final-form drules:quote expr)
\end{lisp}
\emph{will} correctly desugar the quotes from \texttt{expr}.
\end{document}