\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{separator}{separator}
\DefineBNFAbbrev{perverse}{perverse}
\DefineBNFAbbrev{smeval}{smeval}
\DefineBNFAbbrev{step}{step-smeval}
\DefineBNFAbbrev{verifier}{verifier}


\newcommand{\undefv}{\formath{undefined-flag}}
\newcommand{\setbv}{\Code{(quote set!-value)}}

\newcommand{\obscong}{\fortext{\:\cong\:}}
%\newcommand{\size}{\fortext{\operatorname{size}}}
\newcommand{\intsym}{\fortext{\mbox{int-to-sym}}}
\newcommand{\symint}{\fortext{\mbox{sym-to-int}}}
\newcommand{\intsexp}{\fortext{\mbox{int-to-sexp}}}
\newcommand{\sexpint}{\fortext{\mbox{sexp-to-int}}}
\newcommand{\rep}[1]{\fortext{\Code{"}#1}}
%\newcommand{\unrep}[1]{\fortext{\llcorner #1 \lrcorner}}
%\newcommand{\idnum}{\fortext{\operatorname{id-num}}}


\makeatletter

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


\begin{document}

\handout{computability-2}{Scheme Computability, II}%
{11 November 1996; revised 12 December}

\section{Meta-Circular Interpreters and Universal Machines}

\begin{definition}\label{meta}
A {\em meta-circular interpreter for Scheme} is a closed Scheme
expression, \smeval, such that for all Scheme expressions, $M$,
\begin{enumerate}
\item \Code{(\smeval\ '$M$)} halts iff $M$ halts, and

\item\label{prv} if $\valof{M}$ is a \prv, then $\valof{\Code{(\smeval\
'$M$)}} = \valof{M}$.

\end{enumerate}

\end{definition}

\begin{theorem}\label{univ}
There is a meta-circular interpreter for Scheme.

\begin{proof}
The Abelson/Sussman textbook exhibits a meta-circular interpreter.
\end{proof}
\end{theorem}

Abelson/Sussman also exhibit a compiler written in Scheme which compiles
Scheme bodies to register machine code formatted as S-expressions.  They
also show how to write a register machine simulator in Scheme.  So another
meta-circular interpreter for Scheme is
\[\bnf \Code{(lambda (qs) ($<simulate-register-machine>$ ($<compile>$ qs)))}.\]

A third, very different meta-circular interpreter based on term rewriting
is available on the course handouts web-page in the directory
\Code{/rewriting-scheme-code}.

\problem\label{weak-sim} Explain why none of these meta-circular
interpreters satisfy a stronger and more natural version of
of Definition~\ref{meta}, namely,
\begin{quotation}
{\bf Strong Interpretation}.\ \ \ \  For all Scheme expressions, $M$,
\[
 \Code{(\smeval\  '$M$)} \obscong M.
\]

\end{quotation}

{\bf Problem 1.5} Show that if a procedure, \smeval, satisfies the Strong
Interpretation condition, then it is indeed a meta-circular interpreter
according to Definition~\ref{meta}.

{\bf Procedure 1.6}

(a) Let $p$ be a Scheme procedure, and $\mbox{Procs}(p)$ be the set of
lambda expressions in the set $\set{\valof{\Code{($p$ '$S$)}} \mid S
\mbox{ is an S-expression}}$.  Show that the arities (number of formals)
of the lambda expressions in $\mbox{Procs}(p)$ is bounded.

(b) Conclude that there is no ``strong'' meta-circular interpreter, i.e.,
procedure satisfying the Strong Interpretation condition.


{\bf Problem 1.7} Extend kernel Scheme with lambda-expressions of varying
numbers of arguments.  These expressions are of the form
\begin{bnf}
\[
\Code{(lambda $<variable>$ $<body>$)}
\]
\end{bnf}
(notice that the variable foloowing the \Code{lambda} is not
parenthesized), and their behavior is determined by the rewrite rule:
\begin{bnf}
\[
\Code{((lambda $l$ $B$) $V_{1} \dots V_{n}$)} \rulesto \Code{((lambda $(l)$ $B$)
(list $V_{1} \dots V_{n}$))}
\]
\end{bnf}
Show that now there {\em is} a ``strong'' meta-circular interpreter.
\hint Such an interpreter can be obtained by modifying the ``analyzing''
interpreter described in the Abelson/Sussman text.


\medskip

A meta-circular interpreter, or more typically some compiled version of
it, is known as a ``universal machine'': one program or machine which is
capable of simulating any other.  The existence of universal machines was
an insight of a community of researchers in mathematical logic, notably
the German Kurt G\"odel and the Englishman Alan Turing, in the early
1930's.  This idea stimulated the development of the first
general purpose digital computers in the late 1930's and early 40's.

\begin{corollary}
\halts\ is half-decidable.
\begin{proof}
Any meta-circular interpreter is a half-decider for \halts.
\end{proof}
\end{corollary}


\begin{theorem}
Decidable sets are closed under union, intersection, and set-theoretic
difference\footnote{The set-theoretic difference, $A - B$ of sets $A, B$
is $\set{a \in A \alt a \not\in B}$.}.
\begin{proof}
If $D_{\mathcal{A}}$ is a decider for $\mathcal{A}$, and $D_{\mathcal{B}}$
is a decider for $\mathcal{B}$, then
\[
\Code{(lambda (v) (or ($D_{\mathcal{A}}$ v) ($D_{\mathcal{B}}$ v)))}
\]
\[
\Code{(lambda (v) (and ($D_{\mathcal{A}}$ v) ($D_{\mathcal{B}}$ v)))}
\]
\[
\Code{(lambda (v) (and ($D_{\mathcal{A}}$ v) (not ($D_{\mathcal{B}}$
v))))}
\]
are deciders for $\mathcal{A} \union \mathcal{B}$, $\mathcal{A} \intersect
\mathcal{B}$, and $\mathcal{A} - \mathcal{B}$, respectively.
\end{proof}

\end{theorem}

It will now be useful to modify any of the meta-circular interpreters
described above to take an additional, nonnegative integer argument
indicating how many evaluation steps to perform.  With arguments $S$ and
$n$, the modified interpreter tries only to simulate $n$ evaluation steps
of Scheme expression $S$.  If $S$ does not halt within $n$ steps, the
interpreter returns \Code{\#f}.  If $S$ halts within $n$ steps and
$\valof{S}$ is a printable value, the interpreter returns $\Code{(cons
'printable $\valof{S}$)}$.  If $S$ halts in at most $n$ steps and
$\valof{S}$ is not a printable value, the interpreter returns \Code{\#t}.
The following definition abstracts the properties of this modified
interpreter which we need.

\begin{definition}
A {\em stepping meta-circular interpreter for Scheme} is a closed Scheme
expression, \step, such that for all Scheme expressions, $M$,

\begin{enumerate}

\item \Code{(\step\ '$M$ $\widehat{n}$)} halts for all $n \in \nnintegers$,

\item $M$ halts iff there is an $n \in \nnintegers$ such that
$\valof{\Code{(\step\ '$M$ $\widehat{n}$)}} \neq \Code{\#f}$,
and

\item for all $n \in \nnintegers$, if $\valof{\Code{(\step\ '$M$ $\widehat{n}$)}}
\neq \Code{\#f}$, then

\begin{itemize}
\item if $\valof{M}$ is a \prv, then 
\[\valof{\Code{(\step\ '$M$ $\widehat{n}$)}} = \Code{(cons 'printable $\valof{M}$)},\]

\item if $\valof{M}$ is not a \prv, then
\[\valof{\Code{(\step\ '$M$ $\widehat{n}$)}} = \Code{\#t}.\]

\end{itemize}

\end{enumerate}

\end{definition}


\begin{theorem}
There is a stepping meta-circular interpreter for Scheme.
\end{theorem}

\problem Pick one of the meta-circular interpreters described above and
explain how to modify it to obtain a stepping version.


\begin{theorem}
The half-decidable sets are closed under union and intersection.

\begin{proof}
If $H_{\mathcal{A}}$ is a half-decider for $\mathcal{A}$, and
$H_{\mathcal{B}}$ for $\mathcal{B}$, then
\[
\Code{(lambda (v) (begin ($H_{\mathcal{A}}$ v) ($H_{\mathcal{B}}$ v)))}
\]
is a half-decider for $\mathcal{A} \intersect \mathcal{B}$.

A half-decider for $\mathcal{A} \union \mathcal{B}$ is
\[
\begin{array}{l}
\Code{(lambda (v)}\\
\Code{\ \ (define (try n)}\\
\Code{\ \ \ \ (or (\step\  (list '$H_{\mathcal{A}}$ v) n)}\\
\Code{\ \ \ \ \ \ \ \ (\step\  (list '$H_{\mathcal{B}}$ v) n)}\\
\Code{\ \ \ \ \ \ \ \ (try (+ n 1))))}\\
\Code{\ \ (try 0)))}
\end{array}
\]

\end{proof}

\end{theorem}

There is an additional assumption implicit in the above proof.  Note that
it is possible that application of \step\ to some arguments could {\em
interfere} with subsequent applications of \step\ to those same, or other,
arguments.  That is, the first application could have a side-effect which
changed the subsequent behavior of \step\ so that it no longer acted as a
stepping interpreter.  So the expression above for the $\mathcal{A} \union
\mathcal{B}$ half-decider is correct only because {\em we have tacitly
assumed that there is no unexpected interference}.

We will continue to make this ``no interference'' assumption in our
subsequent constructions.  We can justify this assumption by observing
that all three meta-circular interpreters we described above do not
interfere with themselves, as long as they are successively applied only
to Scheme {\em expressions}\footnote{But the Abelson/Sussman interpreters
do not behave the same after being applied to {\em bodies}, because
evaluation of a body may install definitions in a global environment which
carries over to subsequent evaluations.}.  That is, if $M$ is a Scheme
expression, then \Code{(\smeval\ '$M$)} will always evaluate to the same
printable value, if any, no matter what computations have preceded the
application, as long as \smeval\ was previously applied only to
expressions.  The stepping meta-circular interpreter we obtain by
modifying one of the meta-circular interpreters described above will also
be interference-free.

For any decider, $D$, for example, the
expression
\[
\Code{(lambda (qs) (\smeval\  (list '$D$ qs)))}
\]
is decider for the same set, but will interfere neither with itself nor
any other evaluation.


\problem Assume without loss of generality that half-deciders return
\Code{\#t} when they halt.  Explain why
\[
\Code{(lambda (v) (or ($H_{\mathcal{A}}$ v) ($H_{\mathcal{B}}$ v)))}
\]
is a half-decider for $\mathcal{A} \union \mathcal{B}$ iff $\mathcal{B}
\subset \mathcal{A}$.

\medskip

\begin{theorem}
$\mathcal{A}$ is decidable iff $\mathcal{A}$ and $\overline{\mathcal{A}}$
are half-decidable.
\begin{proof}
It is easy to turn a decider into a half-decider, so the proof of the left
to right implication is straightforward.

For the other direction, let $H_1$ be a half-decider for $\mathcal{A}$, and
$H_2$ be a half-decider for $\overline{\mathcal{A}}$.  Then a decider for
$\mathcal{A}$ is
\[
\begin{array}{l}
\Code{(lambda (v)}\\
\Code{\ \ (define (try n)}\\
\Code{\ \ \ \ (cond ((\step\  (list '$H_1$ v) n) \#t)}\\
\Code{\ \ \ \ \ \ \ \ \ \ ((\step\  (list '$H_2$ v) n) \#f)}\\
\Code{\ \ \ \ \ \ \ \ \ \ (else (try (+ n 1)))))}\\
\Code{\ \  (try 0))}
\end{array}
\]

\end{proof}

\end{theorem}

\problem For two sets $\mathcal{A}, \mathcal{B}$ of S-expressions, let
\[
\mathcal{A} \uplus \mathcal{B} = \set{\Code{(0 $A$)} \alt A \in \mathcal{A}} \union
                \set{\Code{(1 $B$)} \alt B \in \mathcal{B}}
\]
Suppose $\mathcal{A}$ is undecidable, and let $\mathcal{S} = \mathcal{A}
\uplus \overline{\mathcal{A}}$.  Prove that neither $\mathcal{S}$ nor
$\overline{\mathcal{S}}$ is half-decidable.


\section{Integer Representations}

In the context of Scheme computability, it was natural to work with sets
of printable values, and Scott's Rice's Theorems identify an extensive
class of noncomputable functions and undecidable sets of printable value
representations of S-expressions.

But instead of translating an S-expression, $S$, into the Scheme
expression, \Code{'$S$}, we can choose to translate S-expressions into
Scheme expressions in very different ways.  This will allow us to discover
undecidable sets of familiar objects like nonnegative integers, as well as
sets of more exotic objects like Scheme procedures.

So let us consider translating an arbitrary S-expression, $S$, into a
Scheme expression which we denote as \rep{S}.  A minimum requirement on
the translation is that the value of \rep{S} should exist and uniquely
determine $S$, i.e.,
\[
S_{1} \neq S_{2} \mbox{  implies  } \valof{\rep{S_{1}}} \neq \valof{\rep{S_{2}}}
\]
for all S-expressions, $S_{1}, S_{2}$.

At this point we can take the definitions of computability,
inseparability, decidability, and half-decidability from Handout 15, as
well as the definitions of meta-circular interpreters above, with
all occurrences of \Code{'$\bnf <phrase>$} replaced by $\bnf
\rep{<phrase>}$.  To avoid ambiguity, we will refer to these modified
definitions as \Code{"}-computability, \Code{"}-inseparability, etc.

For example, we will say that the translation has the {\em self-apply
property} if there is a Scheme expression, $\bnf <rep-self-apply>$, which
computes the translations of self-applications, namely,
\[\bnf \valof{\Code{($<rep-self-apply>$ \rep{S})}} = \valof{\rep{\Code{($S$ \rep{S})}}}
\qquad\qquad(\mbox{self-apply property})\]
for all S-expressions, $S$.

Now, for {\em any} translation with the self-apply property, the proof of
Scott's Rice's First Theorem holds with no change other than modifying the
definition of \perverse\ to be:
\[\bnf
\begin{array}{l}
\Code{(lambda(rep-s)}\\
\Code{\ \ (if (\separator\ ($<rep-self-apply>$ rep-s))}\\
\Code{\ \ \ \ \ \ $B_0$}\\
\Code{\ \ \ \ \ \ $A_0$))},
\end{array}\]
where \Code{rep-s} is a variable not free in $A_{0}$ or
$B_{0}$.\footnote{There is no need to require that \Code{rep-s} not occur
free in \separator\ or $\bnf <rep-self-apply>$.  These expressions are
specified to work at ``top-level'' before any variables have been defined,
so, without loss of generality, we may assume they are closed
expressions.}  So we conclude that \halts\ is \Code{"}-undecidable for any
translation with the self-apply property.

\problem Suppose we choose to translate $S$ into the Scheme expression
\Code{(cons 1 '$S$)} if $S$ halts, and into \Code{(cons 0 '$S$)}
otherwise.  Show that $\halts$ is \Code{"}-decidable and
\Code{"}-separable from $\overline{\halts}$.  Why doesn't Scott's Rice's
Theorem apply in this case?

\problem\label{thunk-trans}
We consider a Scheme definition, $\bnf <code-def>$, of a variable
\Code{code} so that
\[
\valof{\Code{(code '$S$)}} = \Code{(lambda () (code '($S$ '$S$)))}.
\]
Here is such a definition:
\[
\begin{array}{l}
\Code{(define (code pv)}\\
\Code{\ \ (lambda () (code (list pv (list 'quote pv))))}\\
\end{array}
\]
Now define \rep{S} to be
\[\bnf
\Code{((lambda (qs)} <code-def>\  \Code{(lambda () (code qs)) '$S$)}
\]

\subproblem Verify that translating $S$ to \rep{S} has the required
uniqueness property.

\subproblem Verify that this translation has the self-apply property. \hint
Let $\bnf <rep-self-apply>$ be \Code{(lambda (rep-s) (rep-s))}.

\subproblem Show that {\em no} non-trivial set of S-expressions is
\Code{"}-half-decidable.

\subproblem Conclude that the property in Handout 15, Problem 4(a) fails
for \Code{"}-half-decidability.
\medskip

\medskip

Problem~\ref{thunk-trans} shows that the conditions on translations are
not strict enough to avoid pathological cases.  One straightforward way to
find satisfactory nonstandard translations is to ensure that there is a
computable correspondence between the nonstandard translation and the
standard one using \Code{quote}.

\begin{definition}
A translation from S-expressions, $S$, to Scheme expressions, \rep{S},
will be called {\em good} iff there are Scheme expressions, $\bnf
<to-quote>$ and $\bnf <from-quote>$, such that
\[
\valof{\Code{($\bnf <to-quote>$ \rep{S})}} = \valof{\Code{'$S$}}, \mbox{ and}
\]
\[
\valof{\Code{($\bnf <from-quote>$  '$S$)}} = \valof{\rep{S}}.
\]
\end{definition}

It is easy to verify that good translations have the uniqueness,
self-apply, and equality properties above, so all the results of Handout
15 will apply to them, as will essentially all the results we will
establish below about the standard \Code{quote} translation.

So now, if we want an undecidable set, say, of {\em nonnegative integers},
we need only find a {\em good} translation from quoted S-expression values
into nonnegative integers.

However, there {\em isn't any} such good translation using our current
Scheme kernel.  The crux of the problem is that there is no procedure
which can produce an infinite number of symbols starting from non-symbols.

\problem
\subproblem Prove that if $B_{1} \eval1 B_{2}$, then every symbol in body $B_{2}$
must occur in body $B_{1}$.

\subproblem Conclude that for any kernel Scheme expression, $F$,
$\set{\valof{\Code{($F$ $\widehat{n}$)}} \mid n \in \nnintegers}$ contains
only finitely many symbols.

\medskip

So we need to extend Scheme to allow definition of a {\em symbol
enumerator}, namely, a total function from nonnegative integers {\em onto}
the set of symbols.

Real Scheme includes string and string-to-symbol procedures which allow
the definition of symbol enumerators.  We will not bother introducing
string procedures into our kernel, but henceforth include a new,
primitive procedure identifier
\[\bnf \ppridfr ::= \dots | \Code{int->sym}\]
such that \Code{int->sym} is specified to compute some symbol enumerator
\[
\bnf \intsym: \nnintegers \to <symbol>.
\]

Once we have \Code{int->sym}, we can also translate symbols back into
integers:

\begin{lemma}
There is a computable, necessarily one-to-one, total function
\[\bnf
\symint: <symbol> \to \nnintegers
\]
 such that
\[\intsym(\symint(\sigma)) = \sigma\]
for all symbols $\sigma$.

\begin{proof}
\begin{lisp}
(define (sym->int symb)
  (define (search n)
    (if (eq? symb (int->symb n)) n (search (+ n 1))))
  (search 0))
\end{lisp}
\end{proof}
\end{lemma}

Now it will be easy to define a good translation from S-expressions to
nonnegative integers.  We first choose an integer {\em pairing} function,
\pair, which defines a computable one-to-one map from pairs of nonnegative
integers to nonnegative integers.  For example, we can take $\pair(m, n)$
to be $2^{m}3^{n}$.

\problem Show that there are Scheme computable functions, \frst, and
\scnd, such that
\[\frst(\pair(n, m)) = n \mbox{  and  } \scnd(\pair(n, m)) = m.\]

Now we can define $\bnf <from-quote>_{\nnintegers}$ to be
\begin{lisp}
(lambda (pv)
  (define (pair n m) (* (expt 2 n) (expt 3 m)))
  (define (first n) ...)
  (define (second n) ...)
  (define (sexp->int qs)
    (cond
     ((boolean? qs)
      (if qs (pair 0 1) (pair 0 0)))
     ((integer? qs) (pair 1 qs))
     ((symbol? qs) (pair 2 (sym->int qs)))
     ((null? qs) (pair 3 0))
     (else                              
      (pair 4                       ;qs = '(S1...Sk) for k>=1
            (pair (sexp->int (car qs))
                  (sexp->int (cdr qs))))))))
  (sexp->int pv))
\end{lisp}

Note that $\bnf <to-quote>_{\nnintegers}$ above actually defines a
one-to-one total function
\[\
\sexpint:\sexp \to \nnintegers.
\]

\problem\label{int-to-sexp} Exhibit a corresponding definition, $\bnf
<to-quote>_{\nnintegers}$, of a total function
\[
\intsexp: \nnintegers\ \to \sexp
\]
{\em onto} the set of S-expressions.

Now we get a set of nonnegative integers which is undecidable, because by
Scott's Rice's First Theorem for the $\bnf <from-quote>_{\nnintegers}$
translation, \halts\ is \Code{"}-undecidable.  In other words,
\begin{definition}
Let
\[\bnf
\halts_{\nnintegers} ::=  \set{n \mid \widehat{n} =
\valof{\Code{($<from-quote>_{\nnintegers}$\ '$S$)}} \mbox{ for some } S \in \halts}
\]
\end{definition}

\begin{theorem}\label{int-halts}
$\halts_{\nnintegers}$ is undecidable.
\end{theorem}

\problem Let $f(n) = \pair(4, \pair(n, \pair(1, n))))$, and let $F$ be a
Scheme expression computing $f$.  Verify that we can use $F$ as $\bnf
<rep-self-apply>$ for the $\bnf <from-quote>_{\nnintegers}$ translation.

\medskip

So far we have not specified any particular primitive rewrite rules for
\Code{int->sym}.  This makes it possible to include arbitrary new
``decidable'' sets of integers in Scheme extended with
\Code{int->sym}.  Namely, let $Z$ be some set of integers, i.e., $Z
\subset \integers$.  Using rules
\[
\Code{(int->sym $\widehat{2n}$)} \rulesto \Code{'true} \qquad{if } n \in Z,
\]
\[
\Code{(int->sym $\widehat{2n}$)} \rulesto \Code{'false} \qquad{if } n \not\in Z,
\]
for all $n \in \nnintegers$, will imply that $Z$ is decided by the
expression
\begin{lisp}
(lambda (n) (if (eq? 'true (int->sym (* 2 n))) #t #f)) .
\end{lisp}
The remaining rewrite rules for application of \Code{int->sym} to odd numbers
can then be chosen to ensure that \Code{int->sym} is a symbol enumerator.

\problem \subproblem\label{ok-rules} Define primitive rewrite rules for
\Code{int->sym} so that it is a symbol enumerator and so that the same
sets of integers are decidable after extending Scheme with \Code{int->sym}
as before.

\subproblem Describe some simple general conditions on the rewrite rules
for \Code{int->sym} which are sufficient to ensure the property of
part~\ref{ok-rules}.  How about necessary and sufficient? \hint Consider
simulating a Scheme-with-\Code{int->sym} decider for $Z$ by a Scheme
expression which contains no symbols or occurrences of \Code{int->sym}.

\medskip

{\bf Problem 11.5} Define
\begin{eqnarray*}
\mbox{church}(0) & ::= & \Code{(lambda(x) x)},\\
\mbox{church}(n + 1) & ::= & \Code{(lambda (f) (lambda (x) (f
(($\mbox{\rm church}(n)$ f) x))))}.
\end{eqnarray*}
Show that translating $S$ into $\mbox{church}(\sexpint(S))$ is a good
translation of S-expressions into Scheme expressions.

\section{Enumerability}
\begin{definition}
A {\em range set} is the range of a Scheme computable partial function
from \nnintegers\ to S-expressions.
\end{definition}

In other words, $\mathcal{S}$ is a range set iff there is a Scheme
expression, $F$, such that
\[\set{\valof{\Code{($F$ $\widehat{n}$)}} \mid n \in \nnintegers \mbox{
and } \Code{($F$ $\widehat{n}$)} \mbox{ halts}} =
\set{\valof{\Code{'$S$}} \mid S \in \mathcal{S}}.\]

\begin{theorem}\label{range-set}
A set of S-expressions is a range set iff it is half-decidable.
\begin{proof}
To show that range sets are half-decidable, suppose $F$
computes a function, $f$, from \nnintegers\ to S-expressions, then
\[
\begin{array}{l}
\Code{(lambda (qs)}\\
\Code{\ \ (define (first n) \dots)}\\
\Code{\ \ (define (second n) \dots)}\\
\Code{\ \ (define (equal? s t) \dots)}\\
\Code{\ \ (define (in-range? s n)}\\
\Code{\ \ \ \  (or (equal? s (\step\ (list '$F$ (first n)) (second n))}\\
\Code{\ \ \ \  \ \ \ \ (in-range? (+ n 1))))}\\
\Code{\ \ (in-range? qs 0))}
\end{array}
\]
is a half-decider for the range of $f$.

Conversely, suppose $H$ is a half-decider for a set $\mathcal{S}$ of
S-expressions.  The empty set is the range of the function on \nnintegers\
with empty domain, so we may assume there is some $S_{0} \in \mathcal{S}$.
Then $\mathcal{S}$ is the range of the function computed by:
\[
\begin{array}{l}
\Code{(lambda (n)}\\
\Code{\ \ (let ((s-exp (int->sexp (first n))))}\\
\Code{\ \ \ \ (if (\step\ (list '$H$ s-exp) (second n))}\\
\Code{\ \ \ \ \ \ \ \ s-exp}\\
\Code{\ \ \ \ \ \ \ \ $S_{0}$)))}
\end{array}
\]
\end{proof}

\end{theorem}

\problem  Write a Scheme definition of \Code{equal?} such that
\begin{eqnarray*}
\valof{\Code{(equal? '$S$ '$S$)}} & = & \Code{\#t},\\
\valof{\Code{(equal? '$S$ '$T$)}} & = & \Code{\#f} \mbox{ if } S \neq T,
\end{eqnarray*}
for all S-expressions $S, T$.

\medskip

\begin{theorem}\label{bijection}
Every infinite half-decidable set of S-expressions is the range of a
one-to-one, total computable function on the \nnintegers.
\end{theorem}

\problem Prove Theorem~\ref{bijection}.


\begin{definition}
A partial function $f:\nnintegers \to \nnintegers$ is {\em strictly
increasing} if, for all $n < m \in \nnintegers$,
\[m \in \dom(f) \quad \mbox{implies} \quad n \in \dom(f) \mbox{ and } f(n) < f(m) .\]
\end{definition}


\begin{theorem}\label{inc-range}
A set of S-expressions is decidable iff it is the range of $(\intsexp \circ
f)$ for some strictly increasing $f:\nnintegers \to \nnintegers$.
\end{theorem}

\problem
Prove Theorem~\ref{inc-range}.  \hint Treat finite and infinite sets of
S-expressions as separate cases.

\medskip

\begin{definition}
For any partial function $g:\sexp \to \sexp$ and set $\mathcal{S}$ of
S-expressions, let
\[
g(\mathcal{S}) ::= \set{g(S) \mid S \in \mathcal{S} \intersect \dom(g)} .
\]
\end{definition}

\begin{theorem}\label{g-closed}
If $\mathcal{S}$ is half-decidable and $g:\sexp \to \sexp$ is computable,
then $g(\mathcal{S})$ is also half-decidable.
\begin{proof}
If $\mathcal{S}$ is the range of a computable enumerator $h:\nnintegers \to \sexp$,
then $g(\mathcal{S})$ is the range of the computable enumerator $g \circ
h$, and so is half-decidable by Theorem~\ref{range-set}.
\end{proof}

\end{theorem}


\section{Incompleteness}

Any proof system has some set of things called {\em proofs}.  One key
property of a proof is that ``understanding'' is not needed to verify that
it is a proof---the proof can be checked mechanically.  That is, we
require that the set of proofs be {\em decidable}.  In addition, there
must be a mechanical way to extract from the proof the theorem it proves.

For example, we consider proof systems for {\em Scheme equations}:
S-expressions of the form \Code{($M$ = $N$)} where $M, N$ are Scheme
expressions.  We can safely assume that proofs are represented as
S-expressions.  So any proof system is completely determined by a
computable function $v:\sexp \to \sexp$, called a {\em verifier}, which
detects whether an S-expression is a proof, and if it is, extracts the
theorem proved.  Formally, we may as well define the verifer to {\em be}
the proof system:

\begin{definition}
A {\em proof system for Scheme equations} is a computable function,
$v:\sexp \to \sexp$, such that for every S-expression, $S$,
\begin{enumerate}
\item $v(S) = \Code{\#f}$, or
\item $v(S) = Q$ for some Scheme equation, $Q$.
\end{enumerate}
An S-expression, $S$, such that $v(S) = Q$ for some equation, $Q$, is called
a {\em $v$-proof of} $Q$.  An equation which has a $v$-proof is called a
{\em $v$-theorem} and is said to be $v$-{\em provable}; we use the notation
$\vdash_{v}\ Q$ to indicate that $Q$ is $v$-provable.
\end{definition}

\problem Sketch how to write a Scheme program computing the verifier for
the arithmetic equation proof system of Handout 3.

\medskip

\begin{theorem}\label{proofs-re}
The set of theorems of any proof system is half-decidable.
\begin{proof}
The range of $v$ is half-decidable by Theorem~\ref{g-closed}, hence so is
$\ran(v) - \set{\Code{\#f}}$; this set is the set of $v$-theorems, by
definition of $v$-theorem.
\end{proof}

\end{theorem}

Recall from Handout 13:
\begin{definition}
Two Scheme bodies are \emph{observationally distinguishable} iff one
evaluates to a printable value, and the other does not evaluate to exactly
that printable value.

Bodies $M$, $N$ are \emph{observationally congruent}, in symbols,
$M \obscong N$, iff there is {\em no} Scheme context, $C$, such that $C[M]$
and $C[N]$ are observationally distinguishable.

An equation \Code{($M$ = $N$)} is {\em valid} iff $M \obscong N$.  As
usual, we use the notation $\models Q$ to mean that equation $Q$ is valid.

\end{definition}

\begin{lemma}\label{spin-cong}
Let $\bnf <spin>$ be a closed nonhalting expression.  For any closed
Scheme expression, $M$,
\[
M \mbox{ does not halt  iff  } \models {\Code{($M$ = $\bnf <spin>$)}}.
\]
\end{lemma}

\problem Prove Lemma~\ref{spin-cong}.  \hint This will take some work.
\medskip


\begin{lemma}\label{closed-halt}
The set of {\em closed} Scheme expressions which do not halt is not a
half-decidable set.
\end{lemma}

\problem Prove Lemma~\ref{closed-halt}.  \hint Either adapt the proof of
Scott's Rice's Second Theorem (cf. Handout 15), or show that if the closed
nonhalting expressions were half-decidable, then \halts\ would be too.

\begin{corollary}\label{vnhd}
The set of valid Scheme equations is not half-decidable.
\begin{proof}
Let $g:\sexp \to \sexp$ be defined by
\[\bnf
g(S) = \left\{
\begin{array}{ll}
M, &\mbox{if $S$ is \Code{($M$ =
        $\bnf <spin>$)} where $M$ is a closed Scheme expression;}\\
        <spin>, &\mbox{otherwise.}
\end{array}
\right.
\]
Let $\mathcal{V}$ be the set of valid Scheme equations, and $\mathcal{N}$
be the set of closed, nonhalting Scheme expressions.  So by definition,
$g(\mathcal{V})= \mathcal{N}$.  Obviously $g$ is computable.  So, if
$\mathcal{V}$ was half-decidable, then by Theorem~\ref{g-closed},
$\mathcal{N}$ would be half-decidable as well, contradicting
Lemma~\ref{closed-halt}.
\end{proof}

\end{corollary}

\begin{definition}
A proof system, $v$, for Scheme equations is {\em sound} iff $\vdash_{v}\
Q$ implies $\models Q$ for all Scheme equations, $Q$.
\end{definition}

\begin{theorem}\label{incompleteness} {\bf Incompleteness}.
For {\em any} sound proof system for Scheme equations, there is a
valid equation which is not provable.

\begin{proof}
By definition of soundness, the provable equations are a subset of the
valid equations.  By Theorems~\ref{proofs-re} and Corollary~\ref{vnhd},
the set of the provable equations and the set of valid equations are not
equal.  So there must be a valid equation which is not provable.
\end{proof}

\end{theorem}

We show in Section~\ref{kleene}, Problem~\ref{get-unprov} how, given a
Scheme expression computing the verifier for a sound proof system, to
explicitly construct an unprovable valid equation.

\section{Computability in Different Programming Languages}

Are more functions computable in Scheme with side-effects than in
functional Scheme?---in Scheme extended with ``parallel'' operators like
\Code{parallel-or} compared to regular ``sequential'' Scheme?--in Fortran
or C compared to any of these versions of Scheme?---compared to register
machines?  Briefly, the answer is ``No'' for the familiar reason that
there is a simulator or compiler for each of these language dialects in
any of the others.

\problem The \Code{smeval} procedure in the course web-page is a
``nearly'' functional interpreter for Scheme with assignments.  If it were
really functional, it would be a demonstration that any function
computable with assignments was already computable in the functional
kernel.

The one place \Code{smeval} uses a nonfunctional feature is with the
procedure \Code{getfresh}, which generates a ``fresh'' new symbol every
time it is applied.  Explain how to modify \Code{smeval} to be a truly
functional Scheme procedure once the kernel is extended with the
\Code{int->sym} procedure identifier.  (This is a tricky programming
problem.)

\section{The Recursion Theorem}\label{kleene}

The undecidability of the halting problem, and more generally Scott's
Rice's Theorems, revealed the impossibility of having an automatic
procedure to detect any important property of expression evaluation.
Another reflection of the general incomprehensibility of Scheme programs
is Kleene's Recursion Theorem.  This time, given any Scheme expression, we
simply try to change it so it will produce a {\em different} result.  This
too is impossible.

\begin{theorem}
{\bf Kleene's Recursion Theorem.}
Let $\mbox{change}: \sexp \to \sexp$ be a Scheme computable
function.  Then there is a Scheme expression, $F$, such that either
\begin{itemize}
\item $\valof{F}$ and $\valof{\mbox{change}(F)}$ are both undefined, or
\item $\valof{F} = \valof{\mbox{change}(F)}$.
\end{itemize}

\begin{proof}
Let $h$ be the partial function on S-expressions such that $h(S) =
\valof{\mbox{change}( \Code{($S$ '$S$)} )}$.  Assuming change is
computable by some Scheme expression, $C$, we observe that $h$ is
computable by the expression:
\[H ::= \Code{(lambda (qs) (\smeval\: ($C$ (list qs (list 'quote qs)))))}\]
where \Code{qs} is a fresh variable.

So for every S-expression, $S$, either
\begin{itemize}
\item $\valof{\Code{($H$ '$S$)}}$ and
$\valof{\mbox{change}( \Code{($S$ '$S$)} )}$ are both undefined, or

\item $\valof{\Code{($H$ '$S$)}} = \valof{\mbox{change}( \Code{($S$ '$S$)} )}$,
\end{itemize}
by definition of $H$ and \smeval.

Letting $S$ be $H$ above, we see that we can define $F$ to be
$\Code{($H$ '$H$)}$.
\end{proof}
\end{theorem}

Let \fix\ be the function mapping the expression $C$ to the expression $F$
in the above proof.  The construction of $F$ from $C$ shows that \fix\ is
a computable, total function from S-expressions to S-expressions, where by
definition
\[
\valof{\fix(C)} = \valof{\mbox{change}(\fix(C))}
\]
whenever either expression has a value.

As a simple application of the Recursion Theorem, let $\mbox{change}(S) =
\Code{(quote $S$)}$.  So the expression $F$ given in the Recursion Theorem
will satisfy $\valof{F} = \valof{\Code{'$F$}}$; in other words, $F$ is
yet another self-reproducing expression.  We can similarly obtain a doubly
self-reproducing expression (cf. Handout 15, problem 1(c)), by letting
$\mbox{change}(S) = \Code{'($S$ $S$)}$.

\problem

\subproblem Assume our kernel Scheme is extended with a rule-defined
procedure identifier \Code{smeval} which is a meta-circular evaluator.
Write out the self-reproducing and doubly self-reproducing expressions
described above.

\subproblem Check that your expressions work by evaluating them in real
Scheme.  (Note that if you use MIT Scheme's builtin \Code{eval} to act as
the rule-defined \Code{smeval}, you must
supply it with a second argument which is an environment; so you should
first evaluate the definition
\[
\Code{(define smeval (lambda (qs) (eval qs user-initial-environment)))} .
\]
Alternatively, you may use the \Code{smeval} procedure from the course
web-page to serve as the evaluator, modified so it {\em returns} a
printable value instead of pretty-printing it.)

\medskip


The Recursion Theorem yields elegant proofs of many results in
computability theory. For example:

\begin{definition}
Let $\mathcal{A}, \mathcal{B}$ be distinct sets of S-expressions.  An
element in the symmetric difference of $\mathcal{A}$ and $\mathcal{B}$ is
called a {\em witness} that $\mathcal{A} \neq \mathcal{B}$, i.e., a witness
is an element, $W$, such that
\[
W \in \mathcal{A} \quad \mbox{iff} \quad W \not\in \mathcal{B}.
\]

For any Scheme expression, $H$, let $\mathcal{W}_{H}$ be the set of
S-expressions for which $H$ is a half-decider.  That is,
\[
\mathcal{W}_{H} ::= \set{S \in \sexp \mid \Code{($H$ '$S$)} \mbox{ halts}}.
\]

A set $\mathcal{A}$ is {\em productive} if there is a total computable
function, $w:\sexp \to \sexp$, such that $w(H)$ is a witness that
$\mathcal{A} \neq \mathcal{W}_{H}$ for all S-expressions, $H$.  The
function $w$ is called a {\em productive function} for $\mathcal{A}$.
\end{definition}

So productive sets are not half-decidable in a notably demonstrable way.

\begin{theorem}\label{productive}
\nothalts\ is productive.

\begin{proof}
Let $\mbox{change}(S) ::= \Code{($H$ '$S$)}$.  By the Recursion Theorem,
there is an $S_{0}$ such that
\[
S_{0} \mbox{ halts} \quad \mbox{iff} \quad \Code{($H$ '$S_{0}$)} \mbox{ halts}.
\]
Hence,
\[
S_{0} \in \nothalts \mbox{ iff } \Code{($H$ '$S_{0}$)} \in \nothalts
\mbox{ iff } S_{0} \not\in \mathcal{W}_{H},
\]
so $S_{0}$ is a witness that $\mathcal{W}_{H} \neq \nothalts$.  Therefore, the
function mapping $H$ to $S_{0}$ is a productive function for \nothalts; it
is computed by the expression
\[\bnf
\Code{(lambda (h) ($\bnf <fix>$ (lambda (s) (list h (list 'quote s)))))}
\]
where $\bnf <fix>$ is a Scheme expression computing \fix.
\end{proof}

\end{theorem}

\problem\label{get-unprov}
Use Theorem~\ref{productive} to prove that there is a total computable
function, unprov, such that if \verifier\ is a Scheme expression computing the
verifier of a sound proof system for Scheme equations, then unprov$(\verifier)$ is
a valid equation which is not a theorem of the proof system.

\medskip

Another elegant example of the use of the Recursion Theorem is due to
Manuel Blum:

\begin{definition}
A set of S-expressions is {\em immune} if it is infinite but contains no
infinite half-decidable subset.
\end{definition}

So not only is there no ``demon'' which detects the elements in an immune
set, but there isn't even a demon which merely detects an infinite number
of sample elements from the set.

\begin{definition}
A Scheme expression, $S$, is called {\em minimal} iff it halts, and there
is no Scheme expression, $T$, such that 
\[
\valof{T} = \valof{S} \mbox{  and  } \sexpint(T) < \sexpint(S).
\]
\end{definition}

\begin{theorem}
The set of minimal Scheme expressions is immune.

\begin{proof}
By Theorem~\ref{bijection}, we need only show that if $\bnf f:\nnintegers \to
\sexp$ is a Scheme computable, total function with infinite range, then
there is some S-expression $S \in \ran(f)$ which is not minimal.  If there
is an expression in $\ran(f)$ which is not a Scheme expression or does not
halt, then that expression is not minimal.  So we may assume that every
expression in $\ran(f)$ is a Scheme expression which halts.

Let $\mbox{change}(S) = f(k)$ where $k$ is the least nonnegative integer
for which $\sexpint(S) < \sexpint(f(k))$.  Since $f$
is computable, so is the function change.  Since $f$ has infinite range,
change is a total function with the properties that
\[
\sexpint(S) < \sexpint(\mbox{change}(S))
\mbox{  and  }
\mbox{change}(S) \in \ran(f),
\]
for every S-expression, $S$.

Let $F$ be the Scheme expression satisfying the Recursion Theorem for the
function change.  Since $\mbox{change}(F) \in \ran(f)$, it is a Scheme
expression that halts.  So by the Recursion Theorem, $\valof{F} =
\valof{\mbox{change}(F)}$.  But since $\sexpint(F) <
\sexpint(\mbox{change}(F))$ by definition of change, we conclude
that $\mbox{change}(F) \in \ran(f)$ is not minimal.
\end{proof}

\end{theorem}

\problem For any total function $g:\nnintegers \to \nnintegers$ and
S-expressions $S, T$, say that $S$ is {\em at most $g$-larger} than $T$
iff $\sexpint(S) \leq g(\sexpint(T))$.  Call a Scheme expression {\em
$g$-minimal} iff it halts and is at most $g$-larger than any other Scheme
expression with the same value. (So the minimal expressions are the same
as the $g$-minimal expressions for $g(n) = n$.)

Show that the set of $g$-minimal Scheme expressions is immune for any
Scheme computable total function $g$ such that $g(n) \geq n$ for all $n
\in \nnintegers$.

\problem Show that for any Scheme computable total function $g:\nnintegers
\to \nnintegers$, there is an S-expression, $S_{g}$, such that
$\sexpint(\valof{S_{g}}) > g(\sexpint(S_{g}))$.

\problem
\subproblem  Explain why the set of non-minimal Scheme expressions which
halt is half-decidable.

\subproblem Call a Scheme expression {\em except-one-minimal\/} iff it halts, and
there is at most one smaller size Scheme expression with the same value.
Show that the set of except-one-minimal Scheme expressions is immune.

\problem Show that for any Scheme computable total function $g:\nnintegers
\to \nnintegers$, there is a finite set $\mathcal{N}_{g}$ of nonnegative
integers, and a half-decider, $H$, for $\mathcal{N}_{g}$, such that
$\sexpint(M) > g(\sexpint(H))$ for any expression,
$M$, computing the {\em membership} function of $\mathcal{N}_{g}$. \hint
Evaluation of \Code{($H$ $n$)} should dovetail the evaluation of
\Code{($S$ $n$)} for all those Scheme expressions, $S$, numbered less than
$g(\sexpint(H))$ which have not already been {\em hit at $k$}
for some $k < n$.  It halts as soon as one of the expressions $\Code{($S$
$n$)}$ halts with the value \Code{\#f}.  This $S$, if any, is said to be
{\em hit at $n$}.


\end{document}
