\documentclass{report}
%
\usepackage{amsmath}
%
\begin{document}
%
\begin{center}
%
  \textbf{CS 319 -- The Lambda Calculus}\\
  \textbf{Assignment 3, Winter 2000}\\
  Due Monday, 7 February\\
%
\end{center}
%
\begin{enumerate}
\item Demonstrate an interesting encoding of integers in the lambda
  calculus that is \emph{not} suitable for computation.
%
\item Using weak bracket-abstraction, show that the $\overline{\eta}$
  rule below does not imply extensionality.
%
  \begin{gather}
%
    ([x].\alpha x)=_{\overline{\eta}}\alpha
       \text{ where $x$ is not free in $\alpha$}
       \tag{\(\overline{\eta}\)}
%
  \end{gather}
%
\item Using weak bracket-abstraction, bound the length of $[x].\alpha$
  and of $\overline{\alpha}$ in terms of the length of $\alpha$. Give
  examples showing that your bounds are tight. What difference does
  strong bracket-abstraction make?
%
\item Find out what happens to $\overline{\alpha}$ under weak
  reduction when $\alpha$ produces nested residuals under beta reduction.
%
\item Continue to work on general classes of solvable equations. You
  may do this as a joint project, and hand in a single joint
  presentation, if you like.
%
\end{enumerate}
%
\end{document}
