hw01-student.tex

\documentclass[11pt]{exam}
\usepackage[margin=1in]{geometry}
\usepackage{amsmath,amsthm,amssymb}
\usepackage{mathptmx}
\usepackage{mathpartir} %% for inference rules

\title{Assignment 1: \\
       Dynamics and Statics for a Simple Language}
\date{Due: Friday, September 22, 2023}

%% Number questions by section
%\renewcommand{\thequestion}{\thesection.\arabic{question}}

\newcommand{\Lnumstr}{\textbf{\textsf{E}}}
\newcommand{\val}[1]{\ensuremath{#1~\textsf{val}}}
\newcommand{\num}[1]{\texttt{num}[#1]}
\newcommand{\str}[1]{\texttt{str}[#1]}
\newcommand{\plus}[2]{\texttt{plus}(#1; #2)}
\newcommand{\mult}[2]{\texttt{times}(#1; #2)}
\newcommand{\divexp}[2]{\texttt{div}(#1; #2)}
\newcommand{\cat}[2]{\texttt{cat}(#1; #2)}
\newcommand{\len}[1]{\texttt{len}(#1)}
\newcommand{\abst}[2]{#1.#2}
\newcommand{\letbind}[3]{\texttt{let}(#1; \abst{#2}{#3})}
\newcommand{\steps}[2]{\ensuremath{#1 \longmapsto #2}}
\newcommand{\reduces}[2]{\ensuremath{#1 \longmapsto^\ast #2}}
\newcommand{\eval}[2]{\ensuremath{#1 \Downarrow #2}}
\newcommand{\subst}[3]{[#1/#2]#3}
\newcommand{\err}[1]{\ensuremath{#1~\textsf{err}}}

\newcommand{\proves}{\vdash}
\newcommand{\hasType}[2]{#1 : #2}
\newcommand{\typeJ}[3]{#1 \proves \hasType{#2}{#3}}
\newcommand{\ctx}{\Gamma}
\newcommand{\xCtx}[2]{\ctx, \hasType{#1}{#2}}
\newcommand{\typeJC}[2]{\typeJ{\ctx}{#1}{#2}}
\newcommand{\numt}{\texttt{num}}
\newcommand{\strt}{\texttt{str}}

\pagestyle{plain}
\begin{document}
\author{YOUR NAME\thanks{YOUR COLLABORATORS AND ACKNOWLEDGMENTS}}
\maketitle

\begin{questions}
  % 1
\question  

  % 2 
\question  

  % 3
\question  

  % 4
\question  

  % 5
\question  

  % 6
\question  

\end{questions}  

%% Appendix
\clearpage
\appendix

\section{Dynamics of \Lnumstr}

\noindent
\fbox{\inferrule{}{\val{e}}}
\begin{mathpar}
\inferrule{ }
          {\val{\num{n}}}

\inferrule{ }
		  {\val{\str{s}}}
\end{mathpar}
\fbox{\inferrule{}{\steps{e}{e'}}}
\begin{mathpar}
\inferrule{ }{
	\steps{\plus{\num{n_1}}{\num{n_2}}}{\num{n_1 + n_2}}
}

\inferrule{
	\steps{e_1}{e_1'}
}{
	\steps{\plus{e_1}{e_2}}
		  {\plus{e_1'}{e_2}}
}

\inferrule{
	\steps{e_2}{e_2'}
}{
	\steps{\plus{\num{n_1}}{e_2}}
		  {\plus{\num{n_1}}{e_2'}}
}

\inferrule{ }{
	\steps{\mult{\num{n_1}}{\num{n_2}}}{\num{n_1 \cdot n_2}}
}

\inferrule{
	\steps{e_1}{e_1'}
}{
	\steps{\mult{e_1}{e_2}}
		  {\mult{e_1'}{e_2}}
}

\inferrule{
	\steps{e_2}{e_2'}
}{
	\steps{\mult{\num{n_1}}{e_2}}
		  {\mult{\num{n_1}}{e_2'}}
}

\inferrule{ }{
	\steps{\cat{\str{s_1}}{\str{s_2}}}{\str{s_1 \text{\textasciicircum} s_2}}
}

\inferrule{
	\steps{e_1}{e_1'}
}{
	\steps{\cat{e_1}{e_2}}
		  {\cat{e_1'}{e_2}}
}

\inferrule{
	\steps{e_2}{e_2'}
}{
	\steps{\cat{\str{s_1}}{e_2}}
		  {\cat{\str{s_1}}{e_2'}}
}

\inferrule{ }{
	\steps{\len{\str{s}}}{\num{|s|}}
}

\inferrule{
	\steps{e}{e'}
}{
	\steps{\len{e}}{\len{e'}}
}

\inferrule{\val{e_1}}{
	\steps{\letbind{e_1}{x}{e_2}}{\subst{e_1}{x}{e_2}}
}

\inferrule{
	\steps{e_1}{e_1'}
}{
	\steps{\letbind{e_1}{x}{e_2}}
		  {\letbind{e_1'}{x}{e_2}}
}
\end{mathpar}
\fbox{\inferrule{}{\err{e}}}
\begin{mathpar}
\inferrule{ }{
	\err{\plus{\str{s}}{e_2}}
}

\inferrule{ }{
	\err{\plus{\num{n}}{\str{s}}}
}

\inferrule{
	\err{e_1}
}{
	\err{\plus{e_1}{e_2}}
}

\inferrule{
	\err{e_2}
}{
	\err{\plus{\num{n}}{e_2}}
}

\inferrule{ }{
	\err{\mult{\str{s}}{e_2}}
}

\inferrule{ }{
	\err{\mult{\num{n}}{\str{s}}}
}

\inferrule{
	\err{e_1}
}{
	\err{\mult{e_1}{e_2}}
}

\inferrule{
	\err{e_2}
}{
	\err{\mult{\num{n}}{e_2}}
}

\inferrule{ }{
	\err{\cat{\num{n}}{e_2}}
}

\inferrule{ }{
	\err{\cat{\str{s}}{\num{n}}}
}

\inferrule{
	\err{e_1}
}{
	\err{\cat{e_1}{e_2}}
}

\inferrule{
	\err{e_2}
}{
	\err{\cat{\str{s}}{e_2}}
}

\inferrule{ }{
	\err{\len{\num{n}}}
}

\inferrule{\err{e}}{
	\err{\len{e}}
}

\inferrule{\err{e_1}}{
	\err{\letbind{e_1}{x}{e_2}}
}
\end{mathpar}
\fbox{\inferrule{}{\eval{e}{e'}}}
\begin{mathpar}
\inferrule{ }{
	\eval{\num{n}}{\num{n}}
}

\inferrule{ }{
	\eval{\str{s}}{\str{s}}
}

\inferrule{
	\eval{e_1}{\num{n_1}}\\
	\eval{e_2}{\num{n_2}}
}{
	\eval{\plus{e_1}{e_2}}{\num{n_1 + n_2}}
}

\inferrule{
	\eval{e_1}{\num{n_1}}\\
	\eval{e_2}{\num{n_2}}
}{
	\eval{\mult{e_1}{e_2}}{\num{n_1 \cdot n_2}}
}

\inferrule{
	\eval{e_1}{\str{s_1}}\\
	\eval{e_2}{\str{s_2}}
}{
	\eval{\cat{e_1}{e_2}}{\str{s_1 s_2}}
}

\inferrule{
	\eval{e}{\str{s}}\\
  |s| = n
}{
	\eval{\len{e}}{\num{n}}
}

\inferrule{
	\eval{e_1}{e_1'}\\
	\eval{\subst{e_1'}{x}{e_2}}{e_2'}
}{
	\eval{\letbind{e_1}{x}{e_2}}{e_2'}
}
\end{mathpar}

\section{Statics of \Lnumstr}

\noindent\fbox{\inferrule{}{\typeJC{e}{\tau}}}
\begin{mathpar}
\inferrule{\hasType{x}{\tau} \in \ctx}{
	\typeJC{x}{\tau}
}

\inferrule{ }{
	\typeJC{\num{n}}{\numt}
}

\inferrule{ }{
	\typeJC{\str{s}}{\strt}
}

\inferrule{
	\typeJC{e_1}{\numt}\\
	\typeJC{e_2}{\numt}
}{
	\typeJC{\plus{e_1}{e_2}}{\numt}
}

\inferrule{
	\typeJC{e_1}{\numt}\\
	\typeJC{e_2}{\numt}
}{
	\typeJC{\mult{e_1}{e_2}}{\numt}
}

\inferrule{
	\typeJC{e_1}{\strt}\\
	\typeJC{e_2}{\strt}
}{
	\typeJC{\cat{e_1}{e_2}}{\strt}
}

\inferrule{
	\typeJC{e}{\strt}
}{
	\typeJC{\len{e}}{\numt}
}

\inferrule{
	\typeJC{e_1}{\tau_1}\\
	\typeJ{\xCtx{x}{\tau_1}}{e_2}{\tau_2}
}{
	\typeJC{\letbind{e_1}{x}{e_2}}{\tau_2}
}
\end{mathpar}

\end{document}