\documentclass{article} 
\usepackage{amsmath}
\usepackage{611}

\newcommand{\homework}{2}      %%% Replace ? by homework number
\newcommand{\due}{10/01/01}    %%% Due date in MM/DD/YY format
\begin{document}
\hwheader

\section*{What to turn in}

Turn in the assignment during class on the due date.

\begin{enumerate}

\newlength{\howlong}
\newcommand{\strikeout}[1]{
\settowidth{\howlong}{#1}%
#1\unitlength0.5ex%
\begin{picture}(0,0)
\put(0,1){\line(-1,0){\howlong\divide\unitlength}}
\end{picture}%
}

\newcommand{\FOR}{\mbox{\bf for}}
\newcommand{\TO}{\mbox{\bf to}}

\item "Proofs by induction" (25 pts.)\\
Consider a version of IMP that has \FOR\ loops instead of \WHILE\ loops.
We redefine commands $c$ as follows:
\[
c ::= \SKIP \mid x := a \mid \IF~b~\THEN~c_0~\ELSE~c_1 \mid c_0;~c_1
	    \mid \FOR~x= a_0~\TO~a_1~\DO~c
\]
Let us suppose that the large-step semantics are unchanged except that
we substitute the following \FOR\ rules for the \WHILE\ rules:

\[
\infer  [\mbox{where }n_0~\gt~n_1]
        {<\FOR~x = a_0~\TO~a_1~\DO~c, \sigma> \stepsto \sigma}
	{<a_0, \sigma> \stepsto n_0 & <a_1, \sigma> \stepsto n_1}
\]
\[
\infer [\mbox{where }n_0~\le~n_1]
        {<\FOR~x = a_0~\TO~a_1~\DO~c, \sigma> \stepsto \sigma'}
	{<a_0, \sigma> \stepsto n_0 & <a_1, \sigma> \stepsto n_1 &
	 <\FOR~x = n_0~\TO~n_1~\DO~c,\sigma> \stepsto \sigma'}
\]
\[
\infer  [\mbox{where }n_0~\le~n_1 \wedge n'_0 = n_0 + 1]
        {<\FOR~x = n_0~\TO~n_1~\DO~c, \sigma> \stepsto \sigma'}
	{ <c;~\FOR~x = n'_0~\TO~n_1~\DO~c, \sigma[x \mapsto n_0]>
	    \stepsto \sigma'}
\]
Informally, the bounds of the loop are computed once, at the beginning
of the loop, and although the loop index variable can be assigned within
the loop, these assignments do not affect the value of the variable at the
beginning of the next loop iteration.

\begin{enumerate}
\item Write a program in this language that, given an input number in the
variable $n$, outputs the $n$th prime number in the variable $x$.

\item Define a series of programs $P_1, P_2, P_3, \ldots$ such that the length
of program $P_n$ is polynomial in $n$ but the running times of the programs
grow faster than any exponential in $n$.

\item
Despite the fact that we can write many useful programs in this language---it
can compute the _primitive recursive functions_---the language is not universal.
Show that it is not universal by demonstrating that all programs terminate.
(_Hint:_ Use well-founded induction, but make sure you show your well-founded
relation is indeed well-founded!)
\end{enumerate}

\item "Free and bound variables" (10 pts.)\\
Identify the free and bound variables in each of the following expressions:
\begin{enumerate}
\item $(\lambda ("x"~"y"~"z")~"z"~"x"~"y")$
\item $(\lambda ("x"~"y") ~(\lambda "z"~("z"~"y"))~(\lambda "x"~("z"~"x")))$	
\item $((\lambda ("x"~"y")~"y")~"x")$
\end{enumerate}

We defined substitution into a lambda term using the following three rules:
\begin{eqnarray*}
(\lambda x~e_0)\{e_1/x\} & = & (\lambda x~e_0) \\
(\lambda y~e_0)\{e_1/x\} & = & (\lambda y~e_0\{e_1/x\})
 \qquad (\mbox{where}~y\neq x\wedge y\not\in\nm{FV}\SB{e_1}) \\
(\lambda y~e_0)\{e_1/x\} & = & (\lambda y'~e_0\{y'/y\}\{e_1/x\})
 \qquad (\mbox{where}~y'\neq x \wedge
    y'\not\in\nm{FV}\SB{e_0} \wedge
    y'\not\in\nm{FV}\SB{e_1} )
\end{eqnarray*}
\begin{enumerate}
\setcounter{enumii}{3}
\item In these rules, we note a number of conjuncts in the
side-conditions whose purpose is perhaps not immediately apparent. Show
by counterexample that each of the conjuncts above is independently
necessary.
\end{enumerate}

% \item "Alpha equivalence"
% 
% 
% \item Show that 
% \item 
% The third rule might appear to supersede the second. Show that 

\item "Fixed Point Combinator" (10 pts.)\\
In class we have seen a fixed point operator \nm{Y}, which has the property
$\nm Y\/ f=f(\nm Y\/ f)$. This is not the only fixed point operator. Prove that the
combinator \nm{B} defined as the following is also a fixed pointer operator.
\begin{align*}
\nm{A} & \equiv \lambda ("a~b~c~d~e~f~g~h~i~j~k~l~m~n~o~p~q~s~t~u~v~w~x~y~z~r")~"r"("t~h~i~s~i~s~a~f~i~x~e~d~p~o~i~n~t~c~o~m~b~i~n~a~t~o~r")\\
\nm{B} & \equiv "A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A~A"
\end{align*}

\item "Encodings" (25 pts.)\\
We have seen in class one way to represent natural numbers in the
$\lambda$-calculus.  However, there are many other ways to encode numbers in
$\lambda$-calculus.  Consider the following definitions:
\begin {align*}
"TRUE"  & \equiv \lambda ("x"~"y")~"x"\\
"FALSE" & \equiv \lambda ("x"~"y")~"y"\\
0       & \equiv \lambda "x"~"x"\\
n+1     & \equiv \lambda "x"~("x"~"FALSE")~n
\end {align*}

\begin{enumerate}
\item
Show how to write the "DEC" (decrement by one) operation for this number
representation.  Reduce $("DEC"~("DEC"~2))$ to its $\beta\eta$ normal form,
which should be the representation of $0$, above.

\item
Show how to write a $\lambda$-term "ZERO?" that determines whether a number is
zero or not.  It should return "TRUE" when the number is zero, and "FALSE"
otherwise.  Use the definitions of "TRUE" and "FALSE" given above.
\item
Show how to write the "ADD" and "MULT" operations for this number
representation. 
\end{enumerate}


\item "The S and K Combinators" (30 pts.)\\
Consider the following definitions of the \nm S and \nm K combinators:
\begin{align*}
\nm S & \equiv \lambda("x"~"y"~"z")~(("x"~"z")~("y"~"z"))\\
\nm K & \equiv \lambda("x"~"y")~"x"
\end{align*}
\noindent Any $\lambda$-calculus expression
without free variables can be written using only applications
of the \nm S and \nm K combinators; thus,
the $\lambda$-calculus can be universal with only three distinct
identifier names, since both combinators use no more than
three identifiers.

\begin{enumerate}

\item
Show that the \nm S and \nm K combinators can be used to construct an
expression with the same normal form as the identity expression
$\nm I \equiv \lambda "x"~"x"$.

\newcommand\A[1]{{\cal A}\SB{#1}}

\item
Now, we will construct a translation from $\lambda$-calculus expressions to
expressions containing only applications of the \nm S and \nm K
combinators. This translation will be defined in terms of two functions:
$\C{e}$, which converts an expression $e$ into this form, and a function
$\A{x,e}$, which {\em abstracts} the variable $x$ from the expression $e$.
removing all uses of $x$ within $e$.

The idea is that $\A{x,e} = \lambda x~e$, in the sense that the two
expressions have the same effect when applied to any argument (they are
extensionally equal).  Using the function ${\cal A}$, the function ${\cal C}$
can be defined simply by structural induction:
\begin{eqnarray*}
\C{x} &= & x\\
\C{e_0~e_1} & = & (\C{e_0}~\C{e_1}) \\
\C{\lambda x~e} & = & \A{x,\C{e}}
\end{eqnarray*}
Because ${\cal A}$ is only applied to expressions produced by ${\cal C}$, it
needs to be defined only for expressions that are identifiers and applications.
For example, consider $\A{x,x'}$ where $x'\neq x$. We require
$(\A{x,x'} e) = (\lambda x~x') e$ for any $e$, so we obtain the right
effect with the following definition:
\[
\A{x,x'} = (\nm K~x')\qquad (\mbox{\rm where}~x\neq x')
\]

Define the remainder of the translation to the \nm S and \nm K combinators. 
Does this translation result in the most compact equivalent
expression using these combinators?  Justify your answer.

\if 0
\item
In fact, we can define another combinator
\[
X \equiv \lambda "x"~"x"~K~S~K
\]
\noindent 
which can represent all closed $\lambda$-calculus expressions.  Show how we can
use just the \nm X combinator to write the \nm S and \nm K combinators.  Demonstrate
that your encodings are correct by reducing to $\beta$-$\eta$-normal form.

\item
(This problem is just for fun. It is worth 0 point because we don't really want
to count all the parentheses.)
We can even replace all occurences of $X$ combinator with a pair of 
parentheses $()$. Show how to write the identity expression $I$ with a
sequence of parentheses.
\fi
\end{enumerate}

\end{enumerate}
\end{document}
