\documentclass[11pt]{handout}

\usepackage{6044}
\usepackage{time,fullpage}
\usepackage{amsmath}
\usepackage{prooftree}

\newcommand\Atop{\genfrac{}{}{0pt}0}
\newcommand\Over{\genfrac{}{}{}0}
\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}}$}
\def\mop{\mathop{f}}
\def\rep#1{\hbox{$\mop$-term}(#1)}

\newenvironment{btable}{%
    \begin{center}
    \begin{tabular*}{.8\textwidth}{@{}l@{\extracolsep{\fill}}l@{}}
}{%
    \end{tabular*}
    \end{center}
}

\newenvironment{bnfarray}{%
    \bnf
    \begin{eqnarray*}%
}{%
    \end{eqnarray*}%
}

\begin{document}
\handout{final}{Final Exam}{22 December 1995}

This exam is OPEN BOOK.  You have three hours.  Good luck!

\problem Consider the body
\begin{verbatim}
(define u (lambda () (lambda (x) (* 2 x v))))
(define v 4)
(define w (u))
(define x (+ 1 v)
(define y (lambda () x))
(define z (lambda () y))
(cons v w)
\end{verbatim}

\subproblem
Circle the variables whose definitions in the body above can be
garbage-collected at the next step in the rewriting model of Scheme:
\begin{center}
u~~v~~w~~x~~y~~z
\end{center}

\subproblem
Circle the variables whose definitions will have been
garbage-collected when the evaluation of the body is complete:
\begin{center}
u~~v~~w~~x~~y~~z
\end{center}


\problem Consider an equation in Scheme of the following form:
\[\Code{(if $M$ $N$ $N$)} = N.\]

\subproblem
Let $N$ be the variable \Code{z}.  Circle the expressions below which can
be substituted for $M$ so that the above equation holds as an
observational congruence in functional Scheme:
\begin{verbatim}
#t
#f
(spin)
(null? (list N))
(zero? (- N N))
(null? N)
(null? y)
N
(N)
\end{verbatim}

\subproblem
Now let $N$ be \Code{(z)}.  Circle the expressions below which can
be substituted for $M$ so that the above equation holds as an
observational congruence in {\em functional} Scheme:

\begin{verbatim}
#t
#f
(spin)
(null? (list N))
(zero? (- N N))
(null? N)
(null? y)
N
(N)
\end{verbatim}

\subproblem
Mark with a check those expressions in part 2(b) which keep the equation
holding as an observational congruence even in Scheme {\em with
side-effects}.

\problem Show that every recursively enumerable (r.e.) set of expressions
is many-one reducible to the Halting Problem for Scheme.

\problem  We consider strings over the symbols $\{r,l\}$ with the
interpretation that $r$ means the $90^o$ clockwise rotation of a square,
$l$ means the $90^o$ counterclockwise rotation, and string concatenation
denotes composing rotations.

\subproblem  How many different values of strings are there under this
interpretation?

\subproblem Describe ``canonical forms'' for the different values.

\subproblem
Write out a set of equations which are a {\em complete} set of axioms for
this interpretation and briefly explain why they are.

\problem We showed in class that the set of string equations which follow
from a {\em finite} set of string equations is r.e.  Explain why the set
of string equations which follow from an {\em r.e.}, possibly infinite,
set of string equations is still r.e.

\problem We consider (first-order) assertions over the {\em arithmetic
signature} consisting of the binary function symbols, $+, \times$
and constants 0,1.

\subproblem Write an arithmetic assertion which is true under the
the nonnegative integer interpretation, but false under the integer
interpretation.

\subproblem Write an arithmetic assertion which is true under the
the real number interpretation, but false under the rational number
interpretation.

\subproblem Write an arithmetic assertion which is true under the
the integers modulo three interpretation, but false under the integers mod
two interpretation.


\problem We now consider assertions over the signature consisting of a
single binary function symbol, $\mop$.

\subproblem Write an assertion whose meaning is precisely that $\mop$ is
an associative operator.

We can capture the meaning of string equations using such assertions as
follows.

Any string of symbols, $s$, can be represented by a term, $\rep{s}$, over
the $\mop$-signature by explicitly writing $\mop$ for string
concatenation, replacing each symbol, $a$, by a corresponding variable,
$x_a$, and associating to the right.  For example,
\[\rep{abddc} = \mop(x_a, \mop(x_b, \mop(x_d, \mop(x_d, x_c)))).\]

Now, for any particular strings $s_i,t_i, s, t$ over the alphabet
$\{a,b,c\}$, for example, the claim that the set of string equations
$\{s_1=t_1, \ldots, s_n = t_n\}$ implies $s=t$ is equivalent to claiming
the {\em validity} of the assertion saying:
\begin{quotation}
[``$\mop$ is associative'' and\\
``for all $x_a,x_b,x_c$, $(\rep{s_1} =\rep{t_1} \land \ldots \rep{s_n} =\rep{t_n})]\\
\implies \rep{s} = \rep{t}$.''

\end{quotation}
\subproblem
Write out, without abbreviations, the assertion over the signature $\mop$
which means that
\[\{abb=ca, cc=aba\} \models aac = cb\]

\subproblem  Conclude that the Uniform String Equation Problem is many-one
reducible to the Validity Problem for assertions.

\subproblem
Conclude that the Validity Problem for assertions is not decidable.


\problem  We now consider assertions over the string interpretation.
\subproblem
It might seem even easier to reduce the string equation problem to the
{\em truth} of assertions over the string interpretation.  For example,
try reducing the question whether
\[abb=ca, cc=aba \models aac = cb\]
to the question whether the assertion
\[ [abb=ca \land cc=aba] \implies aac = cb\]
is true over the interpretation with domain $\{a,b,c\}^*$.  Briefly
explain why this does not work at all.

\subproblem Even though the reduction above does not work, the Uniform
String Equation Problem really is many-one reducible to the Truth Problem
for assertions over the string interpretation.  Explain why.  (\hint
Appeal to the theorem from class that every r.e.\ set of strings is {\em
expressible} by an assertion over the string interpretation.)

\subproblem Prove that the Truth Problem for assertions over the string
interpretation is {\em not} many-one reducible to the Uniform String
Equation Problem.


\end{document}
