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

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

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

\newcommand{\rewritesto}{\stackrel{\rm rew}{\rulesto}}

\begin{document}
\handout{ps4}{Problem Set 4}{20 October 1995}

\due October 27, 1995

\problem We'll say two Scheme expressions $M$, $N$ are \emph{termination
distinguishable} iff, in the initial Scheme environment, $M$ halts and $N$
does not, or vice versa.  We'll say $M$ and $N$ are \emph{functional
termination congruent}, in symbols, $M \fcte N$, iff $C[M]$ and $C[N]$ are
not termination distinguishable for any functional Scheme context~$C$.
Explain why $\fcte$ defines the \emph{same} relation on expressions
as~$\fe$.  (Remember, the definition of~$\fe$ was like~$\fcte$ except $M$,
$N$ could be distinguished even when both halted, if they had different
printable values.)

\problem
Let ${\cal S}_a$ be the set of Scheme expressions which do \emph{not}
evaluate to the symbol~$a$.

\subproblem
Explain why ${\cal S}_a$ is a nontrivial, evaluation-invariant property of
expressions (cf.~Problem Set~3).

\subproblem\label{sa}
Explain how, given any Scheme expresssion,~$M$, one can find a
symbol,~$a$, such that $M \in {\cal S}_a$.

\subproblem
Why doesn't \ref{sa} contradict the undecidability of nontrivial,
evaluation-invariant properties?

\subproblem Give another interesting example of a family of nontrivial
evaluation-invariant properties, at least one of which can be found
automatically for every Scheme expression.

\problem With any equation $M = N$ we can associate two rewrite rules: $M
\rulesto N$ and $N \rulesto M$.  We can then regard any set of equations,
$\mathcal{E}$, as a set of rewrite rules and use the notation $M
\byrule{\mathcal{E}}^* N$ to mean that $M$ can be rewritten to~$N$ by
repeated use of the $\mathcal{E}$ rules.  We use the notation
$\proves[\mathcal{E}] M = N$ to mean there is a {\em formal equational
proof} that $M = N$ in the system with axioms $\mathcal{E}$ and
(reflexivity), and with inference rules (symmetry), (transitivity),
(congruence).

\subproblem Explain why $M \byrule{\mathcal{E}}^* N$ implies
$\proves[\mathcal{E}] M = N$.

\subproblem
Explain how to transform a proof for $\proves[\mathcal{E}] M = N$
into a rewriting of $M$ into~$N$.  Conclude that
\[
    M \byrule{\mathcal{E}}^* N
    \qquad\text{iff}\qquad
    \proves[\mathcal{E}] M = N.
\]

\subproblem
Describe kinds of $M$ and~$N$ for which the length of a proof that $M
= N$ will be much shorter than a rewriting of~$M$ to~$N$, where $M$,
$N$ are functional Scheme expressions and we use the equational Scheme
axioms from class:
\begin{align*}
M & = N & \quad \parbox[t]{3in}{if $M \rewritesto N$,}\\
\\
((\lambda(x) E[x]) M) & = E[M] &\quad \parbox[t]{3in}{where $E$ is an
evaluation context and $x$ is not free in~$E$,}\\
\\
M & = N &\quad \parbox[t]{3in}{where $N$ is obtained by instantiating a
defined variable in $M$ with another variable.}
\end{align*}

\problem
\subproblem\label{evensteps}
Show that it is undecidable whether a Scheme expression halts in an
\emph{even number} of rewriting steps.

\subproblem
Does \ref{evensteps} follow from the undecidability of
evaluation-invariant properties?

\problem The intersection of two decidable sets is a decidable set. The
intersection of two half-decidable (r.e.) sets is a half-decidable set.
The complement of a half-decidable set in general is not half decidable.
These facts are indicated by the ``D,'' ``H'' and ``N'' entries in the
table below.  Complete the remaining table entries with D (decidable), H
(half-decidable), or N (neither).  Include brief justifications of each
entry, including the given ones.

\begin{center}
\begin{tabular}{@{}r|c|c|@{}}
    \multicolumn1c{operation} & \multicolumn1c{decidable sets}
        & \multicolumn1c{half-decidable sets} \\\hline
    intersection    & D & H \\
    union           &   & \\
    complement      &   & N \\
    cdr             &   &\\\hline
\end{tabular}
\end{center}

\end{document}
