\documentclass{article} 
\usepackage{times}
\usepackage{abstract}
\usepackage{amssymbols}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% Definitions

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

\begin{document}
\title{Type Safety for NanoML}
\author{Assignment 4}
\date{Due: February 25, 2003}
\maketitle
\bibliographystyle{acm}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Syntax of NanoML}

\newtheorem{theorem}{Theorem}[section]
\newtheorem{lemma}[theorem]{Lemma}
\newcommand{\alt}{\,\,\vert\,\,}
\newcommand{\intt}{\texttt{int}}
\newcommand{\boolt}{\texttt{bool}}
\newcommand{\standard}{\mathbin{\longmapsto}}
\newcommand{\ar}{\rightarrow}
\newcommand{\te}{\textsf{true}}
\newcommand{\fe}{\textsf{false}}
\newcommand{\ife}[3]{\textbf{if}~#1~\textbf{then}~#2~\textbf{else}~#3}
\newcommand{\fune}[4]{(\textbf{fun}~#1~#2~(#3)~\{#4\})}

The syntax is given by the following BNF. In the following $n$ ranges
over integer constants:
\[\begin{array}{lrcll}
\textit{Types} & t &::=& \intt & \textit{integer type} \\
           &&\alt& \boolt & \textit{boolean type} \\
\\
\textit{Operators} & o &::=& + \alt - \alt * \alt / \alt = \alt < \\
\\
\textit{Expressions} & e &::=& n & \textit{integer constants} \\
           &&\alt& o(e,e) & \textit{primitive applications} \\
           &&\alt& \te \alt \fe & \textit{boolean constants} \\
           &&\alt& \ife{e}{e}{e} & \textit{conditional expressions} 
\end{array}\]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Static Semantics}

The static semantics filters the set of syntactically correct programs
to exclude those programs that are not well-typed according to the
rules in Figure~\ref{tf}. The intention (which we formalize and prove
in Section~\ref{ts}) is that the evaluation of a well-typed program
will be guaranteed not to encounter a certain class of errors. Note
that a well-typed program may still encounter errors in another class:
non-termination and division by zero in our small language. Also note
that a program that fails to typecheck according to our rules may
still evaluate without any errors. (For example
$\ife{\te}{1}{+(2,\fe)}$ does not typecheck but would evaluate to $1$
if allowed to execute.) In summary, the type rules are a static
approximation of what constitutes ``good behavior.'' The fact that
such static approximations can never be exact means that one can
always develop a more sophisticated type system that accepts a
different class of programs.

%INFERENCE RULES
\newcommand{\Rule}[4]{
\makebox{{\rm #1}
$\displaystyle
\frac{\begin{array}{l}#2\\\end{array}}
{\begin{array}{l}#3\\\end{array}}$
 #4}}
\newcommand{\Axiom}[3]{\makebox{{\rm #1}\enskip$#2$\enskip #3\enskip}}
\newcommand{\axiom}[2]{\makebox{{\rm #1}\enskip $#2$\enskip}}

\begin{figure}[t]
\begin{center}

\Rule{}{}{ \vdash n : \intt}{} 
\qquad
\Rule{}{}{ \vdash \te : \boolt}{}
\qquad
\Rule{}{}{ \vdash \fe : \boolt}{}

\bigskip

\Rule{}{ \vdash e_1 : \intt \qquad 
         \vdash e_2 : \intt}
        { \vdash =(e_1,e_2) : \boolt}{}
\qquad
\Rule{}{ \vdash e_1 : \intt \qquad 
         \vdash e_2 : \intt}
        { \vdash <(e_1,e_2) : \boolt}{}

\bigskip

\Rule{}{ \vdash e_1 : \intt \qquad 
         \vdash e_2 : \intt}
        { \vdash o(e_1,e_2) : \intt}{if $o$ is one of $\{
        +,-,*,/ \}$}

\bigskip

\Rule{}{ \vdash e_1 : \boolt \qquad
         \vdash e_2 : t \qquad
         \vdash e_3 : t}
        { \vdash \ife{e_1}{e_2}{e_3} : t}{}
\end{center}
\caption{\label{tf}Typing Rules}
\end{figure}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Dynamic Semantics}

The dynamic semantics is a function that maps a syntactically valid
program to a value. The function is partial since programs may
diverge, cause errors like division by zero, or get stuck if a
nonsensical operation such as adding $1$ to $\te$ is attempted at
runtime. In the next section we will be concerned with the proof that
well-typed programs can never get stuck during evaluation.

The evaluation proceeds in steps: at each step, a subexpression of the
entire program is chosen for evaluation. The subexpressions of the
program are gradually replaced by their values until the entire
program reduces to a value or evaluation gets stuck.

To specify this evaluation formally, we first need to define the set
of values and then extend the syntax of expressions to accommodate the
fact that some subexpressions may be replaced by values or runtime
errors. 

\newcommand{\nv}[1]{\underline{#1}}
\newcommand{\tv}{\underline{\te}}
\newcommand{\fv}{\underline{\fe}}
\newcommand{\divz}{\underline{\textsl{DivZero}}}

\[\begin{array}{lrcll}
\textit{Values} & v &::=& \nv{n} & \textit{integer values} \\
                &&\alt& \tv \alt \fv & \textit{boolean values} \\
                &&\alt& \divz & \textit{error condition for division by zero} \\
\\
\textit{Proper Values} & v^* &::=& \nv{n} & \textit{integer values} \\
                &&\alt& \tv \alt \fv & \textit{boolean values} \\
\\
\textit{Runtime Expressions} & 
           e &::=& n & \textit{integer constants} \\
           &&\alt& o(e,e) & \textit{primitive applications} \\
           &&\alt& \te \alt \fe & \textit{boolean constants} \\
           &&\alt& \ife{e}{e}{e} & \textit{conditional expressions} \\
           &&\alt& \nv{n} & \textit{integer values} \\
           &&\alt& \tv \alt \fv & \textit{boolean values} \\
           &&\alt& \divz & \textit{error condition for division by zero}
\end{array}\]

The process of choosing one subexpression to evaluate is best
explained using the notion of evaluation contexts defined below.

\[\begin{array}{lrcll}
\textit{Evaluation contexts} & E &::=& [~] & \textit{empty context} \\
    &&\alt& o(E,e) & \textit{evaluate left argument first} \\
    &&\alt& o(v^*,E) & \textit{when done with left argument, go to right} \\
    &&\alt& \ife{E}{e}{e} & \textit{need the value of the test} 
\end{array}\]

It is easy to verify that every runtime expression $e$ has a
\emph{unique decomposition} into an evaluation context $E$ and a
subexpression of interest. This is formalized in the following lemma.

\begin{lemma}[Unique Decomposition]
Every runtime expression $e$ is in one (and only one) of the following
forms:
\begin{itemize}
\item a value $v$, 
\item an evaluation context $E$ filled with:
\begin{enumerate}
\item an integer constant $n$,
\item a boolean constant $\te$ or $\fe$,
\item a primitive operation where the first argument is an exception
$o(\divz,e)$,
\item an application of a primitive operation to two values
$o(v^*_1,v_2)$ where the first value is guaranteed to be a proper
value, 
\item a conditional expression with an evaluated test position
$\ife{v}{e_1}{e_2}$, 
\end{enumerate}
\end{itemize}
\end{lemma}

The evaluation rules are:

\newcommand{\ms}[2]{#1}

\[\begin{array}{rcl}
\ms{E[n]}{\rho} &\standard& \ms{E[\nv{n}]}{\rho} \\
\ms{E[\te]}{\rho} &\standard& \ms{E[\tv]}{\rho} \\
\ms{E[\fe]}{\rho} &\standard& \ms{E[\fv]}{\rho} \\
\\
\ms{E[+(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\nv{n_1+n_2}]}{\rho} \\
\ms{E[*(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\nv{n_1*n_2}]}{\rho} \\
\ms{E[-(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\nv{n_1-n_2}]}{\rho} \\
\ms{E[/(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\nv{n_1/n_2}]}{\rho} 
        \mbox{~if~$n_2 \neq 0$} \\
\ms{E[/(\nv{n},\nv{0})]}{\rho} &\standard& \ms{E[\divz]}{\rho} \\
\ms{E[=(\nv{n},\nv{n})]}{\rho} &\standard& \ms{E[\tv]}{\rho} \\
\ms{E[=(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\fv]}{\rho} 
        \mbox{~if~$n_1 \neq n_2$} \\
\ms{E[<(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\tv]}{\rho} 
        \mbox{~if~$n_1 < n_2$} \\
\ms{E[<(\nv{n_1},\nv{n_2})]}{\rho} &\standard& \ms{E[\fv]}{\rho} 
        \mbox{~if~$n_1 \geq n_2$} \\
\ms{E[o(v,\divz)]}{\rho} &\standard& \ms{E[\divz]}{\rho} \\
\ms{E[o(\divz,e)]}{\rho} &\standard& \ms{E[\divz]}{\rho} \\
\\
\ms{E[\ife{\tv}{e_1}{e_2}]}{\rho} &\standard& \ms{E[e_1]}{\rho} \\
\ms{E[\ife{\fv}{e_1}{e_2}]}{\rho} &\standard& \ms{E[e_2]}{\rho} \\
\ms{E[\ife{\divz}{e_1}{e_2}]}{\rho} &\standard& \ms{E[\divz]}{\rho} 
\end{array}\]

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{Type Safety}
\label{ts}

Type safety means that if a program typechecks then its evaluation
cannot get stuck. Thus what we wish to guarantee is that the
evaluation of a program $p$ of a type $t$ can only result in one of
the following cases:
\begin{itemize}
\item a proper value $v^*$ of type $t$,
\item an exception $\divz$, or
\item an infinite loop.
\end{itemize}

To understand the proof strategy, consider the case of a program $p$
of type $t$ evaluating to a proper value $v^*$ in a million
transitions. To relate the initial program and its type to the value
$v^*$, it is natural to proceed one transition at a time. If we can
prove that each transition preserves the type of the expression, and
that well-typed states can always make progress until they become
final states, then we can conclude our main result by induction on the
number of transitions. This is the gist of our proof technique.

Here is the statement of the proof of type safety. Prove the theorem
as well as any supporting lemmas you might need.

\begin{theorem}[Type Safety]
\label{tst}
If $\vdash e : t_f$ and $e \standard^* v$, then $v$ is of type
$t_f$. (Note that our definition of values includes the $\divz$
exception which has every type.)
\end{theorem}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\end{document}
