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

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

\newcommand{\fcte}{\underset{\rm ftc}{=}}

\def\rewss{\byrule{rew*}}
\def\eval1{\byrule{eval}}
\def\evalss{\byrule{eval*}}

\def\halts{\cal Halts}
\def\nhalts{${\overline{\halts}}$}


\begin{document}
\handout{q1}{Quiz 1}{30 October 1995}

\problem Let $M$ be the expression
\begin{verbatim}
(if (zero? (((lambda (x)
               (define from (lambda (y) (- y (+ x 2))))
               from)
             5)
            3))
    'abort
    (lambda () 'error))
\end{verbatim}

\subproblem
Circle those letters indicating Scheme rewriting rules which are
appplicable to $M$ for a first step of rewriting:
\begin{center}
L~~I~~P~~C~~G
\end{center}

\subproblem
Show the expression or body to which $M$ evaluates-in-{\em one}-step ($M
\eval1 ??$):

\subproblem
Show the body $B$ such $M \rewss B$ and $B$ cannot be further rewritten,
and circle those bracketed phrases which correctly describe $B$:
\begin{center}
[a value]~~[stuck]~~[an immediate value]~~[a printable value]~~[an error]
\end{center}

\problem In the body
\begin{verbatim}
(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{verbatim}
circle the variable definitions which can be garbage-collected:
\begin{center}
u~~v~~w~~x~~y~~z
\end{center}

\problem
Let $M_1$ be \Code{(+ (x) (x))} and $M_2$ be \Code{(* 2 (x))}.

\subproblem  There is a context of the form
\begin{verbatim}
(define (spin) (spin))
(define x (let ((state <blob1>))
            (lambda ()
               (if state
                   (begin (set! state (not state)) <blob2>)
                   (spin)))))
[ ]
\end{verbatim}
which distinguishes $M_1$ and $M_2$.  Describe expressions \Code{<blob1>}
\Code{<blob2>} so the context makes this distinction.

\subproblem
Is there a functional context which distinguishes $M_1$ and $M_2$?
Briefly explain.

\problem Consider equations of the form $\Code{(if M 1 1)} \fe \Code{1}$.

\subproblem
Show that the set of provable equations in the equational proof system for
$\fe$ described in class is not decidable.

\subproblem
Show that the set of {\em false} $\fe$ equations is not half-decidable
(r.e.).

\end{document}

