\documentclass[11pt]{article}
\usepackage{palatino}
\usepackage{latexsym}
\usepackage{verbatim}
\usepackage{amsmath,proof,amsthm,amssymb,enumerate}

\newcommand{\question}[2]
  {\bigskip \noindent
   {\bf Question #1} (#2 points).}

\newcommand{\extracreditquestion}[1]
  {\bigskip \noindent
   {\bf Question #1} (EXTRA CREDIT).}

\newcommand{\definition}[2]
  {\bigskip
   \begin{tabular}{p{1.5in}p{4.0in}}
        \textbf{#1} & #2 \\
        \end{tabular}
  }

\def\prop{\textsf{\,\,prop}}
\def\thm{\textsf{\,\,thm}}
\def\implies{\Rightarrow}

\title{Assignment 1: \\
       Grammars and Induction}
\author{15-312: Foundations of  Programming Languages \\
        Daniel Spoonhower ({\tt spoons+@cs.cmu.edu})}
\date{Out: Thursday, August 28, 2003 \\
Due: Thursday, September 4, 2003 (1:30 pm) \\[1em]
50 points total}

\begin{document}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}

\maketitle

Welcome to 15-312!  This assignment focuses on context-free grammars and
inductive proofs.  It is due September 4$^{th}$ at the start of lecture.  You
are encouraged, but not required, to typeset your answers; if you write them
out by hand, write legibly.  If I can't read it, I can't give credit for it.

Please make sure you understand the policy on collaboration; refer to
$$\texttt{http://www.cs.cmu.edu/\char"7Efp/courses/312/assignments.html}$$


% \clearpage

\section{Grammars (35 points)}

\newcommand{\lp}{\texttt{(}\,}
\newcommand{\rp}{\texttt{)}\,}
\newcommand{\R}{\mathcal{R}}
\newcommand{\wb}{\,\,\,\texttt{wb}}

\newcommand{\arr}{\:\texttt{->}\:}
\newcommand{\base}{\textsf{base}}
\newcommand{\tycon}{\textsf{tycon}}
\newcommand{\type}{\textsf{type}}

\newcommand{\goesto}{\Rightarrow}

Consider the grammar $G$ over the alphabet $\Sigma = \{ \texttt{int},
\texttt{list}, \arr, \lp, \rp \}$ with nonterminals $\tycon$ and $\type$:

\begin{align*}
  \tycon &::= \texttt{int} ~|~ \tycon~\texttt{list} ~|~ \lp \type \rp \\
  \type &::= \tycon ~|~ \type \arr \type 
\end{align*}

\question{1.1}{5}
\begin{quote}
The first production for $\tycon$ can be written in rule notation as
$$
\infer{\texttt{int}~\tycon}
   {}
$$
Write grammar $G$ in rule notation.
\end{quote}

Grammar $G$ is flawed: it does not pin down the associativity
of $\arr$.  For example, there are two different derivations of the
string $\texttt{int} \arr \texttt{int} \arr \texttt{int}$.
We can fix the ambiguity by changing the second production of $\type$ from
\begin{align*}
     \type &::= \type \arr \type
\end{align*}
to
\begin{align*}
     \type &::= \tycon \arr \type
\end{align*}

Making this change results in the grammar $G'$ below.
To avoid confusion, we rename $\tycon$ to $\tycon'$ and $\type$ to $\type'$.
\begin{align*}
  \tycon' &::= \texttt{int} ~|~\tycon'~\texttt{list} ~|~ \lp \type' \rp \\
  \type' &::= \tycon' ~|~ \tycon' \arr \type'
\end{align*}

\question{1.2}{5}
\begin{quote}
    Write grammar $G'$ in rule notation.
\end{quote}

Note, however, that we have not shown that this new grammar $G'$ is equivalent
to $G$, that is, that the languages of $\type$ and $\type'$ are the same:
$L(\type) = L(\type')$.  This can be proved in two steps: first prove
$L(\type') \subseteq L(\type)$, then prove $L(\type) \subseteq L(\type')$.

\question{1.3}{10}
\begin{quote}
  Prove $L(\type') \subseteq L(\type)$ by proving
  \begin{quote}
      If $s~\type'$
       then $s~\type$
  \end{quote}
  by induction.  If you
  need to generalize the induction hypothesis, be sure to clearly
  state your generalized induction hypothesis.  If you need any
  lemmas, state them explicitly and prove them.
\end{quote}

\question{1.4}{15}
\begin{quote}
   Prove $L(\type) \subseteq L(\type')$ by proving
  \begin{quote}
      If $s~\type$
       then $s~\type'$
  \end{quote}
   As in the previous question, clearly state any generalized
induction hypothesis and prove any lemmas you need.
\end{quote}

\section{Propositional logic (15 points)}

In this question we will look at a subset of \emph{Propositional Logic}. Our
universe of terms consists of an infinite number of nullary operators {$P_0,
P_1, \ldots, P_n$} (``propositional variables'') and the binary operator
$\implies$ (``implication''). We define the sets $\! \prop$ and $\! \thm$ over
this universe:

\setlength{\tabcolsep}{0.10in}
\renewcommand{\arraystretch}{3}

\bigskip

\begin{tabular}{l l}
\infer[\textit{Var}]{P_i \prop}{}

&

\infer[K]{A \implies (B \implies A) \thm}
   {A \prop & B \prop}

\\

\infer[\textit{Imp}]{A \implies B \prop}
    {A \prop & B \prop}

&

\infer[S]{(A \implies (B \implies C)) \implies (A \implies B) \implies (A \implies C) \thm}
   {A \prop & B \prop & C \prop}

\\
&
\infer[App]{B \thm}
   {A \implies B \thm & A \thm}

\end{tabular}
\renewcommand{\arraystretch}{1}

\noindent \emph{Truth Value.}
If we have assignments (to \texttt{true} or
\texttt{false}) for all of the propositional variables in a
proposition, its truth value (either \texttt{true} or \texttt{false})
can be computed recursively using the following familiar truth table
for $\implies$:

   \[
    \begin{tabular}{|l|l|}
    \hline
    \textbf{Proposition} & \textbf{Truth Value} \\
    \hline
    $\texttt{false} \implies \texttt{false}$ & \texttt{true} \\
    \hline
    $\texttt{false} \implies \texttt{true}$ & \texttt{true} \\
    \hline
    $\texttt{true} \implies \texttt{false}$ & \texttt{false} \\
    \hline
    $\texttt{true} \implies \texttt{true}$ & \texttt{true} \\
    \hline
    \end{tabular}
   \]

\noindent \emph{Tautology.}
A proposition is a tautology iff for every
assignment of truth values (\texttt{true}, \texttt{false}) to the
propositional variables $P_0, \ldots, P_n$, the truth value of the
proposition is \texttt{true}.


\question{2.1}{15}
\begin{quote}
  Prove, using rule induction, that if $A \thm$ then $A$ is a tautology.
\end{quote}

\extracreditquestion{2.2}
\begin{quote}
  Find a proposition $A$ that is a tautology, but not a theorem (that
is, the judgment $A \thm$ cannot be derived).  You do not need to prove
that it is not a theorem!
\end{quote}

\end{document}
