\documentclass{article}
\usepackage[margin=1in]{geometry}
\usepackage{microtype}
\usepackage{fancyhdr}
\usepackage{amsmath}
\usepackage{mathtools}
\usepackage{mathpartir}
\pagestyle{fancy}
\fancyhf{}
\lhead{CS 225: Programming Languages}
\rhead{UVM, Spring 2018}
\setlength\arraycolsep{0pt}
\begin{document}
\thispagestyle{fancy}
\begin{center}
\Large{Homework 1} \\ \ \\ \normalsize{Due: Friday, Jan 26, 11:59pm}
\end{center}
\subsubsection*{Preface}
Discussing high-level approaches to homework problems with your peers is
encouraged. You must include at the top of your assignment a Collaboration
Statement which declares any other people with whom you discussed homework
problems. For example:
\begin{quote}\em
Collaboration Statement: I discussed problems 1 and 3 with Jamie Smith. I
discussed problem 2 with one of the TAs. I discussed problem 4 with a
personal tutor.
\end{quote}
If you did not discuss the assignment with anyone, you still must declare:
\begin{quote}\em
Collaboration Statement: I did not discuss homework problems with anyone.
\end{quote}
Copying answers or doing the work for another student is not allowed.
Assignment problems which refer to ``Exercise X'' or ``Figure Y'' are referring
to those found in the Types and Programming Languages textbook.
\subsubsection*{Submitting}
Prepare your assignment as either handwritten or using LaTeX. \textbf{I will
not accept homework assignments written in Word, Google Docs, or using any
other text processing software.} Handwritten assignments must be written neatly
or they will receive a 0 grade. Submit the assignment either (1) via scanned
pdf email to me: David.Darais@uvm.edu with ``CS 225 HW1'' in the subject line,
or (2) placed under my office door (Votey~319) at any hour before the deadline.
\subsubsection*{Problem 1 (15 points)}
Recall the definition for the divides relation:
\[ \text{divides} \coloneqq \{ \langle n,m \rangle \mid \exists o\ \textit{s.t.}\ n \times o = m \} \]
Prove formally---and in as much detail as possible---that the divides relation
is transitive, that is:
\[ \text{forall}\ n\ m\ o, \text{if}\ n\ \text{divides}\ m\ \text{and}\ m\ \text{divides}\ o,\ \text{then}\ n\ \text{divides}\ o \]
You may assume basic algebraic arithmetic facts like $n+n=2n$ and $2(n+n) =
2n+2n$. Use the example proof of reflexivity given in class as a guide for the
level of detail you should strive for.
\subsubsection*{Problem 2 (10 points)}
Consider the set of boolean arithmetic terms $\mathcal{T}$ and metafunctions leaves (new) and depth (from Definition 3.3.2):
\[ \begin{array}{l}
t \in \mathcal{T} \Coloneqq T \mid F \mid \texttt{if}\ t\ \texttt{then}\ t\ \texttt{else}\ t
\\
\\ \text{leaves}(T) \coloneqq 1
\\ \text{leaves}(F) \coloneqq 1
\\ \text{leaves}(\texttt{if}\ t_1\ \texttt{then}\ t_2\ \texttt{else}\ t_3)
\coloneqq \text{leaves}(t_1) + \text{leaves}(t_2) + \text{leaves}(t_3)
\\
\\ \text{depth}(T) \coloneqq 1
\\ \text{depth}(F) \coloneqq 1
\\ \text{depth}(\texttt{if}\ t_1\ \texttt{then}\ t_2\ \texttt{else}\ t_3)
\coloneqq \text{max}(\text{depth}(t_1),\text{depth}(t_2),\text{depth}(t_3)) + 1
\end{array}
\]
Define some term $t \in \mathcal{T}$ such that $\text{leaves}(t) = 7$ and $\text{depth}(t) = 3$.
\subsubsection*{Problem 3 (25 points)}
Either prove by structural induction that $\text{leaves}(t)$ always produces an
odd number, or give a counter-example which shows $\text{leaves}(t)$ can produce
an even number.
\subsubsection*{Problem 4 (15 points)}
Draw a derivation tree which justifies the following relationship:
\begin{gather*}
\texttt{if}
\ (\texttt{if}
\ (\texttt{if}\ F\ \texttt{then}\ F\ \texttt{else}\ T)
\ \texttt{then}\ T
\ \texttt{else}\ F)
\ \texttt{then}\ T
\ \texttt{else}\ F
\\ \longrightarrow
\\
\texttt{if}
\ (\texttt{if}
\ T
\ \texttt{then}\ T
\ \texttt{else}\ F)
\ \texttt{then}\ T
\ \texttt{else}\ F
\end{gather*}
\subsubsection*{Problem 5 (30 points)}
Consider the extended small-step semantics described in Exercise 3.5.16 which
explicitly generates the value ``\texttt{wrong}'' in place of where the
semantics from Figure 3-2 gets stuck.
\begin{enumerate}
\item
Design a big-step semantics $t \Downarrow a$ (similar to 3.5.17) which is
equivalent to this small-step semantics.
\item
Prove that your new big-step semantics implies the small-step semantics which
generates ``\texttt{wrong}'', that is, prove:
\[ \textit{forall}\ t\ a,
\ \textit{if}\;\;t \Downarrow a\;\;\textit{then}\;\;t \longrightarrow^* a
\]
This proof need not be as detailed as your answer to Problem~1, but still
must be a convincing formal proof.
\end{enumerate}
You should use the following syntactic categories for terms $t$, numeric values
$nv$, values $v$, and answers $a$:
\[ \begin{array}{rcrcl}
t {}&{} \in {}&{} \mathcal{T} {}&{} \Coloneqq {}&{} T \mid F \mid \texttt{if}\ t\ \texttt{then}\ t\ \texttt{else}\ t
\\ {}&{} {}&{} {}&{} \mid {}&{} 0 \mid \texttt{succ}\ t \mid \texttt{pred}\ t \mid \texttt{iszero}\ t
\\ {}&{} {}&{} {}&{} \mid {}&{} \texttt{wrong}
\\
\\ nv {}&{} \in {}&{} \mathcal{NV} {}&{} \Coloneqq {}&{} 0 \mid \texttt{succ}\ nv
\\ v {}&{} \in {}&{} \mathcal{V} {}&{} \Coloneqq {}&{} T \mid F \mid nv
\\ a {}&{} \in {}&{} \mathcal{A} {}&{} \Coloneqq {}&{} v \mid \texttt{wrong}
\
\end{array}
\]
\subsubsection*{Extra Credit (15 points)}
Prove the other direction of Problem 5, that is:
\[ \textit{forall}\ t\ a,
\ \textit{if}\;\;t \longrightarrow^* a\;\;\textit{then}\;\;t \Downarrow a
\]
\subsubsection*{Problem 6 (5 points)}
Approximately how many hours did you spend working on this assignment?
\end{document}