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

\textheight 8in

\oddsidemargin 11pt
\evensidemargin \oddsidemargin
\marginparwidth 0.5in

\advance\textwidth by -2\oddsidemargin

\newdimen\tablewidth
\tablewidth=\textwidth
\advance \tablewidth by -11pt

\parindent 0.0in
\parskip \medskipamount

\def\halts{\fortext{\mbox{Halts}}}
\def\nothalts{\fortext{\mbox{NotHalts}}}

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

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

\let\to\rightarrow
\let\union\cup
\let\cross\times


\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{pridfr}{procedure\ identifier}
\DefineBNFAbbrev{rspidfr}{rule-specified\ procedure\ id}
\DefineBNFAbbrev{ppridfr}{primitive\ procedure\ id}
\DefineBNFAbbrev{lamexp}{lambda\ expression}

\DefineBNFAbbrev{beginsf}{begin}
\DefineBNFAbbrev{cntxt}{context}
\DefineBNFAbbrev{deflimcntxt}{definition-limiting\ context}
\DefineBNFAbbrev{nondefcntxt}{non-definition\ context}
\DefineBNFAbbrev{nondefhole}{non-def\ or\ hole}
\DefineBNFAbbrev{evcntxt}{eval\ context}
\DefineBNFAbbrev{dcntxt}{definition\ context}
\DefineBNFAbbrev{idef}{immediate\ define}
\DefineBNFAbbrev{ccntxt}{control\ context}

\DefineBNFAbbrev{prv}{printable\ value}
\DefineBNFAbbrev{sexp}{s-expression}
\DefineBNFAbbrev{lsprv}{printable list-value}

%\DefineBNFAbbrev{separator}{separator}
%\DefineBNFAbbrev{msa}{make-self-apply}
%\DefineBNFAbbrev{perverse}{perverse}
\newcommand{\perverse}{\fortext{P}}
\newcommand{\msa}{\fortext{\mbox{make-selfapply}}}
\newcommand{\sep}{\fortext{T}}
%\DefineBNFAbbrev{separator}{separator}

\newcommand{\nextm}{\fortext{\mbox next_M}}

\makeatletter

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

 \vtop{\vbox{\kern3pt#1}\kern3pt}%
 \kern3pt\vrule}}%
 \hrule}}


\begin{document}
\handout{comput1}{Scheme Computability}{25 November 1998; revised Dec 1, 1998}

${}$
\section{Computable Functions on S-Expressions}
What can and can't Scheme do?  We can begin to pin this question down by
asking what functions can be computed by Scheme procedures.
Computability theory is traditionally developed using functions on the
integers, but in our setting with Scheme, it is natural to consider
computability over the set of \emph{S-expressions}:



\begin{bnf}
\begin{eqnarray*}
\sexp &::=& <self-evaluating> | \idfr | "("\sexp^*")"\\
<self-evaluating> &::=& <integer> | <boolean> | <string>\\
\idfr &::=& \hbox{identifiers which are not } <self-evaluating>\\
\end{eqnarray*}
\end{bnf}
S-expressions are the standard print representations of those list
structures that have such representations\footnote{We restrict the numbers
(more precisely, numerals) in printable values to be integers rather than
general Scheme numbers to avoid the messy details of floating point
arithmetic.  For example, in MIT Scheme, \Code{(= 1 1.0000000000000001)}
returns \Code{\#t}.

For simplicity we also omit ``dotted pair'' notation for pairs which are
not lists.}.  For any S-expression, $S$, Scheme provides a simple way to
form an expression whose value would have $S$ as its standard printed
representation.  Namely, the value of the Scheme expression $\Code{(quote
}S\Code{)}$ prints out as $S$.  We shall abbreviate $\Code{(quote
}S\Code{)}$ as $\Code{'}S$.  Most Scheme readers and printers also use
this abbreviation.

The {\em printable values} are exactly what we get from desugaring a quoted
S-expression.  These are the canonical Scheme expressions whose values
would print out as S-expressions:
\begin{bnf}
\begin{eqnarray*}
\prv &::=& <integer> | <boolean> | <string> | <symbol> | \lsprv\\
\lsprv &::=& <nil> | "(list " \prv^{+} ")"\\
<symbol> & ::= & "'"\idfr\\
<nil>  &::=&  "'()"
\end{eqnarray*}
\end{bnf}
So \Code{'$S$} desugars into a printable value which would in turn print
out in standard Scheme as exactly $S$ again.  For example, \Code{'(a b)}
has the standard printable representation \Code{(a b)}.  Note that our
Scheme Substitution Model uses standard \emph{input} representations of
values rather than output representations.  This means the expression
\Code{'(a b)} evaluates in the Substitution Model to the printable value
\Code{(list 'a 'b)}, i.e.,
\[\cnvgto{\Code{'(a b)}}{\Code{(list 'a 'b)}}\]
We let \sxp{E} be the standard S-expression representation of the printable
value of $E$, if any.
\begin{definition}
If $E$ is a Scheme expression, $p$ is a printable value, and $S$ is an
S-expression such that 
\[
\cnvgto{E}{p} \mbox{  and  } \cnvgto{\Code{(quote }S\Code{)}}{p}
\]
then we say that $\sxp{E} = S$.  If $E$ does not converge to a printable
value, then $\sxp{E}$ is undefined.
\end{definition}
So, for example,
\[
\sxp{\Code{'(a b)}} = \Code{(a b)} = \sxp{\Code{(list 'a 'b)}}
 = \sxp{\Code{(cons 'a '(b))}}
\]
It follows from the definition of the Substitution Model and the rules for
desugaring quoted S-expressions that \sxp{E} is a unique S-expression or
is undefined.

Now it is easy to define computable functions on S-expressions:
\begin{definition}
A partial function $f:\sexp^n \to \sexp$ is {\em Scheme computable}
iff there is a Scheme expression $F$ such that
\begin{itemize}
\item $\cnvgto{\Code{($F$ '$S_1$\dots'$S_n$)}}{}$ iff $(S_1\dots,S_n) \in \dom(f)$, and
\item $\sxp{\Code{($F$ '$S_1$\dots'$S_n$)}}
      = \sxp{\Code{(quote } f(S_1,\dots,S_n) \Code{)}}$ for all $(S_1\dots,S_n) \in \dom(f)$.
\end{itemize}
Such an expression $F$ is said to {\em compute} the function $f$.
\end{definition}
Another way to say that $F$ computes $f$ is to say that
\[\Code{(}F\, \Code{'}S_1\,\dots \Code{'}S_n\Code{)} =
\Code{'}f(S_1,\dots,S_n)\]
is a valid Scheme equation for all S-expressions $S_1,\dots,S_n$.

\problem Give an example of a Scheme expression $F$ such that $F$ computes
the identity function on S-expressions, but $\Code{($F$ x)} = \Code{x}$ is not a
valid Scheme equation.
\medskip

For practice with quoting, and in preparation for the non-computability
arguments in the next section, we consider how to make
``self-reproducing'' Scheme expressions.  A Scheme expression, $R$, is
self-reproducing iff evaluation of $R$ returns a printable value
syntactically identical to $R$.  That is, $\sxp{R} = R$!

Here's a way to make one: let \msa\ be an expression such
that
\begin{eqnarray*}
\sxp{\Code{(}\msa\ \Code{'}S\Code{)}} = \Code{(}S\ \Code{'}S\Code{)} \qquad\qquad \mbox{(*)}
\end{eqnarray*}

For example, we could define
\begin{eqnarray*}
\msa  &::=&  \Code{(lambda (s) (list s (list 'quote s)))}
\end{eqnarray*}
Now substituting $\msa$ for $S$ in (*) above yields
\[\sxp{\Code{(}\msa\ \Code{'}\msa\Code{)}} = \Code{(}\msa\ \Code{'}\msa\Code{)}\]
In other words, we can choose $R$ to be $\Code{(}\msa\ \Code{'}\msa \Code{)}$.

\problem

\subproblem Check that this last $R$ is self-reproducing by evaluating it
in real Scheme.

\subproblem Exhibit two other self-reproducing expressions and check them
in real Scheme.  Turn in your pretty-printed output.  \hint It doesn't
matter what \msa\ looks like as long as it satisfies the
specification (*).

\subproblem An expression $D$ is {\em doubly self-reproducing} iff
$\sxp{R} = \Code{($R$ $R$)}$.  Exhibit a doubly self-reproducing
expression and check it in real Scheme.  Turn in your output.

\subproblem {\em Optional} Adapt these ideas to construct a
self-reproducing program in your favorite non-Lisp programming language.
Check your program by running it, and turn in your output.


\section{Scott's Rice's Theorem}

\begin{definition}
A set $\mathcal{S}$ is Scheme
{\em decidable} iff its membership function is Scheme computable, i.e.,
there is a Scheme expression, $D$, called a \emph{decider} for
$\mathcal{S}$, such that
\begin{eqnarray*}
\sxp{\Code{($D$ '$S$)}} &  = & \Code{\#t} \mbox{ for } S \in
\mathcal{S}, \mbox{ and}\\
\sxp{\Code{($D$ '$S$)}}& = &\Code{\#f} \mbox{ for }S \not\in \mathcal{S}.
\end{eqnarray*}
\end{definition}

Let
\[
\halts ::= \set{S \in \sexp \mid \cnvgto{S}{}}.
\]
We aim to prove
\begin{corollary}\label{halting}
\halts\ is not Scheme decidable.
\end{corollary}

This famous result will follow from a slightly more general result of Dana
Scott.

\begin{definition}
Two sets $\mathcal{A}$, $\mathcal{B}$ of S-expressions are {\em Scheme
separable} iff there is a Scheme expression, \sep, called a
\emph{separator} for $\mathcal{A}$, $\mathcal{B}$, with the
following three properties:
\begin{enumerate}
\item
If $S \in \mathcal{A}$, then $\sxp{\Code{(\sep\ `$S$)}} =
\Code{\#t}$,

\item\label{b-sep} If $S \in \mathcal{B}$, then $\sxp{\Code{(\sep\ `$S$)}}
= \Code{\#f}$, and

\item\label{return-truth} for all S-expressions, $S$,
$\sxp{\Code{(\sep\ `$S$)}}$ is defined and equals either
\Code{\#t} or \Code{\#f}.
\end{enumerate}
$\mathcal{A}$ and $\mathcal{B}$ are {\em Scheme inseparable} iff they are
not Scheme separable.
\end{definition}

For any set $\mathcal{S}$ of S-expressions, let $\overline{\mathcal{S}}$
be the complement of $\mathcal{S}$, i.e., the set of S-expressions {\em
not} in $\mathcal{S}$.  A decider for a set of S-expressions is, by
definition, precisely a separator for $\mathcal{S}$ and
$\overline{\mathcal{S}}$.  So a set is Scheme decidable iff it and its
complement are Scheme separable.

\begin{definition}
A set ${\mathcal S}$ of S-expressions is {\em submodel-invariant}
providing $S_{1} \sm1 S_{2}$ implies that $S_1 \in \mathcal{S} \iff S_2
\in \mathcal{S}$, for all S-expressions $S_1$, $S_2$.
\end{definition}

\begin{theorem}\label{scott1} ({\bf Scott's Rice's First Theorem.})
Let $\mathcal{A}$, $\mathcal{B}$ be nonempty, submodel-invariant sets
of S-expressions.  Then $\mathcal{A}$ and $\mathcal{B}$ are computably
inseparable.
\end{theorem}

Notice that \halts\ is obviously a submodel-invariant, nonempty set of
S-expressions, and so is its complement.  Therefore \halts\ and its
complement are inseparable, and hence \halts\ is not Scheme decidable.
This proves Corollary~\ref{halting} above.

Now we proceed to the proof of Theorem~\ref{scott1}:
\begin{proof}

By contradiction.  Suppose there was a separator, \sep, for $\mathcal{A}$
and $\mathcal{B}$.  Assume for simplicity that \sep\ does not contain
\texttt{call/cc} or \texttt{abort}.

Since $\mathcal{A}$ and $\mathcal{B}$ are nonempty, there are
S-expressions $A \in \mathcal{A}$ and $B \in \mathcal{B}$.  Let \Code{s}
be a variable not free in \sep, $A$ or $B$, and define the ``perverse''
expression, \perverse, to be:
\[
\perverse ::= \Code{(lambda(s) (if (\sep\ (list s (list `quote s))) $B$ $A$))}.
\]

Now supppose $S$ is an S-expression such that $\sxp{\Code{(\sep\ '($S$
'$S$))}} = \Code{\#t}$.  This implies that \cnvgto{\Code{(\sep\ (list s
(list `quote s)))}}{\Code{\#t}}, so by definition of \perverse\ above,
\[
\Code{(\perverse\ '$S$)} \sms B.
\]
Hence by submodel-invariance,
\[
\Code{(\perverse\ '$S$)} \in \mathcal{B}.
\]
Now by separator-condition~\ref{b-sep},
\[
\sxp{\Code{(\sep\ '(\perverse\ '$S$))}} = \Code{\#f}.
\]

So we have shown that if 
\[
\sxp{\Code{(\sep\ '($S$ '$S$))}} = \Code{\#t},
\]
then
\[
    \sxp{\Code{(\sep\ '(\perverse\ '$S$))}} = \Code{\#f}.
\]
Similarly, if
\[\sxp{\Code{(\sep\ '($S$ '$S$))}} = \Code{\#f},\]
then
\[
    \sxp{\Code{(\sep\ '(\perverse\ '$S$))}} = \Code{\#t}.
\]
That is, for every S-expression, $S$,
\[\sxp{\Code{(\sep\ '($S$ '$S$))}} = \Code{\#t}
\ \iff\ 
\sxp{\Code{(\sep\ '(\perverse\ '$S$))}} = \Code{\#f}. \qquad\qquad \mbox{(**)}
\]

Now let $S$ be \perverse\ and $C$ be \Code{(\perverse\ '\perverse)}.
Then the equivalence (**) above yields
\[\sxp{\Code{(\sep\ '$C$)}} = \Code{\#t}
\ \iff\ 
\sxp{\Code{(\sep\ '$C$)}} = \Code{\#f}.
\]
which is only possible if \sxp{\Code{(\sep\ '$C$)}} is not defined,
contradicting separator-condition~\ref{return-truth}.
\end{proof}

\textbf{Problem}: (a) Suppose \sep\ did contain \texttt{abort}.  What step
of the above argument would no longer be justified?  \hint Suppose \sep\
was simply of the form \Code{(abort $\sep'$)}.

(b) Justify the assumption that the separator does not contain
\Code{call/cc} or \Code{abort}.  \hint Argue that if there were a
separator which did contain occurrences of \Code{call/cc} or \Code{abort},
then there would also be one which did not.

\medskip

\begin{definition}
A set $\mathcal{S}$ of S-expressions is {\em half-decidable} iff there is
a Scheme expression $H$ such that for all S-expressions $S$,
\[\cnvgto{\Code{($H$ '$S$)}}{} \iff\ S \in \mathcal{S}.\]
Such an $H$ is called a {\em half-decider} for $\mathcal{S}$.
Half-decidable sets are usually called {\em recursively enumerable} (r.e.)
sets.
\end{definition}

\begin{theorem*}\label{scott2} ({\bf Scott's Rice's Second Theorem.})
A set of S-expressions is said to be \emph{nontrivial} iff neither it nor
its complement is empty.  Let $\mathcal{S}$ be a nontrivial,
submodel-invariant set of S-expressions containing $\overline{\halts}$.
Then $\mathcal{S}$ is not half-decidable.
\end{theorem*}

The proof of the Second Theorem is similar to that of the First.

\begin{corollary}\label{nothalts}
$\overline{\halts}$ is not half-decidable.
\end{corollary}

\problem Prove Scott's Rice's Second Theorem.
\medskip

These two theorems reveal that {\em no} nontrivial fact about the value of
a Scheme expression can reliably be predicted by any procedure which could
be expressed in Scheme.  Since we know that Scheme can simulate any other
programming language, we can simply say that no computational procedure of
any kind can reliably determine any nontrivial property of the values
of Scheme expressions.

We observed in the Handout on arithmetic equations that there is no
single true theorem which is intrinsically unprovable, because if it's
true, one can simply include it as axiom in some sound proof system.
Similarly, there is no single Scheme expression and property of its value
which cannot be detected by some procedure -- one can simply include a
test for exactly this expression in a detection procedure.  But if a
procedure tries to detect a nontrivial, submodel-invariant property of every
S-expression to which it may be applied, then it must give a wrong answer,
or fail to give any answer, for {\em some} S-expression argument.

\newpage
\problem
\subproblem
Two sets are said to be \emph{almost equal} iff there are only finitely
many elements in one but not the other.
Show that if $\mathcal{S}_{1}$ is half-decidable and
$\mathcal{S}_2$ is a set of S-expressions which is almost equal to
$\mathcal{S}_1$, then $\mathcal{S}_2$ is also half-decidable.

\subproblem Let $\mathcal{A} = \halts$ and $\mathcal{B} = \overline{\halts}$.
Conclude that any Scheme procedure \sep\ must violate the
separator conditions of Scott's Rice's Theorem for \emph{infinitely many}
S-expressions, $S$.

\medskip

Note that \halts\ itself \emph{is} half-decidable: if the variable
\texttt{eval} is bound to a meta-circular evaluator, then \Code{(eval
'$S$)} halts iff $S \in \halts$, so \Code{eval} would be a half-decider
for \halts.

\section{The Hard Part of Scheme}
The proof that \halts\ is undecidable does not provide much information
about which part of Scheme is the ``hard part.''  For example, we have
noted that Hilbert's 10th Problem is undecidable.  Since Scheme has
integers and can define procedures for evaluating any polynomial, this
alone would lead to the halting problem being undecidable.  But in fact
the presence of integers in Scheme is not an essential cause of
undecidability.  The Halting Problem is still undecidable for a small
fragment of Kernel Scheme, which not only has neither integers, symbols,
nor lists, it doesn't even have conditionals!

To show this, we explain how to ``simulate'' two-counter machines with a
small fragment of Scheme. This implies that the Halting problem for the
small Scheme fragment will be as hard as the Halting Problem for
two-counter machines.  But we have observed earlier that all of Scheme can
be ``compiled'' into two-counter machines, so the Halting problem for
two-counter machines is as hard as the Halting problem for all of Scheme.
Since the full Scheme halting problem is undecidable, so are the Halting
problems for two-counter machines and hence for the small fragment of
Scheme.

For any two-counter machine $M$, a triple, $(n_0,n_1,n_2)$, of natural
numbers describes a ``configuration'' or ``complete state'' at any step in
a computation of $M$: $n_0$ designates the value of the program counter,
and $n_1 ,n_2$ the contents of the two counters.  Let
$\nextm(n_0,n_1,n_2)$ be the triple describing the next complete state of
$M$ after one instruction execution.  For example, if the seventh
instruction of $M$ was \texttt{dec2} --- decrement counter two --- then
$\nextm(7,5,111) = (8,5,110)$, indicating that the program counter next
points to the eighth instruction, counter one is unchanged, and counter
two has decreased by one.  For definiteness, we specify that
$\nextm(n_0,n_1,n_2) = (0,n_1,n_2)$ if $n_0$ is zero or greater than the
number of instructions in $M$.

Suppose $\nextm$ is Scheme computable.  Then $M$ halts starting in
configuration $(1,0,0)$ iff the following Scheme expression halts:

\begin{lisp}
(letrec ((try (lambda (tripl)
                (if (zero? (first trpl))
                    0     ;it doesn't matter what value is returned here
                    (try (nextm (first trpl)
                                (second trpl)
                                (third trpl)))))))
  (try (triple 1 0 0)))
\end{lisp}
where \texttt{nextm} is bound to a procedure for computing $\nextm$.  (We
assume wlog that \texttt{nextm} is an expression without
\texttt{set!}, \texttt{call/cc} or \texttt{abort}.  This ensures that
\texttt{nextm} computes $\nextm$ every time it is applied, and that an
application of \texttt{nextm} returns a value without aborting.)

Actually, to allow the conditional above to be simulated below by a
procedure \texttt{if-proc}, we modify the expression above so \texttt{try}
returns a \emph{delayed} result:
\begin{lisp}
(letrec ((try (lambda (tripl)
                (if (zero? (first trpl))
                    (lambda () 0)
                    (lambda ()
                      ((try
                       (nextm (first trpl)
                              (second trpl)
                              (third trpl)))))))))
  ((try (triple 1 0 0))))
\end{lisp}

Now to ``simulate'' two-counter machines using only a small part of
Scheme, we represent each natural number, $n$, by a lambda expression
$\widehat{n}$.  In the above expression, we would replace 0 and 1 by their
procedure representations $\widehat{0}, \widehat{1}$, and also replace
\texttt{zero?} and \texttt{if} by expressions which work on number
representations instead of numbers.  We know how to represent a pair of
values as a procedure, and we similarly define procedures \texttt{triple},
\texttt{first}, \texttt{second}, and \texttt{third} for forming procedural
representations of any triple of values and for selecting components of a
represented triple (see below).  This reduces the two-counter halting
problem to the halting problem for the part of Scheme we used to handle
the number and pair representations, along with \texttt{letrec} and
combinations.  So now we examine what part of Scheme is needed for these
number and pair representations.

\begin{definition}
Let 
\begin{eqnarray*}
B &::= & \Code{(make-pair (lambda (l r) (lambda (z) (z l r))))}\\
      {} && \Code{(true (lambda (l r) l))}\\
      {} && \Code{(false (lambda (l r) r))}\\
      {} && \Code{(left (lambda (pr) (pr true)))}\\
      {} && \Code{(right (lambda (pr) (pr false)))}\\
      {} && \Code{(triple (lambda (v1 v2 v3) (make-pair v1 (make-pair v2 v3))))}\\
      {} && \Code{(first (lambda (tripl) (left tripl)))}\\
      {} && \Code{(second (lambda (tripl) (left (right tripl))))}\\
      {} && \Code{(third (lambda (tripl) (right (right tripl))))}\\
      {} && \Code{(zero?-proc (lambda (n) \dots))}\\
      {} && \Code{(if-proc (lambda (t c a) \dots))}\\
      {} && \Code{(inc-proc (lambda (n) \dots))}\\
      {} && \Code{(dec-proc (lambda (n) \dots))}\\
\widehat{0} & ::= & \Code{(make-pair true true)}\\
\widehat{n+1} &::= & \Code{(make-pair false $\widehat{n}$)} \mbox{ for }n \in \nnintegers.
\end{eqnarray*}
\end{definition}

\problem

 \subproblem Complete the definition of the binding for
\texttt{zero?-proc} so that 
\[
\cnvgto{\Code{(letrec ($B$) (zero?-proc $\widehat{0}$))}}{\Code{\#t}}
\]
and 
\[
\cnvgto{\Code{(letrec ($B$) (zero?-proc $\widehat{n+1}$))}}{\Code{\#f}}.
\]

\subproblem Complete the definition of the binding for
\texttt{if-proc} so that 
\[
\Code{(letrec ($B$) (if-proc true $C$ $A$))}
\]
is equivalent to \Code{(letrec ($B$) $C$)},
and 
\[
\Code{(letrec ($B$) (if-proc false $C$ $A$))}
\]
is equivalent to \Code{(letrec ($B$) $A$)}
for any Scheme expressions $C, A$ such that \emph{both}
\cnvgto{\Code{(letrec ($B$) $C$)}}{} and 
\cnvgto{\Code{(letrec ($B$) $A$)}}{}.

\subproblem  Complete the definition of the binding for
\texttt{inc-proc} so that 
\[
\Code{(letrec ($B$) (inc-proc $\widehat{n}$))}
]\]
is equivalent to 
\[
\Code{(letrec ($B$) $\widehat{n+1}$)}
\]
for all natural numbers $n$.

\subproblem Complete the definition of the binding for \texttt{dec-proc}
so that 
\[
\Code{(letrec ($B$) (dec-proc $\widehat{n+1}$))}
\]
is equivalent to
\[
\Code{(letrec ($B$) $\widehat{n}$)}
\]
for all natural numbers $n$.

\subproblem Suppose a sequence of instructions defining a two-counter
machine, $M$, is given.  Sketch how to define, in a small fragment of
Scheme, an expression $N$ computing a version of $\nextm$ using the
procedural representations of number triples.  Namely, if
$\nextm(n_0,n_1,n_2) = (m_0,m_1,m_2)$, then 
\[
\Code{(letrec ($B$) ($N\ \widehat{n_0}\ \widehat{n_1}\ \widehat{n_2}$))}
\]
is equivalent to
\[
\Code{(letrec ($B$) (triple $\widehat{m_0}\ \widehat{m_1}\ \widehat{m_2}$))}.
\]

\subproblem To summarize, we have indicated why the halting problem
remains undecidable even for a small fragment of Scheme.  Exhibit a BNF
grammar defining this small fragment.  \hint Since none of the bindings in
$B$ are recursive, the \Code{letrec} of the multiple bindings $B$ can be
eliminated, leaving the binding of \texttt{try} as the sole
\texttt{letrec} binding needed.  (There is even a trick for eliminating
the sole remaining \texttt{letrec}, leaving only combinations of lambda
expressions and variables, but we won't go into that here.)


\end{document}
