\documentclass{article}
\usepackage{fullpage}

\newcommand \bnfdef  {\mathrel{::=}}
\newcommand \bnfalt     {\mathrel{{|}}}
\newcommand \SKIP   {\mathsf{skip}}
\newcommand \pushheap { \mathsf{pushheap} }
\newcommand \popheap[1]  { \mathsf{popheap}\ {#1}}
\newcommand \pushvar[1]  { \mathsf{pushvar}\ {#1}}
\newcommand \popvar[1]  { \mathsf{popvar}\ {#1}}

\begin{document}

\centerline{\textbf{\Large Graduate Programming Languages, Assignment 1}}
\centerline{\textbf{\Large Due: To Be Determined }}
\bigskip
\noindent Ensure you understand the course policies for assignments.\\
\texttt{hw1code.tar}, available on the course website, contains several
Caml files you need.

\medskip

%\noindent Last updated: Summer 2011

\begin{enumerate}
\item (Caml warm-up) Add the following definitions to
  \texttt{trees.ml}.  Do not use mutation.  Do not change the type
  definitions or functions provided to you.  Do not assume trees are
  sorted (though this is largely irrelevant).
\begin{enumerate}
\item Define \texttt{fromList} of type \verb|int list -> inttree| to 
  make a sorted tree containing exactly the ints in the list without
  repeats.  Use \texttt{insert} (provided).
\item Define three functions, \texttt{sum1}, \texttt{prod1},
  and \texttt{avg1}, to compute the sum, product, and average of
  the ints in a tree.  Each has type \verb|inttree -> int|.  The sum
  and product of an empty tree are 0 and 1, respectively.  For
  average, the empty tree should cause a \texttt{DivisionByZero}
  exception to be raised.  For \texttt{sum1} and \texttt{prod1}, do
  not use helper functions.  For \texttt{avg1}, do not traverse the
  tree more than once.  (Hint: Have a helper function do the traversal
  and return a pair.)
\item Define \texttt{map} of type 
  \verb|(int -> int) -> inttree -> inttree| 
  to produce a tree with the same shape as its second
  argument with the int at each position the result of applying the
  first argument to the int at the same position in the second
  argument.
\item Define \texttt{negateAll} of type \verb|inttree -> inttree|
  using \texttt{map}.  It produces a tree of the same shape where each
  int is replaced with its negation.
\item Define \texttt{sum2}, \texttt{prod2}, and \texttt{avg2} to
  compute the sum, product, and average of a tree (see above), but
  using \texttt{fold} (provided).  You should not need more than 1
  line (possibly 2 for \texttt{avg2}).  Use the same pair technique
  for average.
\item In a \emph{short English paragraph}, explain how a client of the
  \texttt{iter} function (provided) would use it to process all the
  ints in a tree.  In a second \emph{short English paragraph}, explain
  how \texttt{iter} is implemented (e.g., ``when'' and ``how'' it
  traverses the tree).\footnote{You might also try implementing
  \texttt{iter} using mutation instead of higher-order functions.  It
  is not very pleasant.}
\item Define \texttt{sum3}, \texttt{prod3}, and \texttt{avg3} to
  compute the sum, product, and average of a tree (see above), but
  using \texttt{iter} (provided).  For product, the code must ``stop
  as soon as it sees a 0'' (this is easier than when using \texttt{fold}).
  Hint: You should need about 5 lines for each function.  For each,
  use a local helper function as a ``loop'' that takes the iterator
  and the answer-so-far.
\item \textbf{Challenge Problem:} When writing functions that cannot always
  produce answers (e.g., average on an empty tree), one chooses
  between raising an exception or returning an option type.  In this
  problem, you write short higher-order wrapper
  functions to ``make the other choice'':
  \begin{itemize}
  \item Write \texttt{optionToException} of type 
    \verb|('a -> 'b option) -> exn -> 'a -> 'b|.  
    It should return a function that
    takes an argument and raises the \texttt{exn} if and only if the
    \verb|'a -> 'b option| returns \texttt{None} for the same
    argument.
  \item Write \texttt{exceptionToOption} of type 
    \verb|('a -> 'b) -> (exn -> bool) -> 'a -> 'b option|.  
    It should return a function
    that takes an argument and returns \texttt{None} if and only if
    the \verb|('a -> 'b)| (when passed the same argument) raises an
    exception that causes the \verb|exn -> bool| to return true.
  \item In English, explain why \texttt{optionToException} takes an
  \texttt{exn} but \texttt{exceptionToOption} takes an \verb|exn -> bool|.
  \end{itemize}
\end{enumerate}

\newpage
\item We will extend IMP with the ability to push and pop heaps:
\begin{itemize}
\item A program state is now $L;H;s$ where $H$ and $s$ are as before
  and $L$ is a list (i.e., a stack of heaps).
\item There are two new statement forms: $\pushheap$ and
  $\popheap{x}$. The former adds the current heap $H$ to the beginning
  of $L$. (Informally, it ``copies'' $H$ ``all at once''.)  The latter
  replaces the current heap $H$ with the first element of $L$
  \emph{except} $x$ maps to $H(x)$ and replaces $L$ with the tail of
  $L$.  If $L$ is the empty list, then $\popheap{x}$ has no effect.
  Both $\pushheap$ and $\popheap{x}$ ``become $\SKIP$'' in one step.
\end{itemize}
\begin{enumerate}
\item Extend the provided interpreter to support this new language.
  Hints/requirements:
  \begin{itemize}
  \item Do not use mutation.
  \item Change only \texttt{interp\_step}, \texttt{iter}, and
    \texttt{interp}.  (The parser is already written.  The code for
    heaps and expressions does not need changing.)
  \item Have \texttt{interp\_step} and \texttt{iter} take a third
  argument (the list of heaps) and have \texttt{interp\_step} also return a
  ``new'' list.
  \item You need to change each case of \texttt{interp\_step} and add
  two more cases.
  \end{itemize}
\item Give an IMP program using $\pushheap$ and $\popheap{x}$ that we
  can use for testing.  Note the parser will let you put parentheses
  around any expression or statement and requires parentheses in
  certain positions.
\item Define a formal small-step operational semantics for this new
  language.  Hints/requirements:
  \begin{itemize}
  \item The inference rules should have the form $L;H;s \rightarrow
  L';H';s'$.
  \item Use the syntax $L \bnfdef [] \bnfalt H{::}L$ for lists.
  \item Because the form of rules has changed, include ``all the
  rules'' (i.e, rules for assignment, conditionals, etc.)
  \item You need 3 rules total for $\pushheap$ and $\popheap{x}$.
  \item You do \emph{not} need to write the semantics for expressions
  because they have not changed.
  \end{itemize}
\item In a short English paragraph, explain why our language would be
  much less useful if popping a heap did not copy one value from the
  popped heap.
\end{enumerate}

\item We will extend IMP with the ability to push and pop variables:
  \begin{itemize}
  \item A heap now maps a variable to a number and a list (i.e., a
    stack) of numbers.  The initial heap maps each variable to 0 and
    the empty-list (though it's not implemented that way).
  \item There are two new statement forms: $\pushvar{x}$ and
  $\popvar{x}$. The former changes $H$ such that $x$ maps to the same
  number and a list that is like the old list except the number is at
  the beginning.  The latter is the inverse of the former and has no
  effect if the list for $x$ is empty.  Both $\pushvar{x}$ and
  $\popvar{x}$ ``become $\SKIP$'' in one step.
  \end{itemize}
  \begin{enumerate}
  \item Extend the provided interpreter to support this new language.
  Hints/requirements:
  \begin{itemize}
  \item Do not use mutation.
  \item Change only \texttt{get\_var}, \texttt{set\_var}, and
    \texttt{interp\_step}, but also add functions \texttt{push\_var}
    and \texttt{pop\_var}, which take a heap and a string and return a
    heap.  For \texttt{interp\_step} you only need to add new cases.
    For \texttt{push\_var} and \texttt{pop\_var}, you typically
    produce a new heap with a different entry for the string.
    However, you must also do the right thing if there is no entry for
    the string, which is equivalent to there being an entry
    like \verb|(str,0,[])| ``before the change''.
    \item Just ``add on'' to your solution the previous problem.  This
    addition is completely orthogonal.
    \end{itemize}
\item Give an IMP program using $\pushvar{x}$ and $\popvar{x}$ that we
  can use for testing.
\item \textbf{Challenge Problem:} Define a formal small-step operational
  semantics for this new language.  Be sure to give a precise
  definition for heaps, explaining your notation.
\end{enumerate}

\newpage

\item We will prove a property of execution for IMP with $\pushheap$
  and $\popheap{x}$.
  \begin{enumerate}
  \item Formally prove the following: (For all $s$, $L$, $H$, and
    $s'$,) If $s$ has no while loops and
    $[];\cdot;s \rightarrow^* L;H;s'$ (i.e., we run $s$ for any number
    of steps), then the length of $L$ does not exceed the number of
    occurrences of $\pushheap$ in $s$ (i.e., in the original
    program).  Hints: 
    \begin{itemize}
    \item Use induction on the number of steps taken, and a second
    inductive proof on the height of the derivation of taking one step.
    \item For both proofs, you need to strengthen the induction
    hypothesis.  Think through how to do so before writing out a long
    incorrect proof.
    \end{itemize}
  \item Formally prove the following: The previous claim is false if
  we allow $s$ to contain while loops.  Hint: Do not use induction.
  \end{enumerate}

\item \textbf{Challenge Problem:} Formally state and prove the following
  for our original IMP language:
  For any $s$ that does not contain the variable \texttt{x}, 
  the IMP programs \texttt{x:=x+1; y:=x*x; $s$; x:=x-1} and\\
  \texttt{y:=(x+1)*(x+1); $s$} are equivalent.

\end{enumerate}

\bigskip

\noindent\textbf{What to turn in:}
\begin{itemize}
\item Caml source code for problem 1 in a file called
  \texttt{trees.ml}.
\item Hard-copy (written or typed) answers to problems 1f, 2c, 2d, and
  4.
\item Caml source code for problems 2a and 3a in a file called
  \texttt{interp.ml}.
\item IMP code for problem 2b and 3b in files called
  \texttt{2b.imp} and \texttt{3b.imp}.
\item For the challenge problems, edit \texttt{trees.ml} and your hardcopy
  solutions.
\end{itemize}

\emph{Do not modify interpreter files other than \texttt{interp.ml}.}

%Email your source code to the TA as
%\verb|firstname-lastname-hw1.tgz| or
%\verb|firstname-lastname-hw1.zip|.  The code should untar/unzip into a
%directory called \verb|firstname-lastname-hw1|.  Hard copy solutions
%can be emailed in a pdf file or given to the TA directly.

 
\end{document}