\documentclass[11pt]{article}
\usepackage{fullpage}
\usepackage{type1cm}
\usepackage{longtable}
\usepackage{amsmath,proof,amssymb}

\newcommand\comment[1]{}

\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}
  }

\newtheorem{theorem}{Theorem}


\newcommand\tx[1]{\mbox{\textrm{#1}}}
\newcommand\alt{\,\,|\,\,}
\DeclareMathOperator\sinn{\texttt{in}}
\DeclareMathOperator\slet{\texttt{let}}
\DeclareMathOperator\send{\texttt{end}}
\DeclareMathOperator\fv{\texttt{FV}}

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

\DeclareMathOperator\ok{\mathrel:\texttt{int}}

\newcommand\INT{\texttt{int}}
\newcommand\G{\Gamma}

\title{Assignment 1: Induction}
\author{15-312: Foundations of Programming Languages \\
        Kevin Watkins ({\tt kw@cmu.edu})}
\date{Out: Thursday, 20 Jan 2005 \\
      Due: Thursday, 27 Jan 2005 {\bf (10:30 am)} \\[1em]
      50 points total}

\begin{document}

\maketitle

Welcome to 15-312! This assignment is intended to give you exercise
with the kind of thinking that we'll do in this course. You are
encouraged, but not required, to typeset your answers; if you write by
hand, write legibly. The assignment is due at the \emph{beginning of
lecture} on Thursday, January 27.

Credit in this assignment will reflect the clarity and mathematical
rigor with which you present your arguments. A proof should be
self-evident. Although some things may seem obvious, please take care
to be precise and complete.

Be sure that what you say in your proof is correct. {\bf Less credit} will be given for incorrect steps than for missing steps. You will receive more points turning in an explanation of your strategy and leaving blank parts where you couldn't finish the proof, than turning in a complete proof with incorrect steps.

Of course, if you have any questions, feel free to e-mail Kevin Watkins
({\tt kw@cmu.edu}) or come to office hours!

\textbf{All work must be your own.} Please read the collaboration policy at
$$\texttt{http://www.cs.cmu.edu/\char"7Ecrary/312/assignments.html}$$


\clearpage

\section{Higher-order abstract syntax (5 points)}

In recitation we saw higher-order abstract syntax for the integral operator $\int_a^b e\;dx$ of calculus.

\question{1.1}{5}
\begin{quote}
  Using our standard notations for higher-order abstract syntax with names: \[
    op(e_1,\dots,e_n),\quad x,\quad x.e,
  \]
  fill in the rest of a grammar for a language of calculus expressions including operators for $e_1 + e_2$, $e_1 \cdot e_2$, $\int_a^b e\;dx$, and $\sum_{i=a}^b e$. The first part is done for you:

\bigskip
\begin{tabular}{rcl}
  $e$ & $::=$ & $\mathrm{plus}(e_1, e_2) \mathrel| \dots$
\end{tabular}
\end{quote}

\extracreditquestion{1.2}
\begin{quote}
  Extend the grammar with higher-order abstract syntax for a derivative operator. (This is tricky!)
\end{quote}

\section{Substitution theorem (25 points)}

An important theorem of a programming language is the
\emph{substitution theorem}. Informally, it states that the result of
substitution of a well-typed term for a free variable of another
well-typed term is itself well-typed. In order to be able to state the
substitution theorem, we need a definition of well-typedness and a
definition of substitution. In class we wrote substitution as a partial function. Here we want to prove a property of substitution by rule induction, so we will define it by a judgment with inference rules instead.

\bigskip

Here are the judgments that we define:

\bigskip

\begin{tabular}{cp{4in}}
  $\G \vdash e : \INT$ & In the context $\G$, $e$ has type $\INT$ (the only type of our language). \\
  $\fv(e) = S$ & $S$ is the set of free variables in $e$. \\
  $\{e_1 / x\} e_2 = e_3$ & Substituting $e_1$ for free occurrences of $x$ in $e_2$ results in expression $e_3$. \\
\end{tabular}

\bigskip

Here is the grammar for our language:

\bigskip

\begin{tabular}{ccl}
 $\G$ & ::= & $\cdot \alt \G, x\ok$ \\
 $e$  & ::= & $k \alt e_1 + e_2 \alt x \alt \slet x = e_1 \sinn e_2 \send$ \\
 $k$  & ::= & $0 \alt 1 \alt \ldots \alt 45 \alt \ldots$ \\
 $x$  & ::= & (variables) \\
\end{tabular}

\clearpage

Here is the definition of well-formedness:


\[\begin{array}{cc}

\infer[\tx{var}]{\G,x\ok,\G'\vdash x\ok}{} &
\infer[\tx{num}]{\G \vdash k\ok}{} \\ \\

\infer[\tx{plus}]{\G\vdash e_1 + e_2\ok}{
  \G\vdash e_1\ok &
  \G\vdash e_2\ok
} &
\infer[\tx{let}]{\G\vdash \slet x = e_1 \sinn e_2 \send \ok}{
  \G\vdash e_1 \ok &
  \G,x\ok\vdash e_2 \ok
} \\ \\

\end{array}\]


Here are the definitions of free variables and substitution:


\[\begin{array}{ccc}

\infer[\tx{fv-var}]{\fv(x) = \{x\}}{} &
\infer[\tx{fv-num}]{\fv(k) = \{\}}{} & 
\infer[\tx{fv-plus}]{\fv(e_1 + e_2) = S_1 \cup S_2}{
  \fv(e_1) = S_1 &
  \fv(e_2) = S_2
} \\ \\

\multicolumn{3}{c}{
  \infer[\tx{fv-let}]{\fv(\slet x = e_1 \sinn e_2 \send) = S_1 \cup (S_2 - \{x\})}{
    \fv(e_1) = S_1 &
    \fv(e_2) = S_2
  }
}

\end{array}\]


\[\begin{array}{cc}

\infer[\tx{s-var=}]{\{e/x\}x = e}{} &
\infer[\tx{s-var}\neq]{\{e/x\}y = y}{x \neq y} \\ \\

\infer[\tx{s-plus}]{\{e/x\}(e_1 + e_2) = (e_1' + e_2')}{
  \{e/x\}e_1 = e_1' &
  \{e/x\}e_2 = e_2'
} &
\infer[\tx{s-num}]{\{e/x\}k = k}{} \\ \\

\multicolumn{2}{c}{
  \infer[\tx{s-let}]{\{e/x\}(\slet y = e_1 \sinn e_2 \send) =
                          (\slet y = e_1' \sinn e_2' \send)}{
    \fv(e) = S &
    y \notin S \cup\{x\} &
    \{e/x\} e_1 = e_1' &
    \{e/x\} e_2 = e_2'
  }
} \\ \\

\end{array}\]


In order to prove the substitution theorem, we will need two lemmas.
One, called \emph{weakening}, roughly states that if an
expression is well-typed in some context, we can add a variable to the
context and still have a well-typed term, \emph{as long as the new
variable is not one of the free variables of $e$}. Weakening depends
on the other lemma, called \emph{exchange}, which tells us that we
can swap the positions of two different variables anywhere in the
context.

\bigskip

Here is the statement of the lemmas and a model proof of weakening. In
the proof below, we write out each case and the steps we follow, alongside their justifications. (\textbf{wts} stands for ``\emph{want to
show}.'') You should follow this model when writing your own proofs.

\bigskip
\textbf{Lemma 1 (Exchange)}\,\,\,

\begin{tabular}{ll}
  If   & $\G,x\ok,y\ok,\G' \vdash e \ok$ \\
  and  & $x \neq y$ \\
  then & $\G,y\ok,x\ok,\G' \vdash e \ok$ \\
\end{tabular}

\bigskip

\textbf{Lemma 2 (Weakening)}\,\,\,

\begin{tabular}{ll}
  If & $\G \vdash e \ok$ \\
  and & $\fv(e) = S$ where $x \notin S$ \\ 
  then & $\G,x\ok \vdash e \ok$. \\
\end{tabular}

\clearpage

Proof of weakening is by induction on the derivation of $\G \vdash e$.

\begin{longtable}{lp{3in}r}

case & \multicolumn{2}{l}{\infer[\tx{var}]{\G,y\ok,\G'\vdash y \ok}{}} \\
\textbf{wts} & $\G,y\ok,\G',x\ok \vdash y \ok$ \\

\textbf{1} & $\fv(x) = \{x\}$ & \textbf{(fv-var)} \\
\textbf{2} & $y \neq x$ because $y \notin \{x\}$ & \textbf{(given)} \\
\, & $\G,y\ok,\G',x\ok \vdash y \ok$ & \textbf{(var)}\footnote{
We could have used this step directly. However, in a language with
more than one type (as most every language we will see after this
assignment) we want to make sure that the newly added variable doesn't
shadow the existing variable at a different type. Therefore, we show
here that the variables must be inequal, so that this proof looks more
like it would in a typed language.} \\ \\ \\

case & \multicolumn{2}{l}{\infer[\tx{num}]{\G \vdash k \ok}{}} \\
\textbf{wts} & $\G,x\ok \vdash k \ok$ \\

\, & $\G,x\ok \vdash k \ok$ & \textbf{(num)} \\ \\ \\

case & \multicolumn{2}{l}{\infer[\tx{plus}]{\G\vdash e_1 + e_2 \ok}{
    \G\vdash e_1 \ok &
    \G\vdash e_2 \ok
  }} \\
\textbf{wts} & $\G,x\ok \vdash e_1 + e_2 \ok$ \\
\textbf{1} & {\raggedright $\fv(e_1 + e_2) = S_1 \cup S_2$ 

where $\fv(e_1) = S_1$ and $\fv(e_2) = S_2$} & \textbf{(inversion on fv-plus)} \\
\textbf{2} & $x \notin S_1 \cup S_2$ & \textbf{(given)} \\
\textbf{3} & $x \notin S_1$ & \textbf{(defn $\notin$, 2)} \\
\textbf{4} & $\G,x\ok \vdash e_1 \ok$ & \textbf{(induction on left premise, 3)} \\
\textbf{5} & $x \notin S_2$ & \textbf{(defn $\notin$, 2)} \\
\textbf{6} & $\G,x\ok \vdash e_2 \ok$ & \textbf{(induction on right premise, 5)} \\
\, & $\G,x\ok \vdash e_1 + e_2 \ok$ & \textbf{(plus on 4,6)} \\ \\ \\

case & \multicolumn{2}{l}{\infer[\tx{let}]{\G\vdash \slet y = e_1 \sinn e_2 \send \ok}{
    \G\vdash e_1 \ok &
    \G,y\ok\vdash e_2 \ok
  }} \\
\textbf{wts} & $\G,x\ok \vdash \slet y = e_1 \sinn e_2 \send \ok$ \\
\textbf{1} & without loss of generality, say $x \neq y$ & \textbf{($\alpha$-eq)}\footnote{
  Here's a nice trick. Since we consider all $\alpha$-equivalent terms to be equal,
  we can simply choose $y$ not equal to $x$ and silently $\alpha$-vary the term to agree
  with our choice.} \\
\textbf{2} & {\raggedright $\fv(\slet y = e_1 \sinn e_2 \send) = S_1 \cup (S_2 - \{y\})$

where $\fv(e_1) = S_1$ and $\fv(e_2) = S_2$} & \textbf{(inversion on fv-let)} \\
\textbf{3} & $x \notin S_1 \cup (S_2 - \{y\})$ & \textbf{(given)} \\
\textbf{4} & $x \notin S_1$ & \textbf{(defn $\notin$, 3)} \\
\textbf{5} & $x \notin S_2$ & \textbf{(defn $\notin$, 3, 1)} \\
\textbf{6} & $\G,x\ok \vdash e_1 \ok$ & \textbf{(induction on left premise, 4)} \\
%\textbf{7} & $\G,y \vdash e_2 \ok$ & \textbf{(exchange on right premise)} \\
\textbf{7} & $\G,y\ok,x\ok \vdash e_2 \ok$ & \textbf{(induction on right premise, 5)} \\
\textbf{8} & $\G,x\ok,y\ok \vdash e_2 \ok$ & \textbf{(exchange on 7)} \\
\, & $\G,x\ok \vdash \slet y = e_1 \sinn e_2 \send \ok$ & \textbf{(let on 6,8)} \\

\end{longtable}

\bigskip

\noindent This concludes the proof of weakening.

\bigskip

\textbf{Theorem 1 (Substitution)}

  \begin{tabular}{ll}
    If & $\G \vdash e_1 \ok$ \\ 
    and & $x\ok,\G \vdash e_2 \ok$ \\
    and & $\{e_1/x\}e_2 = e_3$ \\
    then & $\G \vdash e_3 \ok$. \\
  \end{tabular}


\question{2.1}{25}
\begin{quote}
  Prove the substitution theorem, using rule induction. You may use
  the weakening and exchange lemmas as stated, and do not have to
  prove them.

Hints: Think about which derivation to induct on. You should need
weakening (but not exchange). If you don't, then you are not being
careful enough or are on the wrong track. Remember the principle of
\emph{inversion}: if only one rule could have been used to derive a
judgment that we know is derivable, then we know its premises must
hold.
\end{quote}

\section{Propositional logic (20 points)}

In this question we will look at a subset of \emph{Propositional
Logic}. Our universe of terms consists of an infinite number of arity
0 operators {$P_0, P_1, \ldots, P_n$} (``propositional variables''),
and the binary operator $\implies$ (``implication''). We write $A$, $B$, $\dots$ as metavariables standing for propositions. Thus, the grammar of the language is as follows.
\par\bigskip
\begin{tabular}{rcl}
  $A$ & $::=$ & $P_i \mathrel| A \implies A$ \\
\end{tabular}
\par\bigskip

Next we define a judgment $A \thm$ representing the assertion that $A$ is a theorem of the logic.

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

\bigskip

\begin{tabular}{c}
\infer[K]{A \implies (B \implies A) \thm}
   {}

\\

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

\\
\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}{|ccc|l|}
    \multicolumn{3}{c}{\textbf{Proposition}} & \multicolumn{1}{c}{\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 $A$ is a tautology iff for every
assignment giving a truth value \texttt{true} or \texttt{false} to each of the
propositional variables $P_0, \ldots, P_n$ appearing in $A$, the truth value of the whole
proposition $A$ is \texttt{true}.

\question{3.1}{5}
\begin{quote}
  Rewrite the grammar for the language as a set of inference rules. The rules should inductively define the judgment $A \prop$, which asserts that $A$ is a well-formed proposition.
\end{quote}

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

\extracreditquestion{3.3}
\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}
