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



\newcommand{\cf}[1]{\texttt{#1}}



\newcommand{\countstars}{\ensuremath{\mathit{countstars}}}
\newcommand{\xand}{\cf{ \&\& }}
\newcommand{\xor}{\cf{ || }}



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

\newcommand{\rn}[1]{\textsc{#1}}

\begin{document}
\begin{center}
\fbox{\large\bf CIS 500 Software Foundations}\\[5pt]
{\large\bf Homework Assignment 1}\\[5pt]
Induction; Operational Semantics\\[10pt]
{\bf Due:} Monday, September 19, 2005, by noon
\end{center}



\noindent {\bf Submission instructions:}

\medskip
\noindent

This assignment should be done together with your {\em study group}.  Only
one assignment should be submitted per group, and it does not matter which
group member submits the assignment. However, make sure that all group
members' names and emails are listed on the submission. These members will
be in your group for the entire semester, unless there are special
circumstances. If you receive help from someone outside of your study group,
excluding the course staff, you must also acknowledge them on your
assignment.

Solutions must be submitted electronically (in ascii, postscript, or PDF
format).  Follow the instructions at
\url{http://www.seas.upenn.edu/~cis500/homework.html.}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Consider this simple grammar:
\begin{code}
t ::= $\star$
      $\boxempty$
      t \xand t
      t \xor t
\end{code}

\noindent State the structural induction principle for terms \cf{t}. 
\end{exercise}



\begin{exercise}
Using the terms from above, define the function $\countstars$ that 
returns the number of stars ($\star$) that appear in the term.
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Consider the following relation, defined on terms from the previous
exercises.
$$
   \prooftree
   \justifies
      \star \sim \boxempty
   \using \rn{Ax1}
   \endprooftree
   \quad\quad
   \prooftree
   \justifies
      \boxempty \sim \star
   \using \rn{Ax2}
   \endprooftree
$$
$$
   \prooftree
      \cf{t}_1 \sim \cf{t}_4 \quad\quad
      \cf{t}_2 \sim \cf{t}_3
   \justifies
      (\cf{t}_1 \xand \cf{t}_2) \sim
      (\cf{t}_3 \xand \cf{t}_4)
   \using \rn{Amp1}
   \endprooftree
   \quad\quad
   \prooftree
      (\cf{t}_2 \xand \cf{t}_1) \sim
      (\cf{t}_4 \xand \cf{t}_3)
   \justifies
      (\cf{t}_1 \xand \cf{t}_2) \sim
      (\cf{t}_3 \xand \cf{t}_4)
   \using \rn{Amp2}
   \endprooftree
   \quad\quad
   \prooftree
      \cf{t}_1 \sim \cf{t}_3 \quad\quad
      \cf{t}_2 \sim \cf{t}_4
   \justifies
      (\cf{t}_1 \xor \cf{t}_2) \sim
      (\cf{t}_3 \xor \cf{t}_4)
   \using \rn{Bars}
   \endprooftree
$$

\medskip \noindent Are the following judgments derivable? If so, give a
derivation.  If not, briefly justify why. \begin{enumerate}

   \item[(a)] $(\star \xand \boxempty) \sim (\star \xand \star)$

   \item[(b)] $\big((\star \xor \star) \xand (\star \xand \boxempty)\big) \sim
               \big((\star \xand \boxempty) \xand (\boxempty \xor \boxempty)\big)$

\end{enumerate}
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
What is the induction principle for the $\sim$ relation defined above?
\end{exercise}



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Prove that the $\sim$ relation defined above is symmetric, using induction
on the $\sim$ relation. Recall that the relation is symmetric if $\cf{t}
\sim \cf{s}$ implies that $\cf{s} \sim \cf{t}$.
\end{exercise}



\begin{exercise}
Prove that if $\cf{t} \sim \cf{s}$ is derivable, then it is derivable without 
using the rule \rn{Amp2}.
\end{exercise}



\begin{exercise}
  Give a definition of multistep evaluation $\cf{t} \to^\ast \cf{t}'$
  (Definition 3.5.9 in TAPL) using three inference rules.
\end{exercise}



\begin{exercise}
  The multistep evaluation rule can also be defined with two inference
  rules. 

\[
\prooftree
\justifies
   \cf{t} \Rightarrow \cf{t}
\using \rn{Refl}
\endprooftree
\qquad
\prooftree
   \cf{t} \to \cf{t}' \quad \cf{t}' \Rightarrow \cf{t}''
\justifies
   \cf{t} \Rightarrow \cf{t}''
\using \rn{Trans}
\endprooftree
\]

(We use $\cf{t} \Rightarrow \cf{t}'$ for multi-step evaluation defined by
the above rules to keep it clear which definition we mean.)  Prove that this
definition is equivalent to the one as in Definition 3.5.9.  In other words
a judgment $\cf{t} \to^\ast \cf{t}'$ is derivable if and only if the
judgment $\cf{t} \Rightarrow \cf{t}'$ is derivable.
\end{exercise}



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



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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{exercise}
Suppose we remove the rule \rn{E-Succ} from Figure 3-2 and replace
\rn{E-PredSucc} with the following:
$$
   \prooftree
   \justifies
      \cf{pred (succ t)} \to \cf{t}
   \using \rn{E-PredSucc2}
   \endprooftree
$$
Note the difference: \rn{E-PredSucc} requires that the argument to \cf{pred}
to be a numeric value \cf{nv} whereas \rn{E-PredSucc2} requires only that
the argument look like \cf{(succ t)}.  Which of the following theorems are
true of the language now? Explain why or why not. \begin{enumerate}

   \item[(a)] Every value is in normal form.

   \item[(b)] If \cf{t} is in normal form, then \cf{t} is a value.

   \item[(c)] Uniqueness of normal forms.

   \item[(d)] Termination of evaluation.

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



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\begin{remarks}

Some solutions are sketched in the back of the book. You should write out
your answers to the assignment before looking. Note that we will be looking
for more detail in your proofs than is provided by the back of the book.

\end{remarks}


\end{document}