\documentclass[letterpaper]{article}
\usepackage{fullpage,theorem,prooftree,amssymb,url}
\usepackage{stmaryrd}



\newcommand{\cf}[1]{\ensuremath{\mathtt{#1}}}
\newcommand{\rn}[1]{\textsc{#1}}



\newcommand{\arr}{\Rightarrow}
\newcommand{\cons}{\cf{\ ::\ }}
\newcommand{\match}{\cf{match\ }}
\newcommand{\nil}{\cf{[]}}
\newcommand{\with}{\cf{\ with\ }}
\newcommand{\xbar}{\cf{\ |\ }}
\newcommand{\removenames}{\ensuremath{\mathit{remove}}}
\newcommand{\restorenames}{\ensuremath{\mathit{restore}}}
\newcommand{\remove}{\ensuremath{\mathit{remove}}}
\newcommand{\restore}{\ensuremath{\mathit{restore}}}



%%% Macros from Benjamin

\theoremstyle{margin}
\theorembodyfont{\rmfamily}
\newtheorem{lemma}{Lemma}
\newtheorem{exercise}{Exercise}
\newtheorem{debriefing}[exercise]{Debriefing}
\newtheorem{remarks}[exercise]{Final remarks}
\newtheorem{solution}{Solution}

\begin{document}
\begin{center}
\fbox{\large\bf CIS 500 Software Foundations}\\[5pt]
{\large\bf Homework Assignment 4}\\[5pt]
$\lambda$-calculus, de Bruijn notation\\[10pt]
{\bf Due:} Monday, October 10, 2005, by noon
\end{center}



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

As quick self-checks, you should have done exercises 6.1.1, 6.2.2, 6.2.5,
6.2.7, and 6.3.1 in TAPL when you read Chapter 6.  If you did not, do them
now.\footnote{In general, you should be doing all the one $\star$ exercises
when you read TAPL.  They are designed to make sure you have a minimal
understanding of what you're reading.} Do {\bf not} turn in anything for
this exercise.

\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}

We can extend the untyped $\lambda$-calculus (Figure 5-3 in TAPL) with a
primitive notion of lists as follows.  This is in contrast to encoding lists
in the untyped $\lambda$-calculus, which you saw in exercise 5.2.8 from
TAPL.

$$
\begin{array}{rcll}
   \cf{t} & ::= & \ldots              & \quad \mbox{terms:} \\
          &     & \nil                & \quad \mbox{empty list (nil)} \\
          &     & \cf{t} \cons \cf{t} & \quad \mbox{cons} \\
          &     & \match \cf{t} \with
                     \nil \arr \cf{t}
                     \xbar \cf{x}_1 \cons \cf{x}_2 \arr \cf{t}
                & \quad \mbox{case analysis on lists} \\
   \\
   \cf{v} & ::= & \ldots               & \quad \mbox{values:} \\
          &     & \cf{lv}              & \quad \mbox{list values} \\
   \\
   \cf{lv} & ::= & \nil \\
           &     & \cf{v} \cons \cf{lv}
\end{array}
$$
\medskip
$$
   \prooftree
      \cf{t_1} \rightarrow \cf{t_1}'
      \justifies
      \cf{t_1} \cons \cf{t_2} \rightarrow
      \cf{t_1}' \cons \cf{t_2}
      \using \rn{E-Cons1}
   \endprooftree
   \quad\quad
   \prooftree
      \cf{t_2} \rightarrow \cf{t_2}'
      \justifies
      \cf{v_1} \cons \cf{t_2} \rightarrow
      \cf{v_1} \cons \cf{t_2}'
      \using \rn{E-Cons2}
   \endprooftree
$$
\medskip
$$
   \prooftree
   \cf{t_1} \rightarrow \cf{t_1}'
   \justifies
   (\match \cf{t_1} \with \nil \arr \cf{t_2} \xbar \cf{x_1} \cons \cf{x_2}
   \arr \cf{t_3})
   \rightarrow
   (\match \cf{t_1}' \with \nil \arr \cf{t_2} \xbar \cf{x_1} \cons \cf{x_2}
   \arr \cf{t_3})
   \using \rn{E-Match}
   \endprooftree
$$
\medskip
$$
   \prooftree
   \justifies
   (\match \nil \with \nil \arr \cf{t_2} \xbar \cf{x_1} \cons \cf{x_2}
   \arr \cf{t_3})
   \rightarrow
   \cf{t_2}
   \using \rn{E-MatchNil}
   \endprooftree
$$
\medskip
$$
   \prooftree
   \mbox{side conditions: $\cf{x_2} \not\in FV(\cf{v})$ and $\cf{x_1} \neq
   \cf{x_2}$}
   \justifies
   (\match \cf{v} \cons \cf{lv} \with \nil \arr \cf{t_2} \xbar \cf{x_1} \cons \cf{x_2}
   \arr \cf{t_3})
   \rightarrow
   [\cf{x_2} \mapsto \cf{lv}]
   [\cf{x_1} \mapsto \cf{v}]
   \cf{t_3}
   \using \rn{E-MatchCons}
   \endprooftree
$$

\medskip \noindent In the expression \cf{\match t \with \nil \arr t_1 \xbar
x_1 \cons x_2 \arr t_2}, we consider \cf{x_1} and \cf{x_2} to be bound in
\cf{t_2}, just as we consider \cf{x} to be bound in \cf{t} when we write
$\lambda \cf{x}. \cf{t}$.  As in OCaml, \cons{} associates to the right; for
example, \cf{t_1 \cons t_2 \cons t_3} is the same as \cf{t_1 \cons (t_2
\cons t_3)}.

\begin{enumerate}

\item In one step, what does \cf{\match (\lambda x. y) \cons (\lambda y. x)
\cons \nil \with \nil \arr z \xbar a \cons b \arr (\lambda x. b) \cons
(\lambda y. a) \cons \nil} evaluate to according to the above rules?  Show
the derivation.

\item Read exercise 6.1.5 from TAPL.  You may look at the solution in the
back of the book.  Now, extend the definitions for
$\mathit{removenames}_\Gamma(\cf{t})$ and
$\mathit{restorenames}_\Gamma(\cf{t})$ to include the primitive lists
introduced above.

\item Now prove that
$\mathit{restorenames}_\Gamma(\mathit{removenames}_\Gamma(\cf{t})) = \cf{t}$
for all \cf{t}, up to renaming of bound variables.
Please turn in the entire proof.  However, you may ignore primitive lists
for this particular proof; that is, you may assume that $\cf{t}$ is a term
from the following grammar:
$$
   \begin{array}{rcl}
      \cf{t} &::=& \cf{x} \\ && \cf{t}\ \cf{t} \\ && \lambda \cf{x}.\cf{t}
   \end{array}
$$

\item Extend definition 6.2.4 in TAPL so that it is also defined on your
nameless representation of lists.  That is, give the definition of
substitution on your nameless representation of lists.

\item Write down the nameless equivalents of all the evaluation rules above
(i.e., \rn{E-Cons1}, \rn{E-Cons2}, etc.).  For example, the version of
\rn{E-AppAbs} on p.81 of TAPL is the nameless equivalent of the
\rn{E-AppAbs} rule from Figure 5-3.

\end{enumerate}

\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}

In this exercise, we're back to named $\lambda$-calculus terms.  However,
instead of the familiar call-by-value evaluation rules, we'll consider
leftmost/outermost evaluation.  This is called the ``normal order'' strategy
in TAPL (see p.56).  We can define this evaluation strategy by the following
rules.

$$
\prooftree
\cf{t_1} \rightarrow \cf{t_1}'
\justifies
\cf{t_1}\ \cf{t_2} \rightarrow \cf{t_1}'\ \cf{t_2}
\using \rn{E-App1}
\endprooftree
\quad\quad
\prooftree
\cf{\lambda x. t_1} \not\rightarrow
\justifies
(\cf{\lambda x. t_1})\ \cf{t_2} \rightarrow [\cf{x} \mapsto \cf{t_2}]\cf{t_1}
\using \rn{E-App2}
\endprooftree
\quad\quad
\prooftree
\cf{t_2} \rightarrow \cf{t_2}'
\justifies
\cf{x}\ \cf{t_2} \rightarrow \cf{x}\ \cf{t_2}'
\using \rn{E-App3}
\endprooftree
$$
$$
\prooftree
(\cf{s\ t}) \not\rightarrow \quad\quad
\cf{t_2} \rightarrow \cf{t_2}'
\justifies
(\cf{s\ t})\ \cf{t_2} \rightarrow (\cf{s\ t})\ \cf{t_2}'
\using \rn{E-App4}
\endprooftree
\quad\quad
\prooftree
\cf{t_1} \rightarrow \cf{t_1}'
\justifies
\cf{\lambda x. t_1} \rightarrow \cf{\lambda x. t_1'}
\using \rn{E-Abs}
\endprooftree
$$

\medskip \noindent Here, we use the notation $\cf{t} \not\rightarrow$ to
indicate that for all $\cf{t}'$, we cannot build a derivation of  $\cf{t}
\rightarrow \cf{t}'$.

\begin{enumerate}

\item Spend a few moments convincing yourself that these rules lead to
reducing the leftmost, outermost redex in a term.  Remember that
``leftmost'' and ``outermost'' describe the position of the redex when we
view the term as an abstract syntax tree.  Do {\bf not} turn in anything
for this problem.

\item We can modify the \texttt{eval1} function from Chapter 7 to implement
these rules instead of the familiar call-by-value rules.  Lucky for you,
someone tried to do that already and produced the following code.

\end{enumerate}

\clearpage
\begin{verbatim}
let rec eval1 ctx t = match t with
   (* First case. *)
   TmAbs(fi,x,t1) ->
      let t1' = eval1 ctx t1 in
      TmAbs(fi,x,t1')
 | TmApp(fi,t1,t2) ->
      (try
         (* Second case. *)
         let t1' = eval1 ctx t1 in
         TmApp(fi,t1',t2)
      with
         NoRuleApplies ->
            (* Third case. *)
            let t2' = eval1 ctx t2 in
            TmApp(fi,t1,t2'))
 | _ ->
      raise NoRuleApplies
\end{verbatim}

\begin{enumerate}

\item[] Not so lucky for you, while this code compiles, it does contain some
major mistakes in one of the cases (the comments indicate there are three
cases in the code).  Which case is that and how would you fix it?  Do not
modify an actual implementation for this problem.  Just write out your fix
to the code by hand; we will ignore \textit{minor} syntax errors as long as
your intent is clear (and correct).

\end{enumerate}

\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{debriefing}\
\begin{enumerate}
\item How many hours did each person in your group spend on this assignment,
including time taken to read TAPL?
\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}