\documentclass[11pt]{handout}

\usepackage{alltt}

\usepackage{6044}

\usepackage{amsmath}

\let\proof\relax
\let\endproof\relax

\usepackage{amsthm}

\setlength{\textheight}{8in}
\setlength{\textwidth}{5.5in}
\setlength{\oddsidemargin}{.4in} 
\setlength{\evensidemargin}{0in} 
\parindent0in
\parskip\medskipamount

\newtheorem*{sol}{Solution}

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

\begin{document}
\handout{q2-soln}{Quiz 2 Solutions}{19 November 1996; revised$^{2}$ 24 November}

\medskip

\problem(25)
The Scheme special form \textbf{or} behaves as follows: if $\valof{A}
= \Code{\#f}$, then $\valof{\Code{(or $A$ $B$)}} = \valof{B}$.  If
$\valof{A}$ is not \Code{#f}, then $\valof{\Code{(or $A$ $B$)}} =
\valof{A}$.  (We restrict \Code{or} to having exactly \emph{two}
components, viz., no \Code{(or $A$ $B$ $C$)}.)

\subproblem(7)
Give rewrite rules which completely determine the behavior of
\Code{or} according to the above specification.

\begin{sol}

\begin{align*}
\Code{(or \#f $M$)} &\rulesto M\\
\Code{(or $V$ $M$)} &\rulesto V
\end{align*}
if $V$ is an immediate value not equal to \Code{#f}.

\end{sol}

\subproblem(6)
Give a simple example expression, $A$, which shows why \Code{(or $A$
'dummy)} cannot be regarded as sugar for \Code{(if $A$ $A$ 'dummy)}.

\begin{sol}

Let $A$ be \Code{(counter)}.  Then the context
\begin{lisp}
(define counter
   (let ((init 0))
      (lambda () (set! init (+ init 1))
                 init)))
[ ]
\end{lisp}
distinguishes \Code{(or $A$ 'dummy)}, which returns~1 in this context,
from \Code{(if $A$ $A$ 'dummy)}, which returns~2.

\end{sol}

\subproblem(6)
Show that, nevertheless, \Code{or} can be regarded as sugar.

\begin{sol}

\Code{(or $A$ $B$)} desugars to
\begin{alltt}
    (let ((val-a \(A\)))
        (if val-a val-a \(B\)))
\end{alltt}
where \Code{val-a} is a ``fresh'' variable, specifically a variable which
does not occur in $B$.\footnote{The need for a fresh variable can be
avoided by the slightly trickier desugaring
\begin{alltt}
    (let ((val-a \(A\))
          (thunk-b (lambda () \(B\))))
        (if val-a val-a (thunk-b)))
\end{alltt}}
\end{sol}

\subproblem(6)
Modify the definition of \emph{control context} (Handout~14, p.~6) to
handle the \Code{or} special form, and carefully define an
\Code{or}-evaluation redex (cf.\ Handout~14, p.~6).

\begin{sol}

\[\begin{bnf}
<control\ context>  ::= \dots | \Code{(or $<control\ context>\: <expression>$)}
\end{bnf}\]

An \Code{or}-evaluation redex is $E[T]$ where $E$ is an evaluation context
and $T$ is an \Code{or}-trigger, viz., an expression matching the lefthand
sides of the rules in~1(a).

\end{sol}

\problem(25)
Let
\[
\mathcal{H}_0 ::= \{\, M \mid \text{$M$ is a Scheme expression
and
\Code{($M$ `$M$)} halts}\,\}.
\]

\subproblem(8)
Explain why Scott's Rice's Theorems do \emph{not} directly imply that
$\mathcal{H}_0$ is undecidable.

\begin{sol}

$\mathcal{H}_0$ is not evaluation invariant, e.g., let $M$ be
\begin{lisp}
    (begin (lambda (qn)
                (if (eq? (car qn) 'begin)
                    #t
                    <spin>)))
\end{lisp}
\Code{($M$ '$M$)} halts so $M \in \mathcal{H}_0$, but $\valof{M} =
\Code{($\lambda$(qn) $\cdots$)}$, call this~$P$, so \Code{($P$ '$P$)}
does not halt, and therefore $P \notin \mathcal{H}_0$.

\end{sol}

\subproblem(10)
Prove that $\overline{\mathcal{H}}_0$ is not half-decidable (that is,
not r.e.).

\begin{sol}

Suppose $H_c$ was a half-decider for $\overline{\mathcal{H}}_0$, so
for all Scheme expressions, $M$,
\[ \Code{($H_c$ '$M$)} \mbox{ halts iff } M \notin \mathcal{H}_0 \mbox{
iff } \Code{($M$ '$M$)} \mbox{ does not halt.}
\]

Letting $M$ be $H_c$ yields an immediate contradiction.

\end{sol}

\subproblem(7)
Explain why $\mathcal{H}_0$ is half-decidable.

\begin{sol}\leavevmode

\begin{alltt}
    (\(\lambda\)(qn)
        (smeval
            (list qn (list 'quote qn))))
\end{alltt}
is a half-decider for $\mathcal{H}_0$.

\end{sol}

\problem(25)
Let $\mathcal{H}_0$ be as in Problem~2, and let
\[
    \mathcal{N} ::= \{\, \Code{(0 $S$)} \mid S \in \mathcal{H}_0 \}
    \union
                    \{\, \Code{(1 $S$)} \mid S \notin \mathcal{H}_0 \}    
\]
where $S$ ranges over $S$-expressions.

\subproblem(15)
Suppose $N$ was a Scheme expression which was a half-decider
for~$\mathcal{N}$.  Fill in the expressions \textcircled{1}, \textcircled{2}
below so that the following expression is a decider for
$\mathcal{H}_0$:
\begin{alltt}
\newsavebox{\ebox}\savebox{\ebox}{(list '\(N\) \textcircled{1})}
(lambda (qs)
    (define (try n)
        (cond ( (<\textrm{step-smeval}> \copy\ebox\ n) \#t)
              ( (<\textrm{step-smeval}> \makebox[\wd\ebox][c]{\textcircled{2}} n) \#f)
              (else (try (+ n 1)))))
    (try 0))
\end{alltt}

\begin{sol}
For the expression \textcircled{1}, suppose
\[
\valof{\Code{qs}} = \valof{\Code{'$S$}}.
\]

We want to apply the metacircular interpreter to a quoted expression for
the application of $N$ to \Code{'(0 $S$)}.  Remembering that \Code{'$L$}
abbreviates \Code{(quote $L$)}, we want to apply the metacircular
interpreter to
\[
\Code{'($N$ (quote (0 $S$)))}.
\]
Desugaring the outer quote we get
\[
\Code{(list '$N$ (list 'quote (list 0 '$S$))}.
\]

So expression \textcircled{1} is 
\[
\Code{(list 'quote (list 0 qs))}.
\]

Similarly, expression \textcircled{2} is
\[
\Code{(list '$N$ (list 'quote (list 1 qs))}.
\]

\end{sol}

\subproblem(10)
Explain why neither $\mathcal{N}$ nor $\overline{\mathcal{N}}$ is
half-decidable.

\begin{sol}

If there were a half-decider for~$\mathcal{N}$, part~(a) implies
$\mathcal{H}_0$ would be decidable, which it isn't.  Therefore
$\mathcal{N}$ is not half-decidable.  A symmetric argument shows that
a half-decider of~$\overline{\mathcal{N}}_0$ would yield a decider
for~$\overline{\mathcal{H}}_0$, but $\overline{\mathcal{H}}_0$ is not
decidable either.

\end{sol}

\problem(25)
We consider Scheme extended with
\[\bnf
<primitive procedure id> ::= \dots \alt \Code{int->sym}
\]
where \Code{int->sym} computes a one-to-one total function
\[\bnf
    \inttosym: \mathbb{N} \rightarrow <symbol>.
n\]

\subproblem(20)
Let $M$ be a closed Scheme expression which computes a partial
function $f: \mathbb{Z} \to \mathbb{Z}$.  Sketch how to transform
$M$ into an expression $M'$ such that
\begin{enumerate}

\item
$M'$ also computes $f$,

\item
$M'$ does not contain any symbols,

\item
$M'$ does not contain any occurrence of \Code{int->sym}.

\end{enumerate}

Hint: Represent $\inttosym(n)$ by (the numeral for) $\pair(0, n)$, where
$\pair$ is an integer pairing function.  You may assume $\pair: \mathbb{Z}
\times \mathbb{Z} \to \mathbb{Z}$ is total, computable, and one-to-one.

\begin{sol}

$M'$ will use the number $\pair(0, n)$ to represent $\inttosym(n)$.  To
avoid confusing numbers that represent symbols with numbers that are
numbers, it must represent numbers in some distinguishable way, say, using
the numeral for $\pair(1, n)$ to represent the number~$n$.  (Saying just
this much was worth 16/20 points.)

Now construct $M'$ as follows: replace all numerals, $\hat{n}$ in~$M$,
by $\widehat{\pair(1, n)}$ and symbols $\bnf \Code{'$<name>$}$ by
$\widehat{\pair(0, n)}$ where $\bnf \inttosym(n) = \Code{'$<name>$}$.

We also must replace occurrences of procedure identifiers operating on
numbers or symbols so they work instead on representations of numbers and
symbols.  For example, the procedure identifiers \Code{symbol?} and
\Code{integer?} are replaced by variables (which we presume are fresh)
\Code{rep-symbol?} and \Code{rep-integer?}, which we define as follows;
\begin{lisp}
(define (rep-symbol? n)
  (and (integer? n)
       (= (first n) 0)))

(define (rep-integer? n)
  (and (integer? n)
       (= (first n) 1)))

\end{lisp}

The only other procedure identifiers specifically for symbols are
\Code{eq?} and \Code{int->sym}.  These we replace by variables
\Code{rep-eq?} and \Code{rep-int->sym} with definitions
\begin{lisp}
(define (make-nth-symbol n) (pair 0 n))

(define (make-int-rep n) (pair 1 n))

(define (unrep-int intrep) (second intrep))

(define (number-of-symbol symrep) (second symrep))

(define (rep-eq? symrep1 symrep2)
  (if (and (rep-symbol? symrep1)
           (rep-symbol? symrep2))
      (= (number-of-symbol symrep1)
         (number-of-symbol symrep2))
      (+ +)))                              ;error
  

(define (rep-int->sym intrep)
  (if (rep-integer? intrep)
      (make-nth-symbol (unrep-int intrep))
      (+ +)))                              ;error

\end{lisp}

Also, all integer primitive procedure identifiers must be replaced by
procedures that work on integer representations. For example, we replace
\Code{=} and \Code{*} by \Code{rep-=} and \Code{rep-*} with definitions

\begin{lisp}
(define (rep-= intrep1 intrep2)
   (if (and (rep-integer? intrep1)
            (rep-integer? intrep2))
       (= (unrep-int intrep1)
          (unrep-int intrep2))
       (+ +)))                 ;error

(define (rep-* intrep1 intrep2)
   (if (and (rep-integer? intrep1)
            (rep-integer? intrep2))
       (make-int-rep (* (unrep-int intrep1)
                        (unrep-int intrep2)))
       (+ +)))                 ;error
\end{lisp}

{\em Quibble}: We assume here that the arithmetic operators like \Code{*}
are binary, i.e., take only two arguments.

Finally, let $M_{0}$ be the result of all the above replacements, and define
$M'$ to be:

\begin{quotation}
\begin{alltt}
(lambda (n) (unrep-int (\(M\sb{0}\) (make-int-rep n)))
\end{alltt}
\end{quotation}

\end{sol}

\subproblem(5)
Conclude that the set of $f: \mathbb{Z} \to \mathbb{Z}$ computable in
Scheme extended with a one-to-one \Code{int->sym} is the same as the
set of $f: \mathbb{Z} \to \mathbb{Z}$ computable in Scheme
\emph{without} \Code{int->sym}.

\begin{sol}

Any $f$ computed by $M$ with \Code{int->sym} is computed by $M'$
without \Code{int->sym}, so having \Code{int->sym} leads to no new
computable functions from \integers\ to \integers.

\end{sol}

\end{document}

