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