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

\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{q2}{Quiz 2}{18 November 1996}

\medskip

\problem
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
Give rewrite rules which completely determine the behavior of
\Code{or} according to the above specification.

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

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

\subproblem
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).

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

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

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

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

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

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

\problem
We consider Scheme extended with a $\bnf <primitive procedure id>$,
\Code{int->sym}, which computes a one-to-one total function
\[\bnf
    \inttosym: \mathbb{N} \rightarrow <symbol>.
\]

\subproblem
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 $\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.

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

\end{document}

