\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}

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

\newcommand{\obscong}{\fortext{\:\cong\:}}

\makeatletter

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


\begin{document}
\handout{computability}{Scheme Computability}{1 November 1996; revised 3
\& 6 November}

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.  In functional
Scheme, at least, it is natural to think of procedures as computing
functions, since a (closed) functional procedure always returns the same
value every time it is applied to the same arguments.  But if we try to
pin down the domains and ranges of general Scheme procedures, we know that
we come up against some challenging mathematical problems because of
Scheme's self-applicative values.  To avoid such difficulties, we begin by
considering functions of one argument on the {\em integers}\footnote{We
don't even want to use Scheme numbers which are not integers, e.g., in MIT
Scheme, \Code{(= 1 1.0000000000000001)} returns \Code{\#t}.}.

\begin{definition}
For any integer, $n$, let $\widehat{n}$ be its Scheme numeral.  For example,
$\widehat{23}$ is \Code{23}.
A partial function $f:\integers \to \integers$ is {\em Scheme computable}
iff there is a Scheme expression $F$ such that
\begin{itemize}
\item $\valof{\Code{($F$ $\widehat{n}$)}}$ is defined iff $n \in \dom(f)$, and
\item $\valof{\Code{($F$ $\widehat{n}$)}} = \widehat{f(n)}$ for all $n \in \dom(f)$.
\end{itemize}
Such an expression $F$ is said to {\em compute} the function $f$.
\end{definition}

For example, the function $f(n) = n^{2}$ is Scheme computable because the
expression
\[
    \Code{(lambda (n) (* n n))}
\]
computes it.  Likewise, the function
$t(n)$ which equals a ``stack'' of exponentiated two's of height $n$,
e.g., $t(1) = 2, t(2) = 2^{2}, t(3) = 2^{2^{2}}, \dots$ is computed by the
expression
\begin{lisp}
(lambda (n)
  (define (compose f g)
    (lambda (n) (f (g n))))
  (define (repeatedly-compose f)
    (lambda (k)
      (if (<= k 1) f (compose f ( (repeatedly-compose f) (- k 1) )))))
  (let ((double (lambda (m) (* 2 m))))
    (let ((2-to-the (lambda (n)
                      ( ( (repeatedly-compose double) n ) 1 ))))
      ( ( (repeatedly-compose 2-to-the) n ) 1 ))))
\end{lisp}

In fact, the definition of \Code{compose} above shows that Scheme
computable integer-valued functions one argument are {\em closed under
composition}.  That is, if $f, g$ are Scheme computable functions from
integers to integers, then so is their composition $f \circ g$.  In fact, we
can see that the Scheme computable functions have an endless number of
other closure properties---basically any way of combining functions which
is programmable in Scheme.

It should be clear that the Scheme computable integer-valued functions are
a huge class of functions, containing all the familiar number-theoretic
functions, and indeed all the integer-valued functions anyone outside the
theory computability is likely to think of.  Nevertheless, we will soon
see some clearly defined functions which are {\em not} Scheme computable.

Computability theory is traditionally developed using functions on the
integers as above.  In our setting with Scheme, it is convenient, natural,
and unproblematical to consider computability over the set of {\em
printable values}.  These are Scheme expressions specified by the grammar:
\begin{bnf}
\begin{eqnarray*}
\prv &::=& \pval | "(cons"\: \prv\: \prv")"\\
\pval &::=&  <integer> | <boolean> | <symbol> | "()"\\
<symbol>        &::=& "(quote"\: \vrbl")" | "(quote"\: \pridfr")"\\
        && {}  | "(quote"\: <keyword>")"\\
\end{eqnarray*}
\end{bnf}

\problem

Let $V_{0}$ be some Scheme value.  A $V_{0}$-{\em detector} is a Scheme
expression, $D$, such that $\valof{\Code{($D$ $E$)}} = \Code{\#t}$, for any
Scheme expression, $E$, such that $\valof{E}=V_{0}$, and
$\valof{\Code{($D$ $E$)}} = \Code{\#f}$ for any $E$ such that $\valof{E}$
is defined and is not syntactically {\em identical} to $V_{0}$.

\subproblem

Show that every printable value has a detector.

\subproblem

Show that no Scheme value which is not a printable value has a detector.
\hint You may use the following facts about observational congruence,
\obscong, for Scheme with side-effects:
\[
\Code{(lambda (l) (apply $P$ l))} \obscong P
\]
for all procedure identifiers, $P$.
\[
\Code{((lambda ($x$) $E[x]$) $M$)} \obscong E'[M]
\]
for all evaluation contexts $E, E'$, variables $x$, and expressions $M$
such that the occurrence of $x$ at the hole in $E$ is free and $E'$ is a
fresh renaming of $E$.

\medskip

Printable values are traditionally printed out by Scheme implementations
without the \Code{cons}'s, \Code{quote}'s on symbols, or nil's at the end
of lists.  For example, the printable value
\[
    \Code{(cons \#f (cons (cons 1 (cons 2 ())) (cons (quote a) ())))}
        \qquad\mbox{(*)}
\]
would print out as
\[
\Code{(\#f (1 2) a)}.
\]
Such parenthesized output expressions are called {\em S-expressions}; they
are defined by a simple grammar:
\begin{bnf}
\begin{eqnarray*}
\sexp &::=& \idfr | "("\sexp^*")"
\end{eqnarray*}
\end{bnf}

Scheme provides a standard way, namely \Code{quote}'ing, to convert an
S-expression into the printable-value which would produce it as output.
For example, \Code{(quote (\#f (1 2) a))} is a legitimate Scheme expression,
whose value will be the printable value (*) above.

In our substitution model for Scheme, we treat the \Code{quote} of an
S-expression as sugar.  First, we extend Scheme grammar:
\begin{bnf}
\begin{eqnarray*}
<derived expression> &::=& \dots | <quoted>\\
<quoted> &::=& "(quote"\: \sexp")"
\end{eqnarray*}
\end{bnf}
Next, we describe how to desugar quoted S-expressions into printable
values, namely:
\begin{itemize}
\item If $V$ is an $\bnf <integer>, <boolean>$, or \Code{()}, then (quote
$V$) desugars to $V$.

\item If \Code{(quote $V$)} is a symbol, then \Code{(quote $V$)} desugars
to itself.

\item \Code{(quote ($\idfr_{1}\dots \idfr_{n}$))} desugars recursively to
\[\Code{(cons (quote \idfr_{1}) (quote (\idfr_{2}\dots \idfr_{n}))}.\]
\end{itemize}
The Scheme expression \Code{(quote $S$)} is traditionally abbreviated as
\Code{'$S$}.

These definitions ensure that \Code{'$S$} desugars into a printable value
which traditional implementations would print out as ``$S$.''  Now it is
easy to define computable functions on S-expressions:

\begin{definition}
A partial function $f:\sexp \to \sexp$ is {\em Scheme computable}
iff there is a Scheme expression $F$ such that
\begin{itemize}
\item $\valof{\Code{($F$ '$S$)}}$ is defined iff $S \in \dom(f)$, and
\item $\valof{\Code{($F$ '$S$)}} = \valof{\Code{'}f(S)}$
for all $S \in \dom(f)$.
\end{itemize}
Such an expression $F$ is said to {\em compute} the function $f$.
\end{definition}

For practice with quoting and 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 $\valof{R} = \valof{\Code{'$R$}}$.  So in real
Scheme, evaluation of $R$ would yield output ``$R$''!

Here's a way to make one: let \Code{make-self-apply} be an expression such
that
\[\valof{\Code{(make-self-apply '$S$)}} = \valof{\Code{'($S$ '$S$)}}.\]
For example, we could use the Scheme definition:
\begin{lisp}
(define (make-self-apply qs) (list qs (list 'quote qs)))
\end{lisp}
Then if we evaluated \Code{(make-self-apply 'make-self-apply)} in Scheme,
we would get the output \Code{(make-self-apply 'make-self-apply)}!

This is very nearly self-reproducing, but it hinges on the prior
definition of \Code{make-self-apply}.  To get an entirely self-contained
self-reproducing expression, we incorporate the definition into the
expression.  Let, \perverse\ be the expression
\begin{lisp}
( (lambda ()
    (define (make-self-apply qs)
      (list qs (list 'quote qs)))
    make-self-apply) )
\end{lisp}
Now we have that, even with no prior definitions,
\[
\valof{\Code{(\perverse\ '$S$)}} = \valof{\Code{'($S$ '$S$)}},
\qquad\qquad \mbox{(**)}
\]
for all S-expressions $S$.  Let $R$ be \Code{(\perverse\ '\perverse)} to
obtain a really self-reproducing expression.

\problem

\subproblem Check that this last $R$ is self-reproducing by evaluating it
in real Scheme.  (Use \Code{pp} or \Code{pretty-print} so the output is
readable.)

\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 \perverse\ looks like as long as it satisfies the
specification (**).

\subproblem An expression $D$ is {\em doubly self-reproducing} iff
$\valof{R} = \valof{\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}$ of S-expressions is {\em evaluation-invariant} if
$S_{1} \eval1 S_{2}$ implies that $S_1 \in \mathcal{S} \iff S_2 \in
\mathcal{S}$ for all S-expressions $S_1$, $S_2$.

${\mathcal S}$ is {\em non-trivial} iff ${\mathcal S}$ is nonempty and
does not contain all S-expressions.

Two sets $\mathcal{A}$, $\mathcal{B}$ of S-expressions are {\em computably
inseparable} iff there is no Scheme expression, \separator, with the
following three properties:
\begin{enumerate}
\item
If $A \in \mathcal{A}$, then $\valof{\Code{(\separator\ `$A$)}} =
\Code{\#t}$.

\item\label{b-sep} If $B \in \mathcal{B}$, then $\valof{\Code{(\separator\
`$B$)}} = \Code{\#f}$.

\item\label{return-truth} For all S-expressions, $S$,
$\valof{\Code{(\separator\ `$S$)}}$ is defined and equals either
\Code{\#t} or \Code{\#f}.
\end{enumerate}

\end{definition}

\begin{theorem*} {\bf Scott's Rice's First Theorem.}
Let $\mathcal{A}$, $\mathcal{B}$ be nontrivial, evaluation-invariant sets
of S-expressions.  Then $\mathcal{A}$ and $\mathcal{B}$ are computably
inseparable.

\begin{proof}

By contradiction.  Suppose there was a \separator\ expression as above.
Since $\mathcal{A}$ and $\mathcal{B}$ are nontrivial, there are
S-expressions $A_{0} \in \mathcal{A}$ and $B_0 \in \mathcal{B}$.

Let \Code{pv} be a variable not free in \separator, $A_{0}$ or $B_{0}$,
and define \perverse\ to be the Scheme expression:
\[\begin{array}{l}
\Code{(lambda(pv)}\\
\Code{\ \ (if (\separator\ (list pv (list `quote pv)))}\\
\Code{\ \ \ \ \ \ $B_0$}\\
\Code{\ \ \ \ \ \ $A_0$))}.
\end{array}\]
Suppose $\valof{\Code{(\separator\ '($S$ '$S$))}} = \Code{\#t}$ for some
S-expression $S$.  Then by definition of \perverse\ above,
$\Code{(\perverse\: '$S$)} \evalss B_0$.  So by
evaluation-invariance, $\Code{(\perverse\: '$S$)} \in \mathcal{B}$.
Finally, by \separator-condition~\ref{b-sep}, $\valof{\Code{(\separator\
'(\perverse\: '$S$))}} = \Code{\#f}$.

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

Now let $S$ be \perverse\ and $C$ be \Code{(\perverse\ '\perverse)}.
Then the equivalence above instantiates to
\[\valof{\Code{(\separator\ '$C$)}} = \Code{\#t}
\ \iff\ 
\valof{\Code{(\separator\ '$C$)}} = \Code{\#f}.
\]
which contradicts \separator-condition~\ref{return-truth}.
\end{proof}

\end{theorem*}

\begin{definition}
For any set $\mathcal{S}$ of S-expressions, define the {\em complement} of
$\mathcal{S}$, in symbols, $\overline{\mathcal{S}}$, to be the
set-theoretic complement of $\mathcal{S}$ relative to the set of
S-expressions.  In other words, $\overline{\mathcal{S}}$ is the set of
S-expressions {\em not} in $\mathcal{S}$.  The set $\mathcal{S}$ is Scheme
{\em decidable} iff its membership function is Scheme computable, i.e.,
there is a Scheme expression, $D$, such that $\valof{\Code{($D$ '$S$)}} =
\Code{\#t}$ for $S \in \mathcal{S}$, and $\valof{\Code{($D$ '$S$)}} =
\Code{\#f}$ for $S \in \overline{\mathcal{S}}$.
\end{definition}

\begin{corollary}
The set
\[
\halts ::= \{\, S \in \sexp \mid S\mbox{ is a Scheme expression and }
\valof{S} \mbox{ is defined}\,\}.
\]
is not Scheme decidable.
\end{corollary}
\begin{proof}
If it were, the expression computing its membership function would be a
separator for the set $\mathcal{A} = \halts$ and $\mathcal{B} =
\mathcal{\overline{\halts}}$.
\end{proof}

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

\begin{theorem*} {\bf Scott's Rice's Second Theorem.}
Let $\mathcal{S}$ be a non-trivial, evaluation-invariant set of
S-expressions containing all the non-halting Scheme expressions.  Then
$\mathcal{S}$ is not half-decidable.
\end{theorem*}

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

\begin{corollary}
The set 
\[\nothalts ::= \{\, S \in \sexp \mid S\mbox{ is a Scheme expression and }
\valof{S}\mbox{ is not defined}\,\}
\]
is not half-decidable.
\end{corollary}


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

These two theorems reveal that there is {\em no} property of Scheme
expressions depending only on how they evaluate, that can be detected in
an {\em automatic}, completely reliable, way.  Of course, just as there is
no single unprovable theorem, there is no single program which cannot be
demonstrated to have some particular property.  But any {\em procedure}
that tries to detect a non-trivial, evaluation-invariant property must
give a wrong answer, or fail to give a required answer, for {\em some}
input expression.

\problem
\subproblem
Show that if $\mathcal{S}_{1}$ is half-decidable, and
\[\mathcal{S}_2 = (\mathcal{S}_{1} - \mathcal{F}_1) \union \mathcal{F}_{2}\]
for some finite sets $\mathcal{F}_{1}, \mathcal{F}_{2}$, then
$\mathcal{S}_2$ is half-decidable.

\subproblem Conclude that any Scheme procedure which tries to decide
whether expressions have a non-trivial, evaluation-invariant property
must, give wrong answers, or fail to give an answer when it should, for an
{\em infinite number} of input expressions.


\end{document}

