\documentclass[11pt]{handout}
\usepackage{6044}
\usepackage{time,fullpage}
\usepackage{amsmath}

\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}

\begin{document}
\handout{ps2}{Problem Set 2}{29 September 1995}

\due 6 October 1995.

\problem Here is the scheme body {\em maxtest} from the file {\tt
examples.scm} in the course directory containing the substitution model
code.

\begin{verbatim}
(define (max2d f n)
  (if (zero? n)
      0
      (max (max1d (lambda (i) (f n i)) (- n 1))
           (max1d (lambda (j) (f j n)) n)
           (max2d f (- n 1)))))
(define (max1d h n)
  (define (iter max-so-far k)
    (if (zero? k)
        max-so-far
        (iter
         (max max-so-far (h k))
         (- k 1))))
  (iter 0 n))
(define (m n)
  (lambda (i j)
    (let ((2n (* 2 n)))
      (- 2n (+ i j)))))
(max2d (m 4) 4)
\end{verbatim}
\subproblem Add suffixes to the binding and bound occurrences of the
variables in {\em maxtest} so it becomes an equivalent body satisfying the
Variable Convention.

\subproblem Check your answer by matching it against the result of
applying the {\tt enforce} procedure (in the file {\tt sm-scope.scm}) to
{\em maxtest}.  Is your answer identical to the {\tt enforce} result?  If
not, explain why it is correct anyway.

\subproblem Double-check your answer by applying the procedure {\tt
clean-suffixes} to it.  Does the result match the original {\em maxtest}?

\subproblem Rename the bound variables in {\em maxtest} so that you use
the smallest number of distinct identifiers.

\subproblem How could you use the {\tt clean-suffixes} procedure to aid in
working out the previous subproblem and similar examples?

\problem
\subproblem Give an informal equational proof in the style of lecture on 9/27
that application of Church numerals corresponds to exponentiation.  In
other words, prove that the procedure {\tt church-exp} from Handout 7,
``Church Numerals and Y Operator'' works as claimed.

\subproblem Similarly prove that the composition procedure is associative:
\[\Code{(compose (compose f g) h)} = \Code{(compose f (compose g h))}.\]

\subproblem Complete the definition
\begin{verbatim}
(define (church-add m n) <???>)
\end{verbatim}
from Handout 7, and give an equation-style proof that your definition is
correct.

\problem Let A be any one of the Scheme term-rewriting rules P, C, I, L,
G.  We use the notation $M \byrule{A} N$ to indicate that scheme body $M$
rewrites to become body $N$ by a {\em single} application of rule A, and
$M \byrule{A*} N$ to indicate any number, including zero, applications of
rule A.

\subproblem  Show that if $M \byrule{A} M_{1}$ and also $M \byrule{G}
M_{2}$, then there is an $M_{3}$ such that $M_{1} \byrule{G*} M_{3}$
$M_{2} \byrule{A} M_{3}$.
\subproblem  We can now conclude that it doesn't matter when garbage
collections are performed in the course of rewriting a Scheme expression
into a value.  Give a precise statement of this fact (along the lines of
the Uniqueness Theorem of the handout ``A Term Rewriting Model for
Scheme''), and outline its proof.

\subproblem It follows from the previous subproblem that we get the
``same'' result as any given rewriting model evaluation, if we postpone
all garbage collection steps until the end.  Give an example showing that
it is not possible to perform all the garbage collections at the beginning
and still finish with the same value.
\end{document}
