\documentclass{article}
\begin{document}

\newcommand{\ba}{\[\begin{array}{rcl}}
\newcommand{\ea}{\end{array}\]}
\newcommand{\bnf}{\ |\ }
\renewcommand{\t}{\tau}
\newcommand{\intt}{\mathsf{int}}
\newcommand{\boolt}{\mathsf{bool}}
\newcommand{\arr}{\rightarrow}
\newcommand{\te}{\mathtt{true}}
\newcommand{\fe}{\mathtt{false}}
\renewcommand{\l}{\lambda}
\newcommand{\x}{x}
\newcommand{\ife}[3]{\mathtt{if}~#1~\mathtt{then}~#2~\mathtt{else}~#3}
\newcommand{\fixe}[1]{\mathtt{fix}~#1}
\newcommand{\erre}{\mathtt{error}}

\setlength{\topmargin}{-1.5 in}

\title{B522: Assignment 3}
\date{}
\maketitle

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\vspace{-2cm}
\section{A Small Functional Language}

Syntax:
\ba
o &::=& + \bnf \star \bnf - \bnf / \bnf = \bnf < \bnf \\
\t &::=& \intt \bnf \boolt \bnf \t\arr\t \\
e &::=& x \bnf n \bnf o(e_1,\cdots,e_n) \bnf \te \bnf \fe \bnf \\
&& \ife{e}{e_1}{e_2} \bnf \l\x.e \bnf e_1e_2 \\
&& \fixe{\x.e} \bnf \erre \\
v &::=& x \bnf n \bnf \te \bnf \fe \bnf \l\x.e 
\ea

\noindent Reduction rules:
\ba
+(n_1,n_2) &\arr& n \mbox{~where $n$ is the sum of $n_1$ and $n_2$} \\
\star(n_1,n_2) &\arr& n \mbox{~where $n$ is the product of $n_1$ and $n_2$} \\
-(n_1,n_2) &\arr& n \mbox{~where $n$ is the difference of $n_1$ and $n_2$} \\
/(n_1,n_2) &\arr& n \mbox{~where $n$ is the quotient of $n_1$ and $n_2$} \\
/(n,0) &\arr& \erre \\
=(n,n) &\arr& \te \\
=(n_1,n_2) &\arr& \fe \mbox{~if $n_1$ and $n_2$ are different} \\
<(n_1,n_2) &\arr& \te \mbox{~if $n_1$ is less than $n_2$} \\
<(n_1,n_2) &\arr& \fe \mbox{~if $n_1$ is not less than $n_2$} \\
\ife{\te}{e_1}{e_2} &\arr& e_1 \\
\ife{\fe}{e_1}{e_2} &\arr& e_2 \\
(\l\x.e)v &\arr& e[v/x] \\
\fixe{\x.e} &\arr& e[\l\x.(\fixe{\x.e})x/x] \\
\ \\
o(v_1,\cdots,\erre,e_i,\ldots) &\arr& \erre \\
\ife{\erre}{e_1}{e_2} &\arr& \erre \\
\erre~e &\arr& \erre \\
v~\erre &\arr& \erre
\ea

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\section{To do}

\begin{itemize}
\item Design a type system for the language

\item Complete the formalization of the evaluation by defining evaluation
contexts

\item \emph{State only} the type soundness property

\item \emph{Prove} the interesting cases needed to establish subject
reduction.
\end{itemize}

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

\end{document}
