\gdef\lecturenumber{a2}
\gdef\subsectioncounters{1}
\input preamble.tex
\newcommand{\blanks}[1]{\ensuremath{\dashuline{\hspace{#1}}}}
\begin{document}
\date{due: Tuesday, 5 February 2019}
\Chapter{\vspace*{-2ex}Assignment 2}
\textbf{Name:}\hspace*{220pt}
\textbf{Estimated time spent:}
\vspace*{4.5ex}
Submit your modified \texttt{a2.rkt} by email (joshuad@cs.queensu.ca)
as \texttt{a2-\textit{yourname}.rkt}.
\textbf{Please} fill in the ``Estimated time spent'' (above). Your answer will not change your mark,
but helps me to design reasonable assignments.
\section{Language Extension}
\label{sec:lang-ext}
Consider the following language, defined by a grammar and a big-step evaluation judgment.
The big-step evaluation given is incomplete, in the informal sense that it has no rules saying how to evaluate
$\absexp{e}$.
\begin{grammar}
integers & $n$
\\
values & $v$ &\bnfas& $n$
\\
expressions & $e$ &\bnfas&
$
n
\bnfaltBRK
\plusexp{e_1}{e_2}
\bnfaltBRK
\absexp{e}
$
\end{grammar}
\medskip
\judgbox{e \down v}{expression $e$ evaluates to value $v$}
\vspace*{-1.2ex}
\begin{mathpar}
\Infer{eval-const}
{}
{n \down n}
\and
\Infer{eval-add}
{
e_1 \down n_1
\\
e_2 \down n_2
}
{\plusexp{e_1}{e_2} \down n_1 + n_2}
\end{mathpar}
{\noindent \textbf{Question 1(a).}}
Roughly following the structure of eval-add, design a rule ``eval-abs'' such that
$\absexp{e}$ will compute the absolute value of $e$. Similar to how we used the
standard notation for addition, $n_1 + n_2$, in eval-add, you may use
the notation $|n|$ for the absolute value of $n$.
\[
\Infer{eval-abs}
{
% comment out next line by inserting % at the beginning,
% then add your solution just before the `}'
\hspace*{220pt}
}
{
\absexp{e} \down
% add your solution here (TeX doesn't care about line breaks UNLESS they are repeated)
%
\hspace*{20pt}}
\]
\textbf{Question 1(b).}
Extend the Racket code a2.rkt (which is nearly identical to the expr1.rkt file
that I showed in lecture) to support the construct \absexp{e}:
\begin{enumerate}[(i)]
\item Add a ``variant'' (also called a ``constructor'')
for $\absexp{e}$
to the \textvtt{define-type} declaration.
This will cause Racket to yell at you, because EXPR will then have three variants
instead of two, which makes the \textvtt{type-case} in \texttt{big-step} become incomplete.
The simplest fix (until you extend \texttt{big-step}, below)
is to add an \textvtt{else} branch to the \textvtt{type-case} that uses \texttt{error}.
\item Extend the procedure \texttt{parse} so that it accepts S-expressions that match the production
$\absexp{e}$ in our grammar, and returns your \texttt{Abs} variant.
Write at least two test cases for \texttt{parse} that involve absolute value.
\item Extend the procedure \texttt{big-step} to support absolute value, following your rule eval-abs.
Note that the Racket standard library has a procedure \texttt{abs}.
Write at least three test cases for \texttt{big-step} that involve absolute value.
\end{enumerate}
\clearpage
\section{Proof techniques}
These questions are not about complete proofs.
In some of the questions, the conjecture is not even true, or you
have not been given enough information to do a complete proof.
Instead, they ask you to make progress on several different proofs
by using a specific proof technique.
In all of these questions, the grammar of expressions is the \emph{extended}
grammar (\Sectionref{sec:lang-ext}), and the system of rules deriving $e \down v$ includes the \emph{three} rules eval-const, eval-add, eval-abs.
\textbf{Question 2(a).}
Using the extended grammar of expressions (\Sectionref{sec:lang-ext}),
list the cases produced by \emph{case analysis on $e$}.
The cases must correspond to the grammar.
Do not attempt to complete the cases to show $e' = e''$.
\begin{conjecture*} ~\\
For all expressions $e$, $e'$ and $e''$, \\
if $e \step e'$ and $e \step e''$ \\
then $e' = e''$.
\end{conjecture*}
\begin{proof}
Consider cases of $e$.
\begin{itemize}
\item Case
\end{itemize}
\vspace*{10ex}
\end{proof}
\textbf{Question 2(b).}
In this question, your goal is to derive
\[
\plusexp{0}{\plusexp{e_{21}}{e_{22}}} \down 0
\]
The following are given. Use equations (and the fact that $0 + 0 = 0$)
and apply the rules eval-const, eval-add to
derive the goal.
\begin{llproof}
\Pf{}{}{e_{21} \down n_{21}} {Given}
\Pf{}{}{e_{22} \down n_{22}} {Given}
\Pf{}{}{n_{21} = 0} {Given}
\Pf{}{}{n_{22} = 0} {Given}
\Pf{}{}{\hspace*{150pt}} {}
\end{llproof}
\vspace*{20ex}
\clearpage
\textbf{Question 2(c).}
In this question, use \emph{inversion}: write down all the facts given by inverting
on rule eval-abs. (I can't give you a specific goal because what you get depends on your rule, eval-abs.)
\begin{llproof}
\Pf{}{}{\absexp{e_1} \down n_1} {Given}
\Pf{}{}{\hspace*{150pt}} {}
~\\
~\\
\end{llproof}
\textbf{Question 2(d).}
This question uses notation you have never seen,
but it can still be answered.
\begin{conjecture*} ~\\
For all $\C$, $M_1$, $M_2$ and $\Dee_1$ such that
$\Dee_1$ derives $M_1 \stepR M_2$,
\\
there exists $\Dee_2$ such that
$\Dee_2$ derives $\C[M_1] \stepR \C[M_2]$.
\end{conjecture*}
\begin{itemize}
\item Suppose that I suggest you use structural induction on $\Dee_1$.
Write the appropriate induction hypothesis:
\vspace*{80pt}
\item Suppose that I suggest you use structural induction on $M_1$.
Write the appropriate induction hypothesis (using the subexpression
ordering $\prec$ for $M_1$):
\vspace*{80pt}
\end{itemize}
\clearpage
\section{Typing}
\begin{grammar}
types & $A$ &\bnfas& $\Int$
\end{grammar}
\judgbox{e : A}{expression $e$ has type $A$}
\begin{mathpar}
\Infer{type-const}
{}
{n : \Int}
\and
\Infer{type-abs}
{e : \Int
}
{\absexp{e} : \Int}
\and
\Infer{type-add}
{e_1 : \Int
\\
e_2 : \Int
}
{\plusexp{e_1}{e_2} : \Int}
\end{mathpar}
This is not a terribly interesting type system: every possible expression has the same type, $\Int$. Prove the following conjecture:
\begin{conjecture} ~\\
For all expressions $e$, \\
it is the case that $e : \Int$.
\end{conjecture}
\begin{proof}
By structural induction on $e$. [The only thing given is $e$; we are trying to construct the derivation of $e : \Int$, but it doesn't exist yet. So we have to induct on $e$.]
\textbf{Induction hypothesis:}
For all expressions $e'$ such that $e' \prec e$, it is the case that $e' : \Int$.
\vfill
\end{proof}
\end{document}
% Local Variables:
% TeX-master: "a2"
% End: