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

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

\def\rews{\byrule{rew*}}

\begin{document}
\handout{ps3}{Problem Set 3}{6 October 1995}

\due 13 October 1995.

\problem The \Code{Y} operator described in class satisfied the property
that
\[\Code{(Y $V$) = ($V$ (lambda (z) ((Y $V$) z)))}\]
for any immediate value $V$.  This allows us to simulate recursive
definitions of one argument procedures, i.e., of the form
\Code{(define (f x) $\bnf <expr>$)} by letting \Code{$V =$ (lambda (f)
(lambda (x) $\bnf<expr>$))}.

\subproblem Describe a similar operator \Code{Y2} such that that \Code{(Y2
$V$) = ($V$ (lambda (u v) ((Y2 $V$) u v)))} for any immediate value $V$, so
\Code{Y2} can be used to simulate recursive definitions of two-argument
procedures \Code{(define (g x y) $\bnf <expr>$)}.

\subproblem Explain what happens if we used \Code{Y}, instead of \Code{Y2},
on \Code{g} above?  (You might like to try this using the \Code{smeval}
procedure.)

\subproblem {}(Optional, for discussion) Is there a \Code{Y}-like operator
which handles

\begin{enumerate}
\item \Code{(define x (lambda () x))}?
\item How about \Code{(define x 3)}?
\item \Code{(define x x)}?
\item \Code{(define x (* 0 x))}?
\item \Code{(define x (cons 0 x))}?
\end{enumerate}

\problem We use the notation $M \rews N$ to indicate that expression $M$
can be rewritten to be $N$ by zero or more applications of rules of the
Scheme term rewriting model.

A set, ${\cal P}$, of Scheme expressions is \emph{evaluation-invariant} if,
whenever $M \rews N$, then $M \in{\cal P}$ iff $N \in{\cal P}$.

Two sets ${\cal P, Q}$ of expressions are \emph{Scheme-separable} iff
there is a Scheme procedure, \Code{good-side}, such that for every
expression \Code{$\bnf <expr>$},
\begin{enumerate}
\item there is a truth-value $b$ such that $\Code{(good-side '$\bnf<expr>$)}
\rews b$,

\item
$\Code{(good-side '$\bnf<expr>$)} \rews \Code{\#t}$ whenever
$\Code{$\bnf<expr>$} \in {\cal P}$, and

\item $\Code{(good-side '$\bnf<expr>$)} \rews \Code{\#f}$ whenever
$\Code{$\bnf <expr>$} \in {\cal Q}$.
\end{enumerate}

\subproblem Show that if $P,Q$ are nonempty, evaluation-invariant sets of
expressions, then they are not Scheme-separable.  \hint Consider
\begin{lisp} 
(define (contradict expr)
    (define (make-quoted-self-application expr)
        (list expr (list 'quote expr)))
    (if (good-side? (make-quoted-self-application expr))
        <not-ok-expr> <ok-expr>))) 
\end{lisp}

\subproblem A property of Scheme expressions is \emph{nontrivial} iff
there is some expression $\bnf<ok-expr>$ which has the property and
some expression $\bnf<not-ok-expr>$ which does not.  Conclude that no
nontrivial, evaluation-invariant property of Scheme expressions is
decidable.

\subproblem Give two ``interesting'' simple examples, besides the Halting
Property, of nontrivial, evaluation-invariant properties of Scheme
expressions.  Give two ``interesting'' simple examples of nontrivial
properties which are decidable.

%\problem To be continued ....
\end{document}
