\documentclass[11pt]{handout}

\usepackage{alltt}

\usepackage{6044}
\usepackage{time}
\usepackage[fleqn]{amsmath}
\usepackage{prooftree}
\setlength{\textheight}{8in}
\setlength{\textwidth}{5.5in}
\setlength{\oddsidemargin}{.4in} 
\setlength{\evensidemargin}{0in} 
\parindent0in
\parskip\medskipamount

\newcommand{\ple}{\ensuremath{\vdash_\le\,}}

\newcommand{\inttosym}{\text{int-to-sym}}

\def\f={\mathop{\Code{=}}}
\newcommand{\eqtn}[2]{\Code{( #1 = #2 )}}
\newcommand{\peqtn}[2]{\fortext{\proves \eqtn{#1}{#2}}}
\newcommand{\etrm}[1]{\Code{ = #1}}
\newcommand{\leqtn}[2]{\Code{( #1 <= #2 )}}
\newcommand{\aeqv}{\fortext{\mathrel{=_{\alpha}}}}
\def\proves2{\vdash_{2}}
\def\pran{\formath{nn-range}}

\newcommand{\obscong}{\fortext{\mathrel{\cong}}}
\newcommand{\prcong}{\underset{\rm proc}{\cong}}

\newcommand{\qrule}[1][]{%
    \ifx!#1!\else
        \rlap{\hbox to 4em{\hss#1\hss}}%
    \fi
    \vrule width 4em height -2.1pt depth 2.5pt\relax
}

\def\opCode#1{\mathbin{\Code{#1}}}

\makeatletter

\def\DefineBNFAbbrev#1#2{%
    \expandafter\newcommand\expandafter{\csname#1\endcsname}{\@bnfabbrev{#2}}%
}

\def\@bnfabbrev#1{%
    \@ifnextchar _{\@subabbrev{#1}}{\@plainabbrev{#1}}%
}

\def\@subabbrev#1_#2{\hbox{\normalfont$\langle\mbox{#1}_{#2}\rangle$}}

\def\@plainabbrev#1{\hbox{\normalfont$\langle\mbox{#1}\rangle$}}

% \def\exp{\hbox{$\bnf <expression>$}}

\DefineBNFAbbrev{idfr}{identifier}
\DefineBNFAbbrev{expr}{expression}
\DefineBNFAbbrev{define}{define}
\DefineBNFAbbrev{defines}{defines}
\DefineBNFAbbrev{vrbl}{variable}
\DefineBNFAbbrev{bod}{body}
\DefineBNFAbbrev{init}{init}
\DefineBNFAbbrev{val}{value}
\DefineBNFAbbrev{pval}{primitive\ value}
\DefineBNFAbbrev{ival}{immediate\ value}
\DefineBNFAbbrev{test}{test}
\DefineBNFAbbrev{orsf}{or}
\DefineBNFAbbrev{andsf}{and}
\DefineBNFAbbrev{prvar}{procedure\ variable}
\DefineBNFAbbrev{rspvar}{rule-specified\ procedure\ variable}
\DefineBNFAbbrev{pprvar}{primitive\ procedure\ variable}
\DefineBNFAbbrev{lamexp}{lambda\ expression}
%\DefineBNFAbbrev{beginsf}{begin}

\makeatletter


\def\fbox#1{%
  \vtop{\vbox{\hrule%
     \hbox{\vrule\kern3pt%
 \vtop{\vbox{\kern3pt#1}\kern3pt}%
 \kern3pt\vrule}}%
 \hrule}}

\makeatletter
\renewenvironment{description}
               {\list{}{\labelwidth\z@
                        \leftmargin1em
                        \itemindent-\leftmargin
                        \let\makelabel\descriptionlabel}}
               {\endlist}
\makeatother

\renewcommand*\descriptionlabel[1]{\hspace\labelsep
                                {\normalfont\bfseries #1}:}


\begin{document}
\handout{final}{Final Exam}{16 December 1996; typos corrected 16 Dec.;
points inserted 24 Dec.}

\medskip

This is a closed book final exam.  There are six (6) problems of
approximately equal weight.  You have three hours to complete this exam.
Good luck!


\problem(35)

(Equational Proof Systems).  There are four parts to this problem, but the
last part has double weight.

In this problem we develop another proof system for polynomial equations,
based on rewriting.  For your reference, the axioms and rules of the
polynomial proof system we studied in Handout 3, and homework Problem 3 of
that Handout, are given in the Appendix to this exam.  We continue to use
the notation
\[\provable p = q\]
to indicate that $p = q$ is provable in the system of Handout 3.

The new proof system has only one inference rule: if a series of
rewritings can change $p$ into $q$, then $p = q$ is proved.  That is,
\begingroup
\[
\prooftree
p \rulesto^{*} q
\justifies
p = q
\endprooftree
\]
\endgroup

The rewrite rules of the system are that a polynomial which matches either
side of the equational axioms of arithmetic (cf. Table~\ref{eqaxarith} in
the Appendix) can be replaced by the other side of the axiom.  For
example, by the identity axiom for $+$,
\[
\underline{e * 0} \rulesto 0 + (e * 0) 
\]
and by the inverse axiom for $+$
\[
\underline{0} + (e * 0) \rulesto ((e * 1) + -(e * 1)) + (e * 0)
\]
where, as usual, we have underlined the redex which gets replaced in the
rewriting step.  Continuing, we have
\begin{eqnarray*}
((e * 1) + -(e * 1)) + (e * 0) & \rulesto & (e * 0) + ((e * 1) + -(e * 1))\\
& \rulesto & ((e * 0) + (e * 1)) + -(e * 1)\\
& \rulesto & (e * (0 + 1)) + -(e * 1)\\
& \rulesto & (e * 1) + -(e * 1)\\
& \rulesto & 0.
\end{eqnarray*}
We will use the notation
\[\proves2 p = q\]
to indicate that $p = q$ is provable in the new proof system.  So by the
rewritings above, we conclude that
\[\proves2 e * 0 = 0.\]

\subproblem(5)
For the last five rewriting steps above, indicate the redex and the axiom
which justifies the rewriting.

\subproblem(5)  Explain why $\proves2 p = q$ implies $\proves2 q = p$.

\subproblem(10)  Show that $\proves2 p = q$  implies $\provable p = q$.
\hint Use the appropriate part of Handout 3, Problem 3.

\subproblem(15) Conversely, show that $\provable p = q$ implies $\proves2 p =
q$.

\problem(35)

(Observational Congruence).  We review the definition of observational
congruence of Scheme expressions:

\begin{definition*}
Two Scheme expressions are \emph{observationally distinguishable} iff one
evaluates to a printable value, and the other does not evaluate to exactly
that printable value.  Expressions $M$, $N$ are \emph{observationally
congruent}, in symbols, $M \obscong N$ iff there is no Scheme context,
$C$, such that $C[M]$ and $C[N]$ are observationally distinguishable.
\end{definition*}

\subproblem(15) Say that two bodies are {\em procedure-distinguishable}
iff {\em exactly one} of them evaluates to a procedure.  Two bodies $M$,
$N$ are \emph{procedure congruent}, in symbols, $M \prcong N$ iff there is
no Scheme context, $C$, such that $C[M]$ and $C[N]$ are
procedure-distinguishable.
Prove that
\[
M \prcong N \mbox{ iff } M \obscong N.
\]

\subproblem(10) Let $M$ be \Code{(x (y) (y))} and $N$ be \Code{((lambda (z) (x
z z)) (y))}.  Give a context demonstrating that $M$ and $N$ are {\em not}
observationally congruent in Scheme with side-effects (they are congruent
in functional Scheme).

\subproblem(10) Briefly explain why there can be no complete proof system for
observational congruence in functional Scheme.


\problem(35)

(Polynomial Undecidability).  As usual we consider multivariate
polynomials with integer coefficients whose variables range over the
integers.  The undecidability of many problems about such polynomials
follows from the insight that polynomials can simulate computer programs.
We did not show how to do this in class, but for the last part of this
problem we {\em assume} a result which specifies how polynomials act like
programs and then indicate one of its consequences for polynomial
decidability.

For any polynomial, $p$, let $\pran(p)$ be the nonnegative integers
in the range of $p$.

\subproblem(5) Explain why $\pran(p)$ is half-decidable for every $p$.

\subproblem(10)  Describe some half-decidable set of nonnegative integers
which is not decidable.

\subproblem(5)  Show that for all $n \geq 0$,
\[
n \not\in \pran(p) \quad\mbox{iff}\quad  \models 1 \leq (p - n)^{2}.
\]

\medskip

For the last part of this problem, you may assume:

{\bf Theorem} (Polynomial Programming).  For any half-decidable (that is,
r.e.)~set, $A$, of nonnegative integers, there is a polynomial, $p_{A}$,
such that
\[
A = \pran(p_{A}).
\]


\subproblem(15) Conclude that the valid polynomial inequalities are not
half-decidable.  \hint Choose an undecidable $A$ in the Polynomial
Programming Theorem.


\problem(35)

(Half-Decidability, Turing Reducibility).  Define a relation $\leq_{m}$ on
sets of S-expressions by the rule that ${\cal A} \leq_{m} {\cal B}$ iff
there is a computable function, $f$, from S-expressions to S-expressions
such that for all S-expressions, S,
\begin{enumerate}
\item $f(S)$ is defined, and
\item $S \in {\cal A} \mbox{ iff } f(S) \in {\cal B}$.
\end{enumerate}

\subproblem(10)
\label{down} Show that half-decidability inherits downward under
$\leq_{m}$.

\subproblem(10) Show that ${\cal A} \leq_{m} {\cal B}$ implies ${\cal A}
\leq_T {\cal B}$ (where $\leq_{T}$ denotes Turing reducibility).

\subproblem(15) Give an example of sets ${\cal A}, {\cal B}$ such that ${\cal
A} \leq_{T} {\cal B}$ but not ${\cal A} \leq_{m} {\cal B}$.  \hint Use
part~\ref{down}.

\problem(35)

(Counter Machines, Half-Decidability).  Say that a 2-Counter machine is
{\em 1-2-punched} iff it halts started in configuration $(0, 1, 0)$ and
does not halt started in configuration $(0, 2, 0)$.  Let ${\cal P}$ be the
set of S-expressions representing 1-2-punched 2-Counter
machines\footnote{Each instruction in a Counter machine is a single symbol
(\Code{inc1}, \Code{dec1}, etc.) or a symbol (\Code{ifr1}, \Code{ifr2},
etc.) followed by two nonnegative integers, and a Counter Machine is a
finite sequence of these instructions.  So there is a straightforward way
to represent Counter Machines by S-expressions.}.  Prove that neither
${\cal P}$ nor its complement is half-decidable.


\problem(25)

(Semigroup Word Problem).  In proving the undecidability of the Semigroup
Word Problem, we used the $n+3$ symbol alphabet $\set{\$, \\!, 0, \dots,
n}$ in the word equations corresponding to a 2-Counter Machine of length
$n$.  Let 2-SWP be the SWP for words over a two symbol alphabet.  Show
that 2-SWP is undecidable.



\newpage

\appendix

\section{Appendix: References for Polynomial Equation Proof System}
\begin{table}[h]
\caption{Standard Equational Inference Rules. \label{steqrules}}\small

\[\begin{array}{|c|} \hline
\\
\prooftree
\justifies
    e = e
\using
    \mbox{(reflexivity)}
\endprooftree
\qquad\quad
\prooftree
    e = f
\justifies
    f = e
\using
    \mbox{(symmetry)}
\endprooftree
\qquad\quad
\prooftree
     e = f, \quad f = g
\justifies
    e = g
\using
    \mbox{(transitivity)}
\endprooftree\\
\\
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 + f_1 = e_2 + f_2
\using
    \mbox{($+$-congruence)}
\endprooftree
\quad
\prooftree
    e_{1} = e_{2}, \quad f_{1} = f_{2}
\justifies
    e_1 * f_1 = e_2 * f_2
\using
    \mbox{($*$-congruence)}
\endprooftree
\quad
\prooftree
    e = f
\justifies
   -e = -f
\using
    \mbox{($-$-congruence)}
\endprooftree\\
\\ \hline
\end{array}\]
\end{table}

\begin{table}[h]
\caption{Equational Axioms for Arithmetic\label{eqaxarith}}

\[\begin{array}{|rcll|}
\hline
(e + f) + g &=& e + (f + g) & \mbox{(associativity of $+$)}\\
(e * f) * g &=& e * (f * g) & \mbox{(associativity of $*$)}\\
e + f &=& f + e & \mbox{(commutativity of $+$)}\\
e * f &=& f * e & \mbox{(commutativity of $*$)}\\
0 + e &=& e  & \mbox{(identity for $+$)}\\
1 * e &=& e  & \mbox{(identity for $*$)}\\
e + (-e) &=& 0  & \mbox{(inverse for $+$)}\\
e * (f + g) &=& (e * f) + (e * g) & \mbox{(distributivity)}\\
\hline
\end{array}\]


\end{table}

\begin{center}
{\bf For reference; this is NOT a final exam problem:}
\end{center}

Problem 3 from Handout 3:
%
For arithmetic expressions $e,f$ and variable $x$, the {\em substitution},
$\subst{e}{x}{f}$, of $f$ for $x$ in $e$ is defined by induction on $e$:
\newcommand{\op}{{\it op}}
\begin{eqnarray*}
\subst{x}{x}{f} &=& f,\\
\subst{c}{x}{f} &=& c \quad \mbox{for any constant or variable, $c$, distinct from } x,\\
\subst{(-e_{0})}{x}{f} &=&  -(\subst{e_{0}}{x}{f}),\\
\subst{(e_{0}\ \op\ e_{1})}{x}{f} &=&  \subst{e_{0}}{x}{f}\ \op\ \subst{e_{1}}{x}{f},
\quad \mbox{where \op\ $\in\{+,*\}$}\ .
\end{eqnarray*}

3(a) Prove that
\[
\provable f = g \mbox{  implies  } \provable\ \subst{e}{x}{f} =
\subst{e}{x}{g}.
\]

3(b)
Prove that
\[
\provable e = g \mbox{  implies  } \provable\ \subst{e}{x}{f} =
\subst{g}{x}{f}.
\]


\end{document}

