\documentclass{handout}
\usepackage{6044}
%\documentclass[11pt]{article}
%\usepackage{6001}
\usepackage{time,fullpage}
\usepackage{amsmath}

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



%\newcommand{\byrule}[1]{\mathbin{\mathop{\rulesto}\limits_{\rm #1}}}
%\newcommand{\subst}[3]{#1[#2 := #3]}
%\newcommand{\patch}[3]{#1[#2 \leftarrow #3]}
\newcommand{\rneq}[2]{#1 =_{\hbox{\scriptsize fresh}}#2}

\begin{document}
\handout{ps6}{Problem Set 6}{4 November 1998}

\due Friday, 13 November.

\medskip


\problem

Let $E_1$ be a kernel Scheme expression satisfying the Variable Convention
(VC) defined in \texttt{sm.scm}.  Suppose $E_1$ rewrites by one
Substitution Model rule application into $E_2$.  For most of the rewrite
rules, $E_2$ will still satisfy the VC, but for a few of the rules (you
can find them listed in \texttt{sm.scm}), it will not.  For each of these
rules. give a simple example of $E_1$ satisfying the VC which rewrites to
$E_2$ which does not satisfy the VC.


\problem The definition of \texttt{crules:eq?} in the file
\texttt{sm.scm} has a regrettable property: it allows the substitution
model to return \texttt{\#t} as the value of
\begin{lisp}
(eq? (lambda (x) x) (lambda (x_0) x_0))
\end{lisp}
but \texttt{\#f} as the value of
\begin{lisp}
(eq? (lambda (x) x) (lambda (y) y))
\end{lisp}
This violates an important ``black box'' principal of Scheme, that
printable values of Scheme expressions are invariant under renaming of
bound variables to ``fresh'' variables.

Define a procedure
\[\begin{bnf}
\texttt{canonical-bound-vars}: <Scheme expression> \longrightarrow <Scheme expression>
\end{bnf}
\]
so that this problem with \texttt{eq?} is repaired simply by editing
\texttt{crules:eq?} to call \texttt{canonical-bound-vars} instead of the
\texttt{clean-suffixes} procedure it currrently calls.

\problem Scheme expressions \emph{E} and \emph{F} are said to be
\emph{renaming equivalent}\footnote{In the programming theory literature,
``renaming equivalence'' is often called ``$\alpha$-equivalence,'' written
$=_\alpha$.}, written as,
\[\rneq{E}{F},\]
if they can be tranformed into the same expression by some fresh renaming
of their bound variables.  (That is, the same expression is returned
by \Code{(canonical-bound-vars '\hbox{\emph{E}})} and
\Code{(canonical-bound-vars '\hbox{\emph{F}})}.)

Suppose $E_1$ is a kernel Scheme expression satisfying the VC, and $E_1$
rewrites by one Substitution Model rule application (with the revised
\texttt{crules:eq?}) into $E_2$.  Then, if $\rneq{E_1}{F_1}$ and $F_1$ also
satisfies the VC, it turns out that that $F_1$ must rewrite by one
substitution model rule application into some $F_2$ such that
$\rneq{E_2}{F_2}$.

\subproblem Carefully explain why this property -- that renaming
equivalence of expressions satisfying the VC is preserved by a
Substitution Model rule application -- holds in the particular case that
$E_2$ is obtained from $E_1$ by \texttt{rule:instantiate}.

\subproblem Give a counterexample of $E_1, F_1$ showing that even if $E_1$
satisfies the VC, the hypothesis used above that $F_1$ also satisfies the
VC cannot be relaxed.

\subproblem Conclude that if $\rneq{E_1}{F_1}$, and evaluating $E_1$
returns a printable value, then evaluating $F_1$ (starting in the same
global environment) returns the same printable value.

\problem A set ${\cal R} \subseteq \integers^n$ of $n$-tuples of integers
is said to be a \emph{Diophantine root set} iff there a Diophantine
polynomial, $p$, of $n$ variables such that ${\cal R}$ is the set of roots
of $p$.  A set ${\cal D} \subseteq \integers^m$ is said to be a
Diophantine set if it is the projection on the first $m$ coordinates of
some Diophantine root set.  (That is, ${\cal D} = \set{(k_1,\dots,k_m)
\mid (k_1,\dots,k_m,\dots) \in {\cal R}}$ for some Diophantine root set
${\cal R}$.)

\subproblem Show that the range of any Diophantine polynomial is a
Diophantine set.

\subproblem Let $p(x_1,\dots,x_n)$ be a Diophantine polynomial and ${\cal
D}$ the Diophantine set which is the projection on the first coordinate of
the root set of $p$.  Define
\[f(x_1,\dots,x_n) := (x_1 + 1)(1 - p(x_1,\dots,x_n)^2) - 1.\]
Prove that ${\cal D} \intersect \Int = \ran{f} \intersect \Int$.

\end{document}
