\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 5}\\[5pt]
Type systems, simply-typed $\lambda$-calculus\\[10pt]
{\bf Due:} Monday, October 31, 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 8.2.3, 8.3.5, 9.2.1,
9.2.2, 9.2.3, and 9.4.1 in TAPL when you read Chapter 8 and 9.  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}
Exercise 8.3.4 in TAPL.
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise} Exercise 8.3.6 in TAPL.  \end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Show the derivations of the following typing judgments:
\begin{enumerate}
\item \cf{if\ false\ then\ 0\ else\ succ\ 0 : Nat}
\item \cf{succ\ (if\ iszero\ 0\ then\ succ\  0\  else\  pred\  0) : Nat}
\end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
If we make the following changes to the Arith language, do the
following theorems become false or remain true. If they become false,
give a counterexample. 

\medskip \noindent The theorems:
\begin{itemize}
\item Uniqueness of types  (Theorem 8.2.4)
\item Progress (Theorem 8.3.2)
\item Preservation (Theorem 8.3.3)
\end{itemize}

\medskip \noindent The changes to Arith:
\begin{enumerate}

\item Say we remove the rule {\sc E-PredZero}.

\item Say we add the rule:
 \cf{if\ t_1\ then\ t_2\ else\ t_3 \longrightarrow t_2}


\item Say we add the rules
\begin{quote}
\cf{pred\ true \longrightarrow false} \\
\cf{pred\ false \longrightarrow true}
\end{quote}
and the following typing rule:
\[
\prooftree
   \cf{t : Bool}
\justifies
   \cf{pred\ t : Nat}
\endprooftree
\]

\item
Say we add the rule
\begin{quote}
\cf{if\ 0\ then\ t_2\ else\ t_3 \longrightarrow t_2}
\end{quote}
and the following typing rule:
\[
\prooftree
\cf{t_1 : Nat  \qquad     t_2 : T  \qquad  t_3 : T}
\justifies
\cf{if\ t_1\ then\ t_2\ else\ t_3 : T}
\endprooftree
\]

\item  Say we add the following typing axiom: \cf{0 : Bool}

\end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{exercise}
  Prove the type soundness theorem for Arith.

\begin{quote} {\bf Theorem:}  If \cf{t:T} and \cf{t \longrightarrow^* t'}
and \cf{t' \not\longrightarrow}, then \cf{t'} is a value.  \end{quote}

You should prove this theorem by induction on the following definition of
multistep evaluation. In your proof, you may use the Preservation and
Progress theorems from TAPL (Theorems 8.3.2 and 8.3.3).

\[
\prooftree
    \cf{t \longrightarrow t' \qquad t' \longrightarrow^* t'' }
\justifies
    \cf{t \longrightarrow^* t''}
\using\mbox{\sc EV-Step}
\endprooftree
\qquad
\prooftree
\justifies
    \cf{t \longrightarrow^* t}
\using\mbox{\sc EV-Ref}
\endprooftree
\]

\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{exercise}
  The following exercise concerns the big-step semantics for the
  simply-typed lambda calculus. For simplicity, consider just the language
  with a base value \cf{0} of type \cf{Nat} and functions. 

  The big-step semantics of this calculus is:
  \[
  \prooftree
  \justifies
  \cf{v \Downarrow v}
  \using \mbox{\sc B-Value}
  \endprooftree
  \]

  \[
  \prooftree
  \cf{t_1 \Downarrow \lambda x:T_1. t_{11}   \qquad  t_2 \Downarrow v_2
  \qquad [x \mapsto v_2]t_{11} \Downarrow v}
  \using \mbox{\sc B-App}
  \justifies
  \cf{t_1\ t_2 \Downarrow v}
  \endprooftree
  \]


  \begin{enumerate}
    \item The following theorem is true

      \begin{quote} {\bf Theorem:} If \cf{\emptyset \vdash t : T} then \cf{t
      \Downarrow v} and \cf{\emptyset \vdash v : T}.  \end{quote}

    \noindent but the following proof is flawed. Find the error in the proof
    below.

    \medskip \noindent  Proof by induction on the structure of \cf{t}.

  \begin{itemize}

    \item Case \cf{t = 0}. This case is trivial because \cf{0 \Downarrow 0}
    by \rn{B-Value} and \cf{\emptyset \vdash 0 : Nat}.

    \item Case \cf{t = x}, a variable. This case is trivial because it is
    not the case that \cf{\emptyset \vdash x :T} for any \cf{T}.

    \item Case \cf{t = \lambda x:T_1. t_1}, an abstraction. This case is
    trivial because \cf{\lambda x:T_1.t_1 \Downarrow \lambda x:T_1.t_1} by
    \rn{B-Value} and \cf{\emptyset \vdash \lambda x:T_1.t_1 : T} by
    assumption.

    \item Case \cf{t = t_1\ t_2}.
      \begin{itemize}
        \item By inversion (Lemma 9.3.1), \cf{\emptyset \vdash t_1: T_1 \to
              T} and \cf{\emptyset \vdash t_2: T_1}.
        \item By induction \cf{t_1 \Downarrow v_1} and \cf{\emptyset \vdash v_1 : T_1 \to T}.
        \item By induction \cf{t_2 \Downarrow v_2} and \cf{\emptyset \vdash v_2 : T_1}.
        \item By canonical forms (Lemma 9.3.4), \cf{v_1 = \lambda x:T_1. t_{11}}.
        \item By inversion (Lemma 9.3.1), \cf{x:T_1 \vdash t_{11} : T}.
        \item By substitution (Lemma 9.3.8), \cf{\emptyset \vdash [x \mapsto v_2] t_{11} : T}.
        \item By induction \cf{[x \mapsto v_2] t_{11} \Downarrow v} and \cf{\emptyset \vdash v : T}.
        \item By \rn{B-App}, \cf{t_1\ t_2 \Downarrow v}, and by the above \cf{\emptyset \vdash v : T}.
        \end{itemize}
  \end{itemize}
  \item
    An easier-to-prove statement of the theorem reads:

    \begin{quote} {\bf Theorem:} If \cf{\emptyset \vdash t : T} and \cf{t
    \Downarrow v} then \cf{\emptyset \vdash v : T}.  \end{quote}

    \noindent Prove this theorem.
  \end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
  Suppose we give an implicitly-typed presentation of the simply-typed
  lambda-calculus. In this case, we define typing judgments that apply
  to {\em untyped} lambda calculus terms (plus booleans).

  \begin{enumerate}
    \item What is the typing rule for abstractions?
    \item This style breaks the uniqueness of types property (Theorem
      9.3.3). Give a counterexample.
    \item State the canonical forms lemma for this calculus (analogous
      to 9.3.4).
  \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 to {\tt cis500@cis.upenn.edu}.
\end{debriefing}



\end{document}
