\documentclass[10pt,letterpaper]{article} 
\usepackage{fullpage,url}
\usepackage{theorem}
\usepackage{local}
\usepackage{prooftree}

\newcommand{\infer}[3]{\prooftree{#3}\justifies{#2}\using{#1}\endprooftree}

\newcommand{\finish}[1]{\marginpar{***}{\it [#1]}}
\newcommand{\rn}[1]{\textsc{#1}}

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{lemma}{Lemma}
\newtheorem{exercise}{Exercise}
\newtheorem{solution}{Solution}
\newtheorem{debriefing}[exercise]{Debriefing}
\newcommand{\wrong}{\cf{wrong}}

\begin{document}
\begin{center}
\fbox{\large\bf CIS 500 Software Foundations}\\[5pt]
{\large\bf Homework Assignment 2}\\[5pt]
Untyped Lambda Calculus\\[10pt]
{\bf Due:} Monday, September 26, 2005, by noon
\end{center}



\newcommand{\comp}{\ensuremath{\mathit{comp}}}
\renewcommand{\P}{\ensuremath{\mathit{P}}}
\newcommand{\lam}{\ensuremath{\lambda}}



\noindent {\bf Submission instructions:}

\medskip \noindent You must submit your solutions electronically (in
ascii, postscript, or PDF format).  Electronic solutions should be
submitted following the same instructions as last time; these can be
found at \url{http://www.seas.upenn.edu/~cis500/homework.html}.  Do {\bf
not} email your solutions to us.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
  Show the derivation of one single step for each of these lambda
  calculus terms:

  \begin{enumerate}

    \item \cf{(\lam t. \lam f. t) 
              (\lam t. \lam f. f) 
	      (\lam x .x)}

    \item \cf{(\lambda x. x)(\lambda x. x) (\lambda x.x) (\lambda x. x)}

    \item \cf{(\lambda x. x\ x\ x) (\lambda x. x\ x\ x)}

  \end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
  Write down the normal forms for the following lambda calculus terms if a
  normal form exists:
  \begin{enumerate}
    \item \cf{(\lambda t. \lambda f. t) (\lambda t. \lambda f. f) (\lambda x .x)}
    \item \cf{(\lambda x. x)(\lambda x. x) (\lambda x.x) (\lambda x. x)}
    \item \cf{(\lambda x. x\ x\ x) (\lambda x. x\ x\ x)}
    \item \cf{(\lambda y. (\lambda x. x\ x) (\lambda x. x\ x))}
    \item \cf{(\lambda y. (\lambda x. x\ x)\ y) (\lambda x. x)}
  \end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{exercise} 
   These problems involve programming in the untyped lambda calculus.
   You can test your solutions using the lambda calculus interpreter
   installed on {\tt eniac-l.seas.upenn.edu}.  The interpreter may be
   run with: {\tt $\sim$cis500/fulluntyped/f filename.f} where
   {\tt filename.f} is a file containing lambda calculus expressions.
   The output is the value of evaluating those expressions (if any).
   The syntax can been seen by looking at the examples in the file
   {\tt test.f} in {\tt $\sim$cis500/fulluntyped}.
  
   \begin{enumerate}

   \item TAPL 5.2.4.
   \item TAPL 5.2.7.
   \item TAPL 5.2.8.
     
   \item Define a lambda term that takes two Church booleans and returns the
   logical ``nand'' of \cf{b} and \cf{c} (i.e. ``not and'').
     
   \item Write an \cf{isone} term that takes a Church numeral and returns
   \cf{tru} if it is equivalent to \cf{c_1} and \cf{fls} otherwise. Do not
   use the function \cf{equal} that you defined for TAPL 5.2.7.
 
   \item Using the encoding of lists from 5.2.8, write a function that
   determines if any of the boolean values in a list are \cf{tru} without
   using \cf{fix}.

   \item Now write a version of the function that determines if any of the
   boolean values in a list are \cf{tru} that does use \cf{fix}.

   \end{enumerate}
 \end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise} Questions about scope:

   \begin{enumerate}
   \item Which of these terms are closed?

     \begin{enumerate}

     \item \cf{ \lambda z. z\ z }

     \item \cf{ \lambda w. x }

     \item \cf{ (\lambda m. m)\ m }
   
     \item \cf{ \lambda z. \lambda y. z\ y } 
     \end{enumerate}

   \item Which of these pairs of terms are alpha-equivalent?
 \[
     \begin{array}{cc}
       \cf{ \lambda x. \lambda y. x\ y  } & 
       \cf{ \lambda x. \lambda x. x\ x} \\
       \cf{ \lambda w. \lambda x. \lambda y. w\ (x\ y) } & 
       \cf{ \lambda x. \lambda y. \lambda w. w\ (x\ y) } \\
       \cf{ x  } & \cf{ y } \\
       \cf{ \lambda w. (\lambda x. x)\ x } & 
       \cf{ \lambda v. (\lambda y. y)\ y } \\
       \cf{ \lambda w. \lambda x. \lambda y. w\ (x\ y) } & 
       \cf{ \lambda x. \lambda y. \lambda w. x\ (y\ w) } \\
     \end{array}
     \]
   \end{enumerate}

\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
  TAPL 5.3.8.  Additionally, show that the big step semantics is equivalent to
  the small step semantics.
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
  
  Suppose we add a new non-value term \cf{wrong} to the syntax of the
  untyped lambda calculus, and add the following rules to the big-step
  semantics for lambda calculus terms (that you defined in the previous
  exercise).

  \[
  \prooftree
  \justifies
      \cf{x} \Downarrow \wrong
  \using{\rn{B-VarWrong}}
  \endprooftree
  \qquad
  \prooftree
      \cf{t_1} \Downarrow \wrong
  \justifies
      \cf{t_1\ t_2} \Downarrow \wrong
  \using{\rn{B-App1Wrong}}
  \endprooftree
  \]
  \[
  \prooftree
      \cf{t_1 \Downarrow \lambda x.t_{12}  \quad  t_2 \Downarrow \wrong} 
  \justifies
      \cf{t_1\ t_2 \Downarrow \wrong}
  \using{\rn{B-App2Wrong}}
  \endprooftree
  \qquad
  \prooftree
      \cf{t_1 \Downarrow \lambda x.t_{12}  \quad  t_2 \Downarrow v_2 \quad  [x \mapsto v_2]t_{12} \Downarrow \wrong}
  \justifies
      \cf{t_1\ t_2 \Downarrow \wrong}
  \using{\rn{B-App3Wrong}}
  \endprooftree
  \]

\medskip \noindent Consider the following theorem, that states that the
evaluation of closed terms ``doesn't go wrong''.

    \begin{quotation}
       if $FV(\cf{t}) = \emptyset$ and $\cf{t \Downarrow t'}$ then
       \cf{t'} is not \wrong.
    \end{quotation}

  \begin{enumerate}
    \item Give a derivation of 
      $\cf{(\lambda y.y\ z) (\lambda x. x)} \Downarrow \wrong $.

    \item Why can we not prove the theorem by structural induction on \cf{t}?
    \item What is wrong with stating the theorem as: if
      $FV(\cf{t}) = \emptyset$ then \cf{t \Downarrow v}?
    \item Prove the theorem by induction on the derivation of $\cf{t \Downarrow t'}$.

  \end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{debriefing}\ 
\begin{enumerate}
\item How many hours did you spend on this assignment?
\item Would you rate it as easy, moderate, or difficult?
\item Did everyone in your study group participate?
\item How deeply do you feel you understand the material it covers
(0\%--100\%)? 
\end{enumerate}
If you have any other comments, we would like to hear them; please
send them {\tt cis500@cis.upenn.edu}.
\end{debriefing}


\end{document}