\documentclass[12pt]{article}
\usepackage{fullpage}
\usepackage{code}
\title{Computer Science 131, Fall 2000\\
       Assignment 2: Type Safety}
\date{Out:  Thursday, September 14\\[5pt]
      \textbf{Due: Friday, September 22, 5:00pm}}
\author{}

\newcommand{\NQSML}{NQSML}

\newcommand{\num}[1]{\ensuremath{\overline{\mathcd{#1}}}}

\begin{document}
\maketitle 

This assignment involves no programming.  Your written answers must be
given directly to the professor (or put under his office door, 1253
Olin).  \emph{Your work must be clearly legible.}  If you cannot write
neatly, use \LaTeX\ or otherwise typeset the proofs.

If you submit your solution late, be sure to mark it with the date and
time that it was handed in.  

\section{Warm-up (10\%)}

Show the steps required to evaluate the following program to a value.
You need not justify each step (as long as you are correct).  For
example, if the program were 
\cd{\num{1} + (\num{2} + \num{3})} then the answer would be
\cd{\num{1} + (\num{2} + \num{3})} $\to$ \cd{\num{1} + \num{5}}
$\to$ \cd{\num{6}}.

\begin{enumerate}
\item 
  \begin{code}
    let x be \num{3} in
      let f be (fun g(y:Int):Int is x+y) in
        let x be \num{4} in
          f(x)           
  \end{code}
\item  For the following code, assume that we have rules
  in the dynamic semantics for subtraction and multiplication 
  exactly analogous to
  the three existing rules for addition.
  \begin{code}
    let fact be (fun g(y:Int):Int is
                   if y<\num{1} then \num{1} else y*g(y-\num{1}))
    in
        fact \num{2}
  \end{code}
\end{enumerate}

\section{Adding pairs to \NQSML. (65\%)}
  
Consider the following extension of \NQSML\ of adding pairs.  The
abstract syntax is extended as follows:

\newcommand{\e}{e}
\renewcommand{\t}{t}
\renewcommand{\u}{u}
\renewcommand{\v}{v}
\newcommand{\n}{n}
\newcommand{\x}{x}
\newcommand{\y}{y}
\newcommand{\f}{f}
\newcommand{\G}{\Gamma}
\renewcommand{\tt}{\overline{\mathcd{tt}}}
\newcommand{\ff}{\overline{\mathcd{ff}}}
\newcommand{\efun}[5]{\mathcd{fun}\ #1(#2{:}#3){:}#4\mathcd{\ is\ }#5}
\newcommand{\eif}[3]{\mathcd{if}\ #1\ \mathcd{then}\ #2\ \mathcd{else}\ #3}
\newcommand{\eapply}[2]{#1 \, #2}
\newcommand{\elet}[3]{\mathcd{let}\ #1\ \mathcd{be}\ #2\ \mathcd{in}\ #3}
\newcommand{\eplus}[2]{#1 + #2}
\newcommand{\elt}[2]{#1 < #2}
\newcommand{\tint}{\mathcd{Int}}
\newcommand{\tbool}{\mathcd{Bool}}
\newcommand{\tarrow}[2]{#1\mathcd{->}#2}
\newcommand{\st}[2]{#1\ \ \to\ \ #2}
\newcommand{\sts}[2]{#1\ {\to^{*}}\ #2}
\newcommand{\subst}[3]{#3[{#1}{\mapsto}{#2}]}
\newcommand{\epair}[2]{\langle #1,#2\rangle}
\newcommand{\epi}[2]{#2.#1}
\newcommand{\tprod}[2]{#1 \times #2}
\newcommand{\tc}{{:}}
\newcommand{\wfe}[3]{#1\vdash #2 \mathrel{\tc} #3}
\newcommand{\bs}[2]{#1 \Downarrow #2}


\[
\begin{array}{rll}

\v ::=&\cdots\\
    |&\epair{\v_1}{\v_2}\\[10pt]

\e ::= &\cdots\\
   |&\epair{\e_1}{\e_2}\\
   |&\epi{1}{\e}\\
   |&\epi{2}{\e}\\[10pt]

\t,\u ::= &\cdots\\
   |&\tprod{\t_1}{\t_2}\\
\end{array}
\]

A pair of values is considered a value.  The new syntax allows
creation of a pair, and operations to project out the first or second
component of a pair.  Unlike SML, there is no pattern-matching for
pairs, so in this abstract syntax a function to raise an integer 
to an positive integer power would look like:

\begin{code}
  fun p(arg:Int$\times$Int):Int is
    let x be arg.1 in
       let n be arg.2 in
         if (n < \num{1}) then \num{1} else p($\epair{\mathcd{x}}{\mathcd{n}-\num{1}}$)
\end{code}

The new typing rules are:

\setcounter{equation}{25}

\newcommand{\infrule}[2]{
  \begin{equation}
    \frac{\begin{array}{c}
              #1
          \end{array}}
         {\begin{array}{c}
              #2
          \end{array}}
  \end{equation}}

\infrule
  {\wfe{\G}{\e_1}{\t_1}\qquad\wfe{\G}{\e_2}{\t_2}}
  {\wfe{\G}{\epair{\e_1}{\e_2}}{\tprod{\t_1}{\t_2}}}

\infrule
  {\wfe{\G}{\e}{\tprod{\t_1}{\t_2}}}
  {\wfe{\G}{\epi{1}{\e}}{\t_1}}

\infrule
  {\wfe{\G}{\e}{\tprod{\t_1}{\t_2}}}
  {\wfe{\G}{\epi{2}{\e}}{\t_2}}

and the new evaluation rules are:

\infrule
  {\st{\e_1}{\e'_1}}
  {\st{\epair{\e_1}{\e_2}}{\epair{\e'_1}{\e_2}}}

\infrule
  {\st{\e_2}{\e'_2}}
  {\st{\epair{\v_1}{\e_2}}{\epair{\v_1}{\e'_2}}}

\infrule
  {\st{\e}{\e'}}
  {\st{\epi{1}{\e}}{\epi{1}{\e'}}}

\infrule
  {}
  {\st{\epi{1}{\epair{\v_1}{\v_2}}}{\v_1}}

\infrule
  {\st{\e}{\e'}}
  {\st{\epi{2}{\e}}{\epi{2}{\e'}}}

\infrule
  {}
  {\st{\epi{2}{\epair{\v_1}{\v_2}}}{\v_2}}
  
  One can prove the Type Preservation and Progress properties for this
  extended language by taking the proof for the original system and
  simply adding new cases corresponding to the new rules.  (There will
  be new cases in the Type Preservation proof corresponding to the new
  dynamic semantics rules, and new cases in the Progress proof
  corresponding to the new static semantics rules.)  State the new
  cases required and give the proofs for these cases.
  
  You will need to add new Inversion properties you and to extend the
  Canonical Forms lemma.  You should state these extensions, but need
  not give the proofs.

\section{Natural Semantics (25\%)}

So far you have seen what is called a ``small-step'' operational
semantics, where execution is defined by a relation $\to$ that defines
a single step of evaluation; from this we can define the multi-step
relation $\to^{*}$.  Another common presentation is a ``big-step''
operational semantics, where the notion of ``evaluating to a value''
is defined directly.  This is done by defining a new relation
$\Downarrow$ between programs and values, where $\bs{\e}{\v}$ means
that evaluating the program $\e$ yields the value $\v$.

The natural semantics for the \NQSML\ language (without pairs or lists)
is given by the following collection of inference rules.  As usual,
stating that ``$\bs{\e}{\v}$ holds'' or that ``$\bs{\e}{\v}$ is true''
is equivalent to saying there exists a finite proof that
  $\bs{\e}{\v}$.

\renewcommand{\bs}[2]{#1\ \Downarrow\ #2}

\infrule
  {}
  {\bs{\v}{\v}}

\infrule
  {\bs{\e_1}{\overline{\mathcd{m}_1}}\qquad\bs{\e_2}{\overline{\mathcd{m}_2}}}
  {\bs{\eplus{\e_1}{\e_2}}{\overline{\mathcd{m}_1+\mathcd{m}_2}}}

\infrule
  {\bs{\e_1}{\overline{\mathcd{m}_1}}\qquad\bs{\e_2}{\overline{\mathcd{m}_2}}}
  {\bs{\elt{\e_1}{\e_2}}{\overline{\mathcd{m}_1<\mathcd{m}_2}}}

\infrule
  {\bs{\e_1}{\tt}\qquad\bs{\e_2}{\v_2}}
  {\bs{\eif{\e_1}{\e_2}{\e_3}}{\v_2}}

\infrule
  {\bs{\e_1}{\ff}\qquad\bs{\e_3}{\v_3}}
  {\bs{\eif{\e_1}{\e_2}{\e_3}}{\v_3}}

\infrule
  {\bs{\e_1}{\v_1}\qquad\bs{\subst{\x}{\v_1}{\e_2}}{\v_2}}
  {\bs{\elet{\x}{\e_1}{\e_2}}{\v_2}}

\infrule
  {\bs{\e_1}{(\efun{\f}{\x}{\t_1}{\t_2}{\e'_1})}\qquad
   \bs{\e_2}{\v_2}\\
   \bs{\subst{\f}{(\efun{\f}{\x}{\t_1}{\t_2}{\e'_1})}{(\subst{\x}{\v_2}{\e'_1})}}{\v}}
  {\bs{\eapply{\e_1}{\e_2}}{\v}}

\goodbreak

\renewcommand{\bs}[2]{#1 \Downarrow #2}
\renewcommand{\st}[2]{#1 \to #2}

The two dynamic semantics for \NQSML\ were designed to be equivalent in
the following sense: we expect $\bs{\e}{\v}$ if and only if
$\sts{\e}{\v}$.  The goal of this problem is to prove this fact.

\begin{enumerate}
\item Prove that if $\bs{\e}{\v}$ then $\sts{\e}{\v}$.  Your proof
  should be by induction on \emph{the proof} of $\bs{\e}{\v}$.  
  (You can't prove this by induction on $\e$ itself.)
  
  It is obvious from the definition of the small-step semantics that
  if $\sts{\e_1}{\v_1}$ then
  $\sts{\eplus{\e_1}{\e_2}}{\eplus{\v_1}{\e_2}}$.  You are not required
  to explicitly prove this or the other similar properties that you
  will need.  You will also need to use the fact that (by definition)
  the relation $\to^{*}$ is reflexive and transitive.
  
\item Prove that if $\st{\e}{\e'}$ and $\bs{\e'}{\v}$ then
  $\bs{\e}{\v}$.  Your proof should use induction; state explicitly
  what you are inducting over.
  
\item Prove that if $\sts{\e}{\v}$ then $\bs{\e}{\v}$.  (Hint:  use
  induction on the number of steps needed to get from $\e$ to $\v$.)
\end{enumerate}

\end{document}

